Search for blocks/addresses/...

Proofgold Address

address
PUUqbjESRAKHZjMpfAd1sB9aEHc7yzF3f1H
total
0
mg
-
conjpub
-
current assets
53e42../b8235.. bday: 3760 doc published by PrGxv..
Definition and := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition explicit_Nats := λ x0 x1 . λ x2 : ι → ι . and (and (and (and (prim1 x1 x0) (∀ x3 . prim1 x3 x0prim1 (x2 x3) x0)) (∀ x3 . prim1 x3 x0x2 x3 = x1∀ x4 : ο . x4)) (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)) (∀ x3 : ι → ο . x3 x1(∀ x4 . x3 x4x3 (x2 x4))∀ x4 . prim1 x4 x0x3 x4)
Known and5I : ∀ x0 x1 x2 x3 x4 : ο . x0x1x2x3x4and (and (and (and x0 x1) x2) x3) x4
Theorem explicit_Nats_I : ∀ x0 x1 . ∀ x2 : ι → ι . prim1 x1 x0(∀ x3 . prim1 x3 x0prim1 (x2 x3) x0)(∀ x3 . prim1 x3 x0x2 x3 = x1∀ x4 : ο . x4)(∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)(∀ x3 : ι → ο . x3 x1(∀ x4 . x3 x4x3 (x2 x4))∀ x4 . prim1 x4 x0x3 x4)explicit_Nats x0 x1 x2 (proof)
Known and5E : ∀ x0 x1 x2 x3 x4 : ο . and (and (and (and x0 x1) x2) x3) x4∀ x5 : ο . (x0x1x2x3x4x5)x5
Theorem explicit_Nats_E : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2prim1 x1 x0(∀ x4 . prim1 x4 x0prim1 (x2 x4) x0)(∀ x4 . prim1 x4 x0x2 x4 = x1∀ x5 : ο . x5)(∀ x4 . prim1 x4 x0∀ x5 . prim1 x5 x0x2 x4 = x2 x5x4 = x5)(∀ x4 : ι → ο . x4 x1(∀ x5 . x4 x5x4 (x2 x5))∀ x5 . prim1 x5 x0x4 x5)x3)explicit_Nats x0 x1 x2x3 (proof)
Known andI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem explicit_Nats_ind : ∀ x0 x1 . ∀ x2 : ι → ι . explicit_Nats x0 x1 x2∀ x3 : ι → ο . x3 x1(∀ x4 . prim1 x4 x0x3 x4x3 (x2 x4))∀ x4 . prim1 x4 x0x3 x4 (proof)
Param 48ef8.. : ι
Param 4a7ef.. : ι
Param 4ae4a.. : ιι
Known 8ee89.. : prim1 4a7ef.. 48ef8..
Known 98ac3.. : ∀ x0 . prim1 x0 48ef8..prim1 (4ae4a.. x0) 48ef8..
Known 1b1d1.. : ∀ x0 . 4ae4a.. x0 = 4a7ef..∀ x1 : ο . x1
Known 054cd.. : ∀ x0 x1 . 4ae4a.. x0 = 4ae4a.. x1x0 = x1
Definition ba9d8.. := λ x0 . ∀ x1 : ι → ο . x1 4a7ef..(∀ x2 . x1 x2x1 (4ae4a.. x2))x1 x0
Known c2711.. : ∀ x0 . prim1 x0 48ef8..ba9d8.. x0
Theorem dd179.. : explicit_Nats 48ef8.. 4a7ef.. 4ae4a.. (proof)
Definition bij := λ x0 x1 . λ x2 : ι → ι . and (and (∀ x3 . prim1 x3 x0prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0∀ x4 . prim1 x4 x0x2 x3 = x2 x4x3 = x4)) (∀ x3 . prim1 x3 x1∀ x4 : ο . (∀ x5 . and (prim1 x5 x0) (x2 x5 = x3)x4)x4)
Theorem explicit_Nats_transfer : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 x4 . ∀ x5 x6 : ι → ι . explicit_Nats x0 x1 x2bij x0 x3 x6x6 x1 = x4(∀ x7 . prim1 x7 x0x6 (x2 x7) = x5 (x6 x7))explicit_Nats x3 x4 x5 (proof)
Definition explicit_Field := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . and (and (and (and (and (and (and (and (and (and (and (and (and (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0prim1 (x3 x5 x6) x0) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7)) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x3 x5 x6 = x3 x6 x5)) (prim1 x1 x0)) (∀ x5 . prim1 x5 x0x3 x1 x5 = x5)) (∀ x5 . prim1 x5 x0∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x3 x5 x7 = x1)x6)x6)) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0prim1 (x4 x5 x6) x0)) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7)) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x4 x5 x6 = x4 x6 x5)) (prim1 x2 x0)) (x2 = x1∀ x5 : ο . x5)) (∀ x5 . prim1 x5 x0x4 x2 x5 = x5)) (∀ x5 . prim1 x5 x0(x5 = x1∀ x6 : ο . x6)∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x4 x5 x7 = x2)x6)x6)) (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7))
Known and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0x1x2x3x4x5x6and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6
Theorem explicit_Field_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . (∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0prim1 (x3 x5 x6) x0)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x3 x5 x6 = x3 x6 x5)prim1 x1 x0(∀ x5 . prim1 x5 x0x3 x1 x5 = x5)(∀ x5 . prim1 x5 x0∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x3 x5 x7 = x1)x6)x6)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0prim1 (x4 x5 x6) x0)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0x4 x5 x6 = x4 x6 x5)prim1 x2 x0(x2 = x1∀ x5 : ο . x5)(∀ x5 . prim1 x5 x0x4 x2 x5 = x5)(∀ x5 . prim1 x5 x0(x5 = x1∀ x6 : ο . x6)∀ x6 : ο . (∀ x7 . and (prim1 x7 x0) (x4 x5 x7 = x2)x6)x6)(∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7))explicit_Field x0 x1 x2 x3 x4 (proof)
Known and7E : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6∀ x7 : ο . (x0x1x2x3x4x5x6x7)x7
Theorem explicit_Field_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Field x0 x1 x2 x3 x4(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x3 x6 x7) x0)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x6 x7 = x3 x7 x6)prim1 x1 x0(∀ x6 . prim1 x6 x0x3 x1 x6 = x6)(∀ x6 . prim1 x6 x0∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x3 x6 x8 = x1)x7)x7)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0prim1 (x4 x6 x7) x0)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x4 x6 x7 = x4 x7 x6)prim1 x2 x0(x2 = x1∀ x6 : ο . x6)(∀ x6 . prim1 x6 x0x4 x2 x6 = x6)(∀ x6 . prim1 x6 x0(x6 = x1∀ x7 : ο . x7)∀ x7 : ο . (∀ x8 . and (prim1 x8 x0) (x4 x6 x8 = x2)x7)x7)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8))x5)explicit_Field x0 x1 x2 x3 x4x5 (proof)
Definition explicit_Field_minus := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 . prim0 (λ x6 . and (prim1 x6 x0) (x3 x5 x6 = x1))
Known Eps_i_ex : ∀ x0 : ι → ο . (∀ x1 : ο . (∀ x2 . x0 x2x1)x1)x0 (prim0 x0)
Theorem explicit_Field_minus_prop : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0and (prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x0) (x3 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x1) (proof)
Theorem explicit_Field_minus_clos : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x0 (proof)
Theorem explicit_Field_minus_R : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x3 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x1 (proof)
Theorem explicit_Field_minus_L : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x5 = x1 (proof)
Theorem explicit_Field_plus_cancelL : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x5 x6 = x3 x5 x7x6 = x7 (proof)
Theorem explicit_Field_plus_cancelR : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x3 x5 x7 = x3 x6 x7x5 = x6 (proof)
Theorem explicit_Field_minus_invol : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x5 (proof)
Theorem explicit_Field_minus_one_In : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x0 (proof)
Theorem explicit_Field_zero_multR : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x4 x5 x1 = x1 (proof)
Theorem explicit_Field_zero_multL : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x4 x1 x5 = x1 (proof)
Theorem explicit_Field_minus_mult : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0explicit_Field_minus x0 x1 x2 x3 x4 x5 = x4 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x5 (proof)
Theorem explicit_Field_minus_one_square : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4x4 (explicit_Field_minus x0 x1 x2 x3 x4 x2) (explicit_Field_minus x0 x1 x2 x3 x4 x2) = x2 (proof)
Theorem explicit_Field_minus_square : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4∀ x5 . prim1 x5 x0x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x4 x5 x5 (proof)
Definition iff := λ x0 x1 : ο . and (x0x1) (x1x0)
Definition or := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Definition explicit_OrderedField := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . and (and (and (and (and (explicit_Field x0 x1 x2 x3 x4) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x6 x7x5 x7 x8x5 x6 x8)) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (and (x5 x6 x7) (x5 x7 x6)) (x6 = x7))) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0or (x5 x6 x7) (x5 x7 x6))) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x6 x7x5 (x3 x6 x8) (x3 x7 x8))) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x5 x1 x6x5 x1 x7x5 x1 (x4 x6 x7))
Known and6I : ∀ x0 x1 x2 x3 x4 x5 : ο . x0x1x2x3x4x5and (and (and (and (and x0 x1) x2) x3) x4) x5
Theorem explicit_OrderedField_I : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_Field x0 x1 x2 x3 x4(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x6 x7x5 x7 x8x5 x6 x8)(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0iff (and (x5 x6 x7) (x5 x7 x6)) (x6 = x7))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0or (x5 x6 x7) (x5 x7 x6))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x6 x7x5 (x3 x6 x8) (x3 x7 x8))(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0x5 x1 x6x5 x1 x7x5 x1 (x4 x6 x7))explicit_OrderedField x0 x1 x2 x3 x4 x5 (proof)
Known and6E : ∀ x0 x1 x2 x3 x4 x5 : ο . and (and (and (and (and x0 x1) x2) x3) x4) x5∀ x6 : ο . (x0x1x2x3x4x5x6)x6
Theorem explicit_OrderedField_E : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Field x0 x1 x2 x3 x4(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 x8 x9x5 x7 x9)(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0iff (and (x5 x7 x8) (x5 x8 x7)) (x7 = x8))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0or (x5 x7 x8) (x5 x8 x7))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x5 x7 x8x5 (x3 x7 x9) (x3 x8 x9))(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0x5 x1 x7x5 x1 x8x5 x1 (x4 x7 x8))x6)explicit_OrderedField x0 x1 x2 x3 x4 x5x6 (proof)
Definition lt := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 x7 . and (x5 x6 x7) (x6 = x7∀ x8 : ο . x8)
Definition natOfOrderedField_p := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ι → ο . x7 x1(∀ x8 . x7 x8x7 (x3 x8 x2))x7 x6
Param 1216a.. : ι(ιο) → ι
Known b2421.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 x0x1 x2prim1 x2 (1216a.. x0 x1)
Known 492ff.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1)∀ x3 : ο . (prim1 x2 x0x1 x2x3)x3
Theorem 801aa.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5explicit_Nats (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)) x1 (λ x6 . x3 x6 x2) (proof)
Param 3097a.. : ι(ιι) → ι
Definition b5c9f.. := λ x0 x1 . 3097a.. x1 (λ x2 . x0)
Param f482f.. : ιιι
Definition 62ee1.. := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . and (and (explicit_OrderedField x0 x1 x2 x3 x4 x5) (∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0lt x0 x1 x2 x3 x4 x5 x1 x6x5 x1 x7∀ x8 : ο . (∀ x9 . and (prim1 x9 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))) (x5 x7 (x4 x9 x6))x8)x8)) (∀ x6 . prim1 x6 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))(∀ x8 . prim1 x8 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (and (x5 (f482f.. x6 x8) (f482f.. x7 x8)) (x5 (f482f.. x6 x8) (f482f.. x6 (x3 x8 x2)))) (x5 (f482f.. x7 (x3 x8 x2)) (f482f.. x7 x8)))∀ x8 : ο . (∀ x9 . and (prim1 x9 x0) (∀ x10 . prim1 x10 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (x5 (f482f.. x6 x10) x9) (x5 x9 (f482f.. x7 x10)))x8)x8)
Known and3I : ∀ x0 x1 x2 : ο . x0x1x2and (and x0 x1) x2
Theorem 1f659.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x6 . prim1 x6 x0∀ x7 . prim1 x7 x0lt x0 x1 x2 x3 x4 x5 x1 x6x5 x1 x7∀ x8 : ο . (∀ x9 . and (prim1 x9 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))) (x5 x7 (x4 x9 x6))x8)x8)(∀ x6 . prim1 x6 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))(∀ x8 . prim1 x8 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (and (x5 (f482f.. x6 x8) (f482f.. x7 x8)) (x5 (f482f.. x6 x8) (f482f.. x6 (x3 x8 x2)))) (x5 (f482f.. x7 (x3 x8 x2)) (f482f.. x7 x8)))∀ x8 : ο . (∀ x9 . and (prim1 x9 x0) (∀ x10 . prim1 x10 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (x5 (f482f.. x6 x10) x9) (x5 x9 (f482f.. x7 x10)))x8)x8)62ee1.. x0 x1 x2 x3 x4 x5 (proof)
Known and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2∀ x3 : ο . (x0x1x2x3)x3
Theorem f2fa8.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (62ee1.. x0 x1 x2 x3 x4 x5explicit_OrderedField x0 x1 x2 x3 x4 x5(∀ x7 . prim1 x7 x0∀ x8 . prim1 x8 x0lt x0 x1 x2 x3 x4 x5 x1 x7x5 x1 x8∀ x9 : ο . (∀ x10 . and (prim1 x10 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))) (x5 x8 (x4 x10 x7))x9)x9)(∀ x7 . prim1 x7 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))∀ x8 . prim1 x8 (b5c9f.. x0 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)))(∀ x9 . prim1 x9 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (and (x5 (f482f.. x7 x9) (f482f.. x8 x9)) (x5 (f482f.. x7 x9) (f482f.. x7 (x3 x9 x2)))) (x5 (f482f.. x8 (x3 x9 x2)) (f482f.. x8 x9)))∀ x9 : ο . (∀ x10 . and (prim1 x10 x0) (∀ x11 . prim1 x11 (1216a.. x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5))and (x5 (f482f.. x7 x11) x10) (x5 x10 (f482f.. x8 x11)))x9)x9)x6)62ee1.. x0 x1 x2 x3 x4 x5x6 (proof)
Theorem explicit_Field_transfer : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 x6 x7 . ∀ x8 x9 : ι → ι → ι . ∀ x10 : ι → ι . explicit_Field x0 x1 x2 x3 x4bij x0 x5 x10x10 x1 = x6x10 x2 = x7(∀ x11 . prim1 x11 x0∀ x12 . prim1 x12 x0x10 (x3 x11 x12) = x8 (x10 x11) (x10 x12))(∀ x11 . prim1 x11 x0∀ x12 . prim1 x12 x0x10 (x4 x11 x12) = x9 (x10 x11) (x10 x12))explicit_Field x5 x6 x7 x8 x9 (proof)
Known iffI : ∀ x0 x1 : ο . (x0x1)(x1x0)iff x0 x1
Known orIL : ∀ x0 x1 : ο . x0or x0 x1
Known orIR : ∀ x0 x1 : ο . x1or x0 x1
Theorem explicit_OrderedField_transfer : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 x8 . ∀ x9 x10 : ι → ι → ι . ∀ x11 : ι → ι → ο . ∀ x12 : ι → ι . explicit_OrderedField x0 x1 x2 x3 x4 x5bij x0 x6 x12x12 x1 = x7x12 x2 = x8(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0x12 (x3 x13 x14) = x9 (x12 x13) (x12 x14))(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0x12 (x4 x13 x14) = x10 (x12 x13) (x12 x14))(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0iff (x5 x13 x14) (x11 (x12 x13) (x12 x14)))explicit_OrderedField x6 x7 x8 x9 x10 x11 (proof)
Param 0fc90.. : ι(ιι) → ι
Known d0a1f.. : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . prim1 x2 (1216a.. x0 x1)prim1 x2 x0
Known f22ec.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . prim1 x2 x0f482f.. (0fc90.. x0 x1) x2 = x1 x2
Known d8d74.. : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . prim1 x2 (3097a.. x0 x1)prim1 x3 x0prim1 (f482f.. x2 x3) (x1 x3)
Known 27474.. : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . prim1 x3 x0prim1 (x2 x3) (x1 x3))prim1 (0fc90.. x0 x2) (3097a.. x0 x1)
Theorem 5ece9.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 x7 x8 . ∀ x9 x10 : ι → ι → ι . ∀ x11 : ι → ι → ο . ∀ x12 : ι → ι . 62ee1.. x0 x1 x2 x3 x4 x5bij x0 x6 x12x12 x1 = x7x12 x2 = x8(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0x12 (x3 x13 x14) = x9 (x12 x13) (x12 x14))(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0x12 (x4 x13 x14) = x10 (x12 x13) (x12 x14))(∀ x13 . prim1 x13 x0∀ x14 . prim1 x14 x0iff (x5 x13 x14) (x11 (x12 x13) (x12 x14)))62ee1.. x6 x7 x8 x9 x10 x11 (proof)
Definition 11fac.. := λ x0 . λ x1 x2 : ι → ι . λ x3 x4 x5 . λ x6 x7 : ι → ι → ι . and (and (and (and (and (and (and (and (explicit_Field x0 x3 x4 x6 x7) (∀ x8 : ο . (∀ x9 : ι → ι → ο . 62ee1.. (1216a.. x0 (λ x10 . x1 x10 = x10)) x3 x4 x6 x7 x9x8)x8)) (∀ x8 . prim1 x8 x0prim1 (x2 x8) (1216a.. x0 (λ x9 . x1 x9 = x9)))) (prim1 x5 x0)) (∀ x8 . prim1 x8 x0prim1 (x1 x8) x0)) (∀ x8 . prim1 x8 x0prim1 (x2 x8) x0)) (∀ x8 . prim1 x8 x0x8 = x6 (x1 x8) (x7 x5 (x2 x8)))) (∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x1 x8 = x1 x9x2 x8 = x2 x9x8 = x9)) (x6 (x7 x5 x5) x4 = x3)
Theorem be4f2.. : ∀ x0 . ∀ x1 x2 : ι → ι . ∀ x3 x4 x5 . ∀ x6 x7 : ι → ι → ι . explicit_Field x0 x3 x4 x6 x7(∀ x8 : ο . (∀ x9 : ι → ι → ο . 62ee1.. (1216a.. x0 (λ x10 . x1 x10 = x10)) x3 x4 x6 x7 x9x8)x8)(∀ x8 . prim1 x8 x0prim1 (x2 x8) (1216a.. x0 (λ x9 . x1 x9 = x9)))prim1 x5 x0(∀ x8 . prim1 x8 x0prim1 (x1 x8) x0)(∀ x8 . prim1 x8 x0prim1 (x2 x8) x0)(∀ x8 . prim1 x8 x0x8 = x6 (x1 x8) (x7 x5 (x2 x8)))(∀ x8 . prim1 x8 x0∀ x9 . prim1 x9 x0x1 x8 = x1 x9x2 x8 = x2 x9x8 = x9)x6 (x7 x5 x5) x4 = x311fac.. x0 x1 x2 x3 x4 x5 x6 x7 (proof)

previous assets