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 ∥ 𝑁 ) )