This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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