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 e. Odd -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		zofldiv2ALTV	|- ( K e. Odd -> ( |_ ` ( K / 2 ) ) = ( ( K - 1 ) / 2 ) )
2	1	oveq2d	|- ( K e. Odd -> ( 2 x. ( |_ ` ( K / 2 ) ) ) = ( 2 x. ( ( K - 1 ) / 2 ) ) )
3	2	oveq1d	|- ( K e. Odd -> ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) = ( ( 2 x. ( ( K - 1 ) / 2 ) ) + 1 ) )
4		oddz	|- ( K e. Odd -> K e. ZZ )
5		peano2zm	|- ( K e. ZZ -> ( K - 1 ) e. ZZ )
6	5	zcnd	|- ( K e. ZZ -> ( K - 1 ) e. CC )
7	4 6	syl	|- ( K e. Odd -> ( K - 1 ) e. CC )
8		2cnd	|- ( K e. Odd -> 2 e. CC )
9		2ne0	|- 2 =/= 0
10	9	a1i	|- ( K e. Odd -> 2 =/= 0 )
11	7 8 10	divcan2d	|- ( K e. Odd -> ( 2 x. ( ( K - 1 ) / 2 ) ) = ( K - 1 ) )
12	11	oveq1d	|- ( K e. Odd -> ( ( 2 x. ( ( K - 1 ) / 2 ) ) + 1 ) = ( ( K - 1 ) + 1 ) )
13	4	zcnd	|- ( K e. Odd -> K e. CC )
14		npcan1	|- ( K e. CC -> ( ( K - 1 ) + 1 ) = K )
15	13 14	syl	|- ( K e. Odd -> ( ( K - 1 ) + 1 ) = K )
16	3 12 15	3eqtrrd	|- ( K e. Odd -> K = ( ( 2 x. ( |_ ` ( K / 2 ) ) ) + 1 ) )