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

Metamath Proof Explorer

Theorem oddprmne2

Description: Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021)

Ref Expression
Assertion oddprmne2 ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ ( ℙ ∖ { 2 } ) )

Proof

Step Hyp Ref Expression
1 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
2 zeo2ALTV ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 ∈ Even ↔ ¬ 𝑃 ∈ Odd ) )
3 1 2 syl ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ ¬ 𝑃 ∈ Odd ) )
4 evenprm2 ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Even ↔ 𝑃 = 2 ) )
5 3 4 bitr3d ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 ∈ Odd ↔ 𝑃 = 2 ) )
6 nne ⊢ ( ¬ 𝑃 ≠ 2 ↔ 𝑃 = 2 )
7 5 6 bitr4di ⊢ ( 𝑃 ∈ ℙ → ( ¬ 𝑃 ∈ Odd ↔ ¬ 𝑃 ≠ 2 ) )
8 7 con4bid ⊢ ( 𝑃 ∈ ℙ → ( 𝑃 ∈ Odd ↔ 𝑃 ≠ 2 ) )
9 8 pm5.32i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
10 eldifsn ⊢ ( 𝑃 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑃 ∈ ℙ ∧ 𝑃 ≠ 2 ) )
11 9 10 bitr4i ⊢ ( ( 𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ ( ℙ ∖ { 2 } ) )