Theorem oddprm2

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

	Ref	Expression
Hypothesis	hgt750leme.o	$$⊢O=\left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
Assertion	oddprm2	$$⊢\mathbb{P}\setminus \left\{2\right\}=O\cap \mathbb{P}$$

Proof

Step	Hyp	Ref	Expression
1		hgt750leme.o	$$⊢O=\left\{z\in \mathbb{Z}|\neg 2\parallel z\right\}$$
2		ancom	$$⊢\left(z\in O\wedge z\in \mathbb{P}\right)\leftrightarrow \left(z\in \mathbb{P}\wedge z\in O\right)$$
3		prmz	$$⊢z\in \mathbb{P}\to z\in \mathbb{Z}$$
4	1	rabeq2i	$$⊢z\in O\leftrightarrow \left(z\in \mathbb{Z}\wedge \neg 2\parallel z\right)$$
5	4	baib	$$⊢z\in \mathbb{Z}\to \left(z\in O\leftrightarrow \neg 2\parallel z\right)$$
6	3 5	syl	$$⊢z\in \mathbb{P}\to \left(z\in O\leftrightarrow \neg 2\parallel z\right)$$
7	6	pm5.32i	$$⊢\left(z\in \mathbb{P}\wedge z\in O\right)\leftrightarrow \left(z\in \mathbb{P}\wedge \neg 2\parallel z\right)$$
8	2 7	bitr2i	$$⊢\left(z\in \mathbb{P}\wedge \neg 2\parallel z\right)\leftrightarrow \left(z\in O\wedge z\in \mathbb{P}\right)$$
9		nnoddn2prmb	$$⊢z\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow \left(z\in \mathbb{P}\wedge \neg 2\parallel z\right)$$
10		elin	$$⊢z\in \left(O\cap \mathbb{P}\right)\leftrightarrow \left(z\in O\wedge z\in \mathbb{P}\right)$$
11	8 9 10	3bitr4i	$$⊢z\in \left(\mathbb{P}\setminus \left\{2\right\}\right)\leftrightarrow z\in \left(O\cap \mathbb{P}\right)$$
12	11	eqriv	$$⊢\mathbb{P}\setminus \left\{2\right\}=O\cap \mathbb{P}$$