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	$⊢ φ \to (x \in I ⟼ F) \in 𝐿^{1}$
	fourierdlem47.iblmul	$⊢ (φ \land r \in ℝ) \to (x \in I ⟼ F (- G)) \in 𝐿^{1}$
	fourierdlem47.f	$⊢ (φ \land x \in I) \to F \in ℂ$
	fourierdlem47.g	$⊢ ((φ \land x \in I) \land r \in ℂ) \to G \in ℂ$
	fourierdlem47.absg	$⊢ ((φ \land x \in I) \land r \in ℝ) \to \|G\| \leq 1$
	fourierdlem47.a	$⊢ φ \to A \in ℂ$
	fourierdlem47.x	$⊢ X = \|A\|$
	fourierdlem47.c	$⊢ φ \to C \in ℂ$
	fourierdlem47.y	$⊢ Y = \|C\|$
	fourierdlem47.z	$⊢ Z = \int_{I} \|F\| d x$
	fourierdlem47.e	$⊢ φ \to E \in ℝ^{+}$
	fourierdlem47.b	$⊢ (φ \land r \in ℂ) \to B \in ℂ$
	fourierdlem47.absb	$⊢ (φ \land r \in ℝ) \to \|B\| \leq 1$
	fourierdlem47.d	$⊢ (φ \land r \in ℂ) \to D \in ℂ$
	fourierdlem47.absd	$⊢ (φ \land r \in ℝ) \to \|D\| \leq 1$
	fourierdlem47.m	$⊢ M = ⌊(\frac{X + Y + Z}{E}) + 1⌋ + 1$
Assertion	fourierdlem47	$⊢ φ \to \exists m \in ℕ \forall r \in (m, +∞) \|A (- \frac{B}{r}) - C (- \frac{D}{r}) - \int_{I} F (- \frac{G}{r}) d x\| < E$

Proof

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

Metamath Proof Explorer

Theorem fourierdlem47

Proof