Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: RealsStruct x0.
Let x1 of type ι be given.
Assume H1: x1 ∈ field0 x0.
Let x2 of type ι be given.
Assume H2: x2 ∈ field0 x0.
Assume H3: RealsStruct_leq x0 x1 x2.
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Claim L7: ...
...
Claim L8: ...
...
Claim L9: field1b x0 x2 (field1b x0 (Field_minus (Field_of_RealsStruct x0) x1) (Field_minus (Field_of_RealsStruct x0) x2)) = Field_minus (Field_of_RealsStruct x0) x1
set y3 to be ...
set y4 to be ...
Claim L9: ∀ x5 : ι → ο . x5 y4 ⟶ x5 y3
Let x5 of type ι → ο be given.
Assume H9: x5 (Field_minus (Field_of_RealsStruct x2) y3).
set y6 to be field1b ... ... ...
set y7 to be field1b y3 x5 (field1b y3 (Field_minus (Field_of_RealsStruct y3) x5) (Field_minus (Field_of_RealsStruct y3) y4))
Claim L10: ∀ x8 : ι → ο . x8 y7 ⟶ x8 y6
Let x8 of type ι → ο be given.
Assume H10: x8 (field1b y4 y6 (field1b y4 (Field_minus (Field_of_RealsStruct y4) y6) (Field_minus (Field_of_RealsStruct y4) x5))).
set y9 to be λ x9 . x8
Apply RealsStruct_plus_com with y4, Field_minus (Field_of_RealsStruct y4) x5, Field_minus (Field_of_RealsStruct y4) y6, λ x10 x11 . y9 (field1b y4 y6 x10) (field1b y4 y6 x11) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L4.
The subproof is completed by applying L5.
The subproof is completed by applying H10.
set y8 to be λ x8 . y7
Apply L10 with λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H11: y8 y7 y7.
The subproof is completed by applying H11.
Apply RealsStruct_plus_assoc with x5, y7, Field_minus (Field_of_RealsStruct x5) y7, Field_minus (Field_of_RealsStruct x5) y6, λ x9 . y8 leaving 5 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying L6.
The subproof is completed by applying L5.
set y9 to be field1b x5 (field1b x5 y7 (Field_minus (Field_of_RealsStruct x5) y7)) (Field_minus (Field_of_RealsStruct x5) y6)
set y10 to be field1b y6 (field4 y6) (Field_minus (Field_of_RealsStruct y6) y7)
Claim L11: ∀ x11 : ι → ο . x11 y10 ⟶ x11 y9
Let x11 of type ι → ο be given.
Assume H11: x11 (field1b y7 (field4 y7) (Field_minus (Field_of_RealsStruct y7) y8)).
set y12 to be λ x12 . x11
Apply RealsStruct_minus_R with y7, y9, λ x13 x14 . y12 (field1b y7 x13 (Field_minus (Field_of_RealsStruct y7) y8)) (field1b y7 x14 (Field_minus (Field_of_RealsStruct y7) y8)) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H3.
The subproof is completed by applying H11.
set y11 to be λ x11 . y10
Apply L11 with λ x12 . y11 x12 y10 ⟶ y11 y10 x12 leaving 2 subgoals.
Assume H12: y11 y10 y10.
The subproof is completed by applying H12.
Apply RealsStruct_zero_L with y8, Field_minus (Field_of_RealsStruct y8) y9, λ x12 . y11 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying L6.
The subproof is completed by applying L11.
Let x5 of type ι → ι → ο be given.
Apply L9 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H10: x5 y4 y4.
The subproof is completed by applying H10.
Apply L8 with λ x3 x4 . RealsStruct_leq x0 x3 (Field_minus (Field_of_RealsStruct x0) x1).
Apply L9 with λ x3 x4 . RealsStruct_leq x0 (field1b x0 x1 (field1b x0 (Field_minus (Field_of_RealsStruct x0) x1) (Field_minus (Field_of_RealsStruct x0) x2))) x3.
The subproof is completed by applying L7.
■