Metamath Proof Explorer

Theorem zofldiv2ALTV

Description: The floor of an odd number divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020) (Revised by AV, 18-Jun-2020)

Ref Expression
Assertion zofldiv2ALTV 
|- ( N e. Odd -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( N e. Odd -> N e. ZZ )
2 1 zcnd 
 |-  ( N e. Odd -> N e. CC )
3 npcan1 
 |-  ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
4 3 eqcomd 
 |-  ( N e. CC -> N = ( ( N - 1 ) + 1 ) )
5 4 oveq1d 
 |-  ( N e. CC -> ( N / 2 ) = ( ( ( N - 1 ) + 1 ) / 2 ) )
6 peano2cnm 
 |-  ( N e. CC -> ( N - 1 ) e. CC )
7 1cnd 
 |-  ( N e. CC -> 1 e. CC )
8 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
9 8 a1i 
 |-  ( N e. CC -> ( 2 e. CC /\ 2 =/= 0 ) )
10 divdir 
 |-  ( ( ( N - 1 ) e. CC /\ 1 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( N - 1 ) + 1 ) / 2 ) = ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) )
11 6 7 9 10 syl3anc 
 |-  ( N e. CC -> ( ( ( N - 1 ) + 1 ) / 2 ) = ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) )
12 5 11 eqtrd 
 |-  ( N e. CC -> ( N / 2 ) = ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) )
13 2 12 syl 
 |-  ( N e. Odd -> ( N / 2 ) = ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) )
14 13 fveq2d 
 |-  ( N e. Odd -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) ) )
15 halfge0 
 |-  0 <_ ( 1 / 2 )
16 halflt1 
 |-  ( 1 / 2 ) < 1
17 15 16 pm3.2i 
 |-  ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 )
18 oddm1div2z 
 |-  ( N e. Odd -> ( ( N - 1 ) / 2 ) e. ZZ )
19 halfre 
 |-  ( 1 / 2 ) e. RR
20 flbi2 
 |-  ( ( ( ( N - 1 ) / 2 ) e. ZZ /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( N - 1 ) / 2 ) <-> ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
21 18 19 20 sylancl 
 |-  ( N e. Odd -> ( ( |_ ` ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( N - 1 ) / 2 ) <-> ( 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
22 17 21 mpbiri 
 |-  ( N e. Odd -> ( |_ ` ( ( ( N - 1 ) / 2 ) + ( 1 / 2 ) ) ) = ( ( N - 1 ) / 2 ) )
23 14 22 eqtrd 
 |-  ( N e. Odd -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )