Theorem oddflALTV

Description: Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 18-Jun-2020)

	Ref	Expression
Assertion	oddflALTV	$$⊢K\in \mathrm{Odd}\to K=2⌊\frac{K}{2}⌋+1$$

Proof

Step	Hyp	Ref	Expression
1		zofldiv2ALTV	$$⊢K\in \mathrm{Odd}\to ⌊\frac{K}{2}⌋=\frac{K-1}{2}$$
2	1	oveq2d	$$⊢K\in \mathrm{Odd}\to 2⌊\frac{K}{2}⌋=2\left(\frac{K-1}{2}\right)$$
3	2	oveq1d	$$⊢K\in \mathrm{Odd}\to 2⌊\frac{K}{2}⌋+1=2\left(\frac{K-1}{2}\right)+1$$
4		oddz	$$⊢K\in \mathrm{Odd}\to K\in \mathbb{Z}$$
5		peano2zm	$$⊢K\in \mathbb{Z}\to K-1\in \mathbb{Z}$$
6	5	zcnd	$$⊢K\in \mathbb{Z}\to K-1\in ℂ$$
7	4 6	syl	$$⊢K\in \mathrm{Odd}\to K-1\in ℂ$$
8		2cnd	$$⊢K\in \mathrm{Odd}\to 2\in ℂ$$
9		2ne0	$$⊢2\ne 0$$
10	9	a1i	$$⊢K\in \mathrm{Odd}\to 2\ne 0$$
11	7 8 10	divcan2d	$$⊢K\in \mathrm{Odd}\to 2\left(\frac{K-1}{2}\right)=K-1$$
12	11	oveq1d	$$⊢K\in \mathrm{Odd}\to 2\left(\frac{K-1}{2}\right)+1=K-1+1$$
13	4	zcnd	$$⊢K\in \mathrm{Odd}\to K\in ℂ$$
14		npcan1	$$⊢K\in ℂ\to K-1+1=K$$
15	13 14	syl	$$⊢K\in \mathrm{Odd}\to K-1+1=K$$
16	3 12 15	3eqtrrd	$$⊢K\in \mathrm{Odd}\to K=2⌊\frac{K}{2}⌋+1$$