Theorem 1oddALTV

Description: 1 is an odd number. (Contributed by AV, 3-Feb-2020) (Revised by AV, 18-Jun-2020)

	Ref	Expression
Assertion	1oddALTV	$$⊢1\in \mathrm{Odd}$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		1p1e2	$$⊢1+1=2$$
3	2	oveq1i	$$⊢\frac{1+1}{2}=\frac{2}{2}$$
4		2div2e1	$$⊢\frac{2}{2}=1$$
5	3 4	eqtri	$$⊢\frac{1+1}{2}=1$$
6	5 1	eqeltri	$$⊢\frac{1+1}{2}\in \mathbb{Z}$$
7		isodd	$$⊢1\in \mathrm{Odd}\leftrightarrow \left(1\in \mathbb{Z}\wedge \frac{1+1}{2}\in \mathbb{Z}\right)$$
8	1 6 7	mpbir2an	$$⊢1\in \mathrm{Odd}$$