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