Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: diadic_rational_p x0.
Assume H1: SNoLt 0 x0.
Apply SNoS_E2 with omega, x0, ∃ x1 . and (x1 ∈ omega) (SNoLe (eps_ x1) x0) leaving 3 subgoals.
The subproof is completed by applying omega_ordinal.
Apply diadic_rational_p_SNoS_omega with x0.
The subproof is completed by applying H0.
Assume H2: SNoLev x0 ∈ omega.
Assume H3: ordinal (SNoLev x0).
Assume H4: SNo x0.
Assume H5: SNo_ (SNoLev x0) x0.
Apply H0 with ∃ x1 . and (x1 ∈ omega) (SNoLe (eps_ x1) x0).
Let x1 of type ι be given.
Assume H6: (λ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x2) x3))) x1.
Apply H6 with ∃ x2 . and (x2 ∈ omega) (SNoLe (eps_ x2) x0).
Assume H7: x1 ∈ omega.
Assume H8: ∃ x2 . and (x2 ∈ int) (x0 = mul_SNo (eps_ x1) x2).
Apply H8 with ∃ x2 . and (x2 ∈ omega) (SNoLe (eps_ x2) x0).
Let x2 of type ι be given.
Assume H9: (λ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x1) x3)) x2.
Apply H9 with ∃ x3 . and (x3 ∈ omega) (SNoLe (eps_ x3) x0).
Assume H10: x2 ∈ int.
Assume H11: x0 = mul_SNo (eps_ x1) x2.
Claim L12: ...
...
Let x3 of type ο be given.
Assume H13: ∀ x4 . and (x4 ∈ omega) (SNoLe (eps_ x4) x0) ⟶ x3.
Apply H13 with x1.
Apply andI with x1 ∈ omega, SNoLe (eps_ x1) x0 leaving 2 subgoals.
The subproof is completed by applying H7.
Apply H11 with λ x4 x5 . SNoLe (eps_ x1) x5.
Apply binunionE with omega, {minus_SNo x4|x4 ∈ omega}, x2, SNoLe (eps_ x1) (mul_SNo (eps_ x1) x2) leaving 3 subgoals.
The subproof is completed by applying H10.
Assume H14: x2 ∈ omega.
Apply nat_inv with x2, SNoLe (eps_ x1) (mul_SNo (eps_ x1) x2) leaving 3 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H14.
Assume H15: x2 = 0.
Apply FalseE with SNoLe (eps_ x1) (mul_SNo (eps_ x1) x2).
Apply L12.
Apply H11 with λ x4 x5 . SNoLe x5 0.
Apply H15 with λ x4 x5 . SNoLe (mul_SNo (eps_ x1) x5) 0.
Apply mul_SNo_zeroR with eps_ x1, λ x4 x5 . SNoLe x5 0 leaving 2 subgoals.
Apply SNo_eps_ with x1.
The subproof is completed by applying H7.
The subproof is completed by applying SNoLe_ref with 0.
Assume H15: ∃ x4 . and (nat_p x4) (x2 = ordsucc x4).
Apply H15 with SNoLe (eps_ x1) (mul_SNo (eps_ x1) x2).
Let x4 of type ι be given.
Assume H16: (λ x5 . and (nat_p x5) (x2 = ordsucc x5)) x4.
Apply H16 with SNoLe (eps_ x1) (mul_SNo (eps_ x1) x2).
Assume H17: nat_p x4.
Assume H18: x2 = ordsucc x4.
Apply H18 with λ x5 x6 . SNoLe (eps_ x1) (mul_SNo (eps_ x1) x6).
Apply ordinal_ordsucc_SNo_eq with x4, λ x5 x6 . SNoLe (eps_ x1) (mul_SNo (eps_ x1) x6) leaving 2 subgoals.
Apply nat_p_ordinal with x4.
The subproof is completed by applying H17.
...
...
■