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 2 8 syl 
 |-  ( N e. ZZ -> ( N / 4 ) e. RR )
10 flle 
 |-  ( ( N / 4 ) e. RR -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
11 1 9 10 3syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
12 1red 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 e. RR )
13 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
14 rehalfcl 
 |-  ( N e. RR -> ( N / 2 ) e. RR )
15 1 2 14 3syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) e. RR )
16 2rp 
 |-  2 e. RR+
17 16 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 e. RR+ )
18 eluzle 
 |-  ( N e. ( ZZ>= ` 2 ) -> 2 <_ N )
19 divge1 
 |-  ( ( 2 e. RR+ /\ N e. RR /\ 2 <_ N ) -> 1 <_ ( N / 2 ) )
20 17 13 18 19 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( N / 2 ) )
21 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
22 subhalfhalf 
 |-  ( N e. CC -> ( N - ( N / 2 ) ) = ( N / 2 ) )
23 21 22 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - ( N / 2 ) ) = ( N / 2 ) )
24 20 23 breqtrrd 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 <_ ( N - ( N / 2 ) ) )
25 12 13 15 24 lesubd 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 2 ) <_ ( N - 1 ) )
26 2t2e4 
 |-  ( 2 x. 2 ) = 4
27 26 eqcomi 
 |-  4 = ( 2 x. 2 )
28 27 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> 4 = ( 2 x. 2 ) )
29 28 oveq2d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) = ( N / ( 2 x. 2 ) ) )
30 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
31 30 a1i 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( 2 e. CC /\ 2 =/= 0 ) )
32 divdiv1 
 |-  ( ( N e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
33 21 31 31 32 syl3anc 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) / 2 ) = ( N / ( 2 x. 2 ) ) )
34 29 33 eqtr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) = ( ( N / 2 ) / 2 ) )
35 34 breq1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 4 ) <_ ( ( N - 1 ) / 2 ) <-> ( ( N / 2 ) / 2 ) <_ ( ( N - 1 ) / 2 ) ) )
36 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
37 13 36 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N - 1 ) e. RR )
38 15 37 17 lediv1d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 2 ) <_ ( N - 1 ) <-> ( ( N / 2 ) / 2 ) <_ ( ( N - 1 ) / 2 ) ) )
39 35 38 bitr4d 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( N / 4 ) <_ ( ( N - 1 ) / 2 ) <-> ( N / 2 ) <_ ( N - 1 ) ) )
40 25 39 mpbird 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N / 4 ) <_ ( ( N - 1 ) / 2 ) )
41 8 flcld 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. ZZ )
42 41 zred 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. RR )
43 36 rehalfcld 
 |-  ( N e. RR -> ( ( N - 1 ) / 2 ) e. RR )
44 42 8 43 3jca 
 |-  ( N e. RR -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
45 1 2 44 3syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
46 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 ) ) )
47 45 46 syl 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( ( ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) /\ ( N / 4 ) <_ ( ( N - 1 ) / 2 ) ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) ) )
48 11 40 47 mp2and 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( |_ ` ( N / 4 ) ) <_ ( ( N - 1 ) / 2 ) )