Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: diadic_rational_alt1_p x0.
Apply H0 with x0 ∈ SNoS_ omega.
Let x1 of type ι be given.
Assume H1: (λ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ int_alt1) (x0 = mul_SNo (eps_ x2) x3))) x1.
Apply H1 with x0 ∈ SNoS_ omega.
Assume H2: x1 ∈ omega.
Assume H3: ∃ x2 . and (x2 ∈ int_alt1) (x0 = mul_SNo (eps_ x1) x2).
Apply H3 with x0 ∈ SNoS_ omega.
Let x2 of type ι be given.
Assume H4: (λ x3 . and (x3 ∈ int_alt1) (x0 = mul_SNo (eps_ x1) x3)) x2.
Apply H4 with x0 ∈ SNoS_ omega.
Assume H5: x2 ∈ int_alt1.
Assume H6: x0 = mul_SNo (eps_ x1) x2.
Apply H6 with λ x3 x4 . x4 ∈ SNoS_ omega.
Apply unknownprop_2504c05a08587fe0873ed45685efc417625f0a904281d653d757d643896f9a70 with λ x3 . mul_SNo (eps_ x1) x3 ∈ SNoS_ omega, x2 leaving 3 subgoals.
Let x3 of type ι be given.
Assume H7: x3 ∈ omega.
Apply nonneg_diadic_rational_p_SNoS_omega with x1, x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply omega_nat_p with x3.
The subproof is completed by applying H7.
Let x3 of type ι be given.
Assume H7: x3 ∈ omega.
Apply mul_SNo_minus_distrR with eps_ x1, x3, λ x4 x5 . x5 ∈ SNoS_ omega leaving 3 subgoals.
Apply SNo_eps_ with x1.
The subproof is completed by applying H2.
Apply omega_SNo with x3.
The subproof is completed by applying H7.
Apply minus_SNo_SNoS_omega with mul_SNo (eps_ x1) x3.
Apply nonneg_diadic_rational_p_SNoS_omega with x1, x3 leaving 2 subgoals.
The subproof is completed by applying H2.
Apply omega_nat_p with x3.
The subproof is completed by applying H7.
The subproof is completed by applying H5.
■