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 46225

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 12572	. . . . . 6 ⊢ 2 ∈ ℤ
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
11		fourierdlem114.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
12		tpfi 9283	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
14		pire 26373	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
15	14	renegcli 11490	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
16	15	rexri 11239	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
17	14	rexri 11239	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
18		negpilt0 45286	. . . . . . . . . . . . . . 15 ⊢ -π < 0
19		pipos 26375	. . . . . . . . . . . . . . 15 ⊢ 0 < π
20		0re 11183	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
21	15, 20, 14	lttri 11307	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
22	18, 19, 21	mp2an 692	. . . . . . . . . . . . . 14 ⊢ -π < π
23	15, 14, 22	ltleii 11304	. . . . . . . . . . . . 13 ⊢ -π ≤ π
24		prunioo 13449	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
25	16, 17, 23, 24	mp3an 1463	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
26	25	difeq1i 4088	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
27		difundir 4257	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
28	26, 27	eqtr3i 2755	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
29		fourierdlem114.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
30		prfi 9281	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
31		diffi 9145	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
32	30, 31	mp1i 13	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
33		unfi 9141	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
34	29, 32, 33	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
35	28, 34	eqeltrid 2833	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
36		unfi 9141	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
37	13, 35, 36	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
38	11, 37	eqeltrid 2833	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
39		hashcl 14328	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
40	38, 39	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
41	40	nn0zd 12562	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
42	15, 22	ltneii 11294	. . . . . . 7 ⊢ -π ≠ π
43		hashprg 14367	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
44	15, 14, 43	mp2an 692	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
45	42, 44	mpbi 230	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
46	12	elexi 3473	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
47		ovex 7423	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
48		difexg 5287	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
50	46, 49	unex 7723	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
51	11, 50	eqeltri 2825	. . . . . . . 8 ⊢ 𝐻 ∈ V
52		negex 11426	. . . . . . . . . . 11 ⊢ -π ∈ V
53	52	tpid1 4735	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
54	14	elexi 3473	. . . . . . . . . . 11 ⊢ π ∈ V
55	54	tpid2 4737	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
56		prssi 4788	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
57	53, 55, 56	mp2an 692	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
58		ssun1 4144	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
59	58, 11	sseqtrri 3999	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
60	57, 59	sstri 3959	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
61		hashss 14381	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	51, 60, 61	mp2an 692	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
64	45, 63	eqbrtrrid 5146	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
65		eluz2 12806	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
66	10, 41, 64, 65	syl3anbrc 1344	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
67		uz2m1nn 12889	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
68	66, 67	syl 17	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
69	8, 68	eqeltrid 2833	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
71	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
72		negpitopissre 26456	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
73	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
74		picn 26374	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
75	74	2timesi 12326	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
76	74, 74	subnegi 11508	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
77	75, 2, 76	3eqtr4i 2763	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
78		fourierdlem114.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
79	70, 71, 73, 77, 78	fourierdlem4 46116	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
80	79, 4	ffvelcdmd 7060	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
81	72, 80	sselid 3947	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
82	70, 71, 81	3jca 1128	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
83		fvex 6874	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
84	52, 54, 83	tpss 4804	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
85	82, 84	sylib 218	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
86		iccssre 13397	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
87	15, 14, 86	mp2an 692	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
88		ssdifss 4106	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
89	87, 88	mp1i 13	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
90	85, 89	unssd 4158	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
91	11, 90	eqsstrid 3988	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
92		fourierdlem114.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
93	38, 91, 92, 8	fourierdlem36 46148	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
94		isof1o 7301	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
95		f1of 6803	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
96	93, 94, 95	3syl 18	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
97	96, 91	fssd 6708	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
98		reex 11166	. . . . 5 ⊢ ℝ ∈ V
99		ovex 7423	. . . . 5 ⊢ (0...𝑀) ∈ V
100	98, 99	elmap 8847	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
101	97, 100	sylibr 234	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
102		fveq2 6861	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
103	102	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
104	97	ffvelcdmda 7059	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
105	104	leidd 11751	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
106	105	adantr 480	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
107	103, 106	eqbrtrd 5132	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
108		elfzelz 13492	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
109	108	zred 12645	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
110	109	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
111		elfzle1 13495	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
112	111	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
113		neqne 2934	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
114	113	necomd 2981	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
115	114	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
116	110, 112, 115	ne0gt0d 11318	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
117		nnssnn0 12452	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
118		nn0uz 12842	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
119	117, 118	sseqtri 3998	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
120	119, 69	sselid 3947	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
121		eluzfz1 13499	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
122	120, 121	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
123	96, 122	ffvelcdmd 7060	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
124	91, 123	sseldd 3950	. . . . . . . . . . . 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 7304	. . . . . . . . . . . . 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 11329	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	116, 134	syldan 591	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
136	107, 135	pm2.61dan 812	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
137	136	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
138		simpr 484	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
139	137, 138	breqtrd 5136	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
140	70	rexrd 11231	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
141	71	rexrd 11231	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
142		lbicc2 13432	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
143	16, 17, 23, 142	mp3an 1463	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
144	143	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
145		ubicc2 13433	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
146	16, 17, 23, 145	mp3an 1463	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
148		iocssicc 13405	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
149	148, 80	sselid 3947	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
150		tpssi 4805	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
151	144, 147, 149, 150	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
152		difssd 4103	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
153	151, 152	unssd 4158	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
154	11, 153	eqsstrid 3988	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
155	154, 123	sseldd 3950	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
156		iccgelb 13370	. . . . . . . 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 11323	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
162	139, 158, 161	mpbir2and 713	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
163	59, 53	sselii 3946	. . . . . . 7 ⊢ -π ∈ 𝐻
164		f1ofo 6810	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
165	94, 164	syl 17	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
166		forn 6778	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
167	93, 165, 166	3syl 18	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
168	163, 167	eleqtrrid 2836	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
169		ffn 6691	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
170		fvelrnb 6924	. . . . . . 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 3142	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
174	59, 55	sselii 3946	. . . . . . 7 ⊢ π ∈ 𝐻
175	174, 167	eleqtrrid 2836	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
176		fvelrnb 6924	. . . . . . 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 6708	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
180		eluzfz2 13500	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
181	120, 180	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
182	179, 181	ffvelcdmd 7060	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
183		iccleub 13369	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
184	140, 141, 182, 183	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
185	184	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
186		id 22	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
187	186	eqcomd 2736	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
188	187	3ad2ant3 1135	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
189	105	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
190		fveq2 6861	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
191	190	adantl 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
192	189, 191	breqtrd 5136	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
193	109	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
194		elfzel2 13490	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
195	194	zred 12645	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
196	195	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
197		elfzle2 13496	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
198	197	ad2antlr 727	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
199		neqne 2934	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
200	199	necomd 2981	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
201	200	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
202	193, 196, 198, 201	leneltd 11335	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
203	104	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
204	87, 182	sselid 3947	. . . . . . . . . . . . 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 7304	. . . . . . . . . . . . . 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 11329	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	202, 215	syldan 591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	192, 216	pm2.61dan 812	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
218	217	3adant3 1132	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
219	188, 218	eqbrtrd 5132	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
220	204	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
221	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
222	220, 221	letri3d 11323	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
223	185, 219, 222	mpbir2and 713	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
224	223	rexlimdv3a 3139	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
225	178, 224	mpd 15	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
226		elfzoelz 13627	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
227	226	zred 12645	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
228	227	ltp1d 12120	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
229	228	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
230		elfzofz 13643	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
231		fzofzp1 13732	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
232	230, 231	jca 511	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
233		isorel 7304	. . . . . . 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 3126	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
237	173, 225, 236	jca31 514	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
238	7	fourierdlem2 46114	. . . 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 5949	. . . 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 46139	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
248	247	resabs1d 5982	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
249	242, 248	eqtr2id 2778	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250		fourierdlem114.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
251	250, 7, 69, 240, 11, 167	fourierdlem38 46150	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
252	249, 251	eqeltrd 2829	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
253	249	oveq1d 7405	. . 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 46157	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
264	263	simpld 494	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
265	253, 264	eqnetrd 2993	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
266	249	oveq1d 7405	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
267	263	simprd 495	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
268	266, 267	eqnetrd 2993	. 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 4740	. . . . 5 ⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)}
273		elun1 4148	. . . . 5 ⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
274	272, 273	mp1i 13	. . . 4 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
275	274, 11	eleqtrrdi 2840	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻)
276	275, 167	eleqtrrd 2832	. 2 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
277	1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276	fourierdlem113 46224	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 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2926 ∀wral 3045 ∃wrex 3054 {crab 3408 Vcvv 3450 ∖ cdif 3914 ∪ cun 3915 ⊆ wss 3917 ∅c0 4299 {cpr 4594 {ctp 4596 class class class wbr 5110 ↦ cmpt 5191 dom cdm 5641 ran crn 5642 ↾ cres 5643 ℩cio 6465 Fn wfn 6509 ⟶wf 6510 –onto→wfo 6512 –1-1-onto→wf1o 6513 ‘cfv 6514 Isom wiso 6515 (class class class)co 7390 ↑_m cmap 8802 Fincfn 8921 ℂcc 11073 ℝcr 11074 0cc0 11075 1c1 11076 + caddc 11078 · cmul 11080 +∞cpnf 11212 -∞cmnf 11213 ℝ^*cxr 11214 < clt 11215 ≤ cle 11216 − cmin 11412 -cneg 11413 / cdiv 11842 ℕcn 12193 2c2 12248 ℕ₀cn0 12449 ℤcz 12536 ℤ_≥cuz 12800 (,)cioo 13313 (,]cioc 13314 [,)cico 13315 [,]cicc 13316 ...cfz 13475 ..^cfzo 13622 ⌊cfl 13759 seqcseq 13973 ♯chash 14302 ⇝ cli 15457 Σcsu 15659 sincsin 16036 cosccos 16037 πcpi 16039 –cn→ccncf 24776 ∫citg 25526 lim_ℂ climc 25770 D cdv 25771

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 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2702 ax-rep 5237 ax-sep 5254 ax-nul 5264 ax-pow 5323 ax-pr 5390 ax-un 7714 ax-inf2 9601 ax-cc 10395 ax-cnex 11131 ax-resscn 11132 ax-1cn 11133 ax-icn 11134 ax-addcl 11135 ax-addrcl 11136 ax-mulcl 11137 ax-mulrcl 11138 ax-mulcom 11139 ax-addass 11140 ax-mulass 11141 ax-distr 11142 ax-i2m1 11143 ax-1ne0 11144 ax-1rid 11145 ax-rnegex 11146 ax-rrecex 11147 ax-cnre 11148 ax-pre-lttri 11149 ax-pre-lttrn 11150 ax-pre-ltadd 11151 ax-pre-mulgt0 11152 ax-pre-sup 11153 ax-addf 11154

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2534 df-eu 2563 df-clab 2709 df-cleq 2722 df-clel 2804 df-nfc 2879 df-ne 2927 df-nel 3031 df-ral 3046 df-rex 3055 df-rmo 3356 df-reu 3357 df-rab 3409 df-v 3452 df-sbc 3757 df-csb 3866 df-dif 3920 df-un 3922 df-in 3924 df-ss 3934 df-pss 3937 df-symdif 4219 df-nul 4300 df-if 4492 df-pw 4568 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-int 4914 df-iun 4960 df-iin 4961 df-disj 5078 df-br 5111 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5536 df-eprel 5541 df-po 5549 df-so 5550 df-fr 5594 df-se 5595 df-we 5596 df-xp 5647 df-rel 5648 df-cnv 5649 df-co 5650 df-dm 5651 df-rn 5652 df-res 5653 df-ima 5654 df-pred 6277 df-ord 6338 df-on 6339 df-lim 6340 df-suc 6341 df-iota 6467 df-fun 6516 df-fn 6517 df-f 6518 df-f1 6519 df-fo 6520 df-f1o 6521 df-fv 6522 df-isom 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-of 7656 df-ofr 7657 df-om 7846 df-1st 7971 df-2nd 7972 df-supp 8143 df-frecs 8263 df-wrecs 8294 df-recs 8343 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-omul 8442 df-er 8674 df-map 8804 df-pm 8805 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9861 df-card 9899 df-acn 9902 df-pnf 11217 df-mnf 11218 df-xr 11219 df-ltxr 11220 df-le 11221 df-sub 11414 df-neg 11415 df-div 11843 df-nn 12194 df-2 12256 df-3 12257 df-4 12258 df-5 12259 df-6 12260 df-7 12261 df-8 12262 df-9 12263 df-n0 12450 df-xnn0 12523 df-z 12537 df-dec 12657 df-uz 12801 df-q 12915 df-rp 12959 df-xneg 13079 df-xadd 13080 df-xmul 13081 df-ioo 13317 df-ioc 13318 df-ico 13319 df-icc 13320 df-fz 13476 df-fzo 13623 df-fl 13761 df-mod 13839 df-seq 13974 df-exp 14034 df-fac 14246 df-bc 14275 df-hash 14303 df-shft 15040 df-cj 15072 df-re 15073 df-im 15074 df-sqrt 15208 df-abs 15209 df-limsup 15444 df-clim 15461 df-rlim 15462 df-sum 15660 df-ef 16040 df-sin 16042 df-cos 16043 df-pi 16045 df-struct 17124 df-sets 17141 df-slot 17159 df-ndx 17171 df-base 17187 df-ress 17208 df-plusg 17240 df-mulr 17241 df-starv 17242 df-sca 17243 df-vsca 17244 df-ip 17245 df-tset 17246 df-ple 17247 df-ds 17249 df-unif 17250 df-hom 17251 df-cco 17252 df-rest 17392 df-topn 17393 df-0g 17411 df-gsum 17412 df-topgen 17413 df-pt 17414 df-prds 17417 df-xrs 17472 df-qtop 17477 df-imas 17478 df-xps 17480 df-mre 17554 df-mrc 17555 df-acs 17557 df-mgm 18574 df-sgrp 18653 df-mnd 18669 df-submnd 18718 df-mulg 19007 df-cntz 19256 df-cmn 19719 df-psmet 21263 df-xmet 21264 df-met 21265 df-bl 21266 df-mopn 21267 df-fbas 21268 df-fg 21269 df-cnfld 21272 df-top 22788 df-topon 22805 df-topsp 22827 df-bases 22840 df-cld 22913 df-ntr 22914 df-cls 22915 df-nei 22992 df-lp 23030 df-perf 23031 df-cn 23121 df-cnp 23122 df-t1 23208 df-haus 23209 df-cmp 23281 df-tx 23456 df-hmeo 23649 df-fil 23740 df-fm 23832 df-flim 23833 df-flf 23834 df-xms 24215 df-ms 24216 df-tms 24217 df-cncf 24778 df-ovol 25372 df-vol 25373 df-mbf 25527 df-itg1 25528 df-itg2 25529 df-ibl 25530 df-itg 25531 df-0p 25578 df-ditg 25755 df-limc 25774 df-dv 25775

This theorem is referenced by: fourierdlem115 46226

W3C validator