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 ∈ ℤ ≥ 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 ∈ ℕ 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 ⊢ 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 ∈ ℤ ≥ 5 → N = 5 ∨ N ∈ ℤ ≥ 5 + 1
22 2re ⊢ 2 ∈ ℝ
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 ∈ ℂ
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 ⊢ 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 4div2e2 ⊢ 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 ∈ ℤ ≥ 6 ↔ 6 ∈ ℤ ∧ N ∈ ℤ ∧ 6 ≤ N
64 zre ⊢ N ∈ ℤ → N ∈ ℝ
65 id ⊢ N ∈ ℝ → N ∈ ℝ
66 38 a1i ⊢ N ∈ ℝ → 4 ∈ ℝ
67 30 a1i ⊢ N ∈ ℝ → 4 ≠ 0
68 65 66 67 redivcld ⊢ N ∈ ℝ → N 4 ∈ ℝ
69 flle ⊢ N 4 ∈ ℝ → N 4 ≤ N 4
70 64 68 69 3syl ⊢ N ∈ ℤ → N 4 ≤ N 4
71 70 adantr ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 ≤ N 4
72 68 flcld ⊢ N ∈ ℝ → N 4 ∈ ℤ
73 72 zred ⊢ N ∈ ℝ → N 4 ∈ ℝ
74 36 a1i ⊢ N ∈ ℝ → 1 ∈ ℝ
75 73 68 74 3jca ⊢ N ∈ ℝ → N 4 ∈ ℝ ∧ N 4 ∈ ℝ ∧ 1 ∈ ℝ
76 64 75 syl ⊢ N ∈ ℤ → N 4 ∈ ℝ ∧ N 4 ∈ ℝ ∧ 1 ∈ ℝ
77 76 adantr ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 ∈ ℝ ∧ N 4 ∈ ℝ ∧ 1 ∈ ℝ
78 leadd1 ⊢ N 4 ∈ ℝ ∧ N 4 ∈ ℝ ∧ 1 ∈ ℝ → N 4 ≤ N 4 ↔ N 4 + 1 ≤ N 4 + 1
79 77 78 syl ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 ≤ N 4 ↔ N 4 + 1 ≤ N 4 + 1
80 71 79 mpbid ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 + 1 ≤ N 4 + 1
81 div4p1lem1div2 ⊢ N ∈ ℝ ∧ 6 ≤ N → N 4 + 1 ≤ N − 1 2
82 64 81 sylan ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 + 1 ≤ N − 1 2
83 peano2re ⊢ N 4 ∈ ℝ → N 4 + 1 ∈ ℝ
84 73 83 syl ⊢ N ∈ ℝ → N 4 + 1 ∈ ℝ
85 peano2re ⊢ N 4 ∈ ℝ → N 4 + 1 ∈ ℝ
86 68 85 syl ⊢ N ∈ ℝ → N 4 + 1 ∈ ℝ
87 peano2rem ⊢ N ∈ ℝ → N − 1 ∈ ℝ
88 87 rehalfcld ⊢ N ∈ ℝ → N − 1 2 ∈ ℝ
89 84 86 88 3jca ⊢ N ∈ ℝ → N 4 + 1 ∈ ℝ ∧ N 4 + 1 ∈ ℝ ∧ N − 1 2 ∈ ℝ
90 64 89 syl ⊢ N ∈ ℤ → N 4 + 1 ∈ ℝ ∧ N 4 + 1 ∈ ℝ ∧ N − 1 2 ∈ ℝ
91 90 adantr ⊢ N ∈ ℤ ∧ 6 ≤ N → N 4 + 1 ∈ ℝ ∧ N 4 + 1 ∈ ℝ ∧ N − 1 2 ∈ ℝ
92 letr ⊢ N 4 + 1 ∈ ℝ ∧ N 4 + 1 ∈ ℝ ∧ N − 1 2 ∈ ℝ → N 4 + 1 ≤ N 4 + 1 ∧ N 4 + 1 ≤ N − 1 2 → N 4 + 1 ≤ N − 1 2
93 91 92 syl ⊢ N ∈ ℤ ∧ 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 ∈ ℤ ∧ 6 ≤ N → N 4 + 1 ≤ N − 1 2
95 94 3adant1 ⊢ 6 ∈ ℤ ∧ N ∈ ℤ ∧ 6 ≤ N → N 4 + 1 ≤ N − 1 2
96 63 95 sylbi ⊢ N ∈ ℤ ≥ 6 → N 4 + 1 ≤ N − 1 2
97 5p1e6 ⊢ 5 + 1 = 6
98 97 fveq2i ⊢ ℤ ≥ 5 + 1 = ℤ ≥ 6
99 96 98 eleq2s ⊢ N ∈ ℤ ≥ 5 + 1 → N 4 + 1 ≤ N − 1 2
100 62 99 jaoi ⊢ N = 5 ∨ N ∈ ℤ ≥ 5 + 1 → N 4 + 1 ≤ N − 1 2
101 21 100 syl ⊢ N ∈ ℤ ≥ 5 → N 4 + 1 ≤ N − 1 2
102 20 101 jaoi ⊢ N = 3 ∨ N ∈ ℤ ≥ 5 → N 4 + 1 ≤ N − 1 2