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→N4+1≤N−12

Proof

Step Hyp Ref Expression
1 1le1 ⊢1≤1
2 1 a1i ⊢N=3→1≤1
3 fvoveq1 ⊢N=3→N4=34
4 3lt4 ⊢3<4
5 3nn0 ⊢3∈ℕ0
6 4nn ⊢4∈ℕ
7 divfl0 ⊢3∈ℕ0∧4∈ℕ→3<4↔34=0
8 5 6 7 mp2an ⊢3<4↔34=0
9 4 8 mpbi ⊢34=0
10 3 9 eqtrdi ⊢N=3→N4=0
11 10 oveq1d ⊢N=3→N4+1=0+1
12 0p1e1 ⊢0+1=1
13 11 12 eqtrdi ⊢N=3→N4+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−12=22
18 2div2e1 ⊢22=1
19 17 18 eqtrdi ⊢N=3→N−12=1
20 2 13 19 3brtr4d ⊢N=3→N4+1≤N−12
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→N4=54
26 df-5 ⊢5=4+1
27 26 oveq1i ⊢54=4+14
28 4cn ⊢4∈ℂ
29 ax-1cn ⊢1∈ℂ
30 4ne0 ⊢4≠0
31 28 29 28 30 divdiri ⊢4+14=44+14
32 28 30 dividi ⊢44=1
33 32 oveq1i ⊢44+14=1+14
34 27 31 33 3eqtri ⊢54=1+14
35 34 fveq2i ⊢54=1+14
36 1re ⊢1∈ℝ
37 0le1 ⊢0≤1
38 4re ⊢4∈ℝ
39 4pos ⊢0<4
40 divge0 ⊢1∈ℝ∧0≤1∧4∈ℝ∧0<4→0≤14
41 36 37 38 39 40 mp4an ⊢0≤14
42 1lt4 ⊢1<4
43 recgt1 ⊢4∈ℝ∧0<4→1<4↔14<1
44 38 39 43 mp2an ⊢1<4↔14<1
45 42 44 mpbi ⊢14<1
46 1z ⊢1∈ℤ
47 38 30 rereccli ⊢14∈ℝ
48 flbi2 ⊢1∈ℤ∧14∈ℝ→1+14=1↔0≤14∧14<1
49 46 47 48 mp2an ⊢1+14=1↔0≤14∧14<1
50 41 45 49 mpbir2an ⊢1+14=1
51 35 50 eqtri ⊢54=1
52 25 51 eqtrdi ⊢N=5→N4=1
53 52 oveq1d ⊢N=5→N4+1=1+1
54 1p1e2 ⊢1+1=2
55 53 54 eqtrdi ⊢N=5→N4+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−12=42
60 4d2e2 ⊢42=2
61 59 60 eqtrdi ⊢N=5→N−12=2
62 24 55 61 3brtr4d ⊢N=5→N4+1≤N−12
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∈ℝ→N4∈ℝ
69 flle ⊢N4∈ℝ→N4≤N4
70 64 68 69 3syl ⊢N∈ℤ→N4≤N4
71 70 adantr ⊢N∈ℤ∧6≤N→N4≤N4
72 68 flcld ⊢N∈ℝ→N4∈ℤ
73 72 zred ⊢N∈ℝ→N4∈ℝ
74 36 a1i ⊢N∈ℝ→1∈ℝ
75 73 68 74 3jca ⊢N∈ℝ→N4∈ℝ∧N4∈ℝ∧1∈ℝ
76 64 75 syl ⊢N∈ℤ→N4∈ℝ∧N4∈ℝ∧1∈ℝ
77 76 adantr ⊢N∈ℤ∧6≤N→N4∈ℝ∧N4∈ℝ∧1∈ℝ
78 leadd1 ⊢N4∈ℝ∧N4∈ℝ∧1∈ℝ→N4≤N4↔N4+1≤N4+1
79 77 78 syl ⊢N∈ℤ∧6≤N→N4≤N4↔N4+1≤N4+1
80 71 79 mpbid ⊢N∈ℤ∧6≤N→N4+1≤N4+1
81 div4p1lem1div2 ⊢N∈ℝ∧6≤N→N4+1≤N−12
82 64 81 sylan ⊢N∈ℤ∧6≤N→N4+1≤N−12
83 peano2re ⊢N4∈ℝ→N4+1∈ℝ
84 73 83 syl ⊢N∈ℝ→N4+1∈ℝ
85 peano2re ⊢N4∈ℝ→N4+1∈ℝ
86 68 85 syl ⊢N∈ℝ→N4+1∈ℝ
87 peano2rem ⊢N∈ℝ→N−1∈ℝ
88 87 rehalfcld ⊢N∈ℝ→N−12∈ℝ
89 84 86 88 3jca ⊢N∈ℝ→N4+1∈ℝ∧N4+1∈ℝ∧N−12∈ℝ
90 64 89 syl ⊢N∈ℤ→N4+1∈ℝ∧N4+1∈ℝ∧N−12∈ℝ
91 90 adantr ⊢N∈ℤ∧6≤N→N4+1∈ℝ∧N4+1∈ℝ∧N−12∈ℝ
92 letr ⊢N4+1∈ℝ∧N4+1∈ℝ∧N−12∈ℝ→N4+1≤N4+1∧N4+1≤N−12→N4+1≤N−12
93 91 92 syl ⊢N∈ℤ∧6≤N→N4+1≤N4+1∧N4+1≤N−12→N4+1≤N−12
94 80 82 93 mp2and ⊢N∈ℤ∧6≤N→N4+1≤N−12
95 94 3adant1 ⊢6∈ℤ∧N∈ℤ∧6≤N→N4+1≤N−12
96 63 95 sylbi ⊢N∈ℤ≥6→N4+1≤N−12
97 5p1e6 ⊢5+1=6
98 97 fveq2i ⊢ℤ≥5+1=ℤ≥6
99 96 98 eleq2s ⊢N∈ℤ≥5+1→N4+1≤N−12
100 62 99 jaoi ⊢N=5∨N∈ℤ≥5+1→N4+1≤N−12
101 21 100 syl ⊢N∈ℤ≥5→N4+1≤N−12
102 20 101 jaoi ⊢N=3∨N∈ℤ≥5→N4+1≤N−12