fourierdlem114 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > fourierdlem114		Structured version Visualization version GIF version

Theorem fourierdlem114 46235

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

**Hypotheses**
Ref	Expression
fourierdlem114.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem114.t	⊢ 𝑇 = (2 · π)
fourierdlem114.per	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem114.g	⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
fourierdlem114.dmdv	⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
fourierdlem114.gcn	⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
fourierdlem114.rlim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
fourierdlem114.llim	⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
fourierdlem114.x	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem114.l	⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
fourierdlem114.r	⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
fourierdlem114.a	⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem114.b	⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
fourierdlem114.s	⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
fourierdlem114.p	⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem114.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem114.h	⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
fourierdlem114.m	⊢ 𝑀 = ((♯‘𝐻) − 1)
fourierdlem114.q	⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))

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

Distinct variable groups: 𝐴,𝑛 𝐵,𝑛 𝑥,𝐸 𝑖,𝐹,𝑛,𝑥 𝑖,𝐺,𝑥 𝑔,𝐻 𝑖,𝐿,𝑛 𝑔,𝑀 𝑖,𝑀,𝑛,𝑝 𝑥,𝑀 𝑄,𝑔 𝑄,𝑖,𝑛,𝑝 𝑥,𝑄 𝑅,𝑖,𝑛 𝑇,𝑖,𝑛,𝑝 𝑥,𝑇 𝑖,𝑋,𝑛,𝑝 𝑥,𝑋 𝜑,𝑔 𝜑,𝑖,𝑛,𝑥 Allowed substitution hints: 𝜑(𝑝) 𝐴(𝑥,𝑔,𝑖,𝑝) 𝐵(𝑥,𝑔,𝑖,𝑝) 𝑃(𝑥,𝑔,𝑖,𝑛,𝑝) 𝑅(𝑥,𝑔,𝑝) 𝑆(𝑥,𝑔,𝑖,𝑛,𝑝) 𝑇(𝑔) 𝐸(𝑔,𝑖,𝑛,𝑝) 𝐹(𝑔,𝑝) 𝐺(𝑔,𝑛,𝑝) 𝐻(𝑥,𝑖,𝑛,𝑝) 𝐿(𝑥,𝑔,𝑝) 𝑋(𝑔)

**Proof of Theorem fourierdlem114**
Step	Hyp	Ref	Expression
1		fourierdlem114.f	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem114.t	. 2 ⊢ 𝑇 = (2 · π)
3		fourierdlem114.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierdlem114.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
5		fourierdlem114.l	. 2 ⊢ (𝜑 → 𝐿 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋))
6		fourierdlem114.r	. 2 ⊢ (𝜑 → 𝑅 ∈ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋))
7		fourierdlem114.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
8		fourierdlem114.m	. . 3 ⊢ 𝑀 = ((♯‘𝐻) − 1)
9		2z 12649	. . . . . 6 ⊢ 2 ∈ ℤ
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
11		fourierdlem114.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
12		tpfi 9365	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
14		pire 26500	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
15	14	renegcli 11570	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
16	15	rexri 11319	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
17	14	rexri 11319	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
18		negpilt0 45292	. . . . . . . . . . . . . . 15 ⊢ -π < 0
19		pipos 26502	. . . . . . . . . . . . . . 15 ⊢ 0 < π
20		0re 11263	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
21	15, 20, 14	lttri 11387	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
22	18, 19, 21	mp2an 692	. . . . . . . . . . . . . 14 ⊢ -π < π
23	15, 14, 22	ltleii 11384	. . . . . . . . . . . . 13 ⊢ -π ≤ π
24		prunioo 13521	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
25	16, 17, 23, 24	mp3an 1463	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
26	25	difeq1i 4122	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
27		difundir 4291	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
28	26, 27	eqtr3i 2767	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
29		fourierdlem114.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
30		prfi 9363	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
31		diffi 9215	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
32	30, 31	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
33		unfi 9211	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
34	29, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
35	28, 34	eqeltrid 2845	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
36		unfi 9211	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
37	13, 35, 36	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
38	11, 37	eqeltrid 2845	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
39		hashcl 14395	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
41	40	nn0zd 12639	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
42	15, 22	ltneii 11374	. . . . . . 7 ⊢ -π ≠ π
43		hashprg 14434	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
44	15, 14, 43	mp2an 692	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
45	42, 44	mpbi 230	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
46	12	elexi 3503	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
47		ovex 7464	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
48		difexg 5329	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
50	46, 49	unex 7764	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
51	11, 50	eqeltri 2837	. . . . . . . 8 ⊢ 𝐻 ∈ V
52		negex 11506	. . . . . . . . . . 11 ⊢ -π ∈ V
53	52	tpid1 4768	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
54	14	elexi 3503	. . . . . . . . . . 11 ⊢ π ∈ V
55	54	tpid2 4770	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
56		prssi 4821	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
57	53, 55, 56	mp2an 692	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
58		ssun1 4178	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
59	58, 11	sseqtrri 4033	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
60	57, 59	sstri 3993	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
61		hashss 14448	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	51, 60, 61	mp2an 692	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
64	45, 63	eqbrtrrid 5179	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
65		eluz2 12884	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
66	10, 41, 64, 65	syl3anbrc 1344	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
67		uz2m1nn 12965	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
68	66, 67	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
69	8, 68	eqeltrid 2845	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
71	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
72		negpitopissre 26582	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
73	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
74		picn 26501	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
75	74	2timesi 12404	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
76	74, 74	subnegi 11588	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
77	75, 2, 76	3eqtr4i 2775	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
78		fourierdlem114.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
79	70, 71, 73, 77, 78	fourierdlem4 46126	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
80	79, 4	ffvelcdmd 7105	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
81	72, 80	sselid 3981	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
82	70, 71, 81	3jca 1129	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
83		fvex 6919	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
84	52, 54, 83	tpss 4837	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
85	82, 84	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
86		iccssre 13469	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
87	15, 14, 86	mp2an 692	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
88		ssdifss 4140	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
89	87, 88	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
90	85, 89	unssd 4192	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
91	11, 90	eqsstrid 4022	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
92		fourierdlem114.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
93	38, 91, 92, 8	fourierdlem36 46158	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
94		isof1o 7343	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
95		f1of 6848	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
96	93, 94, 95	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
97	96, 91	fssd 6753	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
98		reex 11246	. . . . 5 ⊢ ℝ ∈ V
99		ovex 7464	. . . . 5 ⊢ (0...𝑀) ∈ V
100	98, 99	elmap 8911	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
101	97, 100	sylibr 234	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
102		fveq2 6906	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
103	102	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
104	97	ffvelcdmda 7104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
105	104	leidd 11829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
106	105	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
107	103, 106	eqbrtrd 5165	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
108		elfzelz 13564	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
109	108	zred 12722	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
110	109	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
111		elfzle1 13567	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
112	111	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
113		neqne 2948	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
114	113	necomd 2996	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
115	114	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
116	110, 112, 115	ne0gt0d 11398	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
117		nnssnn0 12529	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
118		nn0uz 12920	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
119	117, 118	sseqtri 4032	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
120	119, 69	sselid 3981	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
121		eluzfz1 13571	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
122	120, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
123	96, 122	ffvelcdmd 7105	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
124	91, 123	sseldd 3984	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
125	124	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ)
126	104	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ)
127		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖)
128	93	ad2antrr 726	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
129	122	anim1i 615	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
130	129	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
131		isorel 7346	. . . . . . . . . . . . 13 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
132	128, 130, 131	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
133	127, 132	mpbid 232	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖))
134	125, 126, 133	ltled 11409	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	116, 134	syldan 591	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
136	107, 135	pm2.61dan 813	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
137	136	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
138		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
139	137, 138	breqtrd 5169	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
140	70	rexrd 11311	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
141	71	rexrd 11311	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
142		lbicc2 13504	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
143	16, 17, 23, 142	mp3an 1463	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
144	143	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
145		ubicc2 13505	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
146	16, 17, 23, 145	mp3an 1463	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
148		iocssicc 13477	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
149	148, 80	sselid 3981	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
150		tpssi 4838	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
151	144, 147, 149, 150	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
152		difssd 4137	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
153	151, 152	unssd 4192	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
154	11, 153	eqsstrid 4022	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
155	154, 123	sseldd 3984	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
156		iccgelb 13443	. . . . . . . 8 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘0) ∈ (-π[,]π)) → -π ≤ (𝑄‘0))
157	140, 141, 155, 156	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → -π ≤ (𝑄‘0))
158	157	ad2antrr 726	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0))
159	124	ad2antrr 726	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ)
160	15	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈ ℝ)
161	159, 160	letri3d 11403	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
162	139, 158, 161	mpbir2and 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
163	59, 53	sselii 3980	. . . . . . 7 ⊢ -π ∈ 𝐻
164		f1ofo 6855	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
165	94, 164	syl 17	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
166		forn 6823	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
167	93, 165, 166	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
168	163, 167	eleqtrrid 2848	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
169		ffn 6736	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
170		fvelrnb 6969	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
171	96, 169, 170	3syl 18	. . . . . 6 ⊢ (𝜑 → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
172	168, 171	mpbid 232	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)
173	162, 172	r19.29a 3162	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
174	59, 55	sselii 3980	. . . . . . 7 ⊢ π ∈ 𝐻
175	174, 167	eleqtrrid 2848	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
176		fvelrnb 6969	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
177	96, 169, 176	3syl 18	. . . . . 6 ⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
178	175, 177	mpbid 232	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)
179	96, 154	fssd 6753	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
180		eluzfz2 13572	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
181	120, 180	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
182	179, 181	ffvelcdmd 7105	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
183		iccleub 13442	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
184	140, 141, 182, 183	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
185	184	3ad2ant1 1134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
186		id 22	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
187	186	eqcomd 2743	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
188	187	3ad2ant3 1136	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
189	105	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
190		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
191	190	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
192	189, 191	breqtrd 5169	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
193	109	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
194		elfzel2 13562	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
195	194	zred 12722	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
196	195	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
197		elfzle2 13568	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
198	197	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
199		neqne 2948	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
200	199	necomd 2996	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
201	200	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
202	193, 196, 198, 201	leneltd 11415	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
203	104	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
204	87, 182	sselid 3981	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
205	204	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ)
206		simpr 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀)
207	93	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
208		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
209	181	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀))
210	208, 209	jca 511	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
211	210	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
212		isorel 7346	. . . . . . . . . . . . . 14 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
213	207, 211, 212	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
214	206, 213	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀))
215	203, 205, 214	ltled 11409	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	202, 215	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	192, 216	pm2.61dan 813	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
218	217	3adant3 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
219	188, 218	eqbrtrd 5165	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
220	204	3ad2ant1 1134	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
221	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
222	220, 221	letri3d 11403	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
223	185, 219, 222	mpbir2and 713	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
224	223	rexlimdv3a 3159	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
225	178, 224	mpd 15	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
226		elfzoelz 13699	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
227	226	zred 12722	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
228	227	ltp1d 12198	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
229	228	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
230		elfzofz 13715	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
231		fzofzp1 13803	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
232	230, 231	jca 511	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
233		isorel 7346	. . . . . . 7 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
234	93, 232, 233	syl2an 596	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
235	229, 234	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
236	235	ralrimiva 3146	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
237	173, 225, 236	jca31 514	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
238	7	fourierdlem2 46124	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
239	69, 238	syl 17	. . 3 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
240	101, 237, 239	mpbir2and 713	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
241		fourierdlem114.g	. . . . 5 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
242	241	reseq1i 5993	. . . 4 ⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
243	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
244	17	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
245	179	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
246		simpr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
247	243, 244, 245, 246	fourierdlem27 46149	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
248	247	resabs1d 6026	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
249	242, 248	eqtr2id 2790	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250		fourierdlem114.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
251	250, 7, 69, 240, 11, 167	fourierdlem38 46160	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
252	249, 251	eqeltrd 2841	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
253	249	oveq1d 7446	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
254	250	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ))
255		fourierdlem114.rlim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
256	255	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
257		fourierdlem114.llim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
258	257	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
259	93	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
260	259, 94, 95	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻)
261	81	adantr 480	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
262	259, 165, 166	3syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻)
263	254, 256, 258, 259, 260, 246, 235, 247, 261, 11, 262	fourierdlem46 46167	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
264	263	simpld 494	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
265	253, 264	eqnetrd 3008	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
266	249	oveq1d 7446	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
267	263	simprd 495	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
268	266, 267	eqnetrd 3008	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
269		fourierdlem114.a	. 2 ⊢ 𝐴 = (𝑛 ∈ ℕ₀ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (cos‘(𝑛 · 𝑥))) d𝑥 / π))
270		fourierdlem114.b	. 2 ⊢ 𝐵 = (𝑛 ∈ ℕ ↦ (∫(-π(,)π)((𝐹‘𝑥) · (sin‘(𝑛 · 𝑥))) d𝑥 / π))
271		fourierdlem114.s	. 2 ⊢ 𝑆 = (𝑛 ∈ ℕ ↦ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋)))))
272	83	tpid3 4773	. . . . 5 ⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)}
273		elun1 4182	. . . . 5 ⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
274	272, 273	mp1i 13	. . . 4 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
275	274, 11	eleqtrrdi 2852	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻)
276	275, 167	eleqtrrd 2844	. 2 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
277	1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276	fourierdlem113 46234	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3436 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 {cpr 4628 {ctp 4630 class class class wbr 5143 ↦ cmpt 5225 dom cdm 5685 ran crn 5686 ↾ cres 5687 ℩cio 6512 Fn wfn 6556 ⟶wf 6557 –onto→wfo 6559 –1-1-onto→wf1o 6560 ‘cfv 6561 Isom wiso 6562 (class class class)co 7431 ↑_m cmap 8866 Fincfn 8985 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 +∞cpnf 11292 -∞cmnf 11293 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 -cneg 11493 / cdiv 11920 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 (,)cioo 13387 (,]cioc 13388 [,)cico 13389 [,]cicc 13390 ...cfz 13547 ..^cfzo 13694 ⌊cfl 13830 seqcseq 14042 ♯chash 14369 ⇝ cli 15520 Σcsu 15722 sincsin 16099 cosccos 16100 πcpi 16102 –cn→ccncf 24902 ∫citg 25653 lim_ℂ climc 25897 D cdv 25898

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cc 10475 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-symdif 4253 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-acn 9982 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-xnn0 12600 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-fac 14313 df-bc 14342 df-hash 14370 df-shft 15106 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-sum 15723 df-ef 16103 df-sin 16105 df-cos 16106 df-pi 16108 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-t1 23322 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-ovol 25499 df-vol 25500 df-mbf 25654 df-itg1 25655 df-itg2 25656 df-ibl 25657 df-itg 25658 df-0p 25705 df-ditg 25882 df-limc 25901 df-dv 25902

This theorem is referenced by: fourierdlem115 46236

W3C validator