Metamath Proof Explorer


Theorem fourierdlem47

Description: For r large enough, the final expression is less than the given positive E . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem47.ibl
|- ( ph -> ( x e. I |-> F ) e. L^1 )
fourierdlem47.iblmul
|- ( ( ph /\ r e. RR ) -> ( x e. I |-> ( F x. -u G ) ) e. L^1 )
fourierdlem47.f
|- ( ( ph /\ x e. I ) -> F e. CC )
fourierdlem47.g
|- ( ( ( ph /\ x e. I ) /\ r e. CC ) -> G e. CC )
fourierdlem47.absg
|- ( ( ( ph /\ x e. I ) /\ r e. RR ) -> ( abs ` G ) <_ 1 )
fourierdlem47.a
|- ( ph -> A e. CC )
fourierdlem47.x
|- X = ( abs ` A )
fourierdlem47.c
|- ( ph -> C e. CC )
fourierdlem47.y
|- Y = ( abs ` C )
fourierdlem47.z
|- Z = S. I ( abs ` F ) _d x
fourierdlem47.e
|- ( ph -> E e. RR+ )
fourierdlem47.b
|- ( ( ph /\ r e. CC ) -> B e. CC )
fourierdlem47.absb
|- ( ( ph /\ r e. RR ) -> ( abs ` B ) <_ 1 )
fourierdlem47.d
|- ( ( ph /\ r e. CC ) -> D e. CC )
fourierdlem47.absd
|- ( ( ph /\ r e. RR ) -> ( abs ` D ) <_ 1 )
fourierdlem47.m
|- M = ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) + 1 )
Assertion fourierdlem47
|- ( ph -> E. m e. NN A. r e. ( m (,) +oo ) ( 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 fourierdlem47.ibl
 |-  ( ph -> ( x e. I |-> F ) e. L^1 )
2 fourierdlem47.iblmul
 |-  ( ( ph /\ r e. RR ) -> ( x e. I |-> ( F x. -u G ) ) e. L^1 )
3 fourierdlem47.f
 |-  ( ( ph /\ x e. I ) -> F e. CC )
4 fourierdlem47.g
 |-  ( ( ( ph /\ x e. I ) /\ r e. CC ) -> G e. CC )
5 fourierdlem47.absg
 |-  ( ( ( ph /\ x e. I ) /\ r e. RR ) -> ( abs ` G ) <_ 1 )
6 fourierdlem47.a
 |-  ( ph -> A e. CC )
7 fourierdlem47.x
 |-  X = ( abs ` A )
8 fourierdlem47.c
 |-  ( ph -> C e. CC )
9 fourierdlem47.y
 |-  Y = ( abs ` C )
10 fourierdlem47.z
 |-  Z = S. I ( abs ` F ) _d x
11 fourierdlem47.e
 |-  ( ph -> E e. RR+ )
12 fourierdlem47.b
 |-  ( ( ph /\ r e. CC ) -> B e. CC )
13 fourierdlem47.absb
 |-  ( ( ph /\ r e. RR ) -> ( abs ` B ) <_ 1 )
14 fourierdlem47.d
 |-  ( ( ph /\ r e. CC ) -> D e. CC )
15 fourierdlem47.absd
 |-  ( ( ph /\ r e. RR ) -> ( abs ` D ) <_ 1 )
16 fourierdlem47.m
 |-  M = ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) + 1 )
17 6 abscld
 |-  ( ph -> ( abs ` A ) e. RR )
18 7 17 eqeltrid
 |-  ( ph -> X e. RR )
19 8 abscld
 |-  ( ph -> ( abs ` C ) e. RR )
20 9 19 eqeltrid
 |-  ( ph -> Y e. RR )
21 18 20 readdcld
 |-  ( ph -> ( X + Y ) e. RR )
22 3 abscld
 |-  ( ( ph /\ x e. I ) -> ( abs ` F ) e. RR )
23 3 1 iblabs
 |-  ( ph -> ( x e. I |-> ( abs ` F ) ) e. L^1 )
24 22 23 itgrecl
 |-  ( ph -> S. I ( abs ` F ) _d x e. RR )
25 10 24 eqeltrid
 |-  ( ph -> Z e. RR )
26 21 25 readdcld
 |-  ( ph -> ( ( X + Y ) + Z ) e. RR )
27 11 rpred
 |-  ( ph -> E e. RR )
28 11 rpne0d
 |-  ( ph -> E =/= 0 )
29 26 27 28 redivcld
 |-  ( ph -> ( ( ( X + Y ) + Z ) / E ) e. RR )
30 1red
 |-  ( ph -> 1 e. RR )
31 29 30 readdcld
 |-  ( ph -> ( ( ( ( X + Y ) + Z ) / E ) + 1 ) e. RR )
32 31 flcld
 |-  ( ph -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. ZZ )
33 0red
 |-  ( ph -> 0 e. RR )
34 reflcl
 |-  ( ( ( ( ( X + Y ) + Z ) / E ) + 1 ) e. RR -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. RR )
35 31 34 syl
 |-  ( ph -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. RR )
36 0lt1
 |-  0 < 1
37 36 a1i
 |-  ( ph -> 0 < 1 )
38 6 absge0d
 |-  ( ph -> 0 <_ ( abs ` A ) )
39 38 7 breqtrrdi
 |-  ( ph -> 0 <_ X )
40 8 absge0d
 |-  ( ph -> 0 <_ ( abs ` C ) )
41 40 9 breqtrrdi
 |-  ( ph -> 0 <_ Y )
42 18 20 39 41 addge0d
 |-  ( ph -> 0 <_ ( X + Y ) )
43 3 absge0d
 |-  ( ( ph /\ x e. I ) -> 0 <_ ( abs ` F ) )
44 23 22 43 itgge0
 |-  ( ph -> 0 <_ S. I ( abs ` F ) _d x )
45 44 10 breqtrrdi
 |-  ( ph -> 0 <_ Z )
46 21 25 42 45 addge0d
 |-  ( ph -> 0 <_ ( ( X + Y ) + Z ) )
47 26 11 46 divge0d
 |-  ( ph -> 0 <_ ( ( ( X + Y ) + Z ) / E ) )
48 flge0nn0
 |-  ( ( ( ( ( X + Y ) + Z ) / E ) e. RR /\ 0 <_ ( ( ( X + Y ) + Z ) / E ) ) -> ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) e. NN0 )
49 29 47 48 syl2anc
 |-  ( ph -> ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) e. NN0 )
50 nn0addge1
 |-  ( ( 1 e. RR /\ ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) e. NN0 ) -> 1 <_ ( 1 + ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) ) )
51 30 49 50 syl2anc
 |-  ( ph -> 1 <_ ( 1 + ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) ) )
52 1z
 |-  1 e. ZZ
53 fladdz
 |-  ( ( ( ( ( X + Y ) + Z ) / E ) e. RR /\ 1 e. ZZ ) -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) = ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) )
54 29 52 53 sylancl
 |-  ( ph -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) = ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) )
55 49 nn0cnd
 |-  ( ph -> ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) e. CC )
56 30 recnd
 |-  ( ph -> 1 e. CC )
57 55 56 addcomd
 |-  ( ph -> ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) = ( 1 + ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) ) )
58 54 57 eqtr2d
 |-  ( ph -> ( 1 + ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) ) = ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) )
59 51 58 breqtrd
 |-  ( ph -> 1 <_ ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) )
60 33 30 35 37 59 ltletrd
 |-  ( ph -> 0 < ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) )
61 elnnz
 |-  ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. NN <-> ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. ZZ /\ 0 < ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) ) )
62 32 60 61 sylanbrc
 |-  ( ph -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. NN )
63 62 peano2nnd
 |-  ( ph -> ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) + 1 ) e. NN )
64 16 63 eqeltrid
 |-  ( ph -> M e. NN )
65 elioore
 |-  ( r e. ( M (,) +oo ) -> r e. RR )
66 65 2 sylan2
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( x e. I |-> ( F x. -u G ) ) e. L^1 )
67 3 adantlr
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> F e. CC )
68 simpll
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ph )
69 simpr
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> x e. I )
70 65 ad2antlr
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> r e. RR )
71 70 recnd
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> r e. CC )
72 68 69 71 4 syl21anc
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> G e. CC )
73 6 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> A e. CC )
74 8 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> C e. CC )
75 eqid
 |-  ( abs ` S. I ( F x. -u G ) _d x ) = ( abs ` S. I ( F x. -u G ) _d x )
76 11 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> E e. RR+ )
77 65 adantl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> r e. RR )
78 7 eqcomi
 |-  ( abs ` A ) = X
79 9 eqcomi
 |-  ( abs ` C ) = Y
80 78 79 oveq12i
 |-  ( ( abs ` A ) + ( abs ` C ) ) = ( X + Y )
81 80 oveq1i
 |-  ( ( ( abs ` A ) + ( abs ` C ) ) + ( abs ` S. I ( F x. -u G ) _d x ) ) = ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) )
82 17 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` A ) e. RR )
83 19 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` C ) e. RR )
84 82 83 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( abs ` A ) + ( abs ` C ) ) e. RR )
85 72 negcld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> -u G e. CC )
86 67 85 mulcld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( F x. -u G ) e. CC )
87 86 66 itgcl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> S. I ( F x. -u G ) _d x e. CC )
88 87 abscld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` S. I ( F x. -u G ) _d x ) e. RR )
89 84 88 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( abs ` A ) + ( abs ` C ) ) + ( abs ` S. I ( F x. -u G ) _d x ) ) e. RR )
90 81 89 eqeltrrid
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) e. RR )
91 27 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> E e. RR )
92 28 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> E =/= 0 )
93 90 91 92 redivcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) e. RR )
94 1red
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> 1 e. RR )
95 93 94 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) + 1 ) e. RR )
96 7 82 eqeltrid
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> X e. RR )
97 9 83 eqeltrid
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> Y e. RR )
98 96 97 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( X + Y ) e. RR )
99 25 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> Z e. RR )
100 98 99 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( X + Y ) + Z ) e. RR )
101 100 91 92 redivcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + Z ) / E ) e. RR )
102 101 94 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + Z ) / E ) + 1 ) e. RR )
103 102 34 syl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) e. RR )
104 103 94 readdcld
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) + 1 ) e. RR )
105 16 104 eqeltrid
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> M e. RR )
106 86 abscld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` ( F x. -u G ) ) e. RR )
107 86 66 iblabs
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( x e. I |-> ( abs ` ( F x. -u G ) ) ) e. L^1 )
108 106 107 itgrecl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> S. I ( abs ` ( F x. -u G ) ) _d x e. RR )
109 86 66 itgabs
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` S. I ( F x. -u G ) _d x ) <_ S. I ( abs ` ( F x. -u G ) ) _d x )
110 23 adantr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( x e. I |-> ( abs ` F ) ) e. L^1 )
111 67 abscld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` F ) e. RR )
112 67 85 absmuld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` ( F x. -u G ) ) = ( ( abs ` F ) x. ( abs ` -u G ) ) )
113 85 abscld
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` -u G ) e. RR )
114 1red
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> 1 e. RR )
115 67 absge0d
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> 0 <_ ( abs ` F ) )
116 recn
 |-  ( r e. RR -> r e. CC )
117 116 4 sylan2
 |-  ( ( ( ph /\ x e. I ) /\ r e. RR ) -> G e. CC )
118 117 absnegd
 |-  ( ( ( ph /\ x e. I ) /\ r e. RR ) -> ( abs ` -u G ) = ( abs ` G ) )
119 118 5 eqbrtrd
 |-  ( ( ( ph /\ x e. I ) /\ r e. RR ) -> ( abs ` -u G ) <_ 1 )
120 68 69 70 119 syl21anc
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` -u G ) <_ 1 )
121 113 114 111 115 120 lemul2ad
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( ( abs ` F ) x. ( abs ` -u G ) ) <_ ( ( abs ` F ) x. 1 ) )
122 111 recnd
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` F ) e. CC )
123 122 mulid1d
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( ( abs ` F ) x. 1 ) = ( abs ` F ) )
124 121 123 breqtrd
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( ( abs ` F ) x. ( abs ` -u G ) ) <_ ( abs ` F ) )
125 112 124 eqbrtrd
 |-  ( ( ( ph /\ r e. ( M (,) +oo ) ) /\ x e. I ) -> ( abs ` ( F x. -u G ) ) <_ ( abs ` F ) )
126 107 110 106 111 125 itgle
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> S. I ( abs ` ( F x. -u G ) ) _d x <_ S. I ( abs ` F ) _d x )
127 126 10 breqtrrdi
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> S. I ( abs ` ( F x. -u G ) ) _d x <_ Z )
128 88 108 99 109 127 letrd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` S. I ( F x. -u G ) _d x ) <_ Z )
129 88 99 98 128 leadd2dd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) <_ ( ( X + Y ) + Z ) )
130 90 100 76 129 lediv1dd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) <_ ( ( ( X + Y ) + Z ) / E ) )
131 flltp1
 |-  ( ( ( ( X + Y ) + Z ) / E ) e. RR -> ( ( ( X + Y ) + Z ) / E ) < ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) )
132 101 131 syl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + Z ) / E ) < ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) )
133 101 52 53 sylancl
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) = ( ( |_ ` ( ( ( X + Y ) + Z ) / E ) ) + 1 ) )
134 132 133 breqtrrd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + Z ) / E ) < ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) )
135 93 101 103 130 134 lelttrd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) < ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) )
136 93 103 94 135 ltadd1dd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) + 1 ) < ( ( |_ ` ( ( ( ( X + Y ) + Z ) / E ) + 1 ) ) + 1 ) )
137 136 16 breqtrrdi
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) + 1 ) < M )
138 105 rexrd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> M e. RR* )
139 pnfxr
 |-  +oo e. RR*
140 139 a1i
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> +oo e. RR* )
141 simpr
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> r e. ( M (,) +oo ) )
142 ioogtlb
 |-  ( ( M e. RR* /\ +oo e. RR* /\ r e. ( M (,) +oo ) ) -> M < r )
143 138 140 141 142 syl3anc
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> M < r )
144 95 105 77 137 143 lttrd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) + 1 ) < r )
145 95 77 144 ltled
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( ( ( ( X + Y ) + ( abs ` S. I ( F x. -u G ) _d x ) ) / E ) + 1 ) <_ r )
146 77 recnd
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> r e. CC )
147 146 12 syldan
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> B e. CC )
148 65 13 sylan2
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` B ) <_ 1 )
149 146 14 syldan
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> D e. CC )
150 65 15 sylan2
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` D ) <_ 1 )
151 66 67 72 73 7 74 9 75 76 77 145 147 148 149 150 fourierdlem30
 |-  ( ( ph /\ r e. ( M (,) +oo ) ) -> ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E )
152 151 ralrimiva
 |-  ( ph -> A. r e. ( M (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E )
153 oveq1
 |-  ( m = M -> ( m (,) +oo ) = ( M (,) +oo ) )
154 153 raleqdv
 |-  ( m = M -> ( A. r e. ( m (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E <-> A. r e. ( M (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E ) )
155 154 rspcev
 |-  ( ( M e. NN /\ A. r e. ( M (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E ) -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E )
156 64 152 155 syl2anc
 |-  ( ph -> E. m e. NN A. r e. ( m (,) +oo ) ( abs ` ( ( ( A x. -u ( B / r ) ) - ( C x. -u ( D / r ) ) ) - S. I ( F x. -u ( G / r ) ) _d x ) ) < E )