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

Metamath Proof Explorer

Theorem 3prm

Description: 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion 3prm 3 ∈ ℙ

Proof

Step Hyp Ref Expression
1 3z ⊢ 3 ∈ ℤ
2 1lt3 ⊢ 1 < 3
3 eluz2b1 ⊢ ( 3 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 3 ∈ ℤ ∧ 1 < 3 ) )
4 1 2 3 mpbir2an ⊢ 3 ∈ ( ℤ≥ ‘ 2 )
5 elfz1eq ⊢ ( 𝑧 ∈ ( 2 ... 2 ) → 𝑧 = 2 )
6 n2dvds3 ⊢ ¬ 2 ∥ 3
7 breq1 ⊢ ( 𝑧 = 2 → ( 𝑧 ∥ 3 ↔ 2 ∥ 3 ) )
8 6 7 mtbiri ⊢ ( 𝑧 = 2 → ¬ 𝑧 ∥ 3 )
9 5 8 syl ⊢ ( 𝑧 ∈ ( 2 ... 2 ) → ¬ 𝑧 ∥ 3 )
10 3m1e2 ⊢ ( 3 − 1 ) = 2
11 10 oveq2i ⊢ ( 2 ... ( 3 − 1 ) ) = ( 2 ... 2 )
12 9 11 eleq2s ⊢ ( 𝑧 ∈ ( 2 ... ( 3 − 1 ) ) → ¬ 𝑧 ∥ 3 )
13 12 rgen ⊢ ∀ 𝑧 ∈ ( 2 ... ( 3 − 1 ) ) ¬ 𝑧 ∥ 3
14 isprm3 ⊢ ( 3 ∈ ℙ ↔ ( 3 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( 2 ... ( 3 − 1 ) ) ¬ 𝑧 ∥ 3 ) )
15 4 13 14 mpbir2an ⊢ 3 ∈ ℙ