Theorem fourierdlem115 46935

Description: Fourier serier convergence, for piecewise smooth functions. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fourierdlem115.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem115.t	⊢ 𝑇 = (2 · π)
fourierdlem115.per	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem115.g	⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
fourierdlem115.dmdv	⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
fourierdlem115.dvcn	⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
fourierdlem115.rlim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)
fourierdlem115.llim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)
fourierdlem115.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem115.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋))
fourierdlem115.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋))
fourierdlem115.a	⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem115.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem115.s	⊢ 𝑆 = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))

Assertion

Ref	Expression
fourierdlem115	⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘   𝑘,𝐹,𝑛,𝑥   𝑘,𝐺,𝑥   𝑘,𝐿   𝑅,𝑘   𝑇,𝑘,𝑥   𝑘,𝑋,𝑛,𝑥   𝜑,𝑘,𝑥

Allowed substitution hints:   𝜑(𝑛)   𝐴(𝑥,𝑛)   𝐵(𝑥,𝑛)   𝑅(𝑥,𝑛)   𝑆(𝑥,𝑘,𝑛)   𝑇(𝑛)   𝐺(𝑛)   𝐿(𝑥,𝑛)

Proof of Theorem fourierdlem115

Dummy variables 𝑧 𝑓 𝑔 𝑤 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem115.f	. . . 4 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem115.t	. . . 4 ⊢ 𝑇 = (2 · π)
3		fourierdlem115.per	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierdlem115.g	. . . 4 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
5		fourierdlem115.dmdv	. . . 4 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
6		fourierdlem115.dvcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
7		fourierdlem115.rlim	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) limℂ 𝑥) ≠ ∅)
8		fourierdlem115.llim	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) limℂ 𝑥) ≠ ∅)
9		fourierdlem115.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ ℝ)
10		fourierdlem115.l	. . . 4 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) limℂ 𝑋))
11		fourierdlem115.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) limℂ 𝑋))
12		fourierdlem115.a	. . . . 5 ⊢ 𝐴 = (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
13		oveq1 7417	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑥) = (𝑘 · 𝑥))
14	13	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑥)) = (cos‘(𝑘 · 𝑥)))
15	14	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))))
16	15	adantr 485	. . . . . . . 8 ⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))))
17	16	itgeq2dv 25941	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 = ∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥)
18	17	oveq1d 7425	. . . . . 6 ⊢ (𝑛 = 𝑘 → (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π) = (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π))
19	18	cbvmptv 5215	. . . . 5 ⊢ (𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π)) = (𝑘 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π))
20	12, 19	eqtri 2786	. . . 4 ⊢ 𝐴 = (𝑘 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑘 · 𝑥))) d𝑥 / π))
21		fourierdlem115.b	. . . . 5 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
22	13	fveq2d 6885	. . . . . . . . . 10 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑥)) = (sin‘(𝑘 · 𝑥)))
23	22	oveq2d 7426	. . . . . . . . 9 ⊢ (𝑛 = 𝑘 → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))))
24	23	adantr 485	. . . . . . . 8 ⊢ ((𝑛 = 𝑘 ∧ 𝑥 ∈ (-π(,)π)) → ((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) = ((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))))
25	24	itgeq2dv 25941	. . . . . . 7 ⊢ (𝑛 = 𝑘 → ∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 = ∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥)
26	25	oveq1d 7425	. . . . . 6 ⊢ (𝑛 = 𝑘 → (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π) = (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π))
27	26	cbvmptv 5215	. . . . 5 ⊢ (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π)) = (𝑘 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π))
28	21, 27	eqtri 2786	. . . 4 ⊢ 𝐵 = (𝑘 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑘 · 𝑥))) d𝑥 / π))
29		fourierdlem115.s	. . . 4 ⊢ 𝑆 = (𝑘 ∈ ℕ ↦ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
30		eqid 2763	. . . 4 ⊢ (𝑘 ∈ ℕ ↦ {𝑤 ∈ (ℝ ↑m (0...𝑘)) ∣ (((𝑤‘0) = -π ∧ (𝑤‘𝑘) = π) ∧ ∀𝑧 ∈ (0..^𝑘)(𝑤‘𝑧) < (𝑤‘(𝑧 + 1)))}) = (𝑘 ∈ ℕ ↦ {𝑤 ∈ (ℝ ↑m (0...𝑘)) ∣ (((𝑤‘0) = -π ∧ (𝑤‘𝑘) = π) ∧ ∀𝑧 ∈ (0..^𝑘)(𝑤‘𝑧) < (𝑤‘(𝑧 + 1)))})
31		id 23	. . . . . 6 ⊢ (𝑦 = 𝑥 → 𝑦 = 𝑥)
32		oveq2 7418	. . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (π − 𝑦) = (π − 𝑥))
33	32	oveq1d 7425	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → ((π − 𝑦) / 𝑇) = ((π − 𝑥) / 𝑇))
34	33	fveq2d 6885	. . . . . . 7 ⊢ (𝑦 = 𝑥 → (⌊‘((π − 𝑦) / 𝑇)) = (⌊‘((π − 𝑥) / 𝑇)))
35	34	oveq1d 7425	. . . . . 6 ⊢ (𝑦 = 𝑥 → ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇) = ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇))
36	31, 35	oveq12d 7428	. . . . 5 ⊢ (𝑦 = 𝑥 → (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)) = (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
37	36	cbvmptv 5215	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇))) = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
38		eqid 2763	. . . 4 ⊢ ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) = ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
39		eqid 2763	. . . 4 ⊢ ((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1) = ((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)
40		isoeq1 7315	. . . . 5 ⊢ (𝑔 = 𝑓 → (𝑔 Isom < , < ((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) ↔ 𝑓 Isom < , < ((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))))
41	40	cbviotavw 6500	. . . 4 ⊢ (℩𝑔𝑔 Isom < , < ((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))) = (℩𝑓𝑓 Isom < , < ((0...((♯‘({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))) − 1)), ({-π, π, ((𝑦 ∈ ℝ ↦ (𝑦 + ((⌊‘((π − 𝑦) / 𝑇)) · 𝑇)))‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))))
42	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 20, 28, 29, 30, 37, 38, 39, 41	fourierdlem114 46934	. . 3 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))
43	42	simpld 499	. 2 ⊢ (𝜑 → seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)))
44		fveq2 6881	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐴‘𝑛) = (𝐴‘𝑘))
45		oveq1 7417	. . . . . . . 8 ⊢ (𝑛 = 𝑘 → (𝑛 · 𝑋) = (𝑘 · 𝑋))
46	45	fveq2d 6885	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (cos‘(𝑛 · 𝑋)) = (cos‘(𝑘 · 𝑋)))
47	44, 46	oveq12d 7428	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) = ((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))))
48		fveq2 6881	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (𝐵‘𝑛) = (𝐵‘𝑘))
49	45	fveq2d 6885	. . . . . . 7 ⊢ (𝑛 = 𝑘 → (sin‘(𝑛 · 𝑋)) = (sin‘(𝑘 · 𝑋)))
50	48, 49	oveq12d 7428	. . . . . 6 ⊢ (𝑛 = 𝑘 → ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))) = ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
51	47, 50	oveq12d 7428	. . . . 5 ⊢ (𝑛 = 𝑘 → (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
52		nfcv 2925	. . . . 5 ⊢ Ⅎ𝑘(((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))
53		nfmpt1 5210	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ0 ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
54	12, 53	nfcxfr 2923	. . . . . . . 8 ⊢ Ⅎ𝑛𝐴
55		nfcv 2925	. . . . . . . 8 ⊢ Ⅎ𝑛𝑘
56	54, 55	nffv 6891	. . . . . . 7 ⊢ Ⅎ𝑛(𝐴‘𝑘)
57		nfcv 2925	. . . . . . 7 ⊢ Ⅎ𝑛 ·
58		nfcv 2925	. . . . . . 7 ⊢ Ⅎ𝑛(cos‘(𝑘 · 𝑋))
59	56, 57, 58	nfov 7440	. . . . . 6 ⊢ Ⅎ𝑛((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋)))
60		nfcv 2925	. . . . . 6 ⊢ Ⅎ𝑛 +
61		nfmpt1 5210	. . . . . . . . 9 ⊢ Ⅎ𝑛(𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
62	21, 61	nfcxfr 2923	. . . . . . . 8 ⊢ Ⅎ𝑛𝐵
63	62, 55	nffv 6891	. . . . . . 7 ⊢ Ⅎ𝑛(𝐵‘𝑘)
64		nfcv 2925	. . . . . . 7 ⊢ Ⅎ𝑛(sin‘(𝑘 · 𝑋))
65	63, 57, 64	nfov 7440	. . . . . 6 ⊢ Ⅎ𝑛((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))
66	59, 60, 65	nfov 7440	. . . . 5 ⊢ Ⅎ𝑛(((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
67	51, 52, 66	cbvsum 15742	. . . 4 ⊢ Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))) = Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))
68	67	oveq2i 7421	. . 3 ⊢ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋)))))
69	42	simprd 500	. . 3 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑘 ∈ ℕ (((𝐴‘𝑘) · (cos‘(𝑘 · 𝑋))) + ((𝐵‘𝑘) · (sin‘(𝑘 · 𝑋))))) = ((𝐿 + 𝑅) / 2))
70	68, 69	eqtrid 2810	. 2 ⊢ (𝜑 → (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2))
71	43, 70	jca 520	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  {crab 3416   ∖ cdif 3902   ∪ cun 3903  ∅c0 4286  {ctp 4593   class class class wbr 5109   ↦ cmpt 5192  dom cdm 5661   ↾ cres 5663  ℩cio 6490  ⟶wf 6532  ‘cfv 6536   Isom wiso 6537  (class class class)co 7410   ↑_m cmap 8820  Fincfn 8939  ℂcc 11093  ℝcr 11094  0cc0 11095  1c1 11096   + caddc 11098   · cmul 11100  +∞cpnf 11235  -∞cmnf 11236   < clt 11238   − cmin 11436  -cneg 11437   / cdiv 11866  ℕcn 12228  2c2 12290  ℕ₀cn0 12499  (,)cioo 13367  (,]cioc 13368  [,)cico 13369  [,]cicc 13370  ...cfz 13530  ..^cfzo 13678  ⌊cfl 13819  seqcseq 14033  ♯chash 14362   ⇝ cli 15531  Σcsu 15733  sincsin 16112  cosccos 16113  πcpi 16115  –cn→ccncf 25035  ∫citg 25777   lim_ℂ climc 26021   D cdv 26022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cc 10414  ax-cnex 11151  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172  ax-pre-sup 11173  ax-addf 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-symdif 4206  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-tp 4594  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-disj 5077  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-of 7674  df-ofr 7675  df-om 7859  df-1st 7982  df-2nd 7983  df-supp 8153  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-2o 8450  df-oadd 8453  df-omul 8454  df-er 8690  df-map 8822  df-pm 8823  df-ixp 8892  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-fsupp 9318  df-fi 9367  df-sup 9398  df-inf 9399  df-oi 9468  df-dju 9883  df-card 9921  df-acn 9924  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-div 11867  df-nn 12229  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303  df-8 12304  df-9 12305  df-n0 12500  df-xnn0 12573  df-z 12587  df-dec 12707  df-uz 12858  df-q 12968  df-rp 13012  df-xneg 13132  df-xadd 13133  df-xmul 13134  df-ioo 13371  df-ioc 13372  df-ico 13373  df-icc 13374  df-fz 13531  df-fzo 13679  df-fl 13821  df-mod 13899  df-seq 14034  df-exp 14094  df-fac 14306  df-bc 14335  df-hash 14363  df-shft 15100  df-cj 15146  df-re 15147  df-im 15148  df-sqrt 15282  df-abs 15283  df-limsup 15518  df-clim 15535  df-rlim 15536  df-sum 15734  df-ef 16116  df-sin 16118  df-cos 16119  df-pi 16121  df-struct 17202  df-sets 17219  df-slot 17237  df-ndx 17249  df-base 17265  df-ress 17286  df-plusg 17318  df-mulr 17319  df-starv 17320  df-sca 17321  df-vsca 17322  df-ip 17323  df-tset 17324  df-ple 17325  df-ds 17327  df-unif 17328  df-hom 17329  df-cco 17330  df-rest 17470  df-topn 17471  df-0g 17489  df-gsum 17490  df-topgen 17491  df-pt 17492  df-prds 17495  df-xrs 17551  df-qtop 17556  df-imas 17557  df-xps 17559  df-mre 17633  df-mrc 17634  df-acs 17636  df-mgm 18693  df-sgrp 18772  df-mnd 18788  df-submnd 18837  df-mulg 19129  df-cntz 19382  df-cmn 19847  df-psmet 21514  df-xmet 21515  df-met 21516  df-bl 21517  df-mopn 21518  df-fbas 21519  df-fg 21520  df-cnfld 21523  df-top 23051  df-topon 23068  df-topsp 23090  df-bases 23103  df-cld 23176  df-ntr 23177  df-cls 23178  df-nei 23255  df-lp 23293  df-perf 23294  df-cn 23384  df-cnp 23385  df-t1 23471  df-haus 23472  df-cmp 23544  df-tx 23719  df-hmeo 23912  df-fil 24003  df-fm 24095  df-flim 24096  df-flf 24097  df-xms 24477  df-ms 24478  df-tms 24479  df-cncf 25037  df-ovol 25623  df-vol 25624  df-mbf 25778  df-itg1 25779  df-itg2 25780  df-ibl 25781  df-itg 25782  df-0p 25829  df-ditg 26006  df-limc 26025  df-dv 26026

This theorem is referenced by:  fourierd  46936  fourierclimd  46937