Metamath Proof Explorer

Theorem isprm2

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in ApostolNT p. 16. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion isprm2 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )

Proof

Step Hyp Ref Expression
1 1nprm ⊢ ¬ 1 ∈ ℙ
2 eleq1 ⊢ ( 𝑃 = 1 → ( 𝑃 ∈ ℙ ↔ 1 ∈ ℙ ) )
3 2 biimpcd ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 = 1 → 1 ∈ ℙ ) )
4 1 3 mtoi ⊢ ( 𝑃 ∈ ℙ → ¬ 𝑃 = 1 )
5 4 neqned ⊢ ( 𝑃 ∈ ℙ → 𝑃 ≠ 1 )
6 5 pm4.71i ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 1 ) )
7 isprm ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ) )
8 isprm2lem ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ) )
9 eqss ⊢ ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ↔ ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ∧ { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ) )
10 9 imbi2i ⊢ ( ( 𝑃 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ) ↔ ( 𝑃 ∈ ℕ → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ∧ { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ) ) )
11 1idssfct ⊢ ( 𝑃 ∈ ℕ → { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } )
12 jcab ⊢ ( ( 𝑃 ∈ ℕ → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ∧ { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ) ) ↔ ( ( 𝑃 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ∧ ( 𝑃 ∈ ℕ → { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ) ) )
13 11 12 mpbiran2 ⊢ ( ( 𝑃 ∈ ℕ → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ∧ { 1 , 𝑃 } ⊆ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ) ) ↔ ( 𝑃 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
14 10 13 bitri ⊢ ( ( 𝑃 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ) ↔ ( 𝑃 ∈ ℕ → { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
15 14 pm5.74ri ⊢ ( 𝑃 ∈ ℕ → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
16 15 adantr ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } = { 1 , 𝑃 } ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
17 8 16 bitrd ⊢ ( ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
18 17 expcom ⊢ ( 𝑃 ≠ 1 → ( 𝑃 ∈ ℕ → ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ↔ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ) )
19 18 pm5.32d ⊢ ( 𝑃 ≠ 1 → ( ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ≈ 2o ) ↔ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ) )
20 7 19 syl5bb ⊢ ( 𝑃 ≠ 1 → ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ) )
21 20 pm5.32ri ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 1 ) ↔ ( ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ∧ 𝑃 ≠ 1 ) )
22 ancom ⊢ ( ( ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ∧ 𝑃 ≠ 1 ) ↔ ( 𝑃 ≠ 1 ∧ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ) )
23 anass ⊢ ( ( ( 𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ ) ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ↔ ( 𝑃 ≠ 1 ∧ ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ) )
24 22 23 bitr4i ⊢ ( ( ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ∧ 𝑃 ≠ 1 ) ↔ ( ( 𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ ) ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
25 ancom ⊢ ( ( 𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ ) ↔ ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) )
26 eluz2b3 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑃 ∈ ℕ ∧ 𝑃 ≠ 1 ) )
27 25 26 bitr4i ⊢ ( ( 𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ ) ↔ 𝑃 ∈ ( ℤ≥ ‘ 2 ) )
28 27 anbi1i ⊢ ( ( ( 𝑃 ≠ 1 ∧ 𝑃 ∈ ℕ ) ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) )
29 dfss2 ⊢ ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ↔ ∀ 𝑧 ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } → 𝑧 ∈ { 1 , 𝑃 } ) )
30 breq1 ⊢ ( 𝑛 = 𝑧 → ( 𝑛 ∥ 𝑃 ↔ 𝑧 ∥ 𝑃 ) )
31 30 elrab ⊢ ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ↔ ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) )
32 vex ⊢ 𝑧 ∈ V
33 32 elpr ⊢ ( 𝑧 ∈ { 1 , 𝑃 } ↔ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) )
34 31 33 imbi12i ⊢ ( ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } → 𝑧 ∈ { 1 , 𝑃 } ) ↔ ( ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
35 impexp ⊢ ( ( ( 𝑧 ∈ ℕ ∧ 𝑧 ∥ 𝑃 ) → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
36 34 35 bitri ⊢ ( ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } → 𝑧 ∈ { 1 , 𝑃 } ) ↔ ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
37 36 albii ⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } → 𝑧 ∈ { 1 , 𝑃 } ) ↔ ∀ 𝑧 ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
38 df-ral ⊢ ( ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
39 37 38 bitr4i ⊢ ( ∀ 𝑧 ( 𝑧 ∈ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } → 𝑧 ∈ { 1 , 𝑃 } ) ↔ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
40 29 39 bitri ⊢ ( { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ↔ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
41 40 anbi2i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
42 24 28 41 3bitri ⊢ ( ( ( 𝑃 ∈ ℕ ∧ { 𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃 } ⊆ { 1 , 𝑃 } ) ∧ 𝑃 ≠ 1 ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
43 6 21 42 3bitri ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )