oddprmge3

Description: An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 20-Aug-2021)

		Ref	Expression
	Assertion	oddprmge3	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$

Step	Hyp	Ref	Expression
1		eldifi	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℙ$
2		oddprmgt2	$⊢ P \in (ℙ ∖ \{2\}) \to 2 < P$
3		3z	$⊢ 3 \in ℤ$
4	3	a1i	$⊢ (P \in ℙ \land 2 < P) \to 3 \in ℤ$
5		prmz	$⊢ P \in ℙ \to P \in ℤ$
6	5	adantr	$⊢ (P \in ℙ \land 2 < P) \to P \in ℤ$
7		df-3	$⊢ 3 = 2 + 1$
8		2z	$⊢ 2 \in ℤ$
9		zltp1le	$⊢ (2 \in ℤ \land P \in ℤ) \to (2 < P \leftrightarrow 2 + 1 \leq P)$
10	8 5 9	sylancr	$⊢ P \in ℙ \to (2 < P \leftrightarrow 2 + 1 \leq P)$
11	10	biimpa	$⊢ (P \in ℙ \land 2 < P) \to 2 + 1 \leq P$
12	7 11	eqbrtrid	$⊢ (P \in ℙ \land 2 < P) \to 3 \leq P$
13	4 6 12	3jca	$⊢ (P \in ℙ \land 2 < P) \to (3 \in ℤ \land P \in ℤ \land 3 \leq P)$
14	1 2 13	syl2anc	$⊢ P \in (ℙ ∖ \{2\}) \to (3 \in ℤ \land P \in ℤ \land 3 \leq P)$
15		eluz2	$⊢ P \in ℤ_{\geq 3} \leftrightarrow (3 \in ℤ \land P \in ℤ \land 3 \leq P)$
16	14 15	sylibr	$⊢ P \in (ℙ ∖ \{2\}) \to P \in ℤ_{\geq 3}$

Metamath Proof Explorer