Metamath Proof Explorer

Theorem oddprmgt2

Description: An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021)

Ref Expression
Assertion oddprmgt2 ⊢ P ∈ ℙ ∖ 2 → 2 < P

Proof

Step Hyp Ref Expression
1 eldifsn ⊢ P ∈ ℙ ∖ 2 ↔ P ∈ ℙ ∧ P ≠ 2
2 prmuz2 ⊢ P ∈ ℙ → P ∈ ℤ ≥ 2
3 eluz2 ⊢ P ∈ ℤ ≥ 2 ↔ 2 ∈ ℤ ∧ P ∈ ℤ ∧ 2 ≤ P
4 zre ⊢ 2 ∈ ℤ → 2 ∈ ℝ
5 zre ⊢ P ∈ ℤ → P ∈ ℝ
6 ltlen ⊢ 2 ∈ ℝ ∧ P ∈ ℝ → 2 < P ↔ 2 ≤ P ∧ P ≠ 2
7 4 5 6 syl2an ⊢ 2 ∈ ℤ ∧ P ∈ ℤ → 2 < P ↔ 2 ≤ P ∧ P ≠ 2
8 7 biimprd ⊢ 2 ∈ ℤ ∧ P ∈ ℤ → 2 ≤ P ∧ P ≠ 2 → 2 < P
9 8 exp4b ⊢ 2 ∈ ℤ → P ∈ ℤ → 2 ≤ P → P ≠ 2 → 2 < P
10 9 3imp ⊢ 2 ∈ ℤ ∧ P ∈ ℤ ∧ 2 ≤ P → P ≠ 2 → 2 < P
11 3 10 sylbi ⊢ P ∈ ℤ ≥ 2 → P ≠ 2 → 2 < P
12 2 11 syl ⊢ P ∈ ℙ → P ≠ 2 → 2 < P
13 12 imp ⊢ P ∈ ℙ ∧ P ≠ 2 → 2 < P
14 1 13 sylbi ⊢ P ∈ ℙ ∖ 2 → 2 < P