Theorem dfodd5

Description: Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020)

	Ref	Expression
Assertion	dfodd5	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2\ne 0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfodd4	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2=1\right\}$$
2		elmod2	$$⊢z\in \mathbb{Z}\to z\mathrm{mod}2\in \left\{0,1\right\}$$
3		prcom	$$⊢\left\{0,1\right\}=\left\{1,0\right\}$$
4	3	eleq2i	$$⊢z\mathrm{mod}2\in \left\{0,1\right\}\leftrightarrow z\mathrm{mod}2\in \left\{1,0\right\}$$
5	4	biimpi	$$⊢z\mathrm{mod}2\in \left\{0,1\right\}\to z\mathrm{mod}2\in \left\{1,0\right\}$$
6		ax-1ne0	$$⊢1\ne 0$$
7		elprneb	$$⊢\left(z\mathrm{mod}2\in \left\{1,0\right\}\wedge 1\ne 0\right)\to \left(z\mathrm{mod}2=1\leftrightarrow z\mathrm{mod}2\ne 0\right)$$
8	5 6 7	sylancl	$$⊢z\mathrm{mod}2\in \left\{0,1\right\}\to \left(z\mathrm{mod}2=1\leftrightarrow z\mathrm{mod}2\ne 0\right)$$
9	2 8	syl	$$⊢z\in \mathbb{Z}\to \left(z\mathrm{mod}2=1\leftrightarrow z\mathrm{mod}2\ne 0\right)$$
10	9	rabbiia	$$⊢\left\{z\in \mathbb{Z}|z\mathrm{mod}2=1\right\}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2\ne 0\right\}$$
11	1 10	eqtri	$$⊢\mathrm{Odd}=\left\{z\in \mathbb{Z}|z\mathrm{mod}2\ne 0\right\}$$