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	⊢ ( 𝐾 ∈ Odd → 𝐾 = ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		zofldiv2ALTV	⊢ ( 𝐾 ∈ Odd → ( ⌊ ‘ ( 𝐾 / 2 ) ) = ( ( 𝐾 − 1 ) / 2 ) )
2	1	oveq2d	⊢ ( 𝐾 ∈ Odd → ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) = ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) )
3	2	oveq1d	⊢ ( 𝐾 ∈ Odd → ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) = ( ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) + 1 ) )
4		oddz	⊢ ( 𝐾 ∈ Odd → 𝐾 ∈ ℤ )
5		peano2zm	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℤ )
6	5	zcnd	⊢ ( 𝐾 ∈ ℤ → ( 𝐾 − 1 ) ∈ ℂ )
7	4 6	syl	⊢ ( 𝐾 ∈ Odd → ( 𝐾 − 1 ) ∈ ℂ )
8		2cnd	⊢ ( 𝐾 ∈ Odd → 2 ∈ ℂ )
9		2ne0	⊢ 2 ≠ 0
10	9	a1i	⊢ ( 𝐾 ∈ Odd → 2 ≠ 0 )
11	7 8 10	divcan2d	⊢ ( 𝐾 ∈ Odd → ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) = ( 𝐾 − 1 ) )
12	11	oveq1d	⊢ ( 𝐾 ∈ Odd → ( ( 2 · ( ( 𝐾 − 1 ) / 2 ) ) + 1 ) = ( ( 𝐾 − 1 ) + 1 ) )
13	4	zcnd	⊢ ( 𝐾 ∈ Odd → 𝐾 ∈ ℂ )
14		npcan1	⊢ ( 𝐾 ∈ ℂ → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
15	13 14	syl	⊢ ( 𝐾 ∈ Odd → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
16	3 12 15	3eqtrrd	⊢ ( 𝐾 ∈ Odd → 𝐾 = ( ( 2 · ( ⌊ ‘ ( 𝐾 / 2 ) ) ) + 1 ) )