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 ∈ ℙ ∖ 2 → P ∈ ℤ ≥ 3

Proof

Step Hyp Ref Expression
1 eldifi ⊢ P ∈ ℙ ∖ 2 → P ∈ ℙ
2 oddprmgt2 ⊢ P ∈ ℙ ∖ 2 → 2 < P
3 3z ⊢ 3 ∈ ℤ
4 3 a1i ⊢ P ∈ ℙ ∧ 2 < P → 3 ∈ ℤ
5 prmz ⊢ P ∈ ℙ → P ∈ ℤ
6 5 adantr ⊢ P ∈ ℙ ∧ 2 < P → P ∈ ℤ
7 df-3 ⊢ 3 = 2 + 1
8 2z ⊢ 2 ∈ ℤ
9 zltp1le ⊢ 2 ∈ ℤ ∧ P ∈ ℤ → 2 < P ↔ 2 + 1 ≤ P
10 8 5 9 sylancr ⊢ P ∈ ℙ → 2 < P ↔ 2 + 1 ≤ P
11 10 biimpa ⊢ P ∈ ℙ ∧ 2 < P → 2 + 1 ≤ P
12 7 11 eqbrtrid ⊢ P ∈ ℙ ∧ 2 < P → 3 ≤ P
13 4 6 12 3jca ⊢ P ∈ ℙ ∧ 2 < P → 3 ∈ ℤ ∧ P ∈ ℤ ∧ 3 ≤ P
14 1 2 13 syl2anc ⊢ P ∈ ℙ ∖ 2 → 3 ∈ ℤ ∧ P ∈ ℤ ∧ 3 ≤ P
15 eluz2 ⊢ P ∈ ℤ ≥ 3 ↔ 3 ∈ ℤ ∧ P ∈ ℤ ∧ 3 ≤ P
16 14 15 sylibr ⊢ P ∈ ℙ ∖ 2 → P ∈ ℤ ≥ 3