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 47056

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 12654	. . . . . 6 ⊢ 2 ∈ ℤ
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
11		fourierdlem114.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
12		tpfi 9299	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
14		pire 26699	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
15	14	renegcli 11547	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
16	15	rexri 11295	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
17	14	rexri 11295	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
18		negpilt0 46122	. . . . . . . . . . . . . . 15 ⊢ -π < 0
19		pipos 26703	. . . . . . . . . . . . . . 15 ⊢ 0 < π
20		0re 11238	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
21	15, 20, 14	lttri 11364	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
22	18, 19, 21	mp2an 705	. . . . . . . . . . . . . 14 ⊢ -π < π
23	15, 14, 22	ltleii 11361	. . . . . . . . . . . . 13 ⊢ -π ≤ π
24		prunioo 13538	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
25	16, 17, 23, 24	mp3an 1490	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
26	25	difeq1i 4073	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
27		difundir 4240	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
28	26, 27	eqtr3i 2787	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
29		fourierdlem114.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
30		prfi 9297	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
31		diffi 9173	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
32	30, 31	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
33		unfi 9169	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
34	29, 32, 33	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
35	28, 34	eqeltrid 2866	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
36		unfi 9169	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
37	13, 35, 36	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
38	11, 37	eqeltrid 2866	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
39		hashcl 14424	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
40	38, 39	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
41	40	nn0zd 12644	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
42	15, 22	ltneii 11351	. . . . . . 7 ⊢ -π ≠ π
43		hashprg 14463	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
44	15, 14, 43	mp2an 705	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
45	42, 44	mpbi 233	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
46	12	elexi 3475	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
47		ovex 7450	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
48		difexg 5298	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
50	46, 49	unex 7750	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
51	11, 50	eqeltri 2858	. . . . . . . 8 ⊢ 𝐻 ∈ V
52		negex 11483	. . . . . . . . . . 11 ⊢ -π ∈ V
53	52	tpid1 4732	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
54	14	elexi 3475	. . . . . . . . . . 11 ⊢ π ∈ V
55	54	tpid2 4734	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
56		prssi 4785	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
57	53, 55, 56	mp2an 705	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
58		ssun1 4127	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
59	58, 11	sseqtrri 3983	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
60	57, 59	sstri 3943	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
61		hashss 14477	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	51, 60, 61	mp2an 705	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
64	45, 63	eqbrtrrid 5145	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
65		eluz2 12897	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
66	10, 41, 64, 65	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
67		uz2m1nn 12976	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
68	66, 67	syl 18	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
69	8, 68	eqeltrid 2866	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
71	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
72		negpitopissre 26785	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
73	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
74		picn 26701	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
75	74	2timesi 12406	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
76	74, 74	subnegi 11565	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
77	75, 2, 76	3eqtr4i 2795	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
78		fourierdlem114.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
79	70, 71, 73, 77, 78	fourierdlem4 46947	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
80	79, 4	ffvelcdmd 7082	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
81	72, 80	sselid 3932	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
82	70, 71, 81	3jca 1146	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
83		fvex 6895	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
84	52, 54, 83	tpss 4800	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
85	82, 84	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
86		iccssre 13486	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
87	15, 14, 86	mp2an 705	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
88		ssdifss 4090	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
89	87, 88	mp1i 14	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
90	85, 89	unssd 4141	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
91	11, 90	eqsstrid 3972	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
92		fourierdlem114.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
93	38, 91, 92, 8	fourierdlem36 46979	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
94		isof1o 7328	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
95		f1of 6821	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
96	93, 94, 95	3syl 19	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
97	96, 91	fssd 6724	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
98		reex 11219	. . . . 5 ⊢ ℝ ∈ V
99		ovex 7450	. . . . 5 ⊢ (0...𝑀) ∈ V
100	98, 99	elmap 8882	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
101	97, 100	sylibr 237	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
102		fveq2 6882	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
103	102	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
104	97	ffvelcdmda 7081	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
105	104	leidd 11808	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
106	105	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
107	103, 106	eqbrtrd 5131	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
108		elfzelz 13582	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
109	108	zred 12729	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
110	109	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
111		elfzle1 13585	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
112	111	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
113		neqne 2965	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
114	113	necomd 3012	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
115	114	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
116	110, 112, 115	ne0gt0d 11375	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
117		nnssnn0 12535	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
118		nn0uz 12929	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
119	117, 118	sseqtri 3982	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
120	119, 69	sselid 3932	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
121		eluzfz1 13589	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
122	120, 121	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
123	96, 122	ffvelcdmd 7082	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
124	91, 123	sseldd 3935	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
125	124	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ)
126	104	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ)
127		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖)
128	93	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
129	122	anim1i 627	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
130	129	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
131		isorel 7331	. . . . . . . . . . . . 13 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
132	128, 130, 131	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
133	127, 132	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖))
134	125, 126, 133	ltled 11386	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	116, 134	syldan 603	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
136	107, 135	pm2.61dan 825	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
137	136	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
138		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
139	137, 138	breqtrd 5135	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
140	70	rexrd 11287	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
141	71	rexrd 11287	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
142		lbicc2 13521	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
143	16, 17, 23, 142	mp3an 1490	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
144	143	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
145		ubicc2 13522	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
146	16, 17, 23, 145	mp3an 1490	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
148		iocssicc 13494	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
149	148, 80	sselid 3932	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
150		tpssi 4801	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
151	144, 147, 149, 150	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
152		difssd 4087	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
153	151, 152	unssd 4141	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
154	11, 153	eqsstrid 3972	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
155	154, 123	sseldd 3935	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
156		iccgelb 13459	. . . . . . . 8 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘0) ∈ (-π[,]π)) → -π ≤ (𝑄‘0))
157	140, 141, 155, 156	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → -π ≤ (𝑄‘0))
158	157	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0))
159	124	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ)
160	15	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈ ℝ)
161	159, 160	letri3d 11380	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
162	139, 158, 161	mpbir2and 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
163	59, 53	sselii 3931	. . . . . . 7 ⊢ -π ∈ 𝐻
164		f1ofo 6829	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
165	94, 164	syl 18	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
166		forn 6796	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
167	93, 165, 166	3syl 19	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
168	163, 167	eleqtrrid 2869	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
169		ffn 6706	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
170		fvelrnb 6942	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
171	96, 169, 170	3syl 19	. . . . . 6 ⊢ (𝜑 → (-π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
172	168, 171	mpbid 235	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)
173	162, 172	r19.29a 3172	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
174	59, 55	sselii 3931	. . . . . . 7 ⊢ π ∈ 𝐻
175	174, 167	eleqtrrid 2869	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
176		fvelrnb 6942	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
177	96, 169, 176	3syl 19	. . . . . 6 ⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
178	175, 177	mpbid 235	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)
179	96, 154	fssd 6724	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
180		eluzfz2 13590	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
181	120, 180	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
182	179, 181	ffvelcdmd 7082	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
183		iccleub 13458	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
184	140, 141, 182, 183	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
185	184	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
186		id 23	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
187	186	eqcomd 2768	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
188	187	3ad2ant3 1153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
189	105	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
190		fveq2 6882	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
191	190	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
192	189, 191	breqtrd 5135	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
193	109	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
194		elfzel2 13580	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
195	194	zred 12729	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
196	195	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
197		elfzle2 13586	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
198	197	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
199		neqne 2965	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
200	199	necomd 3012	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
201	200	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
202	193, 196, 198, 201	leneltd 11392	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
203	104	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
204	87, 182	sselid 3932	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
205	204	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ)
206		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀)
207	93	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
208		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
209	181	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀))
210	208, 209	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
211	210	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
212		isorel 7331	. . . . . . . . . . . . . 14 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
213	207, 211, 212	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
214	206, 213	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀))
215	203, 205, 214	ltled 11386	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	202, 215	syldan 603	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	192, 216	pm2.61dan 825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
218	217	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
219	188, 218	eqbrtrd 5131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
220	204	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
221	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
222	220, 221	letri3d 11380	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
223	185, 219, 222	mpbir2and 726	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
224	223	rexlimdv3a 3169	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
225	178, 224	mpd 16	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
226		elfzoelz 13718	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
227	226	zred 12729	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
228	227	ltp1d 12173	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
229	228	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
230		elfzofz 13735	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
231		fzofzp1 13824	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
232	230, 231	jca 521	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
233		isorel 7331	. . . . . . 7 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
234	93, 232, 233	syl2an 608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
235	229, 234	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
236	235	ralrimiva 3156	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
237	173, 225, 236	jca31 524	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
238	7	fourierdlem2 46945	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
239	69, 238	syl 18	. . 3 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
240	101, 237, 239	mpbir2and 726	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
241		fourierdlem114.g	. . . . 5 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ (-π(,)π))
242	241	reseq1i 5972	. . . 4 ⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
243	16	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
244	17	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
245	179	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
246		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
247	243, 244, 245, 246	fourierdlem27 46970	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
248	247	resabs1d 6005	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
249	242, 248	eqtr2id 2810	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250		fourierdlem114.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
251	250, 7, 69, 240, 11, 167	fourierdlem38 46981	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
252	249, 251	eqeltrd 2862	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
253	249	oveq1d 7432	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
254	250	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ))
255		fourierdlem114.rlim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
256	255	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
257		fourierdlem114.llim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
258	257	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((-π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
259	93	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
260	259, 94, 95	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻)
261	81	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
262	259, 165, 166	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻)
263	254, 256, 258, 259, 260, 246, 235, 247, 261, 11, 262	fourierdlem46 46988	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
264	263	simpld 500	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
265	253, 264	eqnetrd 3024	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
266	249	oveq1d 7432	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
267	263	simprd 501	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
268	266, 267	eqnetrd 3024	. 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 4737	. . . . 5 ⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)}
273		elun1 4131	. . . . 5 ⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
274	272, 273	mp1i 14	. . . 4 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
275	274, 11	eleqtrrdi 2873	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻)
276	275, 167	eleqtrrd 2865	. 2 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
277	1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276	fourierdlem113 47055	1 ⊢ (𝜑 → (seq1( + , 𝑆) ⇝ (((𝐿 + 𝑅) / 2) − ((𝐴‘0) / 2)) ∧ (((𝐴‘0) / 2) + Σ𝑛 ∈ ℕ (((𝐴‘𝑛) · (cos‘(𝑛 · 𝑋))) + ((𝐵‘𝑛) · (sin‘(𝑛 · 𝑋))))) = ((𝐿 + 𝑅) / 2)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2957 ∀wral 3078 ∃wrex 3088 {crab 3414 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 ∅c0 4282 {cpr 4589 {ctp 4591 class class class wbr 5107 ↦ cmpt 5190 dom cdm 5659 ran crn 5660 ↾ cres 5661 ℩cio 6491 Fn wfn 6532 ⟶wf 6533 –onto→wfo 6535 –1-1-onto→wf1o 6536 ‘cfv 6537 Isom wiso 6538 (class class class)co 7417 ↑_m cmap 8830 Fincfn 8956 ℂcc 11126 ℝcr 11127 0cc0 11128 1c1 11129 + caddc 11131 · cmul 11133 +∞cpnf 11268 -∞cmnf 11269 ℝ^*cxr 11270 < clt 11271 ≤ cle 11272 − cmin 11469 -cneg 11470 / cdiv 11899 ℕcn 12261 2c2 12323 ℕ₀cn0 12532 ℤcz 12619 ℤ_≥cuz 12891 (,)cioo 13402 (,]cioc 13403 [,)cico 13404 [,]cicc 13405 ...cfz 13565 ..^cfzo 13713 ⌊cfl 13855 seqcseq 14069 ♯chash 14398 ⇝ cli 15575 Σcsu 15777 sincsin 16155 cosccos 16156 πcpi 16158 –cn→ccncf 25110 ∫citg 25852 lim_ℂ climc 26096 D cdv 26097

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-rep 5236 ax-sep 5255 ax-nul 5267 ax-pow 5334 ax-pr 5402 ax-un 7740 ax-inf2 9624 ax-cc 10441 ax-cnex 11184 ax-resscn 11185 ax-1cn 11186 ax-icn 11187 ax-addcl 11188 ax-addrcl 11189 ax-mulcl 11190 ax-mulrcl 11191 ax-mulcom 11192 ax-addass 11193 ax-mulass 11194 ax-distr 11195 ax-i2m1 11196 ax-1ne0 11197 ax-1rid 11198 ax-rnegex 11199 ax-rrecex 11200 ax-cnre 11201 ax-pre-lttri 11202 ax-pre-lttrn 11203 ax-pre-ltadd 11204 ax-pre-mulgt0 11205 ax-pre-sup 11206 ax-addf 11207

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-symdif 4202 df-nul 4283 df-if 4486 df-pw 4562 df-sn 4588 df-pr 4590 df-tp 4592 df-op 4594 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-disj 5075 df-br 5108 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-se 5613 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7374 df-ov 7420 df-oprab 7421 df-mpo 7422 df-of 7682 df-ofr 7683 df-om 7867 df-1st 7990 df-2nd 7991 df-supp 8163 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-oadd 8463 df-omul 8464 df-er 8700 df-map 8832 df-pm 8833 df-ixp 8909 df-en 8957 df-dom 8958 df-sdom 8959 df-fin 8960 df-fsupp 9336 df-fi 9385 df-sup 9416 df-inf 9417 df-oi 9486 df-dju 9910 df-card 9948 df-acn 9951 df-pnf 11273 df-mnf 11274 df-xr 11275 df-ltxr 11276 df-le 11277 df-sub 11471 df-neg 11472 df-div 11900 df-nn 12262 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-7 12336 df-8 12337 df-9 12338 df-n0 12533 df-xnn0 12606 df-z 12620 df-dec 12741 df-uz 12892 df-q 13002 df-rp 13047 df-xneg 13167 df-xadd 13168 df-xmul 13169 df-ioo 13406 df-ioc 13407 df-ico 13408 df-icc 13409 df-fz 13566 df-fzo 13714 df-fl 13857 df-mod 13935 df-seq 14070 df-exp 14130 df-fac 14342 df-bc 14371 df-hash 14399 df-shft 15144 df-cj 15190 df-re 15191 df-im 15192 df-sqrt 15326 df-abs 15327 df-limsup 15562 df-clim 15579 df-rlim 15580 df-sum 15778 df-ef 16159 df-sin 16161 df-cos 16162 df-pi 16164 df-struct 17245 df-sets 17262 df-slot 17280 df-ndx 17292 df-base 17308 df-ress 17329 df-plusg 17361 df-mulr 17362 df-starv 17363 df-sca 17364 df-vsca 17365 df-ip 17366 df-tset 17367 df-ple 17368 df-ds 17370 df-unif 17371 df-hom 17372 df-cco 17373 df-rest 17513 df-topn 17514 df-0g 17532 df-gsum 17533 df-topgen 17534 df-pt 17535 df-prds 17538 df-xrs 17594 df-qtop 17599 df-imas 17600 df-xps 17602 df-mre 17676 df-mrc 17677 df-acs 17679 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-submnd 18898 df-mulg 19197 df-cntz 19450 df-cmn 19915 df-psmet 21583 df-xmet 21584 df-met 21585 df-bl 21586 df-mopn 21587 df-fbas 21588 df-fg 21589 df-cnfld 21592 df-top 23125 df-topon 23142 df-topsp 23164 df-bases 23177 df-cld 23250 df-ntr 23251 df-cls 23252 df-nei 23329 df-lp 23367 df-perf 23368 df-cn 23458 df-cnp 23459 df-t1 23545 df-haus 23546 df-cmp 23618 df-tx 23794 df-hmeo 23987 df-fil 24078 df-fm 24170 df-flim 24171 df-flf 24172 df-xms 24552 df-ms 24553 df-tms 24554 df-cncf 25112 df-ovol 25698 df-vol 25699 df-mbf 25853 df-itg1 25854 df-itg2 25855 df-ibl 25856 df-itg 25857 df-0p 25904 df-ditg 26081 df-limc 26100 df-dv 26101

This theorem is used by: fourierdlem115 47057

W3C validator