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

Metamath Proof Explorer

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 ⊢ P ∈ ℙ ∧ P ∈ Odd → P ∈ ℤ ≥ 3

Proof

Step Hyp Ref Expression
1 oddprmne2 ⊢ P ∈ ℙ ∧ P ∈ Odd ↔ P ∈ ℙ ∖ 2
2 oddprmge3 ⊢ P ∈ ℙ ∖ 2 → P ∈ ℤ ≥ 3
3 1 2 sylbi ⊢ P ∈ ℙ ∧ P ∈ Odd → P ∈ ℤ ≥ 3