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

Metamath Proof Explorer

Theorem 2prm

Description: 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Fan Zheng, 16-Jun-2016)

Ref Expression
Assertion 2prm 2 ∈ ℙ

Proof

Step Hyp Ref Expression
1 2z ⊢ 2 ∈ ℤ
2 1lt2 ⊢ 1 < 2
3 eluz2b1 ⊢ ( 2 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 2 ∈ ℤ ∧ 1 < 2 ) )
4 1 2 3 mpbir2an ⊢ 2 ∈ ( ℤ≥ ‘ 2 )
5 ral0 ⊢ ∀ 𝑧 ∈ ∅ ¬ 𝑧 ∥ 2
6 fzssuz ⊢ ( 2 ... ( 2 − 1 ) ) ⊆ ( ℤ≥ ‘ 2 )
7 dfss2 ⊢ ( ( 2 ... ( 2 − 1 ) ) ⊆ ( ℤ≥ ‘ 2 ) ↔ ( ( 2 ... ( 2 − 1 ) ) ∩ ( ℤ≥ ‘ 2 ) ) = ( 2 ... ( 2 − 1 ) ) )
8 6 7 mpbi ⊢ ( ( 2 ... ( 2 − 1 ) ) ∩ ( ℤ≥ ‘ 2 ) ) = ( 2 ... ( 2 − 1 ) )
9 uzdisj ⊢ ( ( 2 ... ( 2 − 1 ) ) ∩ ( ℤ≥ ‘ 2 ) ) = ∅
10 8 9 eqtr3i ⊢ ( 2 ... ( 2 − 1 ) ) = ∅
11 10 raleqi ⊢ ( ∀ 𝑧 ∈ ( 2 ... ( 2 − 1 ) ) ¬ 𝑧 ∥ 2 ↔ ∀ 𝑧 ∈ ∅ ¬ 𝑧 ∥ 2 )
12 5 11 mpbir ⊢ ∀ 𝑧 ∈ ( 2 ... ( 2 − 1 ) ) ¬ 𝑧 ∥ 2
13 isprm3 ⊢ ( 2 ∈ ℙ ↔ ( 2 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( 2 ... ( 2 − 1 ) ) ¬ 𝑧 ∥ 2 ) )
14 4 12 13 mpbir2an ⊢ 2 ∈ ℙ