Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0SNoS_ omega.
Apply SNoS_omega_diadic_rational_p with x0, x0rational leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι be given.
Assume H1: (λ x2 . and (x2omega) (∃ x3 . and (x3int) (x0 = mul_SNo (eps_ x2) x3))) x1.
Apply H1 with x0rational.
Assume H2: x1omega.
Assume H3: ∃ x2 . and (x2int) (x0 = mul_SNo (eps_ x1) x2).
Apply H3 with x0rational.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3int) (x0 = mul_SNo (eps_ x1) x3)) x2.
Apply H4 with x0rational.
Assume H5: x2int.
Assume H6: x0 = mul_SNo (eps_ x1) x2.
Claim L7: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H2.
Apply SepI with real, λ x3 . ∃ x4 . and (x4int) (∃ x5 . and (x5setminus omega (Sing 0)) (x3 = div_SNo x4 x5)), x0 leaving 2 subgoals.
Apply SNoS_omega_real with x0.
The subproof is completed by applying H0.
Let x3 of type ο be given.
Assume H8: ∀ x4 . and (x4int) (∃ x5 . and (x5setminus omega (Sing 0)) (x0 = div_SNo x4 x5))x3.
Apply H8 with x2.
Apply andI with x2int, ∃ x4 . and (x4setminus omega (Sing 0)) (x0 = div_SNo x2 x4) leaving 2 subgoals.
The subproof is completed by applying H5.
Let x4 of type ο be given.
Assume H9: ∀ x5 . and (x5setminus omega (Sing 0)) (x0 = div_SNo x2 x5)x4.
Apply H9 with exp_SNo_nat 2 x1.
Apply andI with exp_SNo_nat 2 x1setminus omega (Sing 0), x0 = div_SNo x2 (exp_SNo_nat 2 x1) leaving 2 subgoals.
Apply setminusI with omega, Sing 0, exp_SNo_nat 2 x1 leaving 2 subgoals.
Apply nat_p_omega with exp_SNo_nat 2 x1.
Apply nat_exp_SNo_nat with 2, x1 leaving 2 subgoals.
The subproof is completed by applying nat_2.
The subproof is completed by applying L7.
Assume H10: exp_SNo_nat 2 x1Sing 0.
Apply neq_1_0.
Apply mul_SNo_eps_power_2 with x1, λ x5 x6 . x5 = 0 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply SingE with 0, exp_SNo_nat 2 x1, λ x5 x6 . mul_SNo (eps_ x1) x6 = 0 leaving 2 subgoals.
The subproof is completed by applying H10.
Apply mul_SNo_zeroR with eps_ x1.
Apply SNo_eps_ with x1.
The subproof is completed by applying H2.
Apply H6 with λ x5 x6 . x6 = mul_SNo x2 (recip_SNo (exp_SNo_nat 2 x1)).
Apply recip_SNo_pow_2 with x1, λ x5 x6 . mul_SNo (eps_ x1) x2 = mul_SNo x2 x6 leaving 2 subgoals.
The subproof is completed by applying L7.
Apply mul_SNo_com with eps_ x1, x2 leaving 2 subgoals.
Apply SNo_eps_ with x1.
The subproof is completed by applying H2.
Apply int_SNo with x2.
The subproof is completed by applying H5.