Metamath Proof Explorer

Theorem fldiv4lem1div2uz2

Description: The floor of an integer greater than 1, divided by 4 is less than or equal to the half of the integer minus 1. (Contributed by AV, 5-Jul-2021) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Assertion fldiv4lem1div2uz2 
|- ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 eluzelz 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. ZZ )
2 zre 
 |-  ( N e. ZZ -> N e. RR )
3 id 
 |-  ( N e. RR -> N e. RR )
4 4re 
 |-  4 e. RR
5 4 a1i 
 |-  ( N e. RR -> 4 e. RR )
6 4ne0 
 |-  4 =/= 0
7 6 a1i 
 |-  ( N e. RR -> 4 =/= 0 )
8 3 5 7 redivcld 
 |-  ( N e. RR -> ( N / 4 ) e. RR )
9 flle 
 |-  ( ( N / 4 ) e. RR -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
10 1 2 8 9 4syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
11 ge2halflem1 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) <_ ( N - 1 ) )
12 2t2e4 
 |-  ( 2 x. 2 ) = 4
13 12 eqcomi 
 |-  4 = ( 2 x. 2 )
14 13 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 4 = ( 2 x. 2 ) )
15 14 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) = ( N / ( 2 x. 2 ) ) )
16 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
17 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
18 17 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. CC /\ 2 =/= 0 ) )
19 divdiv1 
 |-  ( ( N e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
20 16 18 18 19 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
21 15 20 eqtr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) = ( ( N / 2 ) / 2 ) )
22 21 breq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 4 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N / 2 ) / 2 ) <_ ( ( N - 1 ) / 2 ) ) )
23 rehalfcl 
 |-  ( N e. RR -> ( N / 2 ) e. RR )
24 1 2 23 3syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) e. RR )
25 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
26 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
27 25 26 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. RR )
28 2rp 
 |-  2 e. RR+
29 28 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR+ )
30 24 27 29 lediv1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) <_ ( N - 1 ) <-> ( ( N / 2 ) / 2 ) <_ ( ( N - 1 ) / 2 ) ) )
31 22 30 bitr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 4 ) <_ ( ( N - 1 ) / 2 ) <-> ( N / 2 ) <_ ( N - 1 ) ) )
32 11 31 mpbird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) <_ ( ( N - 1 ) / 2 ) )
33 8 flcld 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. ZZ )
34 33 zred 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. RR )
35 26 rehalfcld 
 |-  ( N e. RR -> ( ( N - 1 ) / 2 ) e. RR )
36 34 8 35 3jca 
 |-  ( N e. RR -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
37 letr 
 |-  ( ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) -> ( ( ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) /\ ( N / 4 ) <_ ( ( N - 1 ) / 2 ) ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) ) )
38 1 2 36 37 4syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) /\ ( N / 4 ) <_ ( ( N - 1 ) / 2 ) ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) ) )
39 10 32 38 mp2and 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )