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 = 1 P

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 = 1 P
21 3 12 19 20 syl3anc ⊢ P ∈ ℕ ∧ P ≠ 1 ∧ n ∈ ℕ | n ∥ P ≈ 2 𝑜 → 1 ≠ P → n ∈ ℕ | n ∥ P = 1 P
22 2 21 mpd ⊢ P ∈ ℕ ∧ P ≠ 1 ∧ n ∈ ℕ | n ∥ P ≈ 2 𝑜 → n ∈ ℕ | n ∥ P = 1 P
23 22 ex ⊢ P ∈ ℕ ∧ P ≠ 1 → n ∈ ℕ | n ∥ P ≈ 2 𝑜 → n ∈ ℕ | n ∥ P = 1 P
24 necom ⊢ 1 ≠ P ↔ P ≠ 1
25 pr2ne ⊢ 1 ∈ ℕ ∧ P ∈ ℕ → 1 P ≈ 2 𝑜 ↔ 1 ≠ P
26 8 25 mpan ⊢ P ∈ ℕ → 1 P ≈ 2 𝑜 ↔ 1 ≠ P
27 26 biimpar ⊢ P ∈ ℕ ∧ 1 ≠ P → 1 P ≈ 2 𝑜
28 24 27 sylan2br ⊢ P ∈ ℕ ∧ P ≠ 1 → 1 P ≈ 2 𝑜
29 breq1 ⊢ n ∈ ℕ | n ∥ P = 1 P → n ∈ ℕ | n ∥ P ≈ 2 𝑜 ↔ 1 P ≈ 2 𝑜
30 28 29 syl5ibrcom ⊢ P ∈ ℕ ∧ P ≠ 1 → n ∈ ℕ | n ∥ P = 1 P → n ∈ ℕ | n ∥ P ≈ 2 𝑜
31 23 30 impbid ⊢ P ∈ ℕ ∧ P ≠ 1 → n ∈ ℕ | n ∥ P ≈ 2 𝑜 ↔ n ∈ ℕ | n ∥ P = 1 P