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 ⊢ N ∈ ℙ ∖ 2 ↔ N ∈ ℙ ∧ ¬ 2 ∥ N

Proof

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