Metamath Proof Explorer


Theorem fourierdlem30

Description: Sum of three small pieces is less than ε. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem30.ibl φ x I F G 𝐿 1
fourierlemreimleblemlte22.f φ x I F
fourierdlem30.g φ x I G
fourierdlem30.a φ A
fourierdlem30.x X = A
fourierdlem30.c φ C
fourierdlem30.y Y = C
fourierdlem30.z Z = I F G dx
fourierdlem30.e φ E +
fourierdlem30.r φ R
fourierdlem30.ler φ X + Y + Z E + 1 R
fourierdlem30.b φ B
fourierdlem30.12 φ B 1
fourierdlem30.d φ D
fourierdlem30.14 φ D 1
Assertion fourierdlem30 φ A B R - C D R - I F G R dx < E

Proof

Step Hyp Ref Expression
1 fourierdlem30.ibl φ x I F G 𝐿 1
2 fourierlemreimleblemlte22.f φ x I F
3 fourierdlem30.g φ x I G
4 fourierdlem30.a φ A
5 fourierdlem30.x X = A
6 fourierdlem30.c φ C
7 fourierdlem30.y Y = C
8 fourierdlem30.z Z = I F G dx
9 fourierdlem30.e φ E +
10 fourierdlem30.r φ R
11 fourierdlem30.ler φ X + Y + Z E + 1 R
12 fourierdlem30.b φ B
13 fourierdlem30.12 φ B 1
14 fourierdlem30.d φ D
15 fourierdlem30.14 φ D 1
16 10 recnd φ R
17 0red φ 0
18 1red φ 1
19 0lt1 0 < 1
20 19 a1i φ 0 < 1
21 4 abscld φ A
22 5 21 eqeltrid φ X
23 6 abscld φ C
24 7 23 eqeltrid φ Y
25 22 24 readdcld φ X + Y
26 3 negcld φ x I G
27 2 26 mulcld φ x I F G
28 27 1 itgcl φ I F G dx
29 28 abscld φ I F G dx
30 8 29 eqeltrid φ Z
31 25 30 readdcld φ X + Y + Z
32 9 rpred φ E
33 9 rpne0d φ E 0
34 31 32 33 redivcld φ X + Y + Z E
35 34 18 readdcld φ X + Y + Z E + 1
36 4 absge0d φ 0 A
37 36 5 breqtrrdi φ 0 X
38 6 absge0d φ 0 C
39 38 7 breqtrrdi φ 0 Y
40 22 24 37 39 addge0d φ 0 X + Y
41 28 absge0d φ 0 I F G dx
42 41 8 breqtrrdi φ 0 Z
43 25 30 40 42 addge0d φ 0 X + Y + Z
44 31 9 43 divge0d φ 0 X + Y + Z E
45 18 34 addge02d φ 0 X + Y + Z E 1 X + Y + Z E + 1
46 44 45 mpbid φ 1 X + Y + Z E + 1
47 18 35 10 46 11 letrd φ 1 R
48 17 18 10 20 47 ltletrd φ 0 < R
49 48 gt0ne0d φ R 0
50 12 16 49 divnegd φ B R = B R
51 50 oveq2d φ A B R = A B R
52 12 negcld φ B
53 4 52 16 49 divassd φ A B R = A B R
54 51 53 eqtr4d φ A B R = A B R
55 14 16 49 divnegd φ D R = D R
56 55 oveq2d φ C D R = C D R
57 14 negcld φ D
58 6 57 16 49 divassd φ C D R = C D R
59 56 58 eqtr4d φ C D R = C D R
60 54 59 oveq12d φ A B R C D R = A B R C D R
61 4 52 mulcld φ A B
62 6 57 mulcld φ C D
63 61 62 16 49 divsubdird φ A B C D R = A B R C D R
64 60 63 eqtr4d φ A B R C D R = A B C D R
65 16 49 reccld φ 1 R
66 65 27 1 itgmulc2 φ 1 R I F G dx = I 1 R F G dx
67 28 16 49 divrec2d φ I F G dx R = 1 R I F G dx
68 16 adantr φ x I R
69 49 adantr φ x I R 0
70 3 68 69 divnegd φ x I G R = G R
71 70 oveq2d φ x I F G R = F G R
72 2 26 68 69 divassd φ x I F G R = F G R
73 27 68 69 divrec2d φ x I F G R = 1 R F G
74 71 72 73 3eqtr2d φ x I F G R = 1 R F G
75 74 itgeq2dv φ I F G R dx = I 1 R F G dx
76 66 67 75 3eqtr4rd φ I F G R dx = I F G dx R
77 64 76 oveq12d φ A B R - C D R - I F G R dx = A B C D R I F G dx R
78 61 62 subcld φ A B C D
79 78 28 16 49 divsubdird φ A B - C D - I F G dx R = A B C D R I F G dx R
80 77 79 eqtr4d φ A B R - C D R - I F G R dx = A B - C D - I F G dx R
81 80 fveq2d φ A B R - C D R - I F G R dx = A B - C D - I F G dx R
82 78 28 subcld φ A B - C D - I F G dx
83 82 16 49 absdivd φ A B - C D - I F G dx R = A B - C D - I F G dx R
84 17 10 48 ltled φ 0 R
85 10 84 absidd φ R = R
86 85 oveq2d φ A B - C D - I F G dx R = A B - C D - I F G dx R
87 81 83 86 3eqtrd φ A B R - C D R - I F G R dx = A B - C D - I F G dx R
88 82 abscld φ A B - C D - I F G dx
89 88 10 49 redivcld φ A B - C D - I F G dx R
90 21 23 readdcld φ A + C
91 90 29 readdcld φ A + C + I F G dx
92 91 10 49 redivcld φ A + C + I F G dx R
93 10 48 elrpd φ R +
94 78 abscld φ A B C D
95 94 29 readdcld φ A B C D + I F G dx
96 78 28 abs2dif2d φ A B - C D - I F G dx A B C D + I F G dx
97 61 abscld φ A B
98 62 abscld φ C D
99 97 98 readdcld φ A B + C D
100 61 62 abs2dif2d φ A B C D A B + C D
101 4 52 absmuld φ A B = A B
102 52 abscld φ B
103 12 absnegd φ B = B
104 103 13 eqbrtrd φ B 1
105 102 18 21 36 104 lemul2ad φ A B A 1
106 21 recnd φ A
107 106 mulid1d φ A 1 = A
108 105 107 breqtrd φ A B A
109 101 108 eqbrtrd φ A B A
110 6 57 absmuld φ C D = C D
111 57 abscld φ D
112 14 absnegd φ D = D
113 112 15 eqbrtrd φ D 1
114 111 18 23 38 113 lemul2ad φ C D C 1
115 23 recnd φ C
116 115 mulid1d φ C 1 = C
117 114 116 breqtrd φ C D C
118 110 117 eqbrtrd φ C D C
119 97 98 21 23 109 118 le2addd φ A B + C D A + C
120 94 99 90 100 119 letrd φ A B C D A + C
121 94 90 29 120 leadd1dd φ A B C D + I F G dx A + C + I F G dx
122 88 95 91 96 121 letrd φ A B - C D - I F G dx A + C + I F G dx
123 88 91 93 122 lediv1dd φ A B - C D - I F G dx R A + C + I F G dx R
124 34 ltp1d φ X + Y + Z E < X + Y + Z E + 1
125 17 34 35 44 124 lelttrd φ 0 < X + Y + Z E + 1
126 125 gt0ne0d φ X + Y + Z E + 1 0
127 91 35 126 redivcld φ A + C + I F G dx X + Y + Z E + 1
128 34 44 ge0p1rpd φ X + Y + Z E + 1 +
129 5 eqcomi A = X
130 7 eqcomi C = Y
131 129 130 oveq12i A + C = X + Y
132 8 eqcomi I F G dx = Z
133 131 132 oveq12i A + C + I F G dx = X + Y + Z
134 43 133 breqtrrdi φ 0 A + C + I F G dx
135 128 93 91 134 11 lediv2ad φ A + C + I F G dx R A + C + I F G dx X + Y + Z E + 1
136 133 oveq1i A + C + I F G dx X + Y + Z E + 1 = X + Y + Z X + Y + Z E + 1
137 oveq1 X + Y + Z = 0 X + Y + Z X + Y + Z E + 1 = 0 X + Y + Z E + 1
138 137 adantl φ X + Y + Z = 0 X + Y + Z X + Y + Z E + 1 = 0 X + Y + Z E + 1
139 34 recnd φ X + Y + Z E
140 18 recnd φ 1
141 139 140 addcld φ X + Y + Z E + 1
142 141 adantr φ X + Y + Z = 0 X + Y + Z E + 1
143 oveq1 X + Y + Z = 0 X + Y + Z E = 0 E
144 143 adantl φ X + Y + Z = 0 X + Y + Z E = 0 E
145 9 rpcnd φ E
146 145 adantr φ X + Y + Z = 0 E
147 33 adantr φ X + Y + Z = 0 E 0
148 146 147 div0d φ X + Y + Z = 0 0 E = 0
149 144 148 eqtrd φ X + Y + Z = 0 X + Y + Z E = 0
150 149 oveq1d φ X + Y + Z = 0 X + Y + Z E + 1 = 0 + 1
151 0p1e1 0 + 1 = 1
152 150 151 eqtrdi φ X + Y + Z = 0 X + Y + Z E + 1 = 1
153 ax-1ne0 1 0
154 153 a1i φ X + Y + Z = 0 1 0
155 152 154 eqnetrd φ X + Y + Z = 0 X + Y + Z E + 1 0
156 142 155 div0d φ X + Y + Z = 0 0 X + Y + Z E + 1 = 0
157 138 156 eqtrd φ X + Y + Z = 0 X + Y + Z X + Y + Z E + 1 = 0
158 9 rpgt0d φ 0 < E
159 158 adantr φ X + Y + Z = 0 0 < E
160 157 159 eqbrtrd φ X + Y + Z = 0 X + Y + Z X + Y + Z E + 1 < E
161 31 adantr φ ¬ X + Y + Z = 0 X + Y + Z
162 9 adantr φ ¬ X + Y + Z = 0 E +
163 43 adantr φ ¬ X + Y + Z = 0 0 X + Y + Z
164 neqne ¬ X + Y + Z = 0 X + Y + Z 0
165 164 adantl φ ¬ X + Y + Z = 0 X + Y + Z 0
166 161 163 165 ne0gt0d φ ¬ X + Y + Z = 0 0 < X + Y + Z
167 161 166 elrpd φ ¬ X + Y + Z = 0 X + Y + Z +
168 167 162 rpdivcld φ ¬ X + Y + Z = 0 X + Y + Z E +
169 1rp 1 +
170 169 a1i φ ¬ X + Y + Z = 0 1 +
171 168 170 rpaddcld φ ¬ X + Y + Z = 0 X + Y + Z E + 1 +
172 124 adantr φ ¬ X + Y + Z = 0 X + Y + Z E < X + Y + Z E + 1
173 161 162 171 172 ltdiv23d φ ¬ X + Y + Z = 0 X + Y + Z X + Y + Z E + 1 < E
174 160 173 pm2.61dan φ X + Y + Z X + Y + Z E + 1 < E
175 136 174 eqbrtrid φ A + C + I F G dx X + Y + Z E + 1 < E
176 92 127 32 135 175 lelttrd φ A + C + I F G dx R < E
177 89 92 32 123 176 lelttrd φ A B - C D - I F G dx R < E
178 87 177 eqbrtrd φ A B R - C D R - I F G R dx < E