Metamath Proof Explorer

Theorem isprm2lem

Description: Lemma for isprm2 . (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion isprm2lem ⊢P∈ℕ∧P≠1→n∈ℕ|n∥P≈2𝑜↔n∈ℕ|n∥P=1P

Proof

Step Hyp Ref Expression
1 simplr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→P≠1
2 1 necomd ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→1≠P
3 simpr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→n∈ℕ|n∥P≈2𝑜
4 nnz ⊢P∈ℕ→P∈ℤ
5 1dvds ⊢P∈ℤ→1∥P
6 4 5 syl ⊢P∈ℕ→1∥P
7 6 ad2antrr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→1∥P
8 1nn ⊢1∈ℕ
9 breq1 ⊢n=1→n∥P↔1∥P
10 9 elrab3 ⊢1∈ℕ→1∈n∈ℕ|n∥P↔1∥P
11 8 10 ax-mp ⊢1∈n∈ℕ|n∥P↔1∥P
12 7 11 sylibr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→1∈n∈ℕ|n∥P
13 iddvds ⊢P∈ℤ→P∥P
14 4 13 syl ⊢P∈ℕ→P∥P
15 14 ad2antrr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→P∥P
16 breq1 ⊢n=P→n∥P↔P∥P
17 16 elrab3 ⊢P∈ℕ→P∈n∈ℕ|n∥P↔P∥P
18 17 ad2antrr ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→P∈n∈ℕ|n∥P↔P∥P
19 15 18 mpbird ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→P∈n∈ℕ|n∥P
20 en2eqpr ⊢n∈ℕ|n∥P≈2𝑜∧1∈n∈ℕ|n∥P∧P∈n∈ℕ|n∥P→1≠P→n∈ℕ|n∥P=1P
21 3 12 19 20 syl3anc ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→1≠P→n∈ℕ|n∥P=1P
22 2 21 mpd ⊢P∈ℕ∧P≠1∧n∈ℕ|n∥P≈2𝑜→n∈ℕ|n∥P=1P
23 22 ex ⊢P∈ℕ∧P≠1→n∈ℕ|n∥P≈2𝑜→n∈ℕ|n∥P=1P
24 necom ⊢1≠P↔P≠1
25 pr2ne ⊢1∈ℕ∧P∈ℕ→1P≈2𝑜↔1≠P
26 8 25 mpan ⊢P∈ℕ→1P≈2𝑜↔1≠P
27 26 biimpar ⊢P∈ℕ∧1≠P→1P≈2𝑜
28 24 27 sylan2br ⊢P∈ℕ∧P≠1→1P≈2𝑜
29 breq1 ⊢n∈ℕ|n∥P=1P→n∈ℕ|n∥P≈2𝑜↔1P≈2𝑜
30 28 29 syl5ibrcom ⊢P∈ℕ∧P≠1→n∈ℕ|n∥P=1P→n∈ℕ|n∥P≈2𝑜
31 23 30 impbid ⊢P∈ℕ∧P≠1→n∈ℕ|n∥P≈2𝑜↔n∈ℕ|n∥P=1P