Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: RealsStruct x0.

Apply RealsStruct_Npos_props with x0, RealsStruct_one x0 ∈ RealsStruct_Npos x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Assume H1: RealsStruct_Npos x0 ⊆ field0 x0.

Assume H2: explicit_Nats (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x1 . field1b x0 x1 (RealsStruct_one x0)).

Assume H3: RealsStruct_one x0 ∈ RealsStruct_Npos x0.

Assume H4: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x1 (RealsStruct_one x0) = RealsStruct_one x0 ⟶ ∀ x2 : ο . x2.

Assume H5: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ ∀ x2 : ι → ο . x2 (RealsStruct_one x0) ⟶ (∀ x3 . x3 ∈ RealsStruct_Npos x0 ⟶ x2 (field1b x0 x3 (RealsStruct_one x0))) ⟶ x2 x1.

Assume H6: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_plus (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x1 x2 = field1b x0 x1 x2.

Assume H7: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ explicit_Nats_one_mult (RealsStruct_Npos x0) (RealsStruct_one x0) (λ x3 . field1b x0 x3 (RealsStruct_one x0)) x1 x2 = field2b x0 x1 x2.

Assume H8: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ field1b x0 x1 x2 ∈ RealsStruct_Npos x0.

Assume H9: ∀ x1 . x1 ∈ RealsStruct_Npos x0 ⟶ ∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ field2b x0 x1 x2 ∈ RealsStruct_Npos x0.

The subproof is completed by applying H3.

■