Let x0 of type ι be given.
Assume H1: 1 ∈ x0.
Apply xm with
composite_nat x0,
or (prime_nat x0) (composite_nat x0) leaving 2 subgoals.
Apply orIL with
prime_nat x0,
composite_nat x0.
Apply and3I with
x0 ∈ omega,
1 ∈ x0,
∀ x1 . x1 ∈ omega ⟶ divides_nat x1 x0 ⟶ or (x1 = 1) (x1 = x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x1 of type ι be given.
Apply H4 with
or (x1 = 1) (x1 = x0).
Apply H6 with
or (x1 = 1) (x1 = x0).
Let x2 of type ι be given.
Apply H7 with
or (x1 = 1) (x1 = x0).
Apply dneg with
or (x1 = 1) (x1 = x0).
Assume H10:
not (or (x1 = 1) (x1 = x0)).
Apply H2.
Apply andI with
x0 ∈ omega,
∃ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ omega) (and (and (1 ∈ x3) (1 ∈ x4)) (mul_nat x3 x4 = x0))) leaving 2 subgoals.
The subproof is completed by applying H0.
Let x3 of type ο be given.
Apply H11 with
x1.
Apply andI with
x1 ∈ omega,
∃ x4 . and (x4 ∈ omega) (and (and (1 ∈ x1) (1 ∈ x4)) (mul_nat x1 x4 = x0)) leaving 2 subgoals.
The subproof is completed by applying H3.
Let x4 of type ο be given.
Apply H12 with
x2.
Apply andI with
x2 ∈ omega,
and (and (1 ∈ x1) (1 ∈ x2)) (mul_nat x1 x2 = x0) leaving 2 subgoals.
The subproof is completed by applying H8.
Apply and3I with
1 ∈ x1,
1 ∈ x2,
mul_nat x1 x2 = x0 leaving 3 subgoals.
Apply ordinal_In_Or_Subq with
1,
x1,
1 ∈ x1 leaving 4 subgoals.
Apply nat_p_ordinal with
1.
The subproof is completed by applying nat_1.
Apply nat_p_ordinal with
x1.
Apply omega_nat_p with
x1.
The subproof is completed by applying H3.
Assume H13: 1 ∈ x1.
The subproof is completed by applying H13.
Assume H13: x1 ⊆ 1.
Apply FalseE with
1 ∈ x1.
Apply nat_le1_cases with
x1,
False leaving 4 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H3.
The subproof is completed by applying H13.
Assume H14: x1 = 0.
Apply In_no2cycle with
0,
1 leaving 2 subgoals.
The subproof is completed by applying In_0_1.
set y5 to be ...
set y6 to be ...
Apply H9 with
λ x7 x8 . (λ x9 . y6) ... ... leaving 2 subgoals.