Theorem fourierdlem30

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

	Ref	Expression
Hypotheses	fourierdlem30.ibl	$$⊢\phi \to \left(x\in I⟼F\left(-G\right)\right)\in {𝐿}^1$$
	fourierlemreimleblemlte22.f	$$⊢\left(\phi \wedge x\in I\right)\to F\in ℂ$$
	fourierdlem30.g	$$⊢\left(\phi \wedge x\in I\right)\to G\in ℂ$$
	fourierdlem30.a	$$⊢\phi \to A\in ℂ$$
	fourierdlem30.x	$$⊢X=\left|A\right|$$
	fourierdlem30.c	$$⊢\phi \to C\in ℂ$$
	fourierdlem30.y	$$⊢Y=\left|C\right|$$
	fourierdlem30.z	$$⊢Z=\left|{\int }_{I}F\left(-G\right)dx\right|$$
	fourierdlem30.e	$$⊢\phi \to E\in {ℝ}^{+}$$
	fourierdlem30.r	$$⊢\phi \to R\in ℝ$$
	fourierdlem30.ler	$$⊢\phi \to \left(\frac{X+Y+Z}{E}\right)+1\le R$$
	fourierdlem30.b	$$⊢\phi \to B\in ℂ$$
	fourierdlem30.12	$$⊢\phi \to \left|B\right|\le 1$$
	fourierdlem30.d	$$⊢\phi \to D\in ℂ$$
	fourierdlem30.14	$$⊢\phi \to \left|D\right|\le 1$$
Assertion	fourierdlem30	$$⊢\phi \to \left|A\left(-\frac{B}{R}\right)-C\left(-\frac{D}{R}\right)-{\int }_{I}F\left(-\frac{G}{R}\right)dx\right|<E$$

Proof

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