Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: x0 ∈ setminus omega 2.
Let x1 of type ι be given.
Assume H1: divides_nat x0 x1.
Assume H2: divides_nat x0 (ordsucc x1).
Apply H1 with False.
Assume H3: and (x0 ∈ omega) (x1 ∈ omega).
Apply H3 with (∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1)) ⟶ False.
Assume H4: x0 ∈ omega.
Assume H5: x1 ∈ omega.
Assume H6: ∃ x2 . and (x2 ∈ omega) (mul_nat x0 x2 = x1).
Apply H6 with False.
Let x2 of type ι be given.
Assume H7: (λ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = x1)) x2.
Apply H7 with False.
Assume H8: x2 ∈ omega.
Assume H9: mul_nat x0 x2 = x1.
Apply H2 with False.
Assume H10: and (x0 ∈ omega) (ordsucc x1 ∈ omega).
Assume H11: ∃ x3 . and (x3 ∈ omega) (mul_nat x0 x3 = ordsucc x1).
Apply H11 with False.
Let x3 of type ι be given.
Assume H12: (λ x4 . and (x4 ∈ omega) (mul_nat x0 x4 = ordsucc x1)) x3.
Apply H12 with False.
Assume H13: x3 ∈ omega.
Assume H14: mul_nat x0 x3 = ordsucc x1.
Claim L15: ...
...
Claim L16: ...
...
Claim L17: ...
...
Apply unknownprop_0530dcab0a3350a5792a0eced733df25a629e35a5a7c1120748c0f5f3b566974 with x3, x2, False leaving 3 subgoals.
Apply omega_nat_p with x3.
The subproof is completed by applying H13.
The subproof is completed by applying L17.
Let x4 of type ι be given.
Assume H18: (λ x5 . and (x5 ∈ omega) (add_nat x2 x5 = x3)) x4.
Apply H18 with False.
Assume H19: x4 ∈ omega.
Assume H20: add_nat x2 x4 = x3.
Claim L21: ...
...
Claim L22: ...
...
Claim L23: ...
...
Claim L24: add_nat (mul_nat x0 x2) (mul_nat x0 x4) = add_nat (mul_nat x0 x2) 1
set y5 to be ...
set y6 to be ...
Claim L24: ∀ x7 : ι → ο . x7 y6 ⟶ x7 y5
Let x7 of type ι → ο be given.
Assume H24: x7 (add_nat (mul_nat x2 x4) 1).
set y8 to be ...
Apply mul_add_nat_distrL with x2, x4, y6, λ x9 x10 . y8 x10 x9 leaving 4 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
The subproof is completed by applying L23.
Apply H20 with λ x9 x10 . mul_nat x3 x10 = ordsucc (mul_nat x3 y5), λ x9 . y8 leaving 2 subgoals.
The subproof is completed by applying L15.
Apply add_nat_SR with mul_nat x3 y5, 0, λ x9 x10 . ordsucc (mul_nat x3 y5) = x10, λ x9 . y8 leaving 3 subgoals.
The subproof is completed by applying nat_0.
set y9 to be ...
set y10 to be ...
Claim L25: ...
...
Let x11 of type ι → ι → ο be given.
Apply L25 with λ x12 . x11 x12 y10 ⟶ x11 y10 x12.
Assume H26: x11 ... ....
...
...
Let x7 of type ι → ι → ο be given.
Apply L24 with λ x8 . x7 x8 y6 ⟶ x7 y6 x8.
Assume H25: x7 y6 y6.
The subproof is completed by applying H25.
Claim L25: mul_nat x0 x4 = 1
Apply unknownprop_ff560222020c95f6e7705ee5610e16ac6a9d6789a574689c0536877273f2572a with mul_nat x0 x2, mul_nat x0 x4, 1 leaving 4 subgoals.
Apply mul_nat_p with x0, x2 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying L22.
Apply mul_nat_p with x0, x4 leaving 2 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying L23.
The subproof is completed by applying nat_1.
The subproof is completed by applying L24.
Claim L26: x0 = 1
Apply unknownprop_79be07f7920cf67ee313d822d12bbc88fa1841a75a563c0807dc82891b9eeca5 with x0, x4, x0 = 1 leaving 4 subgoals.
The subproof is completed by applying L21.
The subproof is completed by applying L23.
The subproof is completed by applying L25.
Assume H26: x0 = 1.
Assume H27: x4 = 1.
The subproof is completed by applying H26.
Apply setminusE2 with omega, 2, x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Apply L26 with λ x5 x6 . x6 ∈ 2.
The subproof is completed by applying In_1_2.
■