Metamath Proof Explorer

Theorem fldiv4lem1div2

Description: The floor of a positive integer divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 9-Jul-2021)

Ref Expression
Assertion fldiv4lem1div2 
|- ( N e. NN -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 elnn1uz2 
 |-  ( N e. NN <-> ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) )
2 1lt4 
 |-  1 < 4
3 1nn0 
 |-  1 e. NN0
4 4nn 
 |-  4 e. NN
5 divfl0 
 |-  ( ( 1 e. NN0 /\ 4 e. NN ) -> ( 1 < 4 <-> ( |_ ` ( 1 / 4 ) ) = 0 ) )
6 3 4 5 mp2an 
 |-  ( 1 < 4 <-> ( |_ ` ( 1 / 4 ) ) = 0 )
7 2 6 mpbi 
 |-  ( |_ ` ( 1 / 4 ) ) = 0
8 1re 
 |-  1 e. RR
9 4re 
 |-  4 e. RR
10 4ne0 
 |-  4 =/= 0
11 redivcl 
 |-  ( ( 1 e. RR /\ 4 e. RR /\ 4 =/= 0 ) -> ( 1 / 4 ) e. RR )
12 11 flcld 
 |-  ( ( 1 e. RR /\ 4 e. RR /\ 4 =/= 0 ) -> ( |_ ` ( 1 / 4 ) ) e. ZZ )
13 12 zred 
 |-  ( ( 1 e. RR /\ 4 e. RR /\ 4 =/= 0 ) -> ( |_ ` ( 1 / 4 ) ) e. RR )
14 8 9 10 13 mp3an 
 |-  ( |_ ` ( 1 / 4 ) ) e. RR
15 14 eqlei 
 |-  ( ( |_ ` ( 1 / 4 ) ) = 0 -> ( |_ ` ( 1 / 4 ) ) <_ 0 )
16 7 15 mp1i 
 |-  ( N = 1 -> ( |_ ` ( 1 / 4 ) ) <_ 0 )
17 fvoveq1 
 |-  ( N = 1 -> ( |_ ` ( N / 4 ) ) = ( |_ ` ( 1 / 4 ) ) )
18 oveq1 
 |-  ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
19 1m1e0 
 |-  ( 1 - 1 ) = 0
20 18 19 eqtrdi 
 |-  ( N = 1 -> ( N - 1 ) = 0 )
21 20 oveq1d 
 |-  ( N = 1 -> ( ( N - 1 ) / 2 ) = ( 0 / 2 ) )
22 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
23 div0 
 |-  ( ( 2 e. CC /\ 2 =/= 0 ) -> ( 0 / 2 ) = 0 )
24 22 23 ax-mp 
 |-  ( 0 / 2 ) = 0
25 21 24 eqtrdi 
 |-  ( N = 1 -> ( ( N - 1 ) / 2 ) = 0 )
26 16 17 25 3brtr4d 
 |-  ( N = 1 -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )
27 fldiv4lem1div2uz2 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )
28 26 27 jaoi 
 |-  ( ( N = 1 \/ N e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )
29 1 28 sylbi 
 |-  ( N e. NN -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )