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 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℕ z ∥ P → z = 1 ∨ z = P

Proof

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