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 ∈ ℙ