Let x0 of type ι be given.
Apply dneg with
∃ x1 . and (x1 ∈ setminus x0 (Sing 0)) (∃ x2 . and (x2 ∈ omega) (∃ x3 . and (x3 ∈ omega) (∃ x4 . and (x4 ∈ omega) (∃ x5 . and (x5 ∈ omega) (mul_SNo x1 x0 = add_SNo ((λ x6 . mul_SNo x6 x6) x2) (add_SNo ((λ x6 . mul_SNo x6 x6) x3) (add_SNo ((λ x6 . mul_SNo x6 x6) x4) ((λ x6 . mul_SNo x6 x6) x5)))))))).
Apply H1 with
False.
Assume H4:
∀ x1 . x1 ∈ omega ⟶ x0 = mul_nat 2 x1 ⟶ ∀ x2 : ο . x2.
Apply odd_nat_even_nat_S with
x0,
False leaving 2 subgoals.
The subproof is completed by applying H1.
Apply H14 with
False.
Let x1 of type ι be given.
Apply H15 with
False.
Apply mul_nat_mul_SNo with
2,
x1,
λ x2 x3 . ordsucc x0 = x3 ⟶ False leaving 3 subgoals.
Apply nat_p_omega with
2.
The subproof is completed by applying nat_2.
The subproof is completed by applying H16.
Apply unknownprop_e5d031cf873471b22fe77dee36ebb6254dbd5df83fe741afd4ca8450323be464 with
x1,
λ x2 x3 . ordsucc x0 = x3 ⟶ False leaving 2 subgoals.
The subproof is completed by applying L19.
Apply unknownprop_8a6bdce060c93f04626730b6e01b099cc0487102a697e253c81b39b9a082262d with
x0 leaving 2 subgoals.
Apply omega_nat_p with
x0.
The subproof is completed by applying H3.
Apply H21 with
λ x2 x3 . atleastp x3 x0.
Apply atleastp_tra with
add_SNo x1 x1,
setsum x1 x1,
x0 leaving 2 subgoals.
Apply equip_atleastp with
add_SNo x1 x1,
setsum x1 x1.
Apply add_nat_add_SNo with
x1,
x1,
λ x2 x3 . equip x2 (setsum x1 x1) leaving 3 subgoals.
The subproof is completed by applying H16.
The subproof is completed by applying H16.
Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with
x1,
x1,
x1,
x1 leaving 4 subgoals.
Apply omega_nat_p with
x1.
The subproof is completed by applying H16.
Apply omega_nat_p with
x1.
The subproof is completed by applying H16.
The subproof is completed by applying equip_ref with x1.
The subproof is completed by applying equip_ref with x1.
Let x2 of type ο be given.
Assume H38:
∀ x3 : ι → ι . inj (setsum x1 x1) x0 x3 ⟶ x2.