# Metamath Proof Explorer

## 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 ℤ$
5 peano2zm ${⊢}{K}\in ℤ\to {K}-1\in ℤ$
6 5 zcnd ${⊢}{K}\in ℤ\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$