Theorem oddprm2

Description: Two ways to write the set of odd primes. (Contributed by Thierry Arnoux, 27-Dec-2021)

	Ref	Expression
Hypothesis	hgt750leme.o	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
Assertion	oddprm2	⊢ ( ℙ ∖ { 2 } ) = ( 𝑂 ∩ ℙ )

Proof

Step	Hyp	Ref	Expression
1		hgt750leme.o	⊢ 𝑂 = { 𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧 }
2		ancom	⊢ ( ( 𝑧 ∈ 𝑂 ∧ 𝑧 ∈ ℙ ) ↔ ( 𝑧 ∈ ℙ ∧ 𝑧 ∈ 𝑂 ) )
3		prmz	⊢ ( 𝑧 ∈ ℙ → 𝑧 ∈ ℤ )
4	1	reqabi	⊢ ( 𝑧 ∈ 𝑂 ↔ ( 𝑧 ∈ ℤ ∧ ¬ 2 ∥ 𝑧 ) )
5	4	baib	⊢ ( 𝑧 ∈ ℤ → ( 𝑧 ∈ 𝑂 ↔ ¬ 2 ∥ 𝑧 ) )
6	3 5	syl	⊢ ( 𝑧 ∈ ℙ → ( 𝑧 ∈ 𝑂 ↔ ¬ 2 ∥ 𝑧 ) )
7	6	pm5.32i	⊢ ( ( 𝑧 ∈ ℙ ∧ 𝑧 ∈ 𝑂 ) ↔ ( 𝑧 ∈ ℙ ∧ ¬ 2 ∥ 𝑧 ) )
8	2 7	bitr2i	⊢ ( ( 𝑧 ∈ ℙ ∧ ¬ 2 ∥ 𝑧 ) ↔ ( 𝑧 ∈ 𝑂 ∧ 𝑧 ∈ ℙ ) )
9		nnoddn2prmb	⊢ ( 𝑧 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑧 ∈ ℙ ∧ ¬ 2 ∥ 𝑧 ) )
10		elin	⊢ ( 𝑧 ∈ ( 𝑂 ∩ ℙ ) ↔ ( 𝑧 ∈ 𝑂 ∧ 𝑧 ∈ ℙ ) )
11	8 9 10	3bitr4i	⊢ ( 𝑧 ∈ ( ℙ ∖ { 2 } ) ↔ 𝑧 ∈ ( 𝑂 ∩ ℙ ) )
12	11	eqriv	⊢ ( ℙ ∖ { 2 } ) = ( 𝑂 ∩ ℙ )