Metamath Proof Explorer

Theorem zofldiv2

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

Ref Expression
Assertion zofldiv2 
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )

Proof

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