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 )

Metamath Proof Explorer

Theorem fourierdlem47

Proof