Metamath Proof Explorer


Theorem zofldiv2ALTV

Description: The floor of an odd numer 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 ) )