This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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