Description: A prime number which is odd is an integer greater than or equal to 3. (Contributed by AV, 20-Jul-2020) (Proof shortened by AV, 21-Aug-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | oddprmuzge3 | |- ( ( P e. Prime /\ P e. Odd ) -> P e. ( ZZ>= ` 3 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oddprmne2 | |- ( ( P e. Prime /\ P e. Odd ) <-> P e. ( Prime \ { 2 } ) ) |
|
2 | oddprmge3 | |- ( P e. ( Prime \ { 2 } ) -> P e. ( ZZ>= ` 3 ) ) |
|
3 | 1 2 | sylbi | |- ( ( P e. Prime /\ P e. Odd ) -> P e. ( ZZ>= ` 3 ) ) |