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