Let x0 of type ι be given.

Assume H0: prime_nat x0.

Let x1 of type ι be given.

Assume H1: x1 ∈ int.

Let x2 of type ι be given.

Assume H2: x2 ∈ int.

Apply H0 with divides_int x0 (mul_SNo x1 x2) ⟶ or (divides_int x0 x1) (divides_int x0 x2).

Assume H3: and (x0 ∈ omega) (1 ∈ x0).

Apply H3 with (∀ x3 . x3 ∈ omega ⟶ divides_nat x3 x0 ⟶ or (x3 = 1) (x3 = x0)) ⟶ divides_int x0 (mul_SNo x1 x2) ⟶ or (divides_int x0 x1) (divides_int x0 x2).

Assume H4: x0 ∈ omega.

Assume H5: 1 ∈ x0.

Assume H6: ∀ x3 . x3 ∈ omega ⟶ divides_nat x3 x0 ⟶ or (x3 = 1) (x3 = x0).

Assume H7: divides_int x0 (mul_SNo x1 x2).

Claim L8: ...

...

Claim L9: ...

...

Apply xm with divides_int x0 x1, or (divides_int x0 x1) (divides_int x0 x2) leaving 2 subgoals.

The subproof is completed by applying orIL with divides_int x0 x1, divides_int x0 x2.

Assume H10: not (divides_int x0 x1).

Apply orIR with divides_int x0 x1, divides_int x0 x2.

Apply BezoutThm with x0, x1, 1, divides_int x0 x2 leaving 4 subgoals.

The subproof is completed by applying L9.

The subproof is completed by applying H1.

Assume H11: and (x0 = 0) (x1 = 0).

Apply H11 with False.

Assume H12: x0 = 0.

Assume H13: x1 = 0.

Apply In_no2cycle with 0, 1 leaving 2 subgoals.

The subproof is completed by applying In_0_1.

Apply H12 with λ x3 x4 . 1 ∈ x3.

The subproof is completed by applying H5.

Assume H11: gcd_reln x0 x1 1 ⟶ and (and (int_lin_comb x0 x1 1) (SNoLt 0 1)) (∀ x3 . int_lin_comb x0 x1 x3 ⟶ SNoLt 0 x3 ⟶ SNoLe 1 x3).

Assume H12: and (and (int_lin_comb x0 x1 1) (SNoLt 0 1)) (∀ x3 . int_lin_comb x0 x1 x3 ⟶ SNoLt 0 x3 ⟶ SNoLe 1 x3) ⟶ gcd_reln x0 x1 1.

Apply H11 with divides_int x0 x2 leaving 2 subgoals.

Apply and3I with divides_int 1 x0, divides_int 1 x1, ∀ x3 . divides_int x3 x0 ⟶ divides_int x3 x1 ⟶ SNoLe x3 1 leaving 3 subgoals.

Apply divides_int_1 with x0.

The subproof is completed by applying L9.

Apply divides_int_1 with x1.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Assume H13: divides_int x3 x0.

Assume H14: divides_int x3 x1.

Apply H13 with SNoLe x3 1.

Assume H15: and (x3 ∈ int) (x0 ∈ int).

Assume H16: ∃ x4 . and (x4 ∈ int) (mul_SNo x3 x4 = x0).

Apply H15 with SNoLe x3 1.

Assume H17: x3 ∈ int.

Assume H18: x0 ∈ int.

Apply SNoLtLe_or with x3, 0, SNoLe x3 1 leaving 4 subgoals.

Apply int_SNo with x3.

The subproof is completed by applying H17.

The subproof is completed by applying SNo_0.

Assume H19: SNoLt x3 0.

Apply SNoLtLe with x3, 1.

Apply SNoLt_tra with x3, 0, 1 leaving 5 subgoals.

Apply int_SNo with x3.

The subproof is completed by applying H17.

The subproof is completed by applying SNo_0.

The subproof is completed by applying SNo_1.

...

■

Proofgold Proof