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 46974

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 12644	. . . . . 6 ⊢ 2 ∈ ℤ
10	9	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
11		fourierdlem114.h	. . . . . . . 8 ⊢ 𝐻 = ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
12		tpfi 9295	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ Fin
13	12	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ∈ Fin)
14		pire 26656	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
15	14	renegcli 11537	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
16	15	rexri 11285	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
17	14	rexri 11285	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
18		negpilt0 46040	. . . . . . . . . . . . . . 15 ⊢ -π < 0
19		pipos 26660	. . . . . . . . . . . . . . 15 ⊢ 0 < π
20		0re 11228	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
21	15, 20, 14	lttri 11354	. . . . . . . . . . . . . . 15 ⊢ ((-π < 0 ∧ 0 < π) → -π < π)
22	18, 19, 21	mp2an 705	. . . . . . . . . . . . . 14 ⊢ -π < π
23	15, 14, 22	ltleii 11351	. . . . . . . . . . . . 13 ⊢ -π ≤ π
24		prunioo 13526	. . . . . . . . . . . . 13 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → ((-π(,)π) ∪ {-π, π}) = (-π[,]π))
25	16, 17, 23, 24	mp3an 1490	. . . . . . . . . . . 12 ⊢ ((-π(,)π) ∪ {-π, π}) = (-π[,]π)
26	25	difeq1i 4080	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = ((-π[,]π) ∖ dom 𝐺)
27		difundir 4247	. . . . . . . . . . 11 ⊢ (((-π(,)π) ∪ {-π, π}) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
28	26, 27	eqtr3i 2791	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) = (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺))
29		fourierdlem114.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π(,)π) ∖ dom 𝐺) ∈ Fin)
30		prfi 9293	. . . . . . . . . . . 12 ⊢ {-π, π} ∈ Fin
31		diffi 9169	. . . . . . . . . . . 12 ⊢ ({-π, π} ∈ Fin → ({-π, π} ∖ dom 𝐺) ∈ Fin)
32	30, 31	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → ({-π, π} ∖ dom 𝐺) ∈ Fin)
33		unfi 9165	. . . . . . . . . . 11 ⊢ ((((-π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({-π, π} ∖ dom 𝐺) ∈ Fin) → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
34	29, 32, 33	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → (((-π(,)π) ∖ dom 𝐺) ∪ ({-π, π} ∖ dom 𝐺)) ∈ Fin)
35	28, 34	eqeltrid 2870	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ∈ Fin)
36		unfi 9165	. . . . . . . . 9 ⊢ (({-π, π, (𝐸‘𝑋)} ∈ Fin ∧ ((-π[,]π) ∖ dom 𝐺) ∈ Fin) → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
37	13, 35, 36	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ Fin)
38	11, 37	eqeltrid 2870	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
39		hashcl 14412	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
40	38, 39	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
41	40	nn0zd 12634	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
42	15, 22	ltneii 11341	. . . . . . 7 ⊢ -π ≠ π
43		hashprg 14451	. . . . . . . 8 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π ≠ π ↔ (♯‘{-π, π}) = 2))
44	15, 14, 43	mp2an 705	. . . . . . 7 ⊢ (-π ≠ π ↔ (♯‘{-π, π}) = 2)
45	42, 44	mpbi 233	. . . . . 6 ⊢ (♯‘{-π, π}) = 2
46	12	elexi 3480	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ∈ V
47		ovex 7456	. . . . . . . . . . 11 ⊢ (-π[,]π) ∈ V
48		difexg 5305	. . . . . . . . . . 11 ⊢ ((-π[,]π) ∈ V → ((-π[,]π) ∖ dom 𝐺) ∈ V)
49	47, 48	ax-mp 5	. . . . . . . . . 10 ⊢ ((-π[,]π) ∖ dom 𝐺) ∈ V
50	46, 49	unex 7755	. . . . . . . . 9 ⊢ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ∈ V
51	11, 50	eqeltri 2862	. . . . . . . 8 ⊢ 𝐻 ∈ V
52		negex 11473	. . . . . . . . . . 11 ⊢ -π ∈ V
53	52	tpid1 4739	. . . . . . . . . 10 ⊢ -π ∈ {-π, π, (𝐸‘𝑋)}
54	14	elexi 3480	. . . . . . . . . . 11 ⊢ π ∈ V
55	54	tpid2 4741	. . . . . . . . . 10 ⊢ π ∈ {-π, π, (𝐸‘𝑋)}
56		prssi 4792	. . . . . . . . . 10 ⊢ ((-π ∈ {-π, π, (𝐸‘𝑋)} ∧ π ∈ {-π, π, (𝐸‘𝑋)}) → {-π, π} ⊆ {-π, π, (𝐸‘𝑋)})
57	53, 55, 56	mp2an 705	. . . . . . . . 9 ⊢ {-π, π} ⊆ {-π, π, (𝐸‘𝑋)}
58		ssun1 4134	. . . . . . . . . 10 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺))
59	58, 11	sseqtrri 3989	. . . . . . . . 9 ⊢ {-π, π, (𝐸‘𝑋)} ⊆ 𝐻
60	57, 59	sstri 3949	. . . . . . . 8 ⊢ {-π, π} ⊆ 𝐻
61		hashss 14465	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ {-π, π} ⊆ 𝐻) → (♯‘{-π, π}) ≤ (♯‘𝐻))
62	51, 60, 61	mp2an 705	. . . . . . 7 ⊢ (♯‘{-π, π}) ≤ (♯‘𝐻)
63	62	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{-π, π}) ≤ (♯‘𝐻))
64	45, 63	eqbrtrrid 5152	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
65		eluz2 12886	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
66	10, 41, 64, 65	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
67		uz2m1nn 12965	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
68	66, 67	syl 18	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
69	8, 68	eqeltrid 2870	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
70	15	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
71	14	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
72		negpitopissre 26742	. . . . . . . . . . . 12 ⊢ (-π(,]π) ⊆ ℝ
73	22	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
74		picn 26658	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
75	74	2timesi 12396	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
76	74, 74	subnegi 11555	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
77	75, 2, 76	3eqtr4i 2799	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
78		fourierdlem114.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
79	70, 71, 73, 77, 78	fourierdlem4 46865	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶(-π(,]π))
80	79, 4	ffvelcdmd 7087	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π(,]π))
81	72, 80	sselid 3938	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
82	70, 71, 81	3jca 1146	. . . . . . . . . 10 ⊢ (𝜑 → (-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
83		fvex 6901	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
84	52, 54, 83	tpss 4807	. . . . . . . . . 10 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
85	82, 84	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ ℝ)
86		iccssre 13474	. . . . . . . . . . 11 ⊢ ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
87	15, 14, 86	mp2an 705	. . . . . . . . . 10 ⊢ (-π[,]π) ⊆ ℝ
88		ssdifss 4097	. . . . . . . . . 10 ⊢ ((-π[,]π) ⊆ ℝ → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
89	87, 88	mp1i 14	. . . . . . . . 9 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ ℝ)
90	85, 89	unssd 4148	. . . . . . . 8 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
91	11, 90	eqsstrid 3978	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
92		fourierdlem114.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
93	38, 91, 92, 8	fourierdlem36 46897	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
94		isof1o 7332	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–1-1-onto→𝐻)
95		f1of 6827	. . . . . 6 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)⟶𝐻)
96	93, 94, 95	3syl 19	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
97	96, 91	fssd 6730	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
98		reex 11209	. . . . 5 ⊢ ℝ ∈ V
99		ovex 7456	. . . . 5 ⊢ (0...𝑀) ∈ V
100	98, 99	elmap 8878	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
101	97, 100	sylibr 237	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
102		fveq2 6888	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
103	102	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
104	97	ffvelcdmda 7086	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
105	104	leidd 11798	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
106	105	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
107	103, 106	eqbrtrd 5138	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
108		elfzelz 13570	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
109	108	zred 12718	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
110	109	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
111		elfzle1 13573	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
112	111	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
113		neqne 2969	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
114	113	necomd 3016	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
115	114	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
116	110, 112, 115	ne0gt0d 11365	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
117		nnssnn0 12525	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
118		nn0uz 12918	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
119	117, 118	sseqtri 3988	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
120	119, 69	sselid 3938	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
121		eluzfz1 13577	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
122	120, 121	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
123	96, 122	ffvelcdmd 7087	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
124	91, 123	sseldd 3941	. . . . . . . . . . . 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 7335	. . . . . . . . . . . . 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 11376	. . . . . . . . . 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 5142	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
140	70	rexrd 11277	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
141	71	rexrd 11277	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
142		lbicc2 13509	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ (-π[,]π))
143	16, 17, 23, 142	mp3an 1490	. . . . . . . . . . . . 13 ⊢ -π ∈ (-π[,]π)
144	143	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ (-π[,]π))
145		ubicc2 13510	. . . . . . . . . . . . . 14 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ (-π[,]π))
146	16, 17, 23, 145	mp3an 1490	. . . . . . . . . . . . 13 ⊢ π ∈ (-π[,]π)
147	146	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ (-π[,]π))
148		iocssicc 13482	. . . . . . . . . . . . 13 ⊢ (-π(,]π) ⊆ (-π[,]π)
149	148, 80	sselid 3938	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ (-π[,]π))
150		tpssi 4808	. . . . . . . . . . . 12 ⊢ ((-π ∈ (-π[,]π) ∧ π ∈ (-π[,]π) ∧ (𝐸‘𝑋) ∈ (-π[,]π)) → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
151	144, 147, 149, 150	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → {-π, π, (𝐸‘𝑋)} ⊆ (-π[,]π))
152		difssd 4094	. . . . . . . . . . 11 ⊢ (𝜑 → ((-π[,]π) ∖ dom 𝐺) ⊆ (-π[,]π))
153	151, 152	unssd 4148	. . . . . . . . . 10 ⊢ (𝜑 → ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)) ⊆ (-π[,]π))
154	11, 153	eqsstrid 3978	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ (-π[,]π))
155	154, 123	sseldd 3941	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ (-π[,]π))
156		iccgelb 13447	. . . . . . . 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 11370	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
162	139, 158, 161	mpbir2and 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
163	59, 53	sselii 3937	. . . . . . 7 ⊢ -π ∈ 𝐻
164		f1ofo 6835	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)–1-1-onto→𝐻 → 𝑄:(0...𝑀)–onto→𝐻)
165	94, 164	syl 18	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)–onto→𝐻)
166		forn 6802	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)–onto→𝐻 → ran 𝑄 = 𝐻)
167	93, 165, 166	3syl 19	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
168	163, 167	eleqtrrid 2873	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
169		ffn 6712	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
170		fvelrnb 6948	. . . . . . 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 3176	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
174	59, 55	sselii 3937	. . . . . . 7 ⊢ π ∈ 𝐻
175	174, 167	eleqtrrid 2873	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
176		fvelrnb 6948	. . . . . . 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 6730	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶(-π[,]π))
180		eluzfz2 13578	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
181	120, 180	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
182	179, 181	ffvelcdmd 7087	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ (-π[,]π))
183		iccleub 13446	. . . . . . . . 9 ⊢ ((-π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ (-π[,]π)) → (𝑄‘𝑀) ≤ π)
184	140, 141, 182, 183	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
185	184	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
186		id 23	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
187	186	eqcomd 2772	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
188	187	3ad2ant3 1153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
189	105	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
190		fveq2 6888	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
191	190	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
192	189, 191	breqtrd 5142	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
193	109	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
194		elfzel2 13568	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
195	194	zred 12718	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
196	195	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
197		elfzle2 13574	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
198	197	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
199		neqne 2969	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
200	199	necomd 3016	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
201	200	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
202	193, 196, 198, 201	leneltd 11382	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
203	104	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
204	87, 182	sselid 3938	. . . . . . . . . . . . 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 7335	. . . . . . . . . . . . . 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 11376	. . . . . . . . . . 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 5138	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
220	204	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
221	14	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
222	220, 221	letri3d 11370	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
223	185, 219, 222	mpbir2and 726	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
224	223	rexlimdv3a 3173	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
225	178, 224	mpd 16	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
226		elfzoelz 13706	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
227	226	zred 12718	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
228	227	ltp1d 12163	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
229	228	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
230		elfzofz 13723	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
231		fzofzp1 13812	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
232	230, 231	jca 521	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
233		isorel 7335	. . . . . . 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 3160	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
237	173, 225, 236	jca31 524	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
238	7	fourierdlem2 46863	. . . 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 5979	. . . 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 46888	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π(,)π))
248	247	resabs1d 6012	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ (-π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
249	242, 248	eqtr2id 2814	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
250		fourierdlem114.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
251	250, 7, 69, 240, 11, 167	fourierdlem38 46899	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
252	249, 251	eqeltrd 2866	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
253	249	oveq1d 7438	. . 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 46906	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
264	263	simpld 500	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
265	253, 264	eqnetrd 3028	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
266	249	oveq1d 7438	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
267	263	simprd 501	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
268	266, 267	eqnetrd 3028	. 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 4744	. . . . 5 ⊢ (𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)}
273		elun1 4138	. . . . 5 ⊢ ((𝐸‘𝑋) ∈ {-π, π, (𝐸‘𝑋)} → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
274	272, 273	mp1i 14	. . . 4 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ({-π, π, (𝐸‘𝑋)} ∪ ((-π[,]π) ∖ dom 𝐺)))
275	274, 11	eleqtrrdi 2877	. . 3 ⊢ (𝜑 → (𝐸‘𝑋) ∈ 𝐻)
276	275, 167	eleqtrrd 2869	. 2 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ran 𝑄)
277	1, 2, 3, 4, 5, 6, 7, 69, 240, 252, 265, 268, 269, 270, 271, 78, 276	fourierdlem113 46973	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 2146 ≠ wne 2961 ∀wral 3082 ∃wrex 3092 {crab 3419 Vcvv 3458 ∖ cdif 3905 ∪ cun 3906 ⊆ wss 3908 ∅c0 4289 {cpr 4596 {ctp 4598 class class class wbr 5114 ↦ cmpt 5197 dom cdm 5666 ran crn 5667 ↾ cres 5668 ℩cio 6497 Fn wfn 6538 ⟶wf 6539 –onto→wfo 6541 –1-1-onto→wf1o 6542 ‘cfv 6543 Isom wiso 6544 (class class class)co 7423 ↑_m cmap 8833 Fincfn 8952 ℂcc 11116 ℝcr 11117 0cc0 11118 1c1 11119 + caddc 11121 · cmul 11123 +∞cpnf 11258 -∞cmnf 11259 ℝ^*cxr 11260 < clt 11261 ≤ cle 11262 − cmin 11459 -cneg 11460 / cdiv 11889 ℕcn 12251 2c2 12313 ℕ₀cn0 12522 ℤcz 12609 ℤ_≥cuz 12880 (,)cioo 13390 (,]cioc 13391 [,)cico 13392 [,]cicc 13393 ...cfz 13553 ..^cfzo 13701 ⌊cfl 13843 seqcseq 14057 ♯chash 14386 ⇝ cli 15561 Σcsu 15763 sincsin 16142 cosccos 16143 πcpi 16145 –cn→ccncf 25072 ∫citg 25814 lim_ℂ climc 26058 D cdv 26059

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 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745 ax-inf2 9620 ax-cc 10437 ax-cnex 11174 ax-resscn 11175 ax-1cn 11176 ax-icn 11177 ax-addcl 11178 ax-addrcl 11179 ax-mulcl 11180 ax-mulrcl 11181 ax-mulcom 11182 ax-addass 11183 ax-mulass 11184 ax-distr 11185 ax-i2m1 11186 ax-1ne0 11187 ax-1rid 11188 ax-rnegex 11189 ax-rrecex 11190 ax-cnre 11191 ax-pre-lttri 11192 ax-pre-lttrn 11193 ax-pre-ltadd 11194 ax-pre-mulgt0 11195 ax-pre-sup 11196 ax-addf 11197

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 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-nel 3068 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-pss 3928 df-symdif 4209 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4878 df-int 4918 df-iun 4963 df-iin 4964 df-disj 5082 df-br 5115 df-opab 5179 df-mpt 5198 df-tr 5224 df-id 5561 df-eprel 5566 df-po 5574 df-so 5575 df-fr 5619 df-se 5620 df-we 5621 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-ord 6370 df-on 6371 df-lim 6372 df-suc 6373 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7380 df-ov 7426 df-oprab 7427 df-mpo 7428 df-of 7687 df-ofr 7688 df-om 7872 df-1st 7995 df-2nd 7996 df-supp 8166 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-1o 8462 df-2o 8463 df-oadd 8466 df-omul 8467 df-er 8703 df-map 8835 df-pm 8836 df-ixp 8905 df-en 8953 df-dom 8954 df-sdom 8955 df-fin 8956 df-fsupp 9332 df-fi 9381 df-sup 9412 df-inf 9413 df-oi 9482 df-dju 9906 df-card 9944 df-acn 9947 df-pnf 11263 df-mnf 11264 df-xr 11265 df-ltxr 11266 df-le 11267 df-sub 11461 df-neg 11462 df-div 11890 df-nn 12252 df-2 12321 df-3 12322 df-4 12323 df-5 12324 df-6 12325 df-7 12326 df-8 12327 df-9 12328 df-n0 12523 df-xnn0 12596 df-z 12610 df-dec 12730 df-uz 12881 df-q 12991 df-rp 13035 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13394 df-ioc 13395 df-ico 13396 df-icc 13397 df-fz 13554 df-fzo 13702 df-fl 13845 df-mod 13923 df-seq 14058 df-exp 14118 df-fac 14330 df-bc 14359 df-hash 14387 df-shft 15130 df-cj 15176 df-re 15177 df-im 15178 df-sqrt 15312 df-abs 15313 df-limsup 15548 df-clim 15565 df-rlim 15566 df-sum 15764 df-ef 16146 df-sin 16148 df-cos 16149 df-pi 16151 df-struct 17232 df-sets 17249 df-slot 17267 df-ndx 17279 df-base 17295 df-ress 17316 df-plusg 17348 df-mulr 17349 df-starv 17350 df-sca 17351 df-vsca 17352 df-ip 17353 df-tset 17354 df-ple 17355 df-ds 17357 df-unif 17358 df-hom 17359 df-cco 17360 df-rest 17500 df-topn 17501 df-0g 17519 df-gsum 17520 df-topgen 17521 df-pt 17522 df-prds 17525 df-xrs 17581 df-qtop 17586 df-imas 17587 df-xps 17589 df-mre 17663 df-mrc 17664 df-acs 17666 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-submnd 18873 df-mulg 19165 df-cntz 19418 df-cmn 19883 df-psmet 21551 df-xmet 21552 df-met 21553 df-bl 21554 df-mopn 21555 df-fbas 21556 df-fg 21557 df-cnfld 21560 df-top 23088 df-topon 23105 df-topsp 23127 df-bases 23140 df-cld 23213 df-ntr 23214 df-cls 23215 df-nei 23292 df-lp 23330 df-perf 23331 df-cn 23421 df-cnp 23422 df-t1 23508 df-haus 23509 df-cmp 23581 df-tx 23756 df-hmeo 23949 df-fil 24040 df-fm 24132 df-flim 24133 df-flf 24134 df-xms 24514 df-ms 24515 df-tms 24516 df-cncf 25074 df-ovol 25660 df-vol 25661 df-mbf 25815 df-itg1 25816 df-itg2 25817 df-ibl 25818 df-itg 25819 df-0p 25866 df-ditg 26043 df-limc 26062 df-dv 26063

This theorem is used by: fourierdlem115 46975

W3C validator