Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoLev_ind with λ x0 . x0 ∈ real ⟶ SNoLt 0 x0 ⟶ and (recip_SNo_pos x0 ∈ real) (∀ x1 . nat_p x1 ⟶ and (ap (SNo_recipaux x0 recip_SNo_pos x1) 0 ⊆ real) (ap (SNo_recipaux x0 recip_SNo_pos x1) 1 ⊆ real)).
Let x0 of type ι be given.
Assume H0: SNo x0.
Assume H1: ∀ x1 . x1 ∈ SNoS_ (SNoLev x0) ⟶ x1 ∈ real ⟶ SNoLt 0 x1 ⟶ and (recip_SNo_pos x1 ∈ real) (∀ x2 . nat_p x2 ⟶ and (∀ x3 . x3 ∈ ap (SNo_recipaux x1 recip_SNo_pos x2) 0 ⟶ x3 ∈ real) (∀ x3 . x3 ∈ ap (SNo_recipaux x1 recip_SNo_pos x2) 1 ⟶ x3 ∈ real)).
Assume H2: x0 ∈ real.
Assume H3: SNoLt 0 x0.
Apply real_E with x0, and (recip_SNo_pos x0 ∈ real) (∀ x1 . nat_p x1 ⟶ and (ap (SNo_recipaux x0 recip_SNo_pos x1) 0 ⊆ real) (ap (SNo_recipaux x0 recip_SNo_pos x1) 1 ⊆ real)) leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H4: SNo x0.
Assume H5: SNoLev x0 ∈ ordsucc omega.
Assume H6: x0 ∈ SNoS_ (ordsucc omega).
Assume H7: SNoLt (minus_SNo omega) x0.
Assume H8: SNoLt x0 omega.
Assume H9: ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0.
Assume H10: ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).
Claim L11: ...
...
Claim L12: ...
...
Claim L13: ...
...
Apply andI with recip_SNo_pos x0 ∈ real, ∀ x1 . nat_p x1 ⟶ and (ap (SNo_recipaux x0 recip_SNo_pos x1) 0 ⊆ real) (ap (SNo_recipaux x0 recip_SNo_pos x1) 1 ⊆ real) leaving 2 subgoals.
Claim L14: ...
...
Apply SNoCutP_SNoCut_impred with famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 0), famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 1), recip_SNo_pos x0 ∈ real leaving 2 subgoals.
Apply SNo_recipaux_lem2 with x0, recip_SNo_pos leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
The subproof is completed by applying L14.
Assume H15: SNo (SNoCut (famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 0)) (famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 1))).
Assume H16: SNoLev (SNoCut (famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 0)) (famunion omega (λ x1 . ap (SNo_recipaux x0 recip_SNo_pos x1) 1))) ∈ ....
...
...
■