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 mulid1d
 |-  ( 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 mulid1d
 |-  ( 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 )