Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: prime_nat x0.
Apply H0 with x0setminus omega (Sing 0).
Assume H1: and (x0omega) (1x0).
Apply H1 with (∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0))x0setminus omega (Sing 0).
Assume H2: x0omega.
Assume H3: 1x0.
Assume H4: ∀ x1 . x1omegadivides_nat x1 x0or (x1 = 1) (x1 = x0).
Apply setminusI with omega, Sing 0, x0 leaving 2 subgoals.
The subproof is completed by applying H2.
Assume H5: x0Sing 0.
Apply In_no2cycle with 1, x0 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply SingE with 0, x0, λ x1 x2 . x21 leaving 2 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying In_0_1.