This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isprm2lem

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

Ref Expression
Assertion isprm2lem ( ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ) )

Proof

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