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 ) ( 𝑧 ∥ 𝑃 → 𝑧 = 𝑃 ) ) )