Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ real.
Assume H1: SNoLe 0 x0.
Apply real_E with x0, sqrt_SNo_nonneg x0 ∈ real leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H2: SNo x0.
Assume H3: SNoLev x0 ∈ ordsucc omega.
Assume H4: x0 ∈ SNoS_ (ordsucc omega).
Assume H5: SNoLt (minus_SNo omega) x0.
Assume H6: SNoLt x0 omega.
Assume H7: ∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0.
Assume H8: ∀ x1 . x1 ∈ omega ⟶ ∃ x2 . and (x2 ∈ SNoS_ omega) (and (SNoLt x2 x0) (SNoLt x0 (add_SNo x2 (eps_ x1)))).
Apply sqrt_SNo_nonneg_prop1 with x0, sqrt_SNo_nonneg x0 ∈ real leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H9: and (SNo (sqrt_SNo_nonneg x0)) (SNoLe 0 (sqrt_SNo_nonneg x0)).
Apply H9 with mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0 ⟶ sqrt_SNo_nonneg x0 ∈ real.
Assume H10: SNo (sqrt_SNo_nonneg x0).
Assume H11: SNoLe 0 (sqrt_SNo_nonneg x0).
Assume H12: mul_SNo (sqrt_SNo_nonneg x0) (sqrt_SNo_nonneg x0) = x0.
Apply ordsuccE with omega, SNoLev x0, sqrt_SNo_nonneg x0 ∈ real leaving 3 subgoals.
The subproof is completed by applying H3.
Assume H13: SNoLev x0 ∈ omega.
Apply sqrt_SNo_nonneg_SNoS_omega with x0 leaving 2 subgoals.
Apply SNoS_I with omega, x0, SNoLev x0 leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
The subproof is completed by applying H13.
Apply SNoLev_ with x0.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Assume H13: SNoLev x0 = omega.
Apply sqrt_SNo_nonneg_eq with x0, λ x1 x2 . x2 ∈ real leaving 2 subgoals.
The subproof is completed by applying H2.
Claim L14: ...
...
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Claim L18: ...
...
Claim L19: ...
...
Apply SNoCutP_SNoCut_impred with famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0) x1), famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) x1), SNoCut (famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 0) x1)) (famunion omega (λ x1 . (λ x2 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x2) 1) x1)) ∈ real leaving 2 subgoals.
Apply SNo_sqrt_SNo_SNoCutP with x0 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H1.
Apply sqrt_SNo_nonneg_eq with x0, λ x1 x2 . ... ⟶ ... ⟶ ... ⟶ ... ⟶ (∀ x3 . SNo x3 ⟶ (∀ x4 . x4 ∈ famunion omega (λ x5 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x5) 0) ⟶ SNoLt x4 x3) ⟶ (∀ x4 . x4 ∈ famunion omega (λ x5 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x5) 1) ⟶ SNoLt x3 x4) ⟶ and (SNoLev x1 ⊆ SNoLev x3) (SNoEq_ (SNoLev x1) x1 x3)) ⟶ SNoCut (famunion omega (λ x3 . (λ x4 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x4) 0) x3)) (famunion omega (λ x3 . (λ x4 . ap (SNo_sqrtaux x0 sqrt_SNo_nonneg x4) 1) x3)) ∈ real leaving 2 subgoals.
...
...
■