Proofgold Address

Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
Param omega^omega : ι
Param ordsucc^ordsucc : ι → ι
Param Group^Group : ι → ο
Param ap^ap : ι → ι → ι
Param normal_subgroup^{normal_subgroup} : ι → ι → ο
Param abelian_Group^{abelian_Group} : ι → ο
Param quotient_Group^{quotient_Group} : ι → ι → ι
Param trivial_Group_p^{trivial_Group_p} : ι → ο
Definition solvable_Group_p^{solvable_Group_p} := λ x0 . ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (∀ x3 : ο . (∀ x4 . and (and (and (and (∀ x5 . x5 ∈ ordsucc x2 ⟶ Group (ap x4 x5)) (∀ x5 . x5 ∈ x2 ⟶ normal_subgroup (ap x4 (ordsucc x5)) (ap x4 x5))) (∀ x5 . x5 ∈ x2 ⟶ abelian_Group (quotient_Group (ap x4 x5) (ap x4 (ordsucc x5))))) (x0 = ap x4 0)) (trivial_Group_p (ap x4 x2)) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1
Definition field0^{RealsStruct_carrier} := λ x0 . ap x0 0
Param decode_b^decode_b : ι → ι → ι → ι
Definition field1b^{RealsStruct_plus} := λ x0 . decode_b (ap x0 1)
Param Pi^Pi : ι → (ι → ι) → ι
Definition setexp^setexp := λ x0 x1 . Pi x1 (λ x2 . x0)
Definition Group_Hom^Group_Hom := λ x0 x1 x2 . and (and (and (Group x0) (Group x1)) (x2 ∈ setexp (field0 x1) (field0 x0))) (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (field1b x0 x3 x4) = field1b x1 (ap x2 x3) (ap x2 x4))
Param bij^bij : ι → ι → (ι → ι) → ο
Definition Group_Iso^Group_Iso := λ x0 x1 x2 . and (Group_Hom x0 x1 x2) (bij (field0 x0) (field0 x1) (ap x2))
Definition Group_Isomorphic^{Group_Isomorphic} := λ x0 x1 . ∀ x2 : ο . (∀ x3 . Group_Iso x0 x1 x3 ⟶ x2) ⟶ x2
Param struct_b_b_e_e^{struct_b_b_e_e} : ι → ο
Param unpack_b_b_e_e_o^{unpack_b_b_e_e_o} : ι → (ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ο) → ο
Param explicit_Field^{explicit_Field} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ο
Definition Field^Field := λ x0 . and (struct_b_b_e_e x0) (unpack_b_b_e_e_o x0 (λ x1 . λ x2 x3 : ι → ι → ι . λ x4 x5 . explicit_Field x1 x4 x5 x2 x3))
Definition field2b^{RealsStruct_mult} := λ x0 . decode_b (ap x0 2)
Definition field4^{RealsStruct_zero} := λ x0 . ap x0 4
Definition field3^Field_zero := λ x0 . ap x0 3
Known explicit_Field_plus_cancelL^{explicit_Field_plus_cancelL} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 x5 x6 = x3 x5 x7 ⟶ x6 = x7
Known Field_explicit_Field^{Field_explicit_Field} : ∀ x0 . Field x0 ⟶ explicit_Field (field0 x0) (field3 x0) (field4 x0) (field1b x0) (field2b x0)
Theorem Field_plus_cancelL^{Field_plus_cancelL} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x1 x2 = field1b x0 x1 x3 ⟶ x2 = x3 (proof)
Known explicit_Field_plus_cancelR^{explicit_Field_plus_cancelR} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 x5 x7 = x3 x6 x7 ⟶ x5 = x6
Theorem Field_plus_cancelR^{Field_plus_cancelR} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x1 x3 = field1b x0 x2 x3 ⟶ x1 = x2 (proof)
Param If_i^If_i : ο → ι → ι → ι
Param explicit_Field_minus^{explicit_Field_minus} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι
Definition Field_minus^Field_minus := λ x0 x1 . If_i (x1 ∈ ap x0 0) (explicit_Field_minus (ap x0 0) (ap x0 3) (ap x0 4) (decode_b (ap x0 1)) (decode_b (ap x0 2)) x1) 0
Known If_i_1^If_i_1 : ∀ x0 : ο . ∀ x1 x2 . x0 ⟶ If_i x0 x1 x2 = x1
Theorem Field_minus_eq^{Field_minus_eq} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ Field_minus x0 x1 = explicit_Field_minus (field0 x0) (field3 x0) (field4 x0) (field1b x0) (field2b x0) x1 (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Definition nIn^nIn := λ x0 x1 . not (x0 ∈ x1)
Known If_i_0^If_i_0 : ∀ x0 : ο . ∀ x1 x2 . not x0 ⟶ If_i x0 x1 x2 = x2
Theorem Field_minus_undef^{Field_minus_undef} : ∀ x0 . Field x0 ⟶ ∀ x1 . nIn x1 (field0 x0) ⟶ Field_minus x0 x1 = 0 (proof)
Known explicit_Field_minus_clos^{explicit_Field_minus_clos} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x5 ∈ x0
Theorem Field_minus_clos^{Field_minus_clos} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ Field_minus x0 x1 ∈ field0 x0 (proof)
Known explicit_Field_minus_R^{explicit_Field_minus_R} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x1
Theorem Field_minus_R^{Field_minus_R} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field1b x0 x1 (Field_minus x0 x1) = field3 x0 (proof)
Known explicit_Field_minus_L^{explicit_Field_minus_L} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x5 = x1
Theorem Field_minus_L^{Field_minus_L} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field1b x0 (Field_minus x0 x1) x1 = field3 x0 (proof)
Known explicit_Field_minus_invol^{explicit_Field_minus_invol} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x5
Theorem Field_minus_invol^{Field_minus_invol} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ Field_minus x0 (Field_minus x0 x1) = x1 (proof)
Known Field_one_In^Field_one_In : ∀ x0 . Field x0 ⟶ field4 x0 ∈ field0 x0
Known explicit_Field_minus_one_In^{explicit_Field_minus_one_In} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x2 ∈ x0
Theorem Field_minus_one_In^{Field_minus_one_In} : ∀ x0 . Field x0 ⟶ Field_minus x0 (field4 x0) ∈ field0 x0 (proof)
Known explicit_Field_zero_multR^{explicit_Field_zero_multR} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5 x1 = x1
Theorem Field_zero_multR^{Field_zero_multR} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 x1 (field3 x0) = field3 x0 (proof)
Known explicit_Field_zero_multL^{explicit_Field_zero_multL} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x1 x5 = x1
Theorem Field_zero_multL^{Field_zero_multL} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 (field3 x0) x1 = field3 x0 (proof)
Known explicit_Field_minus_mult^{explicit_Field_minus_mult} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x5 = x4 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x5
Theorem Field_minus_mult^{Field_minus_mult} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ Field_minus x0 x1 = field2b x0 (Field_minus x0 (field4 x0)) x1 (proof)
Known explicit_Field_minus_one_square^{explicit_Field_minus_one_square} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x2) (explicit_Field_minus x0 x1 x2 x3 x4 x2) = x2
Theorem Field_minus_one_square^{Field_minus_one_square} : ∀ x0 . Field x0 ⟶ field2b x0 (Field_minus x0 (field4 x0)) (Field_minus x0 (field4 x0)) = field4 x0 (proof)
Known explicit_Field_minus_square^{explicit_Field_minus_square} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) (explicit_Field_minus x0 x1 x2 x3 x4 x5) = x4 x5 x5
Theorem Field_minus_square^{Field_minus_square} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 (Field_minus x0 x1) (Field_minus x0 x1) = field2b x0 x1 x1 (proof)
Known Field_zero_In^{Field_zero_In} : ∀ x0 . Field x0 ⟶ field3 x0 ∈ field0 x0
Known explicit_Field_minus_zero^{explicit_Field_minus_zero} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x1 = x1
Theorem Field_minus_zero^{Field_minus_zero} : ∀ x0 . Field x0 ⟶ Field_minus x0 (field3 x0) = field3 x0 (proof)
Known explicit_Field_dist_R^{explicit_Field_dist_R} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7)
Theorem Field_dist_R^Field_dist_R : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 (field1b x0 x1 x2) x3 = field1b x0 (field2b x0 x1 x3) (field2b x0 x2 x3) (proof)
Known Field_plus_clos^{Field_plus_clos} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field1b x0 x1 x2 ∈ field0 x0
Known explicit_Field_minus_plus_dist^{explicit_Field_minus_plus_dist} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (x3 x5 x6) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x5) (explicit_Field_minus x0 x1 x2 x3 x4 x6)
Theorem Field_minus_plus_dist^{Field_minus_plus_dist} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ Field_minus x0 (field1b x0 x1 x2) = field1b x0 (Field_minus x0 x1) (Field_minus x0 x2) (proof)
Known Field_mult_clos^{Field_mult_clos} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 ∈ field0 x0
Known explicit_Field_minus_mult_L^{explicit_Field_minus_mult_L} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x5) x6 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6)
Theorem Field_minus_mult_L^{Field_minus_mult_L} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 (Field_minus x0 x1) x2 = Field_minus x0 (field2b x0 x1 x2) (proof)
Known explicit_Field_minus_mult_R^{explicit_Field_minus_mult_R} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x5 x6)
Theorem Field_minus_mult_R^{Field_minus_mult_R} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 (Field_minus x0 x2) = Field_minus x0 (field2b x0 x1 x2) (proof)
Known explicit_Field_square_zero_inv^{explicit_Field_square_zero_inv} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5 x5 = x1 ⟶ x5 = x1
Theorem Field_square_zero_inv^{Field_square_zero_inv} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ field2b x0 x1 x1 = field3 x0 ⟶ x1 = field3 x0 (proof)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known explicit_Field_mult_zero_inv^{explicit_Field_mult_zero_inv} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . explicit_Field x0 x1 x2 x3 x4 ⟶ ∀ x5 . x5 ∈ x0 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x4 x5 x6 = x1 ⟶ or (x5 = x1) (x6 = x1)
Theorem Field_mult_zero_inv^{Field_mult_zero_inv} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ field0 x0 ⟶ field2b x0 x1 x2 = field3 x0 ⟶ or (x1 = field3 x0) (x2 = field3 x0) (proof)
Param nat_primrec^nat_primrec : ι → (ι → ι → ι) → ι → ι
Definition 595d0.. := λ x0 . and (Field x0) (∀ x1 . x1 ∈ omega ⟶ nat_primrec (field4 x0) (λ x3 . field1b x0 (field4 x0)) x1 = field3 x0 ⟶ ∀ x2 : ο . x2)
Definition Subq^Subq := λ x0 x1 . ∀ x2 . x2 ∈ x0 ⟶ x2 ∈ x1
Definition subfield^subfield := λ x0 x1 . and (and (and (and (and (and (Field x0) (Field x1)) (field0 x0 ⊆ field0 x1)) (field3 x0 = field3 x1)) (field4 x0 = field4 x1)) (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x2 x3 = field1b x1 x2 x3)) (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x2 x3 = field2b x1 x2 x3)
Known and7I^and7I : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6
Theorem subfield_I^subfield_I : ∀ x0 x1 . Field x0 ⟶ Field x1 ⟶ field0 x0 ⊆ field0 x1 ⟶ field3 x0 = field3 x1 ⟶ field4 x0 = field4 x1 ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field1b x0 x2 x3 = field1b x1 x2 x3) ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ field2b x0 x2 x3 = field2b x1 x2 x3) ⟶ subfield x0 x1 (proof)
Known and7E^and7E : ∀ x0 x1 x2 x3 x4 x5 x6 : ο . and (and (and (and (and (and x0 x1) x2) x3) x4) x5) x6 ⟶ ∀ x7 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4 ⟶ x5 ⟶ x6 ⟶ x7) ⟶ x7
Theorem subfield_E^subfield_E : ∀ x0 x1 . subfield x0 x1 ⟶ ∀ x2 : ο . (Field x0 ⟶ Field x1 ⟶ field0 x0 ⊆ field0 x1 ⟶ field3 x0 = field3 x1 ⟶ field4 x0 = field4 x1 ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field1b x0 x3 x4 = field1b x1 x3 x4) ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ field2b x0 x3 x4 = field2b x1 x3 x4) ⟶ x2) ⟶ x2 (proof)
Definition Field_Hom^Field_Hom := λ x0 x1 x2 . and (and (and (and (and (and (Field x0) (Field x1)) (x2 ∈ setexp (field0 x1) (field0 x0))) (ap x2 (field3 x0) = field3 x1)) (ap x2 (field4 x0) = field4 x1)) (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (field1b x0 x3 x4) = field1b x1 (ap x2 x3) (ap x2 x4))) (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (field2b x0 x3 x4) = field2b x1 (ap x2 x3) (ap x2 x4))
Theorem Field_Hom_I^Field_Hom_I : ∀ x0 x1 x2 . Field x0 ⟶ Field x1 ⟶ x2 ∈ setexp (field0 x1) (field0 x0) ⟶ ap x2 (field3 x0) = field3 x1 ⟶ ap x2 (field4 x0) = field4 x1 ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (field1b x0 x3 x4) = field1b x1 (ap x2 x3) (ap x2 x4)) ⟶ (∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (field2b x0 x3 x4) = field2b x1 (ap x2 x3) (ap x2 x4)) ⟶ Field_Hom x0 x1 x2 (proof)
Param CRing_with_id_omega_exp^{CRing_omega_exp} : ι → ι → ι → ι
Param nat_p^nat_p : ι → ο
Known omega_nat_p^omega_nat_p : ∀ x0 . x0 ∈ omega ⟶ nat_p x0
Known nat_ind^nat_ind : ∀ x0 : ι → ο . x0 0 ⟶ (∀ x1 . nat_p x1 ⟶ x0 x1 ⟶ x0 (ordsucc x1)) ⟶ ∀ x1 . nat_p x1 ⟶ x0 x1
Known Field_omega_exp_0^{Field_omega_exp_0} : ∀ x0 . Field x0 ⟶ ∀ x1 . CRing_with_id_omega_exp x0 x1 0 = field4 x0
Known Field_omega_exp_S^{Field_omega_exp_S} : ∀ x0 . Field x0 ⟶ ∀ x1 x2 . x2 ∈ omega ⟶ CRing_with_id_omega_exp x0 x1 (ordsucc x2) = field2b x0 x1 (CRing_with_id_omega_exp x0 x1 x2)
Known nat_p_omega^nat_p_omega : ∀ x0 . nat_p x0 ⟶ x0 ∈ omega
Known Field_omega_exp_clos^{Field_omega_exp_clos} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ omega ⟶ CRing_with_id_omega_exp x0 x1 x2 ∈ field0 x0
Known ap_Pi^ap_Pi : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 x3 . x2 ∈ Pi x0 x1 ⟶ x3 ∈ x0 ⟶ ap x2 x3 ∈ x1 x3
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
Param setminus^setminus : ι → ι → ι
Param Sing^Sing : ι → ι
Param Field_div^Field_div : ι → ι → ι → ι
Known Field_one_neq_zero^{Field_one_neq_zero} : ∀ x0 . Field x0 ⟶ field4 x0 = field3 x0 ⟶ ∀ x1 : ο . x1
Known Field_mult_div^{Field_mult_div} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ setminus (field0 x0) (Sing (field3 x0)) ⟶ x1 = field2b x0 x2 (Field_div x0 x1 x2)
Known Field_div_clos^{Field_div_clos} : ∀ x0 . Field x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ ∀ x2 . x2 ∈ setminus (field0 x0) (Sing (field3 x0)) ⟶ Field_div x0 x1 x2 ∈ field0 x0
Known setminusI^setminusI : ∀ x0 x1 x2 . x2 ∈ x0 ⟶ nIn x2 x1 ⟶ x2 ∈ setminus x0 x1
Known SingE^SingE : ∀ x0 x1 . x1 ∈ Sing x0 ⟶ x1 = x0
Theorem Field_Hom_E^Field_Hom_E : ∀ x0 x1 x2 . Field_Hom x0 x1 x2 ⟶ ∀ x3 : ο . (Field x0 ⟶ Field x1 ⟶ x2 ∈ setexp (field0 x1) (field0 x0) ⟶ ap x2 (field3 x0) = field3 x1 ⟶ ap x2 (field4 x0) = field4 x1 ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ ap x2 (field1b x0 x4 x5) = field1b x1 (ap x2 x4) (ap x2 x5)) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ ap x2 (field2b x0 x4 x5) = field2b x1 (ap x2 x4) (ap x2 x5)) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 (Field_minus x0 x4) = Field_minus x1 (ap x2 x4)) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 x4 = field3 x1 ⟶ x4 = field3 x0) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ field0 x0 ⟶ ap x2 x4 = ap x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ field0 x0 ⟶ ∀ x5 . x5 ∈ omega ⟶ ap x2 (CRing_with_id_omega_exp x0 x4 x5) = CRing_with_id_omega_exp x1 (ap x2 x4) x5) ⟶ x3) ⟶ x3 (proof)
Theorem Field_Hom_inj^{Field_Hom_inj} : ∀ x0 x1 x2 . Field_Hom x0 x1 x2 ⟶ ∀ x3 . x3 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ field0 x0 ⟶ ap x2 x3 = ap x2 x4 ⟶ x3 = x4 (proof)
Theorem subfield_refl^{subfield_refl} : ∀ x0 . Field x0 ⟶ subfield x0 x0 (proof)
Known Subq_tra^Subq_tra : ∀ x0 x1 x2 . x0 ⊆ x1 ⟶ x1 ⊆ x2 ⟶ x0 ⊆ x2
Theorem subfield_tra^subfield_tra : ∀ x0 x1 x2 . subfield x0 x1 ⟶ subfield x1 x2 ⟶ subfield x0 x2 (proof)
Definition Field_extension_by_1^{Field_extension_by_1} := λ x0 x1 x2 . and (and (subfield x0 x1) (x2 ∈ setminus (field0 x1) (field0 x0))) (∀ x3 . subfield x0 x3 ⟶ x2 ∈ field0 x3 ⟶ subfield x1 x3)
Known and3I^and3I : ∀ x0 x1 x2 : ο . x0 ⟶ x1 ⟶ x2 ⟶ and (and x0 x1) x2
Theorem Field_extension_by_1_I^{Field_extension_by_1_I} : ∀ x0 x1 x2 . subfield x0 x1 ⟶ x2 ∈ setminus (field0 x1) (field0 x0) ⟶ (∀ x3 . subfield x0 x3 ⟶ x2 ∈ field0 x3 ⟶ subfield x1 x3) ⟶ Field_extension_by_1 x0 x1 x2 (proof)
Known and3E^and3E : ∀ x0 x1 x2 : ο . and (and x0 x1) x2 ⟶ ∀ x3 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3) ⟶ x3
Theorem Field_extension_by_1_E^{Field_extension_by_1_E} : ∀ x0 x1 x2 . Field_extension_by_1 x0 x1 x2 ⟶ ∀ x3 : ο . (subfield x0 x1 ⟶ x2 ∈ setminus (field0 x1) (field0 x0) ⟶ (∀ x4 . subfield x0 x4 ⟶ x2 ∈ field0 x4 ⟶ subfield x1 x4) ⟶ x3) ⟶ x3 (proof)
Definition radical_field_extension^{radical_field_extension} := λ x0 x1 . ∀ x2 : ο . (∀ x3 . and (x3 ∈ omega) (∀ x4 : ο . (∀ x5 . and (and (and (ap x5 0 = x0) (ap x5 x3 = x1)) (∀ x6 . x6 ∈ ordsucc x3 ⟶ Field (ap x5 x6))) (∀ x6 . x6 ∈ x3 ⟶ ∀ x7 : ο . (∀ x8 . and (x8 ∈ field0 (ap x5 (ordsucc x6))) (∀ x9 : ο . (∀ x10 . and (x10 ∈ omega) (and (CRing_with_id_omega_exp (ap x5 (ordsucc x6)) x8 x10 ∈ field0 (ap x5 x6)) (Field_extension_by_1 (ap x5 x6) (ap x5 (ordsucc x6)) x8)) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7) ⟶ x4) ⟶ x4) ⟶ x2) ⟶ x2
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Known and4I^and4I : ∀ x0 x1 x2 x3 : ο . x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ and (and (and x0 x1) x2) x3
Theorem radical_field_extension_I^{radical_field_extension_I} : ∀ x0 x1 x2 . x2 ∈ omega ⟶ ∀ x3 . ap x3 0 = x0 ⟶ ap x3 x2 = x1 ⟶ (∀ x4 . x4 ∈ ordsucc x2 ⟶ Field (ap x3 x4)) ⟶ (∀ x4 . x4 ∈ x2 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ field0 (ap x3 (ordsucc x4))) (∀ x7 : ο . (∀ x8 . and (x8 ∈ omega) (and (CRing_with_id_omega_exp (ap x3 (ordsucc x4)) x6 x8 ∈ field0 (ap x3 x4)) (Field_extension_by_1 (ap x3 x4) (ap x3 (ordsucc x4)) x6)) ⟶ x7) ⟶ x7) ⟶ x5) ⟶ x5) ⟶ radical_field_extension x0 x1 (proof)
Known ordsuccI2^ordsuccI2 : ∀ x0 . x0 ∈ ordsucc x0
Known nat_0_in_ordsucc^{nat_0_in_ordsucc} : ∀ x0 . nat_p x0 ⟶ 0 ∈ ordsucc x0
Known nat_p_trans^nat_p_trans : ∀ x0 . nat_p x0 ⟶ ∀ x1 . x1 ∈ x0 ⟶ nat_p x1
Known nat_ordsucc^nat_ordsucc : ∀ x0 . nat_p x0 ⟶ nat_p (ordsucc x0)
Known cases_1^cases_1 : ∀ x0 . x0 ∈ 1 ⟶ ∀ x1 : ι → ο . x1 0 ⟶ x1 x0
Known ordsuccE^ordsuccE : ∀ x0 x1 . x1 ∈ ordsucc x0 ⟶ or (x1 ∈ x0) (x1 = x0)
Known ordsuccI1^ordsuccI1 : ∀ x0 . x0 ⊆ ordsucc x0
Param ordinal^ordinal : ι → ο
Definition TransSet^TransSet := λ x0 . ∀ x1 . x1 ∈ x0 ⟶ x1 ⊆ x0
Known ordinal_TransSet^{ordinal_TransSet} : ∀ x0 . ordinal x0 ⟶ TransSet x0
Known nat_p_ordinal^{nat_p_ordinal} : ∀ x0 . nat_p x0 ⟶ ordinal x0
Theorem radical_field_extension_E^{radical_field_extension_E} : ∀ x0 x1 . radical_field_extension x0 x1 ⟶ ∀ x2 : ο . (Field x0 ⟶ Field x1 ⟶ subfield x0 x1 ⟶ ∀ x3 . x3 ∈ omega ⟶ ∀ x4 . ap x4 0 = x0 ⟶ ap x4 x3 = x1 ⟶ (∀ x5 . x5 ∈ ordsucc x3 ⟶ Field (ap x4 x5)) ⟶ (∀ x5 . x5 ∈ ordsucc x3 ⟶ ∀ x6 . x6 ∈ ordsucc x5 ⟶ subfield (ap x4 x6) (ap x4 x5)) ⟶ (∀ x5 . x5 ∈ x3 ⟶ ∀ x6 : ο . (∀ x7 . and (x7 ∈ field0 (ap x4 (ordsucc x5))) (∀ x8 : ο . (∀ x9 . and (x9 ∈ omega) (and (CRing_with_id_omega_exp (ap x4 (ordsucc x5)) x7 x9 ∈ field0 (ap x4 x5)) (Field_extension_by_1 (ap x4 x5) (ap x4 (ordsucc x5)) x7)) ⟶ x8) ⟶ x8) ⟶ x6) ⟶ x6) ⟶ x2) ⟶ x2 (proof)
Param CRing_with_id_eval_poly^{CRing_eval_poly} : ι → ι → ι → ι → ι
Definition ca601.. := λ x0 x1 x2 x3 . and (and (subfield x0 x1) (x3 ∈ setexp (field0 x0) (ordsucc x2))) (∀ x4 : ο . (∀ x5 . and (x5 ∈ setminus (field0 x0) (Sing (field3 x0))) (and (ap x3 x2 = x5) (∀ x6 : ο . (∀ x7 . and (x7 ∈ setexp (setexp (field0 x1) 2) x2) (and (∀ x8 . x8 ∈ x2 ⟶ ap (ap x7 x8) 1 = field4 x0) (∀ x8 . x8 ∈ field0 x1 ⟶ CRing_with_id_eval_poly x1 (ordsucc x2) x3 x8 = nat_primrec x5 (λ x10 x11 . field2b x1 x11 (CRing_with_id_eval_poly x1 2 (ap x7 x10) x8)) x2)) ⟶ x6) ⟶ x6)) ⟶ x4) ⟶ x4)
Definition e95e2.. := λ x0 x1 x2 x3 . and (ca601.. x0 x1 x2 x3) (∀ x4 . ca601.. x0 x4 x2 x3 ⟶ ∀ x5 : ο . (∀ x6 . and (and (Field_Hom x1 x4 x6) (∀ x7 . x7 ∈ field0 x0 ⟶ ap x6 x7 = x7)) (∀ x7 . x7 ∈ field0 x0 ⟶ ∀ x8 . x8 ∈ field0 x0 ⟶ ap x6 x7 = ap x6 x8 ⟶ x7 = x8) ⟶ x5) ⟶ x5)
Definition a42d3.. := λ x0 x1 x2 . ∀ x3 : ο . (∀ x4 . (∀ x5 : ο . (∀ x6 . and (and (e95e2.. x0 x4 x1 x2) (subfield x4 x6)) (radical_field_extension x0 x6) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Definition Field_automorphism_fixing^{Field_automorphism_fixing} := λ x0 x1 x2 . and (and (and (subfield x1 x0) (Field_Hom x0 x0 x2)) (∀ x3 . x3 ∈ ap x0 0 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ ap x0 0) (ap x2 x5 = x3) ⟶ x4) ⟶ x4)) (∀ x3 . x3 ∈ ap x1 0 ⟶ ap x2 x3 = x3)
Theorem Field_automorphism_fixing_I^{Field_automorphism_fixing_I} : ∀ x0 x1 x2 . subfield x1 x0 ⟶ Field_Hom x0 x0 x2 ⟶ (∀ x3 . x3 ∈ ap x0 0 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ ap x0 0) (ap x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ (∀ x3 . x3 ∈ ap x1 0 ⟶ ap x2 x3 = x3) ⟶ Field_automorphism_fixing x0 x1 x2 (proof)
Known and4E^and4E : ∀ x0 x1 x2 x3 : ο . and (and (and x0 x1) x2) x3 ⟶ ∀ x4 : ο . (x0 ⟶ x1 ⟶ x2 ⟶ x3 ⟶ x4) ⟶ x4
Theorem Field_automorphism_fixing_E^{Field_automorphism_fixing_E} : ∀ x0 x1 x2 . Field_automorphism_fixing x0 x1 x2 ⟶ ∀ x3 : ο . (subfield x1 x0 ⟶ Field_Hom x0 x0 x2 ⟶ (∀ x4 . x4 ∈ ap x0 0 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ ap x0 0) (ap x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ (∀ x4 . x4 ∈ ap x1 0 ⟶ ap x2 x4 = x4) ⟶ x3) ⟶ x3 (proof)
Param lam^Sigma : ι → (ι → ι) → ι
Definition lam_comp^lam_comp := λ x0 x1 x2 . lam x0 (λ x3 . ap x1 (ap x2 x3))
Definition lam_id^lam_id := λ x0 . lam x0 (λ x1 . x1)
Known lam_Pi^lam_Pi : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1 x3) ⟶ lam x0 x2 ∈ Pi x0 x1
Theorem lam_comp_exp_In^{lam_comp_exp_In} : ∀ x0 x1 x2 x3 . x3 ∈ setexp x1 x0 ⟶ ∀ x4 . x4 ∈ setexp x2 x1 ⟶ lam_comp x0 x4 x3 ∈ setexp x2 x0 (proof)
Theorem lam_id_exp_In^{lam_id_exp_In} : ∀ x0 . lam_id x0 ∈ setexp x0 x0 (proof)
Known encode_u_ext^encode_u_ext : ∀ x0 . ∀ x1 x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x1 x3 = x2 x3) ⟶ lam x0 x1 = lam x0 x2
Known beta^beta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ x0 ⟶ ap (lam x0 x1) x2 = x1 x2
Theorem lam_comp_assoc^{lam_comp_assoc} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ ∀ x3 x4 . lam_comp x0 x4 (lam_comp x0 x3 x2) = lam_comp x0 (lam_comp x1 x4 x3) x2 (proof)
Known Pi_eta^Pi_eta : ∀ x0 . ∀ x1 : ι → ι . ∀ x2 . x2 ∈ Pi x0 x1 ⟶ lam x0 (ap x2) = x2
Theorem lam_comp_id_L^{lam_comp_id_L} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 (lam_id x1) x2 = x2 (proof)
Theorem lam_comp_id_R^{lam_comp_id_R} : ∀ x0 x1 x2 . x2 ∈ setexp x1 x0 ⟶ lam_comp x0 x2 (lam_id x0) = x2 (proof)
Theorem Field_Hom_id^Field_Hom_id : ∀ x0 . Field x0 ⟶ Field_Hom x0 x0 (lam_id (ap x0 0)) (proof)
Theorem Field_Hom_comp^{Field_Hom_comp} : ∀ x0 x1 x2 x3 x4 . Field_Hom x0 x1 x3 ⟶ Field_Hom x1 x2 x4 ⟶ Field_Hom x0 x2 (lam_comp (ap x0 0) x4 x3) (proof)
Param pack_b^pack_b : ι → CT2 ι
Param Sep^Sep : ι → (ι → ο) → ι
Definition Galois_Group^Galois_Group := λ x0 x1 . pack_b (Sep (setexp (ap x0 0) (ap x0 0)) (Field_automorphism_fixing x0 x1)) (lam_comp (ap x0 0))
Known pack_b_0_eq2^pack_b_0_eq2 : ∀ x0 . ∀ x1 : ι → ι → ι . x0 = ap (pack_b x0 x1) 0
Theorem Galois_Group_0^{Galois_Group_0} : ∀ x0 x1 . ap (Galois_Group x0 x1) 0 = Sep (setexp (ap x0 0) (ap x0 0)) (Field_automorphism_fixing x0 x1) (proof)
Definition explicit_Group^{explicit_Group} := λ x0 . λ x1 : ι → ι → ι . and (and (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4)) (∀ x2 : ο . (∀ x3 . and (x3 ∈ x0) (and (∀ x4 . x4 ∈ x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (and (x1 x4 x6 = x3) (x1 x6 x4 = x3)) ⟶ x5) ⟶ x5)) ⟶ x2) ⟶ x2)
Known GroupI^GroupI : ∀ x0 . ∀ x1 : ι → ι → ι . explicit_Group x0 x1 ⟶ Group (pack_b x0 x1)
Known SepI^SepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ⟶ x2 ∈ Sep x0 x1
Param inv^inv : ι → (ι → ι) → ι → ι
Known bijE^bijE : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ ∀ x3 : ο . ((∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x1) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 . x4 ∈ x1 ⟶ ∀ x5 : ο . (∀ x6 . and (x6 ∈ x0) (x2 x6 = x4) ⟶ x5) ⟶ x5) ⟶ x3) ⟶ x3
Known inj_linv_coddep : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ ∀ x3 . x3 ∈ x0 ⟶ inv x0 x2 (x2 x3) = x3
Known surj_rinv^surj_rinv : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ ∀ x3 . x3 ∈ x1 ⟶ and (inv x0 x2 x3 ∈ x0) (x2 (inv x0 x2 x3) = x3)
Known bij_inv^bij_inv : ∀ x0 x1 . ∀ x2 : ι → ι . bij x0 x1 x2 ⟶ bij x1 x0 (inv x0 x2)
Known bijI^bijI : ∀ x0 x1 . ∀ x2 : ι → ι . (∀ x3 . x3 ∈ x0 ⟶ x2 x3 ∈ x1) ⟶ (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4) ⟶ (∀ x3 . x3 ∈ x1 ⟶ ∀ x4 : ο . (∀ x5 . and (x5 ∈ x0) (x2 x5 = x3) ⟶ x4) ⟶ x4) ⟶ bij x0 x1 x2
Known SepE^SepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2 ∈ Sep x0 x1 ⟶ and (x2 ∈ x0) (x1 x2)
Theorem Galois_Group_Group^{Galois_Group_Group} : ∀ x0 x1 . subfield x0 x1 ⟶ Group (Galois_Group x1 x0) (proof)
Param pack_b_b_e_e^pack_b_b_e_e : ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι
Known pack_struct_b_b_e_e_I : ∀ x0 . ∀ x1 : ι → ι → ι . (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 x3 ∈ x0) ⟶ ∀ x2 : ι → ι → ι . (∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ x2 x3 x4 ∈ x0) ⟶ ∀ x3 . x3 ∈ x0 ⟶ ∀ x4 . x4 ∈ x0 ⟶ struct_b_b_e_e (pack_b_b_e_e x0 x1 x2 x3 x4)
Param RealsStruct^RealsStruct : ι → ο
Param RealsStruct_Q^{RealsStruct_Q} : ι → ι
Param RealsStruct_one^{RealsStruct_one} : ι → ι
Param Field_of_RealsStruct^{Field_of_RealsStruct} : ι → ι
Param natOfOrderedField_p^{natOfOrderedField_p} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ι → ο
Param RealsStruct_leq^{RealsStruct_leq} : ι → ι → ι → ο
Definition RealsStruct_N^{RealsStruct_N} := λ x0 . Sep (field0 x0) (natOfOrderedField_p (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0))
Definition RealsStruct_Npos^{RealsStruct_Npos} := λ x0 . {x1 ∈ RealsStruct_N x0|x1 = field4 x0 ⟶ ∀ x2 : ο . x2}
Definition RealsStruct_Z^{RealsStruct_Z} := λ x0 . {x1 ∈ field0 x0|or (or (Field_minus (Field_of_RealsStruct x0) x1 ∈ RealsStruct_Npos x0) (x1 = field4 x0)) (x1 ∈ RealsStruct_Npos x0)}
Definition explicit_OrderedField_rationalp^{explicit_OrderedField_rationalp} := λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . λ x6 . ∀ x7 : ο . (∀ x8 . and (x8 ∈ {x9 ∈ x0|or (or (explicit_Field_minus x0 x1 x2 x3 x4 x9 ∈ {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1 ⟶ ∀ x11 : ο . x11}) (x9 = x1)) (x9 ∈ {x10 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x10 = x1 ⟶ ∀ x11 : ο . x11})}) (∀ x9 : ο . (∀ x10 . and (x10 ∈ {x11 ∈ Sep x0 (natOfOrderedField_p x0 x1 x2 x3 x4 x5)|x11 = x1 ⟶ ∀ x12 : ο . x12}) (x4 x10 x6 = x8) ⟶ x9) ⟶ x9) ⟶ x7) ⟶ x7
Param explicit_OrderedField^{explicit_OrderedField} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ο
Known explicit_Field_E^{explicit_Field_E} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ο . (explicit_Field x0 x1 x2 x3 x4 ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 x6 x7 ∈ x0) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x3 x6 (x3 x7 x8) = x3 (x3 x6 x7) x8) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 x6 x7 = x3 x7 x6) ⟶ x1 ∈ x0 ⟶ (∀ x6 . x6 ∈ x0 ⟶ x3 x1 x6 = x6) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 : ο . (∀ x8 . and (x8 ∈ x0) (x3 x6 x8 = x1) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x6 x7 ∈ x0) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x4 x6 (x4 x7 x8) = x4 (x4 x6 x7) x8) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x4 x6 x7 = x4 x7 x6) ⟶ x2 ∈ x0 ⟶ (x2 = x1 ⟶ ∀ x6 : ο . x6) ⟶ (∀ x6 . x6 ∈ x0 ⟶ x4 x2 x6 = x6) ⟶ (∀ x6 . x6 ∈ x0 ⟶ (x6 = x1 ⟶ ∀ x7 : ο . x7) ⟶ ∀ x7 : ο . (∀ x8 . and (x8 ∈ x0) (x4 x6 x8 = x2) ⟶ x7) ⟶ x7) ⟶ (∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x4 x6 (x3 x7 x8) = x3 (x4 x6 x7) (x4 x6 x8)) ⟶ x5) ⟶ explicit_Field x0 x1 x2 x3 x4 ⟶ x5
Known Field_unpack_eq^{Field_unpack_eq} : ∀ x0 . ∀ x1 x2 : ι → ι → ι . ∀ x3 x4 . unpack_b_b_e_e_o (pack_b_b_e_e x0 x1 x2 x3 x4) (λ x6 . λ x7 x8 : ι → ι → ι . λ x9 x10 . explicit_Field x6 x9 x10 x7 x8) = explicit_Field x0 x3 x4 x1 x2
Known explicit_OrderedField_explicit_Field_Q^{explicit_OrderedField_explicit_Field_Q} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ explicit_Field (Sep x0 (explicit_OrderedField_rationalp x0 x1 x2 x3 x4 x5)) x1 x2 x3 x4
Known explicit_OrderedField_of_RealsStruct^{explicit_OrderedField_of_RealsStruct} : ∀ x0 . RealsStruct x0 ⟶ explicit_OrderedField (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) (RealsStruct_leq x0)
Known RealsStruct_Q_props^{RealsStruct_Q_props} : ∀ x0 . RealsStruct x0 ⟶ ∀ x1 : ο . (RealsStruct_Q x0 ⊆ field0 x0 ⟶ (∀ x2 . x2 ∈ RealsStruct_Q x0 ⟶ ∀ x3 : ο . (x2 ∈ field0 x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Z x0 ⟶ ∀ x5 . x5 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x5 x2 = x4 ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ field0 x0 ⟶ ∀ x3 . x3 ∈ RealsStruct_Z x0 ⟶ ∀ x4 . x4 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x4 x2 = x3 ⟶ x2 ∈ RealsStruct_Q x0) ⟶ x1) ⟶ x1
Known set_ext^set_ext : ∀ x0 x1 . x0 ⊆ x1 ⟶ x1 ⊆ x0 ⟶ x0 = x1
Known RealsStruct_minus_eq2^{RealsStruct_minus_eq2} : ∀ x0 . RealsStruct x0 ⟶ ∀ x1 . x1 ∈ field0 x0 ⟶ Field_minus (Field_of_RealsStruct x0) x1 = explicit_Field_minus (field0 x0) (field4 x0) (RealsStruct_one x0) (field1b x0) (field2b x0) x1
Theorem Field_RealsStruct_Q^{Field_RealsStruct_Q} : ∀ x0 . RealsStruct x0 ⟶ Field (pack_b_b_e_e (RealsStruct_Q x0) (field1b x0) (field2b x0) (field4 x0) (RealsStruct_one x0)) (proof)
Definition RealsStruct_omega_embedding^{RealsStruct_omega_embedding} := λ x0 . nat_primrec (field4 x0) (λ x1 x2 . field1b x0 x2 (RealsStruct_one x0))
Param explicit_Nats^{explicit_Nats} : ι → ι → (ι → ι) → ο
Known explicit_Nats_E^{explicit_Nats_E} : ∀ x0 x1 . ∀ x2 : ι → ι . ∀ x3 : ο . (explicit_Nats x0 x1 x2 ⟶ x1 ∈ x0 ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 ∈ x0) ⟶ (∀ x4 . x4 ∈ x0 ⟶ x2 x4 = x1 ⟶ ∀ x5 : ο . x5) ⟶ (∀ x4 . x4 ∈ x0 ⟶ ∀ x5 . x5 ∈ x0 ⟶ x2 x4 = x2 x5 ⟶ x4 = x5) ⟶ (∀ x4 : ι → ο . x4 x1 ⟶ (∀ x5 . x4 x5 ⟶ x4 (x2 x5)) ⟶ ∀ x5 . x5 ∈ x0 ⟶ x4 x5) ⟶ x3) ⟶ explicit_Nats x0 x1 x2 ⟶ x3
Known nat_primrec_0^{nat_primrec_0} : ∀ x0 . ∀ x1 : ι → ι → ι . nat_primrec x0 x1 0 = x0
Known nat_primrec_S^{nat_primrec_S} : ∀ x0 . ∀ x1 : ι → ι → ι . ∀ x2 . nat_p x2 ⟶ nat_primrec x0 x1 (ordsucc x2) = x1 x2 (nat_primrec x0 x1 x2)
Known RealsStruct_natOfOrderedField^{RealsStruct_natOfOrderedField} : ∀ x0 . RealsStruct x0 ⟶ explicit_Nats (RealsStruct_N x0) (field4 x0) (λ x1 . field1b x0 x1 (RealsStruct_one x0))
Theorem RealsStruct_omega_embedding_N^{RealsStruct_omega_embedding_N} : ∀ x0 . RealsStruct x0 ⟶ ∀ x1 . x1 ∈ omega ⟶ RealsStruct_omega_embedding x0 x1 ∈ RealsStruct_N x0 (proof)