Let x0 of type ι be given.
Assume H2: 1 ∈ x0.
Let x1 of type ο be given.
Assume H3:
∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ 1 ∈ x2 ⟶ 1 ∈ x3 ⟶ x0 = mul_nat x2 x3 ⟶ x1.
Apply dneg with
x1.
Apply H1.
Apply and3I with
x0 ∈ omega,
1 ∈ x0,
∀ x2 . x2 ∈ omega ⟶ divides_nat x2 x0 ⟶ or (x2 = 1) (x2 = x0) leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Let x2 of type ι be given.
Apply H6 with
or (x2 = 1) (x2 = x0).
Apply H8 with
or (x2 = 1) (x2 = x0).
Let x3 of type ι be given.
Apply H9 with
or (x2 = 1) (x2 = x0).
Apply dneg with
or (x2 = 1) (x2 = x0).
Assume H12:
not (or (x2 = 1) (x2 = x0)).
Claim L19: 1 ∈ x3
Apply L18 with
x3,
1 ∈ x3 leaving 3 subgoals.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Assume H19:
or (x3 = 0) (x3 = 1).
Apply H19 with
1 ∈ x3 leaving 2 subgoals.
Assume H20: x3 = 0.
Apply FalseE with
1 ∈ x3.
Apply L15.
The subproof is completed by applying H20.
Claim L20: x3 ∈ x0
Apply ordinal_In_Or_Subq with
x3,
x0,
x3 ∈ x0 leaving 4 subgoals.
Apply nat_p_ordinal with
x3.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Apply nat_p_ordinal with
x0.
Apply omega_nat_p with
x0.
The subproof is completed by applying H0.
Assume H20: x3 ∈ x0.
The subproof is completed by applying H20.
Assume H20: x0 ⊆ x3.
Apply FalseE with
x3 ∈ x0.
Claim L21: x3 = x0
Apply set_ext with
x3,
x0 leaving 2 subgoals.
Apply H11 with
λ x4 x5 . x3 ⊆ x4.
Apply mul_nat_com with
x2,
x3,
λ x4 x5 . x3 ⊆ x5 leaving 3 subgoals.
Apply omega_nat_p with
x2.
The subproof is completed by applying H5.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Apply unknownprop_bdf0eb0ad914e7080c1a90c10a5be5aadacffe01a001ae1e9b4568b2273272d9 with
x3,
x2,
x3 ⊆ mul_nat x3 x2 leaving 4 subgoals.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Apply omega_nat_p with
x2.
The subproof is completed by applying H5.
Assume H21: x2 = 0.
Apply FalseE with
x3 ⊆ mul_nat x3 x2.
Apply L14.
The subproof is completed by applying H21.
The subproof is completed by applying H21.
The subproof is completed by applying H20.
Claim L22: x2 = 1
Apply unknownprop_db897f3f49b8c848a3d81fbc7ed013179113267e2c53f0b5582e9ca05f6f06d5 with
x2,
x3 leaving 4 subgoals.
Apply omega_nat_p with
x2.
The subproof is completed by applying H5.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Apply mul_nat_com with
x3,
x2,
λ x4 x5 . x5 = x3 leaving 3 subgoals.
Apply omega_nat_p with
x3.
The subproof is completed by applying H10.
Apply omega_nat_p with
x2.
The subproof is completed by applying H5.
Apply H11 with
λ x4 x5 . x5 = x3.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying L21 with λ x5 x6 . x4 x6 x5.
The subproof is completed by applying L15.
Apply In_irref with
x2.
Apply L22 with
λ x4 x5 . x5 ∈ x2.
The subproof is completed by applying L16.
Apply H4.
Apply H3 with
x2,
x3 leaving 5 subgoals.
The subproof is completed by applying L17.
The subproof is completed by applying L20.
The subproof is completed by applying L16.
The subproof is completed by applying L19.
Let x4 of type ι → ι → ο be given.
The subproof is completed by applying H11 with λ x5 x6 . x4 x6 x5.