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

Metamath Proof Explorer

Theorem prmgt1

Description: A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018)

		Ref	Expression
	Assertion	prmgt1	$⊢ P \in ℙ \to 1 < P$

Step	Hyp	Ref	Expression
1		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
2		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
3	1 2	syl	$⊢ P \in ℙ \to 1 < P$