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 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( ℤ≥ ‘ 2 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ) )

Proof

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