Metamath Proof Explorer


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 ) )