Let x0 of type ι → ι be given.

Let x1 of type ι be given.

Assume H0: prime_nat x1.

Apply nat_ind with λ x2 . (∀ x3 . x3 ∈ x2 ⟶ x0 x3 ∈ int) ⟶ divides_int x1 (05ecb.. x0 x2) ⟶ ∃ x3 . and (x3 ∈ x2) (divides_int x1 (x0 x3)) leaving 2 subgoals.

Assume H1: ∀ x2 . x2 ∈ 0 ⟶ x0 x2 ∈ int.

Apply unknownprop_89e7310d38716ec0d15b566dbd8df2f84011da8cd7b706cd43ff87121048033c with x0, λ x2 x3 . divides_int x1 x3 ⟶ ∃ x4 . and (x4 ∈ 0) (divides_int x1 (x0 x4)).

Assume H2: divides_int x1 1.

Apply FalseE with ∃ x2 . and (x2 ∈ 0) (divides_int x1 (x0 x2)).

Apply unknownprop_b9f761a9aaf971afc2c321abccc5415a4ba796124b1aaa309d3f974fda1d3d26 with x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Assume H1: nat_p x2.

Assume H2: (∀ x3 . x3 ∈ x2 ⟶ x0 x3 ∈ int) ⟶ divides_int x1 (05ecb.. x0 x2) ⟶ ∃ x3 . and (x3 ∈ x2) (divides_int x1 (x0 x3)).

Assume H3: ∀ x3 . x3 ∈ ordsucc x2 ⟶ x0 x3 ∈ int.

Apply unknownprop_bfe386a724e0556e84046f452d416531498b4ec738b589b2f6a1e7f84e7dc85a with x0, x2, λ x3 x4 . divides_int x1 x4 ⟶ ∃ x5 . and (x5 ∈ ordsucc x2) (divides_int x1 (x0 x5)) leaving 2 subgoals.

The subproof is completed by applying H1.

Assume H4: divides_int x1 (mul_SNo (05ecb.. x0 x2) (x0 x2)).

Apply Euclid_lemma with x1, 05ecb.. x0 x2, x0 x2, ∃ x3 . and (x3 ∈ ordsucc x2) (divides_int x1 (x0 x3)) leaving 6 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_011f99952d91f5c9bc9ff9ee00f31f06ef53c987461d5dae73baece4fa270e16 with x0, x2 leaving 2 subgoals.

The subproof is completed by applying H1.

Let x3 of type ι be given.

Assume H5: x3 ∈ x2.

Apply H3 with x3.

Apply ordsuccI1 with x2, x3.

The subproof is completed by applying H5.

Apply H3 with x2.

The subproof is completed by applying ordsuccI2 with x2.

The subproof is completed by applying H4.

Assume H5: divides_int x1 (05ecb.. x0 x2).

Apply H2 with ∃ x3 . and (x3 ∈ ordsucc x2) (divides_int x1 (x0 x3)) leaving 3 subgoals.

Let x3 of type ι be given.

Assume H6: x3 ∈ x2.

Apply H3 with x3.

Apply ordsuccI1 with x2, x3.

The subproof is completed by applying H6.

The subproof is completed by applying H5.

Let x3 of type ι be given.

Assume H6: (λ x4 . and (x4 ∈ x2) (divides_int x1 (x0 x4))) x3.

Apply H6 with ∃ x4 . and (x4 ∈ ordsucc x2) (divides_int x1 (x0 x4)).

Assume H7: x3 ∈ x2.

Assume H8: divides_int x1 (x0 x3).

Let x4 of type ο be given.

Assume H9: ∀ x5 . and (x5 ∈ ordsucc x2) (divides_int x1 (x0 x5)) ⟶ x4.

Apply H9 with x3.

Apply andI with x3 ∈ ordsucc x2, divides_int x1 (x0 x3) leaving 2 subgoals.

Apply ordsuccI1 with x2, x3.

The subproof is completed by applying H7.

The subproof is completed by applying H8.

Assume H5: divides_int x1 (x0 x2).

Let x3 of type ο be given.

Assume H6: ∀ x4 . and (x4 ∈ ordsucc x2) (divides_int x1 (x0 x4)) ⟶ x3.

Apply H6 with x2.

Apply andI with x2 ∈ ordsucc x2, divides_int x1 (x0 x2) leaving 2 subgoals.

The subproof is completed by applying ordsuccI2 with x2.

The subproof is completed by applying H5.

■

Proofgold Proof