This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( ph -> ( x e. I |-> ( F x. -u G ) ) e. L^1 )
fourierlemreimleblemlte22.f 
|- ( ( ph /\ x e. I ) -> F e. CC )
fourierdlem30.g 
|- ( ( ph /\ x e. I ) -> G e. CC )
fourierdlem30.a 
|- ( ph -> A e. CC )
fourierdlem30.x 
|- X = ( abs ` A )
fourierdlem30.c 
|- ( ph -> C e. CC )
fourierdlem30.y 
|- Y = ( abs ` C )
fourierdlem30.z 
|- Z = ( abs ` S. I ( F x. -u G ) _d x )
fourierdlem30.e 
|- ( ph -> E e. RR+ )
fourierdlem30.r 
|- ( ph -> R e. RR )
fourierdlem30.ler 
|- ( ph -> ( ( ( ( X + Y ) + Z ) / E ) + 1 ) <_ R )
fourierdlem30.b 
|- ( ph -> B e. CC )
fourierdlem30.12 
|- ( ph -> ( abs ` B ) <_ 1 )
fourierdlem30.d 
|- ( ph -> D e. CC )
fourierdlem30.14 
|- ( ph -> ( abs ` D ) <_ 1 )
Assertion fourierdlem30 
|- ( ph -> ( abs ` ( ( ( A x. -u ( B / R ) ) - ( C x. -u ( D / R ) ) ) - S. I ( F x. -u ( G / R ) ) _d x ) ) < E )

Proof

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