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 ( ๐พ โˆˆ 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 ) )