Theorem oddprmgt2

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

	Ref	Expression
Assertion	oddprmgt2	|- ( P e. ( Prime \ { 2 } ) -> 2 < P )

Proof

Step	Hyp	Ref	Expression
1		eldifsn	|- ( P e. ( Prime \ { 2 } ) <-> ( P e. Prime /\ P =/= 2 ) )
2		prmuz2	|- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
3		eluz2	|- ( P e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ P e. ZZ /\ 2 <_ P ) )
4		zre	|- ( 2 e. ZZ -> 2 e. RR )
5		zre	|- ( P e. ZZ -> P e. RR )
6		ltlen	|- ( ( 2 e. RR /\ P e. RR ) -> ( 2 < P <-> ( 2 <_ P /\ P =/= 2 ) ) )
7	4 5 6	syl2an	|- ( ( 2 e. ZZ /\ P e. ZZ ) -> ( 2 < P <-> ( 2 <_ P /\ P =/= 2 ) ) )
8	7	biimprd	|- ( ( 2 e. ZZ /\ P e. ZZ ) -> ( ( 2 <_ P /\ P =/= 2 ) -> 2 < P ) )
9	8	exp4b	|- ( 2 e. ZZ -> ( P e. ZZ -> ( 2 <_ P -> ( P =/= 2 -> 2 < P ) ) ) )
10	9	3imp	|- ( ( 2 e. ZZ /\ P e. ZZ /\ 2 <_ P ) -> ( P =/= 2 -> 2 < P ) )
11	3 10	sylbi	|- ( P e. ( ZZ>= ` 2 ) -> ( P =/= 2 -> 2 < P ) )
12	2 11	syl	|- ( P e. Prime -> ( P =/= 2 -> 2 < P ) )
13	12	imp	|- ( ( P e. Prime /\ P =/= 2 ) -> 2 < P )
14	1 13	sylbi	|- ( P e. ( Prime \ { 2 } ) -> 2 < P )