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 ( ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )

Proof

Step Hyp Ref Expression
1 1le1 ⊢ 1 ≤ 1
2 1 a1i ⊢ ( 𝑁 = 3 → 1 ≤ 1 )
3 fvoveq1 ⊢ ( 𝑁 = 3 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = ( ⌊ ‘ ( 3 / 4 ) ) )
4 3lt4 ⊢ 3 < 4
5 3nn0 ⊢ 3 ∈ ℕ0
6 4nn ⊢ 4 ∈ ℕ
7 divfl0 ⊢ ( ( 3 ∈ ℕ0 ∧ 4 ∈ ℕ ) → ( 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 ⊢ ( 𝑁 = 3 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = 0 )
11 10 oveq1d ⊢ ( 𝑁 = 3 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) = ( 0 + 1 ) )
12 0p1e1 ⊢ ( 0 + 1 ) = 1
13 11 12 eqtrdi ⊢ ( 𝑁 = 3 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) = 1 )
14 oveq1 ⊢ ( 𝑁 = 3 → ( 𝑁 − 1 ) = ( 3 − 1 ) )
15 3m1e2 ⊢ ( 3 − 1 ) = 2
16 14 15 eqtrdi ⊢ ( 𝑁 = 3 → ( 𝑁 − 1 ) = 2 )
17 16 oveq1d ⊢ ( 𝑁 = 3 → ( ( 𝑁 − 1 ) / 2 ) = ( 2 / 2 ) )
18 2div2e1 ⊢ ( 2 / 2 ) = 1
19 17 18 eqtrdi ⊢ ( 𝑁 = 3 → ( ( 𝑁 − 1 ) / 2 ) = 1 )
20 2 13 19 3brtr4d ⊢ ( 𝑁 = 3 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
21 uzp1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( 𝑁 = 5 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) ) )
22 2re ⊢ 2 ∈ ℝ
23 22 leidi ⊢ 2 ≤ 2
24 23 a1i ⊢ ( 𝑁 = 5 → 2 ≤ 2 )
25 fvoveq1 ⊢ ( 𝑁 = 5 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = ( ⌊ ‘ ( 5 / 4 ) ) )
26 df-5 ⊢ 5 = ( 4 + 1 )
27 26 oveq1i ⊢ ( 5 / 4 ) = ( ( 4 + 1 ) / 4 )
28 4cn ⊢ 4 ∈ ℂ
29 ax-1cn ⊢ 1 ∈ ℂ
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 ∈ ℝ
37 0le1 ⊢ 0 ≤ 1
38 4re ⊢ 4 ∈ ℝ
39 4pos ⊢ 0 < 4
40 divge0 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 ≤ 1 ) ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → 0 ≤ ( 1 / 4 ) )
41 36 37 38 39 40 mp4an ⊢ 0 ≤ ( 1 / 4 )
42 1lt4 ⊢ 1 < 4
43 recgt1 ⊢ ( ( 4 ∈ ℝ ∧ 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 ∈ ℤ
47 38 30 rereccli ⊢ ( 1 / 4 ) ∈ ℝ
48 flbi2 ⊢ ( ( 1 ∈ ℤ ∧ ( 1 / 4 ) ∈ ℝ ) → ( ( ⌊ ‘ ( 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 ⊢ ( 𝑁 = 5 → ( ⌊ ‘ ( 𝑁 / 4 ) ) = 1 )
53 52 oveq1d ⊢ ( 𝑁 = 5 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) = ( 1 + 1 ) )
54 1p1e2 ⊢ ( 1 + 1 ) = 2
55 53 54 eqtrdi ⊢ ( 𝑁 = 5 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) = 2 )
56 oveq1 ⊢ ( 𝑁 = 5 → ( 𝑁 − 1 ) = ( 5 − 1 ) )
57 5m1e4 ⊢ ( 5 − 1 ) = 4
58 56 57 eqtrdi ⊢ ( 𝑁 = 5 → ( 𝑁 − 1 ) = 4 )
59 58 oveq1d ⊢ ( 𝑁 = 5 → ( ( 𝑁 − 1 ) / 2 ) = ( 4 / 2 ) )
60 4div2e2 ⊢ ( 4 / 2 ) = 2
61 59 60 eqtrdi ⊢ ( 𝑁 = 5 → ( ( 𝑁 − 1 ) / 2 ) = 2 )
62 24 55 61 3brtr4d ⊢ ( 𝑁 = 5 → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
63 eluz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) ↔ ( 6 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) )
64 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
65 id ⊢ ( 𝑁 ∈ ℝ → 𝑁 ∈ ℝ )
66 38 a1i ⊢ ( 𝑁 ∈ ℝ → 4 ∈ ℝ )
67 30 a1i ⊢ ( 𝑁 ∈ ℝ → 4 ≠ 0 )
68 65 66 67 redivcld ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 / 4 ) ∈ ℝ )
69 flle ⊢ ( ( 𝑁 / 4 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
70 64 68 69 3syl ⊢ ( 𝑁 ∈ ℤ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
71 70 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) )
72 68 flcld ⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℤ )
73 72 zred ⊢ ( 𝑁 ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ )
74 36 a1i ⊢ ( 𝑁 ∈ ℝ → 1 ∈ ℝ )
75 73 68 74 3jca ⊢ ( 𝑁 ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ 1 ∈ ℝ ) )
76 64 75 syl ⊢ ( 𝑁 ∈ ℤ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ 1 ∈ ℝ ) )
77 76 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ 1 ∈ ℝ ) )
78 leadd1 ⊢ ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ ∧ ( 𝑁 / 4 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ↔ ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 / 4 ) + 1 ) ) )
79 77 78 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ≤ ( 𝑁 / 4 ) ↔ ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 / 4 ) + 1 ) ) )
80 71 79 mpbid ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 / 4 ) + 1 ) )
81 div4p1lem1div2 ⊢ ( ( 𝑁 ∈ ℝ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
82 64 81 sylan ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
83 peano2re ⊢ ( ( ⌊ ‘ ( 𝑁 / 4 ) ) ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ )
84 73 83 syl ⊢ ( 𝑁 ∈ ℝ → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ )
85 peano2re ⊢ ( ( 𝑁 / 4 ) ∈ ℝ → ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ )
86 68 85 syl ⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ )
87 peano2rem ⊢ ( 𝑁 ∈ ℝ → ( 𝑁 − 1 ) ∈ ℝ )
88 87 rehalfcld ⊢ ( 𝑁 ∈ ℝ → ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ )
89 84 86 88 3jca ⊢ ( 𝑁 ∈ ℝ → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
90 64 89 syl ⊢ ( 𝑁 ∈ ℤ → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
91 90 adantr ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) )
92 letr ⊢ ( ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 / 4 ) + 1 ) ∈ ℝ ∧ ( ( 𝑁 − 1 ) / 2 ) ∈ ℝ ) → ( ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 / 4 ) + 1 ) ∧ ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
93 91 92 syl ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 / 4 ) + 1 ) ∧ ( ( 𝑁 / 4 ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) ) )
94 80 82 93 mp2and ⊢ ( ( 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
95 94 3adant1 ⊢ ( ( 6 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 6 ≤ 𝑁 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
96 63 95 sylbi ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 6 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
97 5p1e6 ⊢ ( 5 + 1 ) = 6
98 97 fveq2i ⊢ ( ℤ≥ ‘ ( 5 + 1 ) ) = ( ℤ≥ ‘ 6 )
99 96 98 eleq2s ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
100 62 99 jaoi ⊢ ( ( 𝑁 = 5 ∨ 𝑁 ∈ ( ℤ≥ ‘ ( 5 + 1 ) ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
101 21 100 syl ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 5 ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )
102 20 101 jaoi ⊢ ( ( 𝑁 = 3 ∨ 𝑁 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( ⌊ ‘ ( 𝑁 / 4 ) ) + 1 ) ≤ ( ( 𝑁 − 1 ) / 2 ) )