Let x0 of type ι be given.

Let x1 of type ι be given.

Assume H0: diadic_rational_alt1_p x0.

Apply H0 with diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (mul_SNo x0 x1).

Let x2 of type ι be given.

Assume H1: (λ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ int_alt1) (x0 = mul_SNo (eps_ x3) x4))) x2.

Apply H1 with diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (mul_SNo x0 x1).

Assume H2: x2 ∈ omega.

Assume H3: ∃ x3 . and (x3 ∈ int_alt1) (x0 = mul_SNo (eps_ x2) x3).

Apply H3 with diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (mul_SNo x0 x1).

Let x3 of type ι be given.

Assume H4: (λ x4 . and (x4 ∈ int_alt1) (x0 = mul_SNo (eps_ x2) x4)) x3.

Apply H4 with diadic_rational_alt1_p x1 ⟶ diadic_rational_alt1_p (mul_SNo x0 x1).

Assume H5: x3 ∈ int_alt1.

Assume H6: x0 = mul_SNo (eps_ x2) x3.

Assume H7: diadic_rational_alt1_p x1.

Apply H7 with diadic_rational_alt1_p (mul_SNo x0 x1).

Let x4 of type ι be given.

Assume H8: (λ x5 . and (x5 ∈ omega) (∃ x6 . and (x6 ∈ int_alt1) (x1 = mul_SNo (eps_ x5) x6))) x4.

Apply H8 with diadic_rational_alt1_p (mul_SNo x0 x1).

Assume H9: x4 ∈ omega.

Assume H10: ∃ x5 . and (x5 ∈ int_alt1) (x1 = mul_SNo (eps_ x4) x5).

Apply H10 with diadic_rational_alt1_p (mul_SNo x0 x1).

Let x5 of type ι be given.

Assume H11: (λ x6 . and (x6 ∈ int_alt1) (x1 = mul_SNo (eps_ x4) x6)) x5.

Apply H11 with diadic_rational_alt1_p (mul_SNo x0 x1).

Assume H12: x5 ∈ int_alt1.

Assume H13: x1 = mul_SNo (eps_ x4) x5.

Let x6 of type ο be given.

Assume H14: ∀ x7 . and (x7 ∈ omega) (∃ x8 . and (x8 ∈ int_alt1) (mul_SNo x0 x1 = mul_SNo (eps_ x7) x8)) ⟶ x6.

Apply H14 with add_SNo x2 x4.

Apply andI with add_SNo x2 x4 ∈ omega, ∃ x7 . and (x7 ∈ int_alt1) (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.

Assume H15: ∀ x8 . and (x8 ∈ int_alt1) (mul_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) x8) ⟶ x7.

Apply H15 with mul_SNo x3 x5.

Apply andI with mul_SNo x3 x5 ∈ int_alt1, mul_SNo x0 x1 = mul_SNo (eps_ (add_SNo x2 x4)) (mul_SNo x3 x5) leaving 2 subgoals.

Apply unknownprop_3f000c087708670f2a9497d0587231f65beb85593b7ebdaf7909fe5e7d4b8c27 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.

Apply SNo_eps_ with ....

...

■

Proofgold Proof