Theorem 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 e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )

Proof

Step	Hyp	Ref	Expression
1		eldifi	|- ( P e. ( Prime \ { 2 } ) -> P e. Prime )
2		oddprmgt2	|- ( P e. ( Prime \ { 2 } ) -> 2 < P )
3		3z	|- 3 e. ZZ
4	3	a1i	|- ( ( P e. Prime /\ 2 < P ) -> 3 e. ZZ )
5		prmz	|- ( P e. Prime -> P e. ZZ )
6	5	adantr	|- ( ( P e. Prime /\ 2 < P ) -> P e. ZZ )
7		df-3	|- 3 = ( 2 + 1 )
8		2z	|- 2 e. ZZ
9		zltp1le	|- ( ( 2 e. ZZ /\ P e. ZZ ) -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
10	8 5 9	sylancr	|- ( P e. Prime -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
11	10	biimpa	|- ( ( P e. Prime /\ 2 < P ) -> ( 2 + 1 ) <_ P )
12	7 11	eqbrtrid	|- ( ( P e. Prime /\ 2 < P ) -> 3 <_ P )
13	4 6 12	3jca	|- ( ( P e. Prime /\ 2 < P ) -> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) )
14	1 2 13	syl2anc	|- ( P e. ( Prime \ { 2 } ) -> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) )
15		eluz2	|- ( P e. ( ZZ>= ` 3 ) <-> ( 3 e. ZZ /\ P e. ZZ /\ 3 <_ P ) )
16	14 15	sylibr	|- ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) )