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 < 𝑃 )