Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H0: 1 ∈ x0.
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: nat_p x0
Apply omega_nat_p with x0.
The subproof is completed by applying H4.
Claim L16: nat_p x1
Apply omega_nat_p with x1.
The subproof is completed by applying H5.
Claim L17: nat_p x2
Apply omega_nat_p with x2.
The subproof is completed by applying H8.
Claim L18: nat_p x3
Apply omega_nat_p with x3.
The subproof is completed by applying H13.
Apply In_irref with mul_nat x0 x3.
Apply H9 with λ x4 x5 . add_nat x0 x4 ⊆ mul_nat x0 x3, mul_nat x0 x3 leaving 2 subgoals.
Apply mul_nat_SR with x0, x2, λ x4 x5 . x4 ⊆ mul_nat x0 x3 leaving 2 subgoals.
The subproof is completed by applying L17.
Apply unknownprop_929864532141b40b768d022d9a5eb271b4e76fb202303c61c5984df8eb73ceb2 with ordsucc x2, x3, x0 leaving 4 subgoals.
Apply nat_ordsucc with x2.
The subproof is completed by applying L17.
The subproof is completed by applying L18.
Apply ordinal_In_Or_Subq with x2, x3, ordsucc x2 ⊆ x3 leaving 4 subgoals.
Apply nat_p_ordinal with x2.
The subproof is completed by applying L17.
Apply nat_p_ordinal with x3.
The subproof is completed by applying L18.
Apply ordinal_ordsucc_In_Subq with x3, x2.
Apply nat_p_ordinal with x3.
The subproof is completed by applying L18.
Assume H19: x3 ⊆ x2.
Apply FalseE with ordsucc x2 ⊆ x3.
Apply In_irref with x1.
Apply H14 with λ x4 x5 . x4 ⊆ x1, x1 leaving 2 subgoals.
Apply H9 with λ x4 x5 . mul_nat x0 x3 ⊆ x4.
Apply unknownprop_929864532141b40b768d022d9a5eb271b4e76fb202303c61c5984df8eb73ceb2 with x3, x2, x0 leaving 4 subgoals.
The subproof is completed by applying L18.
The subproof is completed by applying L17.
The subproof is completed by applying H19.
The subproof is completed by applying L15.
The subproof is completed by applying ordsuccI2 with x1.
The subproof is completed by applying L15.
Apply H14 with λ x4 x5 . x5 ∈ add_nat x0 x1.
Apply add_nat_SL with 0, x1, λ x4 x5 . x5 = ordsucc x1, λ x4 x5 . x4 ∈ add_nat x0 x1 leaving 4 subgoals.
The subproof is completed by applying nat_0.
The subproof is completed by applying L16.
set y4 to be ordsucc x1
Claim L19: ∀ x5 : ι → ο . x5 y4 ⟶ x5 (ordsucc (add_nat 0 x1))
Let x5 of type ι → ο be given.
Apply add_nat_0L with x2, λ x6 x7 . (λ x8 . x5) (ordsucc x6) (ordsucc x7).
The subproof is completed by applying L16.
Let x5 of type ι → ι → ο be given.
Apply L19 with λ x6 . x5 x6 y4 ⟶ x5 y4 x6.
Assume H20: x5 y4 y4.
The subproof is completed by applying H20.
Apply unknownprop_5699b3df204a64fe208917e4d013131a9b09ccf51d6c02bdbd470402e8fe7c26 with x1, 1, x0 leaving 4 subgoals.
The subproof is completed by applying L16.
The subproof is completed by applying nat_1.
The subproof is completed by applying L15.
The subproof is completed by applying H0.
■