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 , 𝑃 } ) )