Apply nat_complete_ind with λ x0 . 1 ∈ x0 ⟶ ∃ x1 . and (prime_nat x1) (divides_nat x1 x0).

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: ∀ x1 . x1 ∈ x0 ⟶ 1 ∈ x1 ⟶ ∃ x2 . and (prime_nat x2) (divides_nat x2 x1).

Assume H2: 1 ∈ x0.

Apply prime_nat_or_composite_nat with x0, ∃ x1 . and (prime_nat x1) (divides_nat x1 x0) leaving 4 subgoals.

Apply nat_p_omega with x0.

The subproof is completed by applying H0.

The subproof is completed by applying H2.

Assume H3: prime_nat x0.

Let x1 of type ο be given.

Assume H4: ∀ x2 . and (prime_nat x2) (divides_nat x2 x0) ⟶ x1.

Apply H4 with x0.

Apply andI with prime_nat x0, divides_nat x0 x0 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply unknownprop_98e7544997c6005aa9c4dc938c620a6df3d89601058380b842e41b24814e6d5b with x0.

The subproof is completed by applying H0.

Assume H3: composite_nat x0.

Apply H3 with ∃ x1 . and (prime_nat x1) (divides_nat x1 x0).

Assume H4: x0 ∈ omega.

Assume H5: ∃ x1 . and (x1 ∈ omega) (∃ x2 . and (x2 ∈ omega) (and (and (1 ∈ x1) (1 ∈ x2)) (mul_nat x1 x2 = x0))).

Apply H5 with ∃ x1 . and (prime_nat x1) (divides_nat x1 x0).

Let x1 of type ι be given.

Assume H6: (λ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ omega) (and (and (1 ∈ x2) (1 ∈ x3)) (mul_nat x2 x3 = x0)))) x1.

Apply H6 with ∃ x2 . and (prime_nat x2) (divides_nat x2 x0).

Assume H7: x1 ∈ omega.

Assume H8: ∃ x2 . and (x2 ∈ omega) (and (and (1 ∈ x1) (1 ∈ x2)) (mul_nat x1 x2 = x0)).

Apply H8 with ∃ x2 . and (prime_nat x2) (divides_nat x2 x0).

Let x2 of type ι be given.

Assume H9: (λ x3 . and (x3 ∈ omega) (and (and (1 ∈ x1) (1 ∈ x3)) (mul_nat x1 x3 = x0))) x2.

Apply H9 with ∃ x3 . and (prime_nat x3) (divides_nat x3 x0).

Assume H10: x2 ∈ omega.

Assume H11: and (and (1 ∈ x1) (1 ∈ x2)) (mul_nat x1 x2 = x0).

Apply H11 with ∃ x3 . and (prime_nat x3) (divides_nat x3 x0).

Assume H12: and (1 ∈ x1) (1 ∈ x2).

Apply H12 with mul_nat x1 x2 = x0 ⟶ ∃ x3 . and (prime_nat x3) (divides_nat x3 x0).

Assume H13: 1 ∈ x1.

Assume H14: 1 ∈ x2.

Assume H15: mul_nat x1 x2 = x0.

Apply H1 with x1, ∃ x3 . and (prime_nat x3) (divides_nat x3 x0) leaving 3 subgoals.

Apply H15 with λ x3 x4 . x1 ∈ x3.

Apply unknownprop_64298609228a1928dde1d66da0f04038e1112049f8f6469ec832eccc379525c0 with x1, x2 leaving 4 subgoals.

Apply omega_nat_p with x1.

The subproof is completed by applying H7.

Apply omega_nat_p with x2.

The subproof is completed by applying H10.

Apply nat_trans with x1, 1, 0 leaving 3 subgoals.

...

■

Proofgold Proof