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 ) )