Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: even_nat x0.
Apply H0 with not (odd_nat x0).
Assume H1: x0 ∈ omega.
Assume H2: ∃ x1 . and (x1 ∈ omega) (x0 = mul_nat 2 x1).
Apply H2 with not (odd_nat x0).
Let x1 of type ι be given.
Assume H3: (λ x2 . and (x2 ∈ omega) (x0 = mul_nat 2 x2)) x1.
Apply H3 with not (odd_nat x0).
Assume H4: x1 ∈ omega.
Assume H5: x0 = mul_nat 2 x1.
Assume H6: odd_nat x0.
Apply H6 with False.
Assume H7: x0 ∈ omega.
Assume H8: ∀ x2 . x2 ∈ omega ⟶ x0 = mul_nat 2 x2 ⟶ ∀ x3 : ο . x3.
Apply H8 with x1 leaving 2 subgoals.
The subproof is completed by applying H4.
The subproof is completed by applying H5.
■