Proofgold Address

Theorem f_eq_i^f_eq_i : ∀ x0 : ι → ι . ∀ x1 x2 . x1 = x2 ⟶ x0 x1 = x0 x2 (proof)
Theorem f_eq_i_i^f_eq_i_i : ∀ x0 : ι → ι → ι . ∀ x1 x2 x3 x4 . x1 = x2 ⟶ x3 = x4 ⟶ x0 x1 x3 = x0 x2 x4 (proof)
Param explicit_Field^{explicit_Field} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ο
Param explicit_Field_minus^{explicit_Field_minus} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → ι → ι
Definition and^and := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x1 ⟶ x2) ⟶ x2
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 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 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
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 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 (proof)
Theorem 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) (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
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 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) (proof)
Theorem 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) (proof)
Theorem 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) (proof)
Definition False^False := ∀ x0 : ο . x0
Definition not^not := λ x0 : ο . x0 ⟶ False
Known dneg^dneg : ∀ x0 : ο . not (not x0) ⟶ x0
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 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 (proof)
Param explicit_OrderedField^{explicit_OrderedField} : ι → ι → ι → (ι → ι → ι) → (ι → ι → ι) → (ι → ι → ο) → ο
Definition iff^iff := λ x0 x1 : ο . and (x0 ⟶ x1) (x1 ⟶ x0)
Definition or^or := λ x0 x1 : ο . ∀ x2 : ο . (x0 ⟶ x2) ⟶ (x1 ⟶ x2) ⟶ x2
Known explicit_OrderedField_E^{explicit_OrderedField_E} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . ∀ x6 : ο . (explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ explicit_Field x0 x1 x2 x3 x4 ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ x5 x7 x8 ⟶ x5 x8 x9 ⟶ x5 x7 x9) ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ iff (and (x5 x7 x8) (x5 x8 x7)) (x7 = x8)) ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ or (x5 x7 x8) (x5 x8 x7)) ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ ∀ x9 . x9 ∈ x0 ⟶ x5 x7 x8 ⟶ x5 (x3 x7 x9) (x3 x8 x9)) ⟶ (∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x5 x1 x7 ⟶ x5 x1 x8 ⟶ x5 x1 (x4 x7 x8)) ⟶ x6) ⟶ explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ x6
Theorem explicit_OrderedField_minus_leq^{explicit_OrderedField_minus_leq} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x6 x7 ⟶ x5 (explicit_Field_minus x0 x1 x2 x3 x4 x7) (explicit_Field_minus x0 x1 x2 x3 x4 x6) (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 explicit_OrderedField_square_nonneg^{explicit_OrderedField_square_nonneg} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ x5 x1 (x4 x6 x6) (proof)
Theorem explicit_OrderedField_sum_squares_nonneg^{explicit_OrderedField_sum_squares_nonneg} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x1 (x3 (x4 x6 x6) (x4 x7 x7)) (proof)
Known andI^andI : ∀ x0 x1 : ο . x0 ⟶ x1 ⟶ and x0 x1
Theorem 19c47.. : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x1 x6 ⟶ x5 x1 x7 ⟶ x3 x6 x7 = x1 ⟶ x7 = x1 (proof)
Theorem explicit_OrderedField_sum_nonneg_zero_inv^{explicit_OrderedField_sum_nonneg_zero_inv} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x5 x1 x6 ⟶ x5 x1 x7 ⟶ x3 x6 x7 = x1 ⟶ and (x6 = x1) (x7 = x1) (proof)
Theorem explicit_OrderedField_sum_squares_zero_inv^{explicit_OrderedField_sum_squares_zero_inv} : ∀ x0 x1 x2 . ∀ x3 x4 : ι → ι → ι . ∀ x5 : ι → ι → ο . explicit_OrderedField x0 x1 x2 x3 x4 x5 ⟶ ∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x0 ⟶ x3 (x4 x6 x6) (x4 x7 x7) = x1 ⟶ and (x6 = x1) (x7 = x1) (proof)