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		df-ss	⊢ ( ( 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 ∈ ℙ