Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Apply RealsStruct_Npos_props with x0, RealsStruct_Npos x0 ⊆ field0 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 H1.
■