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

Metamath Proof Explorer

Theorem 4nprm

Description: 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011) (Proof shortened by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion 4nprm ⊢ ¬ 4 ∈ ℙ

Proof

Step Hyp Ref Expression
1 2nn ⊢ 2 ∈ ℕ
2 1lt2 ⊢ 1 < 2
3 2t2e4 ⊢ 2 ⋅ 2 = 4
4 1 1 2 2 3 nprmi ⊢ ¬ 4 ∈ ℙ