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

Metamath Proof Explorer

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 )