Theorem oddprmuzge3

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	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )

Proof

Step	Hyp	Ref	Expression
1		oddprmne2	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ ( ℙ ∖ { 2 } ) )
2		oddprmge3	⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )
3	1 2	sylbi	⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) → 𝑃 ∈ ( ℤ≥ ‘ 3 ) )