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

Metamath Proof Explorer

Theorem oddprmgt2

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

Ref Expression
Assertion oddprmgt2 ( 𝑃 ∈ ( ℙ ∖ { 2 } ) → 2 < 𝑃 )

Proof

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