Proofgold Proof

Apply explicit_OrderedField_E with x0, x1, x2, x3, x4, x5, ∀ x6 : ο . (... ⟶ ... ⟶ ... ⟶ ... ⟶ (∀ x7 . ... ⟶ ∀ x8 : ι → ο . ... ⟶ (∀ x9 . x9 ∈ {x10 ∈ {x10 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 ... ...}|...} ⟶ x8 (x3 x9 x2)) ⟶ x8 x7) ⟶ (∀ x7 . x7 ∈ {x8 ∈ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} ⟶ ∀ x8 . x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} ⟶ explicit_Nats_one_plus {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} x2 (λ x9 . x3 x9 x2) x7 x8 = x3 x7 x8) ⟶ (∀ x7 . x7 ∈ {x8 ∈ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} ⟶ ∀ x8 . x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} ⟶ explicit_Nats_one_mult {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} x2 (λ x9 . x3 x9 x2) x7 x8 = x4 x7 x8) ⟶ (∀ x7 . x7 ∈ {x8 ∈ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} ⟶ ∀ x8 . x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} ⟶ x3 x7 x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10}) ⟶ (∀ x7 . x7 ∈ {x8 ∈ {x8 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x8}|x8 = x1 ⟶ ∀ x9 : ο . x9} ⟶ ∀ x8 . x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10} ⟶ x4 x7 x8 ∈ {x9 ∈ {x9 ∈ x0|natOfOrderedField_p x0 x1 x2 x3 x4 x5 x9}|x9 = x1 ⟶ ∀ x10 : ο . x10}) ⟶ x6) ⟶ x6.