fourierdlem102 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem102 47485

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

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

**Assertion**
Ref	Expression
fourierdlem102	⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅))

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

**Proof of Theorem fourierdlem102**
Step	Hyp	Ref	Expression
1		fourierdlem102.f	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
2		fourierdlem102.t	. 2 ⊢ 𝑇 = (2 · π)
3		fourierdlem102.per	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
4		fourierdlem102.x	. 2 ⊢ (𝜑 → 𝑋 ∈ ℝ)
5		fourierdlem102.p	. 2 ⊢ 𝑃 = (𝑛 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑛)) ∣ (((𝑝‘0) = -π ∧ (𝑝‘𝑛) = π) ∧ ∀𝑖 ∈ (0..^𝑛)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
6		fourierdlem102.m	. . 3 ⊢ 𝑀 = ((♯‘𝐻) − 1)
7		2z 12766	. . . . . 6 ⊢ 2 ∈ ℤ
8	7	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℤ)
9		fourierdlem102.h	. . . . . . . 8 ⊢ 𝐻 = ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺))
10		tpfi 9353	. . . . . . . . . 10 ⊢ { -π, π, (𝐸‘𝑋)} ∈ Fin
11	10	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → { -π, π, (𝐸‘𝑋)} ∈ Fin)
12		pire 26829	. . . . . . . . . . . . . . 15 ⊢ π ∈ ℝ
13	12	renegcli 11656	. . . . . . . . . . . . . 14 ⊢ -π ∈ ℝ
14	13	rexri 11404	. . . . . . . . . . . . 13 ⊢ -π ∈ ℝ^*
15	12	rexri 11404	. . . . . . . . . . . . 13 ⊢ π ∈ ℝ^*
16		negpilt0 46564	. . . . . . . . . . . . . . 15 ⊢ -π < 0
17		pipos 26833	. . . . . . . . . . . . . . 15 ⊢ 0 < π
18		0re 11347	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ ℝ
19	13, 18, 12	lttri 11473	. . . . . . . . . . . . . . 15 ⊢ (( -π < 0 ∧ 0 < π) → -π < π)
20	16, 17, 19	mp2an 705	. . . . . . . . . . . . . 14 ⊢ -π < π
21	13, 12, 20	ltleii 11470	. . . . . . . . . . . . 13 ⊢ -π ≤ π
22		prunioo 13650	. . . . . . . . . . . . 13 ⊢ (( -π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → (( -π(,)π) ∪ { -π, π}) = ( -π[,]π))
23	14, 15, 21, 22	mp3an 1491	. . . . . . . . . . . 12 ⊢ (( -π(,)π) ∪ { -π, π}) = ( -π[,]π)
24	23	difeq1i 4062	. . . . . . . . . . 11 ⊢ ((( -π(,)π) ∪ { -π, π}) ∖ dom 𝐺) = (( -π[,]π) ∖ dom 𝐺)
25		difundir 4239	. . . . . . . . . . 11 ⊢ ((( -π(,)π) ∪ { -π, π}) ∖ dom 𝐺) = ((( -π(,)π) ∖ dom 𝐺) ∪ ({ -π, π} ∖ dom 𝐺))
26	24, 25	eqtr3i 2788	. . . . . . . . . 10 ⊢ (( -π[,]π) ∖ dom 𝐺) = ((( -π(,)π) ∖ dom 𝐺) ∪ ({ -π, π} ∖ dom 𝐺))
27		fourierdlem102.dmdv	. . . . . . . . . . 11 ⊢ (𝜑 → (( -π(,)π) ∖ dom 𝐺) ∈ Fin)
28		prfi 9351	. . . . . . . . . . . 12 ⊢ { -π, π} ∈ Fin
29		diffi 9226	. . . . . . . . . . . 12 ⊢ ({ -π, π} ∈ Fin → ({ -π, π} ∖ dom 𝐺) ∈ Fin)
30	28, 29	mp1i 14	. . . . . . . . . . 11 ⊢ (𝜑 → ({ -π, π} ∖ dom 𝐺) ∈ Fin)
31		unfi 9222	. . . . . . . . . . 11 ⊢ (((( -π(,)π) ∖ dom 𝐺) ∈ Fin ∧ ({ -π, π} ∖ dom 𝐺) ∈ Fin) → ((( -π(,)π) ∖ dom 𝐺) ∪ ({ -π, π} ∖ dom 𝐺)) ∈ Fin)
32	27, 30, 31	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((( -π(,)π) ∖ dom 𝐺) ∪ ({ -π, π} ∖ dom 𝐺)) ∈ Fin)
33	26, 32	eqeltrid 2868	. . . . . . . . 9 ⊢ (𝜑 → (( -π[,]π) ∖ dom 𝐺) ∈ Fin)
34		unfi 9222	. . . . . . . . 9 ⊢ (({ -π, π, (𝐸‘𝑋)} ∈ Fin ∧ (( -π[,]π) ∖ dom 𝐺) ∈ Fin) → ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺)) ∈ Fin)
35	11, 33, 34	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺)) ∈ Fin)
36	9, 35	eqeltrid 2868	. . . . . . 7 ⊢ (𝜑 → 𝐻 ∈ Fin)
37		hashcl 14539	. . . . . . 7 ⊢ (𝐻 ∈ Fin → (♯‘𝐻) ∈ ℕ₀)
38	36, 37	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘𝐻) ∈ ℕ₀)
39	38	nn0zd 12756	. . . . 5 ⊢ (𝜑 → (♯‘𝐻) ∈ ℤ)
40	13, 20	ltneii 11460	. . . . . . 7 ⊢ -π ≠ π
41		hashprg 14578	. . . . . . . 8 ⊢ (( -π ∈ ℝ ∧ π ∈ ℝ) → ( -π ≠ π ↔ (♯‘{ -π, π}) = 2))
42	13, 12, 41	mp2an 705	. . . . . . 7 ⊢ ( -π ≠ π ↔ (♯‘{ -π, π}) = 2)
43	40, 42	mpbi 233	. . . . . 6 ⊢ (♯‘{ -π, π}) = 2
44	10	elexi 3476	. . . . . . . . . 10 ⊢ { -π, π, (𝐸‘𝑋)} ∈ V
45		ovex 7482	. . . . . . . . . . 11 ⊢ ( -π[,]π) ∈ V
46		difexg 5296	. . . . . . . . . . 11 ⊢ (( -π[,]π) ∈ V → (( -π[,]π) ∖ dom 𝐺) ∈ V)
47	45, 46	ax-mp 5	. . . . . . . . . 10 ⊢ (( -π[,]π) ∖ dom 𝐺) ∈ V
48	44, 47	unex 7791	. . . . . . . . 9 ⊢ ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺)) ∈ V
49	9, 48	eqeltri 2860	. . . . . . . 8 ⊢ 𝐻 ∈ V
50		negex 11592	. . . . . . . . . . 11 ⊢ -π ∈ V
51	50	tpid1 4729	. . . . . . . . . 10 ⊢ -π ∈ { -π, π, (𝐸‘𝑋)}
52	12	elexi 3476	. . . . . . . . . . 11 ⊢ π ∈ V
53	52	tpid2 4731	. . . . . . . . . 10 ⊢ π ∈ { -π, π, (𝐸‘𝑋)}
54		prssi 4780	. . . . . . . . . 10 ⊢ (( -π ∈ { -π, π, (𝐸‘𝑋)} ∧ π ∈ { -π, π, (𝐸‘𝑋)}) → { -π, π} ⊆ { -π, π, (𝐸‘𝑋)})
55	51, 53, 54	mp2an 705	. . . . . . . . 9 ⊢ { -π, π} ⊆ { -π, π, (𝐸‘𝑋)}
56		ssun1 4179	. . . . . . . . . 10 ⊢ { -π, π, (𝐸‘𝑋)} ⊆ ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺))
57	56, 9	sseqtrri 3962	. . . . . . . . 9 ⊢ { -π, π, (𝐸‘𝑋)} ⊆ 𝐻
58	55, 57	sstri 3922	. . . . . . . 8 ⊢ { -π, π} ⊆ 𝐻
59		hashss 14592	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ { -π, π} ⊆ 𝐻) → (♯‘{ -π, π}) ≤ (♯‘𝐻))
60	49, 58, 59	mp2an 705	. . . . . . 7 ⊢ (♯‘{ -π, π}) ≤ (♯‘𝐻)
61	60	a1i 11	. . . . . 6 ⊢ (𝜑 → (♯‘{ -π, π}) ≤ (♯‘𝐻))
62	43, 61	eqbrtrrid 5145	. . . . 5 ⊢ (𝜑 → 2 ≤ (♯‘𝐻))
63		eluz2 13009	. . . . 5 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) ↔ (2 ∈ ℤ ∧ (♯‘𝐻) ∈ ℤ ∧ 2 ≤ (♯‘𝐻)))
64	8, 39, 62, 63	syl3anbrc 1362	. . . 4 ⊢ (𝜑 → (♯‘𝐻) ∈ (ℤ_≥‘2))
65		uz2m1nn 13088	. . . 4 ⊢ ((♯‘𝐻) ∈ (ℤ_≥‘2) → ((♯‘𝐻) − 1) ∈ ℕ)
66	64, 65	syl 18	. . 3 ⊢ (𝜑 → ((♯‘𝐻) − 1) ∈ ℕ)
67	6, 66	eqeltrid 2868	. 2 ⊢ (𝜑 → 𝑀 ∈ ℕ)
68	13	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → -π ∈ ℝ)
69	12	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → π ∈ ℝ)
70		negpitopissre 26914	. . . . . . . . . . . 12 ⊢ ( -π(,]π) ⊆ ℝ
71	20	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝜑 → -π < π)
72		picn 26831	. . . . . . . . . . . . . . . 16 ⊢ π ∈ ℂ
73	72	2timesi 12518	. . . . . . . . . . . . . . 15 ⊢ (2 · π) = (π + π)
74	72, 72	subnegi 11674	. . . . . . . . . . . . . . 15 ⊢ (π − -π) = (π + π)
75	73, 2, 74	3eqtr4i 2796	. . . . . . . . . . . . . 14 ⊢ 𝑇 = (π − -π)
76		fourierdlem102.e	. . . . . . . . . . . . . 14 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((π − 𝑥) / 𝑇)) · 𝑇)))
77	68, 69, 71, 75, 76	fourierdlem4 47388	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐸:ℝ⟶( -π(,]π))
78	77, 4	ffvelcdmd 7115	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ( -π(,]π))
79	70, 78	sselid 3911	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ℝ)
80	68, 69, 79	3jca 1146	. . . . . . . . . 10 ⊢ (𝜑 → ( -π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ))
81		fvex 6927	. . . . . . . . . . 11 ⊢ (𝐸‘𝑋) ∈ V
82	50, 52, 81	tpss 4795	. . . . . . . . . 10 ⊢ (( -π ∈ ℝ ∧ π ∈ ℝ ∧ (𝐸‘𝑋) ∈ ℝ) ↔ { -π, π, (𝐸‘𝑋)} ⊆ ℝ)
83	80, 82	sylib 221	. . . . . . . . 9 ⊢ (𝜑 → { -π, π, (𝐸‘𝑋)} ⊆ ℝ)
84		iccssre 13598	. . . . . . . . . . 11 ⊢ (( -π ∈ ℝ ∧ π ∈ ℝ) → ( -π[,]π) ⊆ ℝ)
85	13, 12, 84	mp2an 705	. . . . . . . . . 10 ⊢ ( -π[,]π) ⊆ ℝ
86		ssdifss 4079	. . . . . . . . . 10 ⊢ (( -π[,]π) ⊆ ℝ → (( -π[,]π) ∖ dom 𝐺) ⊆ ℝ)
87	85, 86	mp1i 14	. . . . . . . . 9 ⊢ (𝜑 → (( -π[,]π) ∖ dom 𝐺) ⊆ ℝ)
88	83, 87	unssd 4193	. . . . . . . 8 ⊢ (𝜑 → ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺)) ⊆ ℝ)
89	9, 88	eqsstrid 3951	. . . . . . 7 ⊢ (𝜑 → 𝐻 ⊆ ℝ)
90		fourierdlem102.q	. . . . . . 7 ⊢ 𝑄 = (℩𝑔𝑔 Isom < , < ((0...𝑀), 𝐻))
91	36, 89, 90, 6	fourierdlem36 47420	. . . . . 6 ⊢ (𝜑 → 𝑄 Isom < , < ((0...𝑀), 𝐻))
92		isof1o 7360	. . . . . 6 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)⟶1-1onto𝐻)
93		f1of 6852	. . . . . 6 ⊢ (𝑄:(0...𝑀)⟶1-1onto𝐻 → 𝑄:(0...𝑀)⟶𝐻)
94	91, 92, 93	3syl 19	. . . . 5 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶𝐻)
95	94, 89	fssd 6755	. . . 4 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
96		reex 11328	. . . . 5 ⊢ ℝ ∈ V
97		ovex 7482	. . . . 5 ⊢ (0...𝑀) ∈ V
98	96, 97	elmap 8935	. . . 4 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ)
99	95, 98	sylibr 237	. . 3 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
100		fveq2 6914	. . . . . . . . . . 11 ⊢ (0 = 𝑖 → (𝑄‘0) = (𝑄‘𝑖))
101	100	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) = (𝑄‘𝑖))
102	95	ffvelcdmda 7114	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
103	102	leidd 11920	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
104	103	adantr 486	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
105	101, 104	eqbrtrd 5131	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
106		elfzelz 13694	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℤ)
107	106	zred 12841	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ∈ ℝ)
108	107	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ∈ ℝ)
109		elfzle1 13698	. . . . . . . . . . . 12 ⊢ (𝑖 ∈ (0...𝑀) → 0 ≤ 𝑖)
110	109	ad2antlr 740	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 ≤ 𝑖)
111		neqne 2967	. . . . . . . . . . . . 13 ⊢ (¬ 0 = 𝑖 → 0 ≠ 𝑖)
112	111	necomd 3014	. . . . . . . . . . . 12 ⊢ (¬ 0 = 𝑖 → 𝑖 ≠ 0)
113	112	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 𝑖 ≠ 0)
114	108, 110, 113	ne0gt0d 11484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → 0 < 𝑖)
115		nnssnn0 12647	. . . . . . . . . . . . . . . . 17 ⊢ ℕ ⊆ ℕ₀
116		nn0uz 13041	. . . . . . . . . . . . . . . . 17 ⊢ ℕ₀ = (ℤ_≥‘0)
117	115, 116	sseqtri 3961	. . . . . . . . . . . . . . . 16 ⊢ ℕ ⊆ (ℤ_≥‘0)
118	117, 67	sselid 3911	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑀 ∈ (ℤ_≥‘0))
119		eluzfz1 13702	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 0 ∈ (0...𝑀))
120	118, 119	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 ∈ (0...𝑀))
121	94, 120	ffvelcdmd 7115	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘0) ∈ 𝐻)
122	89, 121	sseldd 3914	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄‘0) ∈ ℝ)
123	122	ad2antrr 739	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ∈ ℝ)
124	102	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘𝑖) ∈ ℝ)
125		simpr 490	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 0 < 𝑖)
126	91	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
127	120	anim1i 627	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
128	127	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀)))
129		isorel 7363	. . . . . . . . . . . . 13 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (0 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
130	126, 128, 129	syl2anc 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (0 < 𝑖 ↔ (𝑄‘0) < (𝑄‘𝑖)))
131	125, 130	mpbid 235	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) < (𝑄‘𝑖))
132	123, 124, 131	ltled 11495	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 0 < 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
133	114, 132	syldan 603	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 0 = 𝑖) → (𝑄‘0) ≤ (𝑄‘𝑖))
134	105, 133	pm2.61dan 825	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘0) ≤ (𝑄‘𝑖))
135	134	adantr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ (𝑄‘𝑖))
136		simpr 490	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘𝑖) = -π)
137	135, 136	breqtrd 5135	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ≤ -π)
138	68	rexrd 11396	. . . . . . . 8 ⊢ (𝜑 → -π ∈ ℝ^*)
139	69	rexrd 11396	. . . . . . . 8 ⊢ (𝜑 → π ∈ ℝ^*)
140		lbicc2 13633	. . . . . . . . . . . . . 14 ⊢ (( -π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → -π ∈ ( -π[,]π))
141	14, 15, 21, 140	mp3an 1491	. . . . . . . . . . . . 13 ⊢ -π ∈ ( -π[,]π)
142	141	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → -π ∈ ( -π[,]π))
143		ubicc2 13634	. . . . . . . . . . . . . 14 ⊢ (( -π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ -π ≤ π) → π ∈ ( -π[,]π))
144	14, 15, 21, 143	mp3an 1491	. . . . . . . . . . . . 13 ⊢ π ∈ ( -π[,]π)
145	144	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → π ∈ ( -π[,]π))
146		iocssicc 13606	. . . . . . . . . . . . 13 ⊢ ( -π(,]π) ⊆ ( -π[,]π)
147	146, 78	sselid 3911	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐸‘𝑋) ∈ ( -π[,]π))
148		tpssi 4796	. . . . . . . . . . . 12 ⊢ (( -π ∈ ( -π[,]π) ∧ π ∈ ( -π[,]π) ∧ (𝐸‘𝑋) ∈ ( -π[,]π)) → { -π, π, (𝐸‘𝑋)} ⊆ ( -π[,]π))
149	142, 145, 147, 148	syl3anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → { -π, π, (𝐸‘𝑋)} ⊆ ( -π[,]π))
150		difssd 4076	. . . . . . . . . . 11 ⊢ (𝜑 → (( -π[,]π) ∖ dom 𝐺) ⊆ ( -π[,]π))
151	149, 150	unssd 4193	. . . . . . . . . 10 ⊢ (𝜑 → ({ -π, π, (𝐸‘𝑋)} ∪ (( -π[,]π) ∖ dom 𝐺)) ⊆ ( -π[,]π))
152	9, 151	eqsstrid 3951	. . . . . . . . 9 ⊢ (𝜑 → 𝐻 ⊆ ( -π[,]π))
153	152, 121	sseldd 3914	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘0) ∈ ( -π[,]π))
154		iccgelb 13571	. . . . . . . 8 ⊢ (( -π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘0) ∈ ( -π[,]π)) → -π ≤ (𝑄‘0))
155	138, 139, 153, 154	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → -π ≤ (𝑄‘0))
156	155	ad2antrr 739	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ≤ (𝑄‘0))
157	122	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) ∈ ℝ)
158	13	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → -π ∈ ℝ)
159	157, 158	letri3d 11489	. . . . . 6 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → ((𝑄‘0) = -π ↔ ((𝑄‘0) ≤ -π ∧ -π ≤ (𝑄‘0))))
160	137, 156, 159	mpbir2and 726	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ (𝑄‘𝑖) = -π) → (𝑄‘0) = -π)
161	57, 51	sselii 3910	. . . . . . 7 ⊢ -π ∈ 𝐻
162		f1ofo 6860	. . . . . . . . 9 ⊢ (𝑄:(0...𝑀)⟶1-1onto𝐻 → 𝑄:(0...𝑀)⟶onto𝐻)
163	92, 162	syl 18	. . . . . . . 8 ⊢ (𝑄 Isom < , < ((0...𝑀), 𝐻) → 𝑄:(0...𝑀)⟶onto𝐻)
164		forn 6827	. . . . . . . 8 ⊢ (𝑄:(0...𝑀)⟶onto𝐻 → ran 𝑄 = 𝐻)
165	91, 163, 164	3syl 19	. . . . . . 7 ⊢ (𝜑 → ran 𝑄 = 𝐻)
166	161, 165	eleqtrrid 2871	. . . . . 6 ⊢ (𝜑 → -π ∈ ran 𝑄)
167		ffn 6737	. . . . . . 7 ⊢ (𝑄:(0...𝑀)⟶𝐻 → 𝑄 Fn (0...𝑀))
168		fvelrnb 6974	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → ( -π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
169	94, 167, 168	3syl 19	. . . . . 6 ⊢ (𝜑 → ( -π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π))
170	166, 169	mpbid 235	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = -π)
171	160, 170	r19.29a 3174	. . . 4 ⊢ (𝜑 → (𝑄‘0) = -π)
172	57, 53	sselii 3910	. . . . . . 7 ⊢ π ∈ 𝐻
173	172, 165	eleqtrrid 2871	. . . . . 6 ⊢ (𝜑 → π ∈ ran 𝑄)
174		fvelrnb 6974	. . . . . . 7 ⊢ (𝑄 Fn (0...𝑀) → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
175	94, 167, 174	3syl 19	. . . . . 6 ⊢ (𝜑 → (π ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π))
176	173, 175	mpbid 235	. . . . 5 ⊢ (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π)
177	94, 152	fssd 6755	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶( -π[,]π))
178		eluzfz2 13703	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (ℤ_≥‘0) → 𝑀 ∈ (0...𝑀))
179	118, 178	syl 18	. . . . . . . . . 10 ⊢ (𝜑 → 𝑀 ∈ (0...𝑀))
180	177, 179	ffvelcdmd 7115	. . . . . . . . 9 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ( -π[,]π))
181		iccleub 13570	. . . . . . . . 9 ⊢ (( -π ∈ ℝ^* ∧ π ∈ ℝ^* ∧ (𝑄‘𝑀) ∈ ( -π[,]π)) → (𝑄‘𝑀) ≤ π)
182	138, 139, 180, 181	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘𝑀) ≤ π)
183	182	3ad2ant1 1151	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ≤ π)
184		id 23	. . . . . . . . . 10 ⊢ ((𝑄‘𝑖) = π → (𝑄‘𝑖) = π)
185	184	eqcomd 2769	. . . . . . . . 9 ⊢ ((𝑄‘𝑖) = π → π = (𝑄‘𝑖))
186	185	3ad2ant3 1153	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π = (𝑄‘𝑖))
187	103	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑖))
188		fveq2 6914	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
189	188	adantl 487	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) = (𝑄‘𝑀))
190	187, 189	breqtrd 5135	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
191	107	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ∈ ℝ)
192		elfzel2 13692	. . . . . . . . . . . . . 14 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℤ)
193	192	zred 12841	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑀 ∈ ℝ)
194	193	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ∈ ℝ)
195		elfzle2 13699	. . . . . . . . . . . . 13 ⊢ (𝑖 ∈ (0...𝑀) → 𝑖 ≤ 𝑀)
196	195	ad2antlr 740	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 ≤ 𝑀)
197		neqne 2967	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑖 = 𝑀 → 𝑖 ≠ 𝑀)
198	197	necomd 3014	. . . . . . . . . . . . 13 ⊢ (¬ 𝑖 = 𝑀 → 𝑀 ≠ 𝑖)
199	198	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑀 ≠ 𝑖)
200	191, 194, 196, 199	leneltd 11501	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → 𝑖 < 𝑀)
201	102	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ∈ ℝ)
202	85, 180	sselid 3911	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑄‘𝑀) ∈ ℝ)
203	202	ad2antrr 739	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑀) ∈ ℝ)
204		simpr 490	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑖 < 𝑀)
205	91	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
206		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
207	179	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑀 ∈ (0...𝑀))
208	206, 207	jca 521	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
209	208	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀)))
210		isorel 7363	. . . . . . . . . . . . . 14 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ 𝑀 ∈ (0...𝑀))) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
211	205, 209, 210	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑖 < 𝑀 ↔ (𝑄‘𝑖) < (𝑄‘𝑀)))
212	204, 211	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) < (𝑄‘𝑀))
213	201, 203, 212	ltled 11495	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ 𝑖 < 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
214	200, 213	syldan 603	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ (0...𝑀)) ∧ ¬ 𝑖 = 𝑀) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
215	190, 214	pm2.61dan 825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
216	215	3adant3 1150	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑖) ≤ (𝑄‘𝑀))
217	186, 216	eqbrtrd 5131	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ≤ (𝑄‘𝑀))
218	202	3ad2ant1 1151	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) ∈ ℝ)
219	12	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → π ∈ ℝ)
220	218, 219	letri3d 11489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → ((𝑄‘𝑀) = π ↔ ((𝑄‘𝑀) ≤ π ∧ π ≤ (𝑄‘𝑀))))
221	183, 217, 220	mpbir2and 726	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀) ∧ (𝑄‘𝑖) = π) → (𝑄‘𝑀) = π)
222	221	rexlimdv3a 3171	. . . . 5 ⊢ (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑄‘𝑖) = π → (𝑄‘𝑀) = π))
223	176, 222	mpd 16	. . . 4 ⊢ (𝜑 → (𝑄‘𝑀) = π)
224		elfzoelz 13831	. . . . . . . . 9 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℤ)
225	224	zred 12841	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ ℝ)
226	225	ltp1d 12285	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 < (𝑖 + 1))
227	226	adantl 487	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 < (𝑖 + 1))
228		elfzofz 13848	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
229		fzofzp1 13937	. . . . . . . 8 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
230	228, 229	jca 521	. . . . . . 7 ⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀)))
231		isorel 7363	. . . . . . 7 ⊢ ((𝑄 Isom < , < ((0...𝑀), 𝐻) ∧ (𝑖 ∈ (0...𝑀) ∧ (𝑖 + 1) ∈ (0...𝑀))) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
232	91, 230, 231	syl2an 608	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 < (𝑖 + 1) ↔ (𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
233	227, 232	mpbid 235	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
234	233	ralrimiva 3158	. . . 4 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
235	171, 223, 234	jca31 524	. . 3 ⊢ (𝜑 → (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
236	5	fourierdlem2 47386	. . . 4 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
237	67, 236	syl 18	. . 3 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = -π ∧ (𝑄‘𝑀) = π) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
238	99, 235, 237	mpbir2and 726	. 2 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
239		fourierdlem102.g	. . . . 5 ⊢ 𝐺 = ((ℝ D 𝐹) ↾ ( -π(,)π))
240	239	reseq1i 5980	. . . 4 ⊢ (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (((ℝ D 𝐹) ↾ ( -π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
241	14	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ^*)
242	15	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → π ∈ ℝ^*)
243	177	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶( -π[,]π))
244		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
245	241, 242, 243, 244	fourierdlem27 47411	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ( -π(,)π))
246	245	resabs1d 6014	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ( -π(,)π)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
247	240, 246	eqtr2id 2811	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
248		fourierdlem102.gcn	. . . 4 ⊢ (𝜑 → 𝐺 ∈ (dom 𝐺–cn→ℂ))
249	248, 5, 67, 238, 9, 165	fourierdlem38 47422	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
250	247, 249	eqeltrd 2864	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
251	247	oveq1d 7464	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
252	248	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (dom 𝐺–cn→ℂ))
253		fourierdlem102.rlim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
254	253	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (( -π[,)π) ∖ dom 𝐺)) → ((𝐺 ↾ (𝑥(,)+∞)) lim_ℂ 𝑥) ≠ ∅)
255		fourierdlem102.llim	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
256	255	adantlr 728	. . . . 5 ⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (( -π(,]π) ∖ dom 𝐺)) → ((𝐺 ↾ (-∞(,)𝑥)) lim_ℂ 𝑥) ≠ ∅)
257	91	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄 Isom < , < ((0...𝑀), 𝐻))
258	257, 92, 93	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶𝐻)
259	79	adantr 486	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐸‘𝑋) ∈ ℝ)
260	257, 163, 164	3syl 19	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ran 𝑄 = 𝐻)
261	252, 254, 256, 257, 258, 244, 233, 245, 259, 9, 260	fourierdlem46 47429	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅ ∧ ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅))
262	261	simpld 500	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
263	251, 262	eqnetrd 3026	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) ≠ ∅)
264	247	oveq1d 7464	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
265	261	simprd 501	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
266	264, 265	eqnetrd 3026	. 2 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((ℝ D 𝐹) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) ≠ ∅)
267	1, 2, 3, 4, 5, 67, 238, 250, 263, 266	fourierdlem94 47477	1 ⊢ (𝜑 → (((𝐹 ↾ (-∞(,)𝑋)) lim_ℂ 𝑋) ≠ ∅ ∧ ((𝐹 ↾ (𝑋(,)+∞)) lim_ℂ 𝑋) ≠ ∅))

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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∪ cun 4152 ∅c0 4281 {cpr 4590 {ctp 4592 class class class wbr 5106 ↦ cmpt 5190 dom cdm 5656 ran crn 5657 ↾ cres 5658 ℩cio 6516 Fn wfn 6559 ⟶wf 6560 ⟶ontowfo 6562 ⟶1-1ontowf1o 6563 ‘cfv 6564 Isom wiso 6565 (class class class)co 7449 ↑_m cmap 8883 Fincfn 9009 ℂcc 11235 ℝcr 11236 0cc0 11237 1c1 11238 + caddc 11240 · cmul 11242 +∞cpnf 11377 -∞cmnf 11378 ℝ^*cxr 11379 < clt 11380 ≤ cle 11381 − cmin 11578 -cneg 11579 / cdiv 12011 ℕcn 12373 2c2 12435 ℕ₀cn0 12644 ℤcz 12731 ℤ_≥cuz 13003 (,)cioo 13514 (,]cioc 13515 [,)cico 13516 [,]cicc 13517 ...cfz 13677 ..^cfzo 13826 ⌊cfl 13968 ♯chash 14513 πcpi 16273 –cn→ccncf 25241 lim_ℂ climc 26226 D cdv 26227

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7781 ax-inf2 9677 ax-cnex 11293 ax-resscn 11294 ax-1cn 11295 ax-icn 11296 ax-addcl 11297 ax-addrcl 11298 ax-mulcl 11299 ax-mulrcl 11300 ax-mulcom 11301 ax-addass 11302 ax-mulass 11303 ax-distr 11304 ax-i2m1 11305 ax-1ne0 11306 ax-1rid 11307 ax-rnegex 11308 ax-rrecex 11309 ax-cnre 11310 ax-pre-lttri 11311 ax-pre-lttrn 11312 ax-pre-ltadd 11313 ax-pre-mulgt0 11314 ax-pre-sup 11315 ax-addf 11316

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6328 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6518 df-fun 6566 df-fn 6567 df-f 6568 df-f1 6569 df-fo 6570 df-f1o 6571 df-fv 6572 df-isom 6573 df-riota 7406 df-ov 7452 df-oprab 7453 df-mpo 7454 df-of 7723 df-om 7910 df-1st 8033 df-2nd 8034 df-supp 8213 df-frecs 8335 df-wrecs 8366 df-recs 8415 df-rdg 8454 df-1o 8512 df-2o 8513 df-oadd 8516 df-er 8753 df-map 8885 df-pm 8886 df-ixp 8962 df-en 9010 df-dom 9011 df-sdom 9012 df-fin 9013 df-fsupp 9390 df-fi 9438 df-sup 9469 df-inf 9470 df-oi 9539 df-dju 10017 df-card 10055 df-pnf 11382 df-mnf 11383 df-xr 11384 df-ltxr 11385 df-le 11386 df-sub 11580 df-neg 11581 df-div 12012 df-nn 12374 df-2 12443 df-3 12444 df-4 12445 df-5 12446 df-6 12447 df-7 12448 df-8 12449 df-9 12450 df-n0 12645 df-xnn0 12718 df-z 12732 df-dec 12853 df-uz 13004 df-q 13114 df-rp 13159 df-xneg 13279 df-xadd 13280 df-xmul 13281 df-ioo 13518 df-ioc 13519 df-ico 13520 df-icc 13521 df-fz 13678 df-fzo 13827 df-fl 13970 df-seq 14183 df-exp 14243 df-fac 14457 df-bc 14486 df-hash 14514 df-shft 15261 df-cj 15307 df-re 15308 df-im 15309 df-sqrt 15443 df-abs 15444 df-limsup 15679 df-clim 15696 df-rlim 15697 df-sum 15895 df-ef 16274 df-sin 16276 df-cos 16277 df-pi 16279 df-struct 17366 df-sets 17383 df-slot 17401 df-ndx 17413 df-base 17429 df-ress 17450 df-plusg 17482 df-mulr 17483 df-starv 17484 df-sca 17485 df-vsca 17486 df-ip 17487 df-tset 17488 df-ple 17489 df-ds 17491 df-unif 17492 df-hom 17493 df-cco 17494 df-rest 17634 df-topn 17635 df-0g 17653 df-gsum 17654 df-topgen 17655 df-pt 17656 df-prds 17659 df-xrs 17715 df-qtop 17720 df-imas 17721 df-xps 17723 df-mre 17797 df-mrc 17798 df-acs 17800 df-mgm 18857 df-sgrp 18949 df-mnd 18965 df-submnd 19020 df-mulg 19319 df-cntz 19573 df-cmn 20038 df-psmet 21712 df-xmet 21713 df-met 21714 df-bl 21715 df-mopn 21716 df-fbas 21717 df-fg 21718 df-cnfld 21721 df-top 23256 df-topon 23273 df-topsp 23295 df-bases 23308 df-cld 23381 df-ntr 23382 df-cls 23383 df-nei 23460 df-lp 23498 df-perf 23499 df-cn 23589 df-cnp 23590 df-haus 23677 df-cmp 23749 df-tx 23925 df-hmeo 24118 df-fil 24209 df-fm 24301 df-flim 24302 df-flf 24303 df-xms 24683 df-ms 24684 df-tms 24685 df-cncf 25243 df-limc 26230 df-dv 26231

This theorem is used by: fourierdlem106 47489

W3C validator