Search for blocks/addresses/...

Proofgold Proof

pf
Apply nat_complete_ind with λ x0 . ∀ x1 . nat_p x1 ⟶ mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1) ⟶ x1 = 0.
Let x0 of type ι be given.
Assume H0: nat_p x0.
Assume H1: ∀ x1 . x1 ∈ x0 ⟶ ∀ x2 . nat_p x2 ⟶ mul_nat x1 x1 = mul_nat 2 (mul_nat x2 x2) ⟶ x2 = 0.
Let x1 of type ι be given.
Assume H2: nat_p x1.
Assume H3: mul_nat x0 x0 = mul_nat 2 (mul_nat x1 x1).
Claim L4: ...
...
Claim L5: ...
...
Claim L6: ...
...
Apply L6 with x1 = 0.
Assume H7: x0 ∈ omega.
Assume H8: ∃ x2 . and (x2 ∈ omega) (x0 = mul_nat 2 x2).
Apply H8 with x1 = 0.
Let x2 of type ι be given.
Assume H9: (λ x3 . and (x3 ∈ omega) (x0 = mul_nat 2 x3)) x2.
Apply H9 with x1 = 0.
Assume H10: x2 ∈ omega.
Assume H11: x0 = mul_nat 2 x2.
Apply dneg with x1 = 0.
Assume H12: x1 = 0 ⟶ ∀ x3 : ο . x3.
Claim L13: ...
...
Claim L14: ...
...
Claim L15: mul_nat x1 x1 = mul_nat 2 (mul_nat x2 x2)
Apply double_nat_cancel with mul_nat x1 x1, mul_nat 2 (mul_nat x2 x2) leaving 3 subgoals.
The subproof is completed by applying L4.
Apply mul_nat_p with 2, mul_nat x2 x2 leaving 2 subgoals.
The subproof is completed by applying nat_2.
Apply mul_nat_p with x2, x2 leaving 2 subgoals.
The subproof is completed by applying L13.
The subproof is completed by applying L13.
Apply H3 with λ x3 x4 . x3 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2)).
Apply H11 with λ x3 x4 . mul_nat x4 x4 = mul_nat 2 (mul_nat 2 (mul_nat x2 x2)).
Apply mul_nat_asso with mul_nat 2 x2, 2, x2, λ x3 x4 . x3 = mul_nat 2 (mul_nat 2 (mul_nat x2 ...)) leaving 4 subgoals.
...
...
...
...
Claim L16: x1 ∈ x0
Apply ordinal_In_Or_Subq with x1, x0, x1 ∈ x0 leaving 4 subgoals.
Apply nat_p_ordinal with x1.
The subproof is completed by applying H2.
Apply nat_p_ordinal with x0.
The subproof is completed by applying H0.
Assume H16: x1 ∈ x0.
The subproof is completed by applying H16.
Assume H16: x0 ⊆ x1.
Apply FalseE with x1 ∈ x0.
Apply H12.
Claim L17: mul_nat x1 x1 = 0
Apply double_nat_Subq_0 with mul_nat x1 x1 leaving 2 subgoals.
The subproof is completed by applying L4.
Apply H3 with λ x3 x4 . x3 ⊆ mul_nat x1 x1.
Apply square_nat_Subq with x0, x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H16.
Apply mul_nat_0_inv with x1, x1, x1 = 0 leaving 5 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
The subproof is completed by applying L17.
Assume H18: x1 = 0.
The subproof is completed by applying H18.
Assume H18: x1 = 0.
The subproof is completed by applying H18.
Claim L17: x2 = 0
Apply H1 with x1, x2 leaving 3 subgoals.
The subproof is completed by applying L16.
Apply omega_nat_p with x2.
The subproof is completed by applying H10.
The subproof is completed by applying L15.
Claim L18: mul_nat x1 x1 = 0
Apply L15 with λ x3 x4 . x4 = 0.
Apply L17 with λ x3 x4 . mul_nat 2 (mul_nat x4 x4) = 0.
Apply mul_nat_0R with 0, λ x3 x4 . mul_nat 2 x4 = 0.
The subproof is completed by applying mul_nat_0R with 2.
Apply H12.
Apply mul_nat_0_inv with x1, x1, x1 = 0 leaving 5 subgoals.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
Apply nat_p_omega with x1.
The subproof is completed by applying H2.
The subproof is completed by applying L18.
Assume H19: x1 = 0.
The subproof is completed by applying H19.
Assume H19: x1 = 0.
The subproof is completed by applying H19.
■