Apply and7I with ∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln x0 x0 x0, ∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln 0 x0 x0, ∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln x0 0 x0, ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ SNoLt x0 x1 ⟶ ∀ x2 . gcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2 ⟶ gcd_reln x0 x1 x2, ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ SNoLt x1 x0 ⟶ ∀ x2 . gcd_reln x1 x0 x2 ⟶ gcd_reln x0 x1 x2, ∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ int ⟶ SNoLt x1 0 ⟶ ∀ x2 . gcd_reln x0 (minus_SNo x1) x2 ⟶ gcd_reln x0 x1 x2, ∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ SNoLt x0 0 ⟶ ∀ x2 . gcd_reln (minus_SNo x0) x1 x2 ⟶ gcd_reln x0 x1 x2 leaving 7 subgoals.

The subproof is completed by applying gcd_id.

The subproof is completed by applying gcd_0.

Let x0 of type ι be given.

Assume H0: x0 ∈ setminus omega (Sing 0).

Apply gcd_sym with 0, x0, x0.

Apply gcd_0 with x0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι be given.

Assume H1: x1 ∈ omega.

Assume H2: SNoLt x0 x1.

Let x2 of type ι be given.

Apply euclidean_algorithm_prop_1 with x0, x1, x2.

Apply Subq_omega_int with x1.

The subproof is completed by applying H1.

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι be given.

Assume H1: x1 ∈ omega.

Assume H2: SNoLt x1 x0.

The subproof is completed by applying gcd_sym with x1, x0.

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ι be given.

Assume H1: x1 ∈ int.

Assume H2: SNoLt x1 0.

Let x2 of type ι be given.

Apply minus_SNo_invol with x1, λ x3 x4 . gcd_reln x0 (minus_SNo x1) x2 ⟶ gcd_reln x0 x3 x2 leaving 2 subgoals.

Apply int_SNo with x1.

The subproof is completed by applying H1.

The subproof is completed by applying gcd_minus with x0, minus_SNo x1, x2.

Let x0 of type ι be given.

Assume H0: x0 ∈ int.

Let x1 of type ι be given.

Assume H1: x1 ∈ int.

Assume H2: SNoLt x0 0.

Let x2 of type ι be given.

Assume H3: gcd_reln (minus_SNo x0) x1 x2.

Apply gcd_sym with x1, x0, x2.

Apply minus_SNo_invol with x0, λ x3 x4 . gcd_reln x1 x3 x2 leaving 2 subgoals.

Apply int_SNo with x0.

The subproof is completed by applying H0.

Apply gcd_minus with x1, minus_SNo x0, x2.

Apply gcd_sym with minus_SNo x0, x1, x2.

The subproof is completed by applying H3.

■

Proofgold Proof