Search for blocks/addresses/...

Proofgold Proof

pf
Assume H0: finite primes.
Apply H0 with False.
Let x0 of type ι be given.
Assume H1: (λ x1 . and (x1 ∈ omega) (equip primes x1)) x0.
Apply H1 with False.
Assume H2: x0 ∈ omega.
Assume H3: equip primes x0.
Apply equip_sym with primes, x0, False leaving 2 subgoals.
The subproof is completed by applying H3.
Let x1 of type ι → ι be given.
Assume H4: bij x0 primes x1.
Apply H4 with False.
Assume H5: and (∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ primes) (∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3).
Apply H5 with (∀ x2 . x2 ∈ primes ⟶ ∃ x3 . and (x3 ∈ x0) (x1 x3 = x2)) ⟶ False.
Assume H6: ∀ x2 . x2 ∈ x0 ⟶ x1 x2 ∈ primes.
Assume H7: ∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.
Assume H8: ∀ x2 . x2 ∈ primes ⟶ ∃ x3 . and (x3 ∈ x0) (x1 x3 = x2).
Claim L9: ...
...
Claim L10: ...
...
Claim L11: ...
...
Claim L12: ...
...
Apply L11 with ordsucc (Pi_nat x1 x0) leaving 2 subgoals.
Apply and3I with ordsucc (Pi_nat x1 x0) ∈ omega, 1 ∈ ordsucc (Pi_nat x1 x0), ∀ x2 . x2 ∈ omega ⟶ divides_nat x2 (ordsucc (Pi_nat x1 x0)) ⟶ or (x2 = 1) (x2 = ordsucc (Pi_nat x1 x0)) leaving 3 subgoals.
Apply nat_p_omega with ordsucc (Pi_nat x1 x0).
Apply nat_ordsucc with Pi_nat x1 x0.
The subproof is completed by applying L10.
The subproof is completed by applying L12.
Let x2 of type ι be given.
Assume H13: x2 ∈ omega.
Assume H14: divides_nat x2 (ordsucc (Pi_nat x1 x0)).
Apply orIL with x2 = 1, x2 = ordsucc (Pi_nat x1 x0).
Apply ordinal_In_Or_Subq with 1, x2, x2 = 1 leaving 4 subgoals.
Apply nat_p_ordinal with 1.
The subproof is completed by applying nat_1.
Apply nat_p_ordinal with x2.
Apply omega_nat_p with x2.
The subproof is completed by applying H13.
Assume H15: 1 ∈ x2.
Apply prime_nat_divisor_ex with x2, x2 = 1 leaving 3 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Let x3 of type ι be given.
Assume H16: (λ x4 . and (prime_nat x4) (divides_nat x4 x2)) x3.
Apply H16 with x2 = 1.
Assume H17: prime_nat x3.
Assume H18: divides_nat x3 x2.
Apply L11 with x3, x2 = 1 leaving 2 subgoals.
The subproof is completed by applying H17.
Apply unknownprop_f799b99d854d7bca6941dc7751c0c00a5bf29ac2d7e070aa318a7a7ed9ce8fa0 with x3, x2, ordsucc (Pi_nat x1 x0) leaving 2 subgoals.
The subproof is completed by applying H18.
The subproof is completed by applying H14.
Assume H15: x2 ⊆ 1.
Apply nat_le1_cases with x2, x2 = 1 leaving 4 subgoals.
Apply omega_nat_p with x2.
The subproof is completed by applying H13.
The subproof is completed by applying H15.
Assume H16: x2 = 0.
Apply FalseE with x2 = 1.
Apply H14 with False.
Assume H17: and (x2 ∈ omega) (ordsucc (Pi_nat x1 x0) ∈ omega).
Assume H18: ∃ x3 . and (x3 ∈ omega) (mul_nat x2 x3 = ordsucc (Pi_nat x1 x0)).
Apply H18 with False.
Let x3 of type ι be given.
Assume H19: (λ x4 . and (x4 ∈ omega) (mul_nat x2 x4 = ordsucc (Pi_nat x1 ...))) ....
...
...
...
■