oddprmgt2

Description: An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021)

		Ref	Expression
	Assertion	oddprmgt2	$⊢ P \in (ℙ ∖ \{2\}) \to 2 < P$

Step	Hyp	Ref	Expression
1		eldifsn	$⊢ P \in (ℙ ∖ \{2\}) \leftrightarrow (P \in ℙ \land P \neq 2)$
2		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
3		eluz2	$⊢ P \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land P \in ℤ \land 2 \leq P)$
4		zre	$⊢ 2 \in ℤ \to 2 \in ℝ$
5		zre	$⊢ P \in ℤ \to P \in ℝ$
6		ltlen	$⊢ (2 \in ℝ \land P \in ℝ) \to (2 < P \leftrightarrow (2 \leq P \land P \neq 2))$
7	4 5 6	syl2an	$⊢ (2 \in ℤ \land P \in ℤ) \to (2 < P \leftrightarrow (2 \leq P \land P \neq 2))$
8	7	biimprd	$⊢ (2 \in ℤ \land P \in ℤ) \to ((2 \leq P \land P \neq 2) \to 2 < P)$
9	8	exp4b	$⊢ 2 \in ℤ \to (P \in ℤ \to (2 \leq P \to (P \neq 2 \to 2 < P)))$
10	9	3imp	$⊢ (2 \in ℤ \land P \in ℤ \land 2 \leq P) \to (P \neq 2 \to 2 < P)$
11	3 10	sylbi	$⊢ P \in ℤ_{\geq 2} \to (P \neq 2 \to 2 < P)$
12	2 11	syl	$⊢ P \in ℙ \to (P \neq 2 \to 2 < P)$
13	12	imp	$⊢ (P \in ℙ \land P \neq 2) \to 2 < P$
14	1 13	sylbi	$⊢ P \in (ℙ ∖ \{2\}) \to 2 < P$

Metamath Proof Explorer