Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
diadic_rational_p x1 ⟶ diadic_rational_p (mul_SNo x0 x1).
Let x2 of type ι be given.
Apply H1 with
diadic_rational_p x1 ⟶ diadic_rational_p (mul_SNo x0 x1).
Assume H2:
x2 ∈ omega.
Apply H3 with
diadic_rational_p x1 ⟶ diadic_rational_p (mul_SNo x0 x1).
Let x3 of type ι be given.
Apply H4 with
diadic_rational_p x1 ⟶ diadic_rational_p (mul_SNo x0 x1).
Apply H7 with
diadic_rational_p (mul_SNo x0 x1).
Let x4 of type ι be given.
Apply H8 with
diadic_rational_p (mul_SNo x0 x1).
Assume H9:
x4 ∈ omega.
Apply H10 with
diadic_rational_p (mul_SNo x0 x1).
Let x5 of type ι be given.
Apply H11 with
diadic_rational_p (mul_SNo x0 x1).
Let x6 of type ο be given.
Apply H14 with
add_SNo x2 x4.
Apply andI with
add_SNo x2 x4 ∈ omega,
∃ x7 . and (x7 ∈ int) (mul_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) x7) leaving 2 subgoals.
Apply add_SNo_In_omega with
x2,
x4 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H9.
Let x7 of type ο be given.
Apply H15 with
mul_SNo x3 x5.
Apply andI with
mul_SNo x3 x5 ∈ int,
mul_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) (mul_SNo x3 x5) leaving 2 subgoals.
Apply int_mul_SNo with
x3,
x5 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H12.
Apply mul_SNo_eps_eps_add_SNo with
x2,
x4,
λ x8 x9 . mul_SNo x0 x1 = mul_SNo x8 (mul_SNo x3 x5) leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H9.
Apply mul_SNo_com_4_inner_mid with
eps_ x2,
eps_ x4,
x3,
x5,
λ x8 x9 . mul_SNo x0 x1 = x9 leaving 5 subgoals.
Apply SNo_eps_ with
x2.
The subproof is completed by applying H2.