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

Metamath Proof Explorer

Theorem isprm4

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only divisor greater than or equal to 2 is itself. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion isprm4 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P

Proof

Step Hyp Ref Expression
1 isprm2 ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℕ z ∥ P → z = 1 ∨ z = P
2 eluz2b3 ⊢ z ∈ ℤ ≥ 2 ↔ z ∈ ℕ ∧ z ≠ 1
3 2 imbi1i ⊢ z ∈ ℤ ≥ 2 → z ∥ P → z = P ↔ z ∈ ℕ ∧ z ≠ 1 → z ∥ P → z = P
4 impexp ⊢ z ∈ ℕ ∧ z ≠ 1 → z ∥ P → z = P ↔ z ∈ ℕ → z ≠ 1 → z ∥ P → z = P
5 bi2.04 ⊢ z ≠ 1 → z ∥ P → z = P ↔ z ∥ P → z ≠ 1 → z = P
6 df-ne ⊢ z ≠ 1 ↔ ¬ z = 1
7 6 imbi1i ⊢ z ≠ 1 → z = P ↔ ¬ z = 1 → z = P
8 df-or ⊢ z = 1 ∨ z = P ↔ ¬ z = 1 → z = P
9 7 8 bitr4i ⊢ z ≠ 1 → z = P ↔ z = 1 ∨ z = P
10 9 imbi2i ⊢ z ∥ P → z ≠ 1 → z = P ↔ z ∥ P → z = 1 ∨ z = P
11 5 10 bitri ⊢ z ≠ 1 → z ∥ P → z = P ↔ z ∥ P → z = 1 ∨ z = P
12 11 imbi2i ⊢ z ∈ ℕ → z ≠ 1 → z ∥ P → z = P ↔ z ∈ ℕ → z ∥ P → z = 1 ∨ z = P
13 4 12 bitri ⊢ z ∈ ℕ ∧ z ≠ 1 → z ∥ P → z = P ↔ z ∈ ℕ → z ∥ P → z = 1 ∨ z = P
14 3 13 bitri ⊢ z ∈ ℤ ≥ 2 → z ∥ P → z = P ↔ z ∈ ℕ → z ∥ P → z = 1 ∨ z = P
15 14 ralbii2 ⊢ ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P ↔ ∀ z ∈ ℕ z ∥ P → z = 1 ∨ z = P
16 15 anbi2i ⊢ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℕ z ∥ P → z = 1 ∨ z = P
17 1 16 bitr4i ⊢ P ∈ ℙ ↔ P ∈ ℤ ≥ 2 ∧ ∀ z ∈ ℤ ≥ 2 z ∥ P → z = P