Claim L0: ∀ x0 . nat_p x0 ⟶ x0 ∈ setminus omega 2 ⟶ ∃ x1 . and (x1 ∈ omega) (and (prime_nat x1) (divides_nat x1 x0))

Apply nat_complete_ind with λ x0 . x0 ∈ setminus omega 2 ⟶ ∃ x1 . and (x1 ∈ omega) (and (prime_nat x1) (divides_nat x1 x0)).

Let x0 of type ι be given.

Assume H0: nat_p x0.

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

Assume H2: x0 ∈ setminus omega 2.

Apply xm with ∃ x1 . and (x1 ∈ setminus omega 2) (∃ x2 . and (x2 ∈ setminus omega 2) (mul_nat x1 x2 = x0)), ∃ x1 . and (x1 ∈ omega) (and (prime_nat x1) (divides_nat x1 x0)) leaving 2 subgoals.

Assume H3: ∃ x1 . and (x1 ∈ setminus omega 2) (∃ x2 . and (x2 ∈ setminus omega 2) (mul_nat x1 x2 = x0)).

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

Let x1 of type ι be given.

Assume H4: (λ x2 . and (x2 ∈ setminus omega 2) (∃ x3 . and (x3 ∈ setminus omega 2) (mul_nat x2 x3 = x0))) x1.

Apply H4 with ∃ x2 . and (x2 ∈ omega) (and (prime_nat x2) (divides_nat x2 x0)).

Assume H5: x1 ∈ setminus omega 2.

Assume H6: ∃ x2 . and (x2 ∈ setminus omega 2) (mul_nat x1 x2 = x0).

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

Let x2 of type ι be given.

Assume H7: (λ x3 . and (x3 ∈ setminus omega 2) (mul_nat x1 x3 = x0)) x2.

Apply H7 with ∃ x3 . and (x3 ∈ omega) (and (prime_nat x3) (divides_nat x3 x0)).

Assume H8: x2 ∈ setminus omega 2.

Assume H9: mul_nat x1 x2 = x0.

Claim L10: ...

...

Claim L11: ...

...

Claim L12: ...

...

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

The subproof is completed by applying L12.

The subproof is completed by applying H8.

Let x3 of type ι be given.

Assume H13: (λ x4 . and (x4 ∈ omega) (and (prime_nat x4) (divides_nat x4 x2))) x3.

Apply H13 with ∃ x4 . and (... ∈ ...) ....

...

Let x0 of type ι be given.

Assume H1: x0 ∈ setminus omega 2.

Claim L2: nat_p x0

Apply omega_nat_p with x0.

Apply setminusE1 with omega, 2, x0.

The subproof is completed by applying H1.

Apply L0 with x0 leaving 2 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying H1.

■

Proofgold Proof