Metamath Proof Explorer

Theorem fldiv4p1lem1div2

Description: The floor of an integer equal to 3 or greater than 4, increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021)

Ref Expression
Assertion fldiv4p1lem1div2 
|- ( ( N = 3 \/ N e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 1le1 
 |-  1 <_ 1
2 1 a1i 
 |-  ( N = 3 -> 1 <_ 1 )
3 fvoveq1 
 |-  ( N = 3 -> ( |_ ` ( N / 4 ) ) = ( |_ ` ( 3 / 4 ) ) )
4 3lt4 
 |-  3 < 4
5 3nn0 
 |-  3 e. NN0
6 4nn 
 |-  4 e. NN
7 divfl0 
 |-  ( ( 3 e. NN0 /\ 4 e. NN ) -> ( 3 < 4 <-> ( |_ ` ( 3 / 4 ) ) = 0 ) )
8 5 6 7 mp2an 
 |-  ( 3 < 4 <-> ( |_ ` ( 3 / 4 ) ) = 0 )
9 4 8 mpbi 
 |-  ( |_ ` ( 3 / 4 ) ) = 0
10 3 9 eqtrdi 
 |-  ( N = 3 -> ( |_ ` ( N / 4 ) ) = 0 )
11 10 oveq1d 
 |-  ( N = 3 -> ( ( |_ ` ( N / 4 ) ) + 1 ) = ( 0 + 1 ) )
12 0p1e1 
 |-  ( 0 + 1 ) = 1
13 11 12 eqtrdi 
 |-  ( N = 3 -> ( ( |_ ` ( N / 4 ) ) + 1 ) = 1 )
14 oveq1 
 |-  ( N = 3 -> ( N - 1 ) = ( 3 - 1 ) )
15 3m1e2 
 |-  ( 3 - 1 ) = 2
16 14 15 eqtrdi 
 |-  ( N = 3 -> ( N - 1 ) = 2 )
17 16 oveq1d 
 |-  ( N = 3 -> ( ( N - 1 ) / 2 ) = ( 2 / 2 ) )
18 2div2e1 
 |-  ( 2 / 2 ) = 1
19 17 18 eqtrdi 
 |-  ( N = 3 -> ( ( N - 1 ) / 2 ) = 1 )
20 2 13 19 3brtr4d 
 |-  ( N = 3 -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
21 uzp1 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( N = 5 \/ N e. ( ZZ>= ` ( 5 + 1 ) ) ) )
22 2re 
 |-  2 e. RR
23 22 leidi 
 |-  2 <_ 2
24 23 a1i 
 |-  ( N = 5 -> 2 <_ 2 )
25 fvoveq1 
 |-  ( N = 5 -> ( |_ ` ( N / 4 ) ) = ( |_ ` ( 5 / 4 ) ) )
26 df-5 
 |-  5 = ( 4 + 1 )
27 26 oveq1i 
 |-  ( 5 / 4 ) = ( ( 4 + 1 ) / 4 )
28 4cn 
 |-  4 e. CC
29 ax-1cn 
 |-  1 e. CC
30 4ne0 
 |-  4 =/= 0
31 28 29 28 30 divdiri 
 |-  ( ( 4 + 1 ) / 4 ) = ( ( 4 / 4 ) + ( 1 / 4 ) )
32 28 30 dividi 
 |-  ( 4 / 4 ) = 1
33 32 oveq1i 
 |-  ( ( 4 / 4 ) + ( 1 / 4 ) ) = ( 1 + ( 1 / 4 ) )
34 27 31 33 3eqtri 
 |-  ( 5 / 4 ) = ( 1 + ( 1 / 4 ) )
35 34 fveq2i 
 |-  ( |_ ` ( 5 / 4 ) ) = ( |_ ` ( 1 + ( 1 / 4 ) ) )
36 1re 
 |-  1 e. RR
37 0le1 
 |-  0 <_ 1
38 4re 
 |-  4 e. RR
39 4pos 
 |-  0 < 4
40 divge0 
 |-  ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( 4 e. RR /\ 0 < 4 ) ) -> 0 <_ ( 1 / 4 ) )
41 36 37 38 39 40 mp4an 
 |-  0 <_ ( 1 / 4 )
42 1lt4 
 |-  1 < 4
43 recgt1 
 |-  ( ( 4 e. RR /\ 0 < 4 ) -> ( 1 < 4 <-> ( 1 / 4 ) < 1 ) )
44 38 39 43 mp2an 
 |-  ( 1 < 4 <-> ( 1 / 4 ) < 1 )
45 42 44 mpbi 
 |-  ( 1 / 4 ) < 1
46 1z 
 |-  1 e. ZZ
47 38 30 rereccli 
 |-  ( 1 / 4 ) e. RR
48 flbi2 
 |-  ( ( 1 e. ZZ /\ ( 1 / 4 ) e. RR ) -> ( ( |_ ` ( 1 + ( 1 / 4 ) ) ) = 1 <-> ( 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) < 1 ) ) )
49 46 47 48 mp2an 
 |-  ( ( |_ ` ( 1 + ( 1 / 4 ) ) ) = 1 <-> ( 0 <_ ( 1 / 4 ) /\ ( 1 / 4 ) < 1 ) )
50 41 45 49 mpbir2an 
 |-  ( |_ ` ( 1 + ( 1 / 4 ) ) ) = 1
51 35 50 eqtri 
 |-  ( |_ ` ( 5 / 4 ) ) = 1
52 25 51 eqtrdi 
 |-  ( N = 5 -> ( |_ ` ( N / 4 ) ) = 1 )
53 52 oveq1d 
 |-  ( N = 5 -> ( ( |_ ` ( N / 4 ) ) + 1 ) = ( 1 + 1 ) )
54 1p1e2 
 |-  ( 1 + 1 ) = 2
55 53 54 eqtrdi 
 |-  ( N = 5 -> ( ( |_ ` ( N / 4 ) ) + 1 ) = 2 )
56 oveq1 
 |-  ( N = 5 -> ( N - 1 ) = ( 5 - 1 ) )
57 5m1e4 
 |-  ( 5 - 1 ) = 4
58 56 57 eqtrdi 
 |-  ( N = 5 -> ( N - 1 ) = 4 )
59 58 oveq1d 
 |-  ( N = 5 -> ( ( N - 1 ) / 2 ) = ( 4 / 2 ) )
60 4d2e2 
 |-  ( 4 / 2 ) = 2
61 59 60 eqtrdi 
 |-  ( N = 5 -> ( ( N - 1 ) / 2 ) = 2 )
62 24 55 61 3brtr4d 
 |-  ( N = 5 -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
63 eluz2 
 |-  ( N e. ( ZZ>= ` 6 ) <-> ( 6 e. ZZ /\ N e. ZZ /\ 6 <_ N ) )
64 zre 
 |-  ( N e. ZZ -> N e. RR )
65 id 
 |-  ( N e. RR -> N e. RR )
66 38 a1i 
 |-  ( N e. RR -> 4 e. RR )
67 30 a1i 
 |-  ( N e. RR -> 4 =/= 0 )
68 65 66 67 redivcld 
 |-  ( N e. RR -> ( N / 4 ) e. RR )
69 flle 
 |-  ( ( N / 4 ) e. RR -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
70 64 68 69 3syl 
 |-  ( N e. ZZ -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
71 70 adantr 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) )
72 68 flcld 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. ZZ )
73 72 zred 
 |-  ( N e. RR -> ( |_ ` ( N / 4 ) ) e. RR )
74 36 a1i 
 |-  ( N e. RR -> 1 e. RR )
75 73 68 74 3jca 
 |-  ( N e. RR -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ 1 e. RR ) )
76 64 75 syl 
 |-  ( N e. ZZ -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ 1 e. RR ) )
77 76 adantr 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ 1 e. RR ) )
78 leadd1 
 |-  ( ( ( |_ ` ( N / 4 ) ) e. RR /\ ( N / 4 ) e. RR /\ 1 e. RR ) -> ( ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) <-> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N / 4 ) + 1 ) ) )
79 77 78 syl 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( |_ ` ( N / 4 ) ) <_ ( N / 4 ) <-> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N / 4 ) + 1 ) ) )
80 71 79 mpbid 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N / 4 ) + 1 ) )
81 div4p1lem1div2 
 |-  ( ( N e. RR /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
82 64 81 sylan 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
83 peano2re 
 |-  ( ( |_ ` ( N / 4 ) ) e. RR -> ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR )
84 73 83 syl 
 |-  ( N e. RR -> ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR )
85 peano2re 
 |-  ( ( N / 4 ) e. RR -> ( ( N / 4 ) + 1 ) e. RR )
86 68 85 syl 
 |-  ( N e. RR -> ( ( N / 4 ) + 1 ) e. RR )
87 peano2rem 
 |-  ( N e. RR -> ( N - 1 ) e. RR )
88 87 rehalfcld 
 |-  ( N e. RR -> ( ( N - 1 ) / 2 ) e. RR )
89 84 86 88 3jca 
 |-  ( N e. RR -> ( ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR /\ ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
90 64 89 syl 
 |-  ( N e. ZZ -> ( ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR /\ ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
91 90 adantr 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR /\ ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) )
92 letr 
 |-  ( ( ( ( |_ ` ( N / 4 ) ) + 1 ) e. RR /\ ( ( N / 4 ) + 1 ) e. RR /\ ( ( N - 1 ) / 2 ) e. RR ) -> ( ( ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N / 4 ) + 1 ) /\ ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) ) )
93 91 92 syl 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N / 4 ) + 1 ) /\ ( ( N / 4 ) + 1 ) <_ ( ( N - 1 ) / 2 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) ) )
94 80 82 93 mp2and 
 |-  ( ( N e. ZZ /\ 6 <_ N ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
95 94 3adant1 
 |-  ( ( 6 e. ZZ /\ N e. ZZ /\ 6 <_ N ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
96 63 95 sylbi 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
97 5p1e6 
 |-  ( 5 + 1 ) = 6
98 97 fveq2i 
 |-  ( ZZ>= ` ( 5 + 1 ) ) = ( ZZ>= ` 6 )
99 96 98 eleq2s 
 |-  ( N e. ( ZZ>= ` ( 5 + 1 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
100 62 99 jaoi 
 |-  ( ( N = 5 \/ N e. ( ZZ>= ` ( 5 + 1 ) ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
101 21 100 syl 
 |-  ( N e. ( ZZ>= ` 5 ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )
102 20 101 jaoi 
 |-  ( ( N = 3 \/ N e. ( ZZ>= ` 5 ) ) -> ( ( |_ ` ( N / 4 ) ) + 1 ) <_ ( ( N - 1 ) / 2 ) )