Let x0 of type ι be given.
Apply H0 with
∀ x1 . nat_p x1 ⟶ iff (odd_nat x1) (odd_nat (mul_nat x0 x1)).
Assume H2:
∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2.
Apply omega_nat_p with
x0.
The subproof is completed by applying H1.
Apply nat_ind with
λ x1 . iff (odd_nat x1) (odd_nat (mul_nat x0 x1)) leaving 2 subgoals.
Apply mul_nat_0R with
x0,
λ x1 x2 . iff (odd_nat 0) (odd_nat x2).
The subproof is completed by applying iff_refl with
odd_nat 0.
Let x1 of type ι be given.
Apply H5 with
iff (odd_nat (ordsucc x1)) (odd_nat (mul_nat x0 (ordsucc x1))).
Apply mul_nat_SR with
x0,
x1,
λ x2 x3 . iff (odd_nat (ordsucc x1)) (odd_nat x3) leaving 2 subgoals.
The subproof is completed by applying H4.
Apply iffI with
odd_nat (ordsucc x1),
odd_nat (add_nat x0 (mul_nat x0 x1)) leaving 2 subgoals.
Apply add_nat_com with
x0,
mul_nat x0 x1,
λ x2 x3 . odd_nat x3 leaving 3 subgoals.
The subproof is completed by applying L3.
Apply mul_nat_p with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H4.
Apply unknownprop_414262d1e5b2db2262078b4488f97bc47bc9ca3b09dbbe687ba5589aa53bd3b9 with
mul_nat x0 x1,
x0 leaving 2 subgoals.
Apply mul_nat_com with
x0,
x1,
λ x2 x3 . even_nat x3 leaving 3 subgoals.
The subproof is completed by applying L3.
The subproof is completed by applying H4.
Apply unknownprop_8cee5e8832051d733b2e2fcc5efb84026997457a76807022c9037e4a253cef30 with
x1,
x0 leaving 2 subgoals.
Apply even_nat_or_odd_nat with
x1,
even_nat x1 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Apply even_nat_not_odd_nat with
ordsucc x1,
even_nat x1 leaving 2 subgoals.
Apply odd_nat_even_nat_S with
x1.
The subproof is completed by applying H9.
The subproof is completed by applying H8.
The subproof is completed by applying L3.
The subproof is completed by applying H0.
Apply even_nat_odd_nat_S with
x1.
Apply even_nat_or_odd_nat with
x1,
even_nat x1 leaving 3 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H9.
Apply even_nat_not_odd_nat with
add_nat x0 (mul_nat x0 x1),
even_nat x1 leaving 2 subgoals.
Apply unknownprop_d79d4f48cc8316d2cfd7d64249eea9eca38257f800721e161e9a4245bd603310 with
x0,
mul_nat x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H6.
The subproof is completed by applying H9.
The subproof is completed by applying H8.