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

Metamath Proof Explorer

Theorem nnoddn2prmb

Description: A number is a prime number not equal to 2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion nnoddn2prmb ( 𝑁 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → 𝑁 ∈ ℙ )
2 oddn2prm ⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ¬ 2 ∥ 𝑁 )
3 1 2 jca ⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) → ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) )
4 simpl ⊢ ( ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ℙ )
5 z2even ⊢ 2 ∥ 2
6 breq2 ⊢ ( 𝑁 = 2 → ( 2 ∥ 𝑁 ↔ 2 ∥ 2 ) )
7 5 6 mpbiri ⊢ ( 𝑁 = 2 → 2 ∥ 𝑁 )
8 7 a1i ⊢ ( 𝑁 ∈ ℙ → ( 𝑁 = 2 → 2 ∥ 𝑁 ) )
9 8 con3dimp ⊢ ( ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) → ¬ 𝑁 = 2 )
10 9 neqned ⊢ ( ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ≠ 2 )
11 nelsn ⊢ ( 𝑁 ≠ 2 → ¬ 𝑁 ∈ { 2 } )
12 10 11 syl ⊢ ( ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) → ¬ 𝑁 ∈ { 2 } )
13 4 12 eldifd ⊢ ( ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) → 𝑁 ∈ ( ℙ ∖ { 2 } ) )
14 3 13 impbii ⊢ ( 𝑁 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁 ) )