fourierdlem91 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem91 46640

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem91.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem91.t	⊢ 𝑇 = (𝐵 − 𝐴)
fourierdlem91.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem91.q	⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
fourierdlem91.f	⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
fourierdlem91.6	⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
fourierdlem91.fcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem91.l	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
fourierdlem91.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem91.d	⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
fourierdlem91.o	⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem91.h	⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem91.n	⊢ 𝑁 = ((♯‘𝐻) − 1)
fourierdlem91.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem91.e	⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
fourierdlem91.J	⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
fourierdlem91.17	⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
fourierdlem91.u	⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))
fourierdlem91.i	⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ))
fourierdlem91.w	⊢ 𝑊 = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)

**Assertion**
Ref	Expression
fourierdlem91	⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘(𝐽 + 1))))

Distinct variable groups: 𝐴,𝑓,𝑘,𝑦 𝐴,𝑖,𝑥,𝑘,𝑦 𝐴,𝑚,𝑝,𝑖 𝐵,𝑓,𝑘,𝑦 𝐵,𝑖,𝑥 𝐵,𝑚,𝑝 𝐶,𝑓,𝑦 𝐶,𝑖,𝑚,𝑝 𝑥,𝐶 𝐷,𝑓,𝑦 𝐷,𝑖,𝑚,𝑝 𝑥,𝐷 𝑓,𝐸,𝑘,𝑦 𝑖,𝐸,𝑥 𝑖,𝐹,𝑥,𝑦 𝑓,𝐻 𝑥,𝐻 𝑓,𝐼,𝑘,𝑦 𝑖,𝐼,𝑥 𝑖,𝐽,𝑥,𝑦 𝑖,𝑀,𝑥 𝑚,𝑀,𝑝 𝑓,𝑁,𝑘,𝑦 𝑖,𝑁,𝑥 𝑚,𝑁,𝑝 𝑄,𝑓,𝑘,𝑦 𝑄,𝑖,𝑥 𝑄,𝑝 𝑆,𝑓,𝑘,𝑦 𝑆,𝑖,𝑥 𝑆,𝑝 𝑇,𝑓,𝑘,𝑦 𝑇,𝑖,𝑥 𝑥,𝑈,𝑦 𝑥,𝑊,𝑦 𝑖,𝑍,𝑥,𝑦 𝜑,𝑓,𝑘,𝑦 𝜑,𝑖,𝑥 Allowed substitution hints: 𝜑(𝑚,𝑝) 𝐶(𝑘) 𝐷(𝑘) 𝑃(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑄(𝑚) 𝑆(𝑚) 𝑇(𝑚,𝑝) 𝑈(𝑓,𝑖,𝑘,𝑚,𝑝) 𝐸(𝑚,𝑝) 𝐹(𝑓,𝑘,𝑚,𝑝) 𝐻(𝑦,𝑖,𝑘,𝑚,𝑝) 𝐼(𝑚,𝑝) 𝐽(𝑓,𝑘,𝑚,𝑝) 𝐿(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑀(𝑦,𝑓,𝑘) 𝑂(𝑥,𝑦,𝑓,𝑖,𝑘,𝑚,𝑝) 𝑊(𝑓,𝑖,𝑘,𝑚,𝑝) 𝑍(𝑓,𝑘,𝑚,𝑝)

Proof of Theorem fourierdlem91 Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem91.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2		fourierdlem91.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem91.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 46552	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 233	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 495	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		elmapi 8786	. . . . . . . . . 10 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
10		fzossfz 13624	. . . . . . . . . 10 ⊢ (0..^𝑀) ⊆ (0...𝑀)
11		fourierdlem91.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝐵 − 𝐴)
12		fourierdlem91.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
13		fourierdlem91.J	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
14		fourierdlem91.i	. . . . . . . . . . . . 13 ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ))
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 46587	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))})))
16	15	simpld 495	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17		fourierdlem91.c	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
18		fourierdlem91.d	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
19		elioore 13319	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℝ)
21		elioo4g 13350	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (𝐶(,)+∞) ↔ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
22	18, 21	sylib 219	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
23	22	simprd 496	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 < 𝐷 ∧ 𝐷 < +∞))
24	23	simpld 495	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 < 𝐷)
25		fourierdlem91.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
27	26	eleq1d 2824	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3163	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3401	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4095	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
31		fourierdlem91.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = ((♯‘𝐻) − 1)
32		fourierdlem91.h	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
33	32	fveq2i 6830	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
34	33	oveq1i 7366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
35	31, 34	eqtri 2762	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
36		fourierdlem91.s	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
37		isoeq5 7265	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
38	32, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
39	38	iotabii 6470	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
40	36, 39	eqtri 2762	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
41	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40	fourierdlem54 46603	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
42	41	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
43	42	simprd 496	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
44	42	simpld 495	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
45	25	fourierdlem2 46552	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
46	44, 45	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
47	43, 46	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
48	47	simpld 495	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
49		elmapi 8786	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
51		fourierdlem91.17	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
52		elfzofz 13621	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
53	51, 52	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
54	50, 53	ffvelcdmd 7026	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
55	16, 54	ffvelcdmd 7026	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
56	10, 55	sselid 3913	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0...𝑀))
57	9, 56	ffvelcdmd 7026	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
58	57	rexrd 11186	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
59	58	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
60		fzofzp1 13710	. . . . . . . . . 10 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
61	55, 60	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
62	9, 61	ffvelcdmd 7026	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ)
63	62	rexrd 11186	. . . . . . 7 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
64	63	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
65	3, 2, 1	fourierdlem11 46561	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
66	65	simp1d 1148	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	66	rexrd 11186	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
68	65	simp2d 1149	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
69		iocssre 13371	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
70	67, 68, 69	syl2anc 590	. . . . . . . 8 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
71	65	simp3d 1150	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 < 𝐵)
72	66, 68, 71, 11, 12	fourierdlem4 46554	. . . . . . . . 9 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
73		fzofzp1 13710	. . . . . . . . . . 11 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
74	51, 73	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
75	50, 74	ffvelcdmd 7026	. . . . . . . . 9 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
76	72, 75	ffvelcdmd 7026	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ (𝐴(,]𝐵))
77	70, 76	sseldd 3916	. . . . . . 7 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
78	77	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
79	66, 68	iccssred 13378	. . . . . . . . 9 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
80	66, 68, 71, 13	fourierdlem17 46567	. . . . . . . . . 10 ⊢ (𝜑 → 𝑍:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
81	72, 54	ffvelcdmd 7026	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘(𝑆‘𝐽)) ∈ (𝐴(,]𝐵))
82	80, 81	ffvelcdmd 7026	. . . . . . . . 9 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ (𝐴[,]𝐵))
83	79, 82	sseldd 3916	. . . . . . . 8 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
84	47	simprrd 779	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
85		fveq2 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘𝑖) = (𝑆‘𝐽))
86		oveq1 7363	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐽 → (𝑖 + 1) = (𝐽 + 1))
87	86	fveq2d 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘(𝑖 + 1)) = (𝑆‘(𝐽 + 1)))
88	85, 87	breq12d 5085	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐽 → ((𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
89	88	rspccva 3559	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
90	84, 51, 89	syl2anc 590	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
91	54, 75	posdifd 11728	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽) < (𝑆‘(𝐽 + 1)) ↔ 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
92	90, 91	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
93		eleq1 2827	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝑗 ∈ (0..^𝑁) ↔ 𝐽 ∈ (0..^𝑁)))
94	93	anbi2d 636	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (0..^𝑁))))
95		oveq1 7363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝐽 → (𝑗 + 1) = (𝐽 + 1))
96	95	fveq2d 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝐽 + 1)))
97	96	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐸‘(𝑆‘(𝐽 + 1))))
98		fveq2 6827	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑗 = 𝐽 → (𝑆‘𝑗) = (𝑆‘𝐽))
99	98	fveq2d 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘𝑗)) = (𝐸‘(𝑆‘𝐽)))
100	99	fveq2d 6831	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
101	97, 100	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
102	96, 98	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
103	101, 102	eqeq12d 2755	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
104	94, 103	imbi12d 345	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))))
105	11	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑘 · 𝑇) = (𝑘 · (𝐵 − 𝐴))
106	105	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵 − 𝐴)))
107	106	eleq1i 2830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
108	107	rexbii 3086	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
109	108	rgenw 3057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
110		rabbi 3421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
111	109, 110	mpbi 231	. . . . . . . . . . . . . . . . . . . 20 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}
112	111	uneq2i 4095	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
113	112	fveq2i 6830	. . . . . . . . . . . . . . . . . 18 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
114	113	oveq1i 7366	. . . . . . . . . . . . . . . . 17 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
115	35, 114	eqtri 2762	. . . . . . . . . . . . . . . 16 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
116		isoeq5 7265	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
117	112, 116	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
118	117	iotabii 6470	. . . . . . . . . . . . . . . . 17 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
119	40, 118	eqtri 2762	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
120		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
121	3, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120	fourierdlem65 46614	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
122	104, 121	vtoclg 3500	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
123	122	anabsi7 677	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
124	51, 123	mpdan 693	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
125	92, 124	breqtrrd 5100	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
126	83, 77	posdifd 11728	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))) ↔ 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽))))))
127	125, 126	mpbird 258	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
128	100, 97	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))))
129	98	fveq2d 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐼‘(𝑆‘𝑗)) = (𝐼‘(𝑆‘𝐽)))
130	129	fveq2d 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
131	129	oveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
132	131	fveq2d 6831	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
133	130, 132	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
134	128, 133	sseq12d 3948	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) ↔ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
135	94, 134	imbi12d 345	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
136	32, 30	eqtri 2762	. . . . . . . . . . . . . 14 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
137		eqid 2739	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
138	11, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14	fourierdlem79 46628	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
139	135, 138	vtoclg 3500	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
140	139	anabsi7 677	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
141	51, 140	mpdan 693	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
142	57, 62, 83, 77, 127, 141	fourierdlem10 46560	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))) ∧ (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
143	142	simpld 495	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
144	57, 83, 77, 143, 127	lelttrd 11295	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
145	144	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
146	62	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ)
147	142	simprd 496	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
148	147	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
149		neqne 2942	. . . . . . . . 9 ⊢ (¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) → (𝐸‘(𝑆‘(𝐽 + 1))) ≠ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
150	149	necomd 2989	. . . . . . . 8 ⊢ (¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ≠ (𝐸‘(𝑆‘(𝐽 + 1))))
151	150	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ≠ (𝐸‘(𝑆‘(𝐽 + 1))))
152	78, 146, 148, 151	leneltd 11291	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝐸‘(𝑆‘(𝐽 + 1))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
153	59, 64, 78, 145, 152	eliood 45943	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
154		fvres 6846	. . . . 5 ⊢ ((𝐸‘(𝑆‘(𝐽 + 1))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1)))) = (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1)))))
155	153, 154	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1)))) = (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1)))))
156	155	eqcomd 2745	. . 3 ⊢ ((𝜑 ∧ ¬ (𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1)))))
157	156	ifeq2da 4487	. 2 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1))))) = if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))))
158		fourierdlem91.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
159		fdm 6664	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
160	158, 159	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 = ℝ)
161	160	feq2d 6639	. . . . . 6 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:ℝ⟶ℂ))
162	158, 161	mpbird 258	. . . . 5 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
163		ioosscn 13352	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ
164	163	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ)
165		ioossre 13351	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℝ
166	165, 160	sseqtrrid 3958	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ dom 𝐹)
167		fourierdlem91.u	. . . . . . 7 ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))
168	75, 77	resubcld 11569	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
169	167, 168	eqeltrid 2843	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ ℝ)
170	169	recnd 11164	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ ℂ)
171		eqid 2739	. . . . 5 ⊢ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}
172	83, 77, 169	iooshift 45967	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)})
173		ioossre 13351	. . . . . . 7 ⊢ (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ ℝ
174	173, 160	sseqtrrid 3958	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ dom 𝐹)
175	172, 174	eqsstrrd 3950	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} ⊆ dom 𝐹)
176		elioore 13319	. . . . . 6 ⊢ (𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑦 ∈ ℝ)
177	68, 66	resubcld 11569	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
178	11, 177	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
179	178	recnd 11164	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
180	66, 68	posdifd 11728	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
181	71, 180	mpbid 233	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
182	181, 11	breqtrrdi 5114	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑇)
183	182	gt0ne0d 11705	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≠ 0)
184	170, 179, 183	divcan1d 11923	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈 / 𝑇) · 𝑇) = 𝑈)
185	184	eqcomd 2745	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = ((𝑈 / 𝑇) · 𝑇))
186	185	oveq2d 7372	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
187	186	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
188	187	fveq2d 6831	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))))
189	158	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
190	178	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
191	77	recnd 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
192	75	recnd 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
193	191, 192	negsubdi2d 11512	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
194	193	eqcomd 2745	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) = -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))
195	194	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
196	167	oveq1i 7366	. . . . . . . . . . . 12 ⊢ (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇)
197	196	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇))
198	12	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
199		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
200		oveq2 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
201	200	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
202	201	fveq2d 6831	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
203	202	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
204	199, 203	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
205	204	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
206	68, 75	resubcld 11569	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
207	206, 178, 183	redivcld 11974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
208	207	flcld 13748	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
209	208	zred 12624	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
210	209, 178	remulcld 11166	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
211	75, 210	readdcld 11165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
212	198, 205, 75, 211	fvmptd 6943	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
213	212	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))))
214	208	zcnd 12625	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℂ)
215	214, 179	mulcld 11156	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℂ)
216	192, 215	pncan2d 11498	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
217	213, 216	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
218	217, 215	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℂ)
219	218, 179, 183	divnegd 11935	. . . . . . . . . . 11 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
220	195, 197, 219	3eqtr4d 2784	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 / 𝑇) = -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
221	217	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇))
222	214, 179, 183	divcan4d 11928	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
223	221, 222	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
224	223, 208	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
225	224	znegcld 12626	. . . . . . . . . 10 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
226	220, 225	eqeltrd 2839	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 / 𝑇) ∈ ℤ)
227	226	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑈 / 𝑇) ∈ ℤ)
228		simpr 485	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
229		fourierdlem91.6	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
230	229	adantlr 721	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
231	189, 190, 227, 228, 230	fperiodmul 45752	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))) = (𝐹‘𝑦))
232	188, 231	eqtrd 2774	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
233	176, 232	sylan2 599	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
234	6	simprrd 779	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
235		fveq2 6827	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘𝑖) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
236		oveq1 7363	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
237	236	fveq2d 6831	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
238	235, 237	breq12d 5085	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
239	238	rspccva 3559	. . . . . . . 8 ⊢ ((∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
240	234, 55, 239	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
241	55	ancli 553	. . . . . . . 8 ⊢ (𝜑 → (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
242		eleq1 2827	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 ∈ (0..^𝑀) ↔ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
243	242	anbi2d 636	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))))
244	235, 237	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
245	244	reseq2d 5931	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
246	244	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) = (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
247	245, 246	eleq12d 2833	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) ↔ (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
248	243, 247	imbi12d 345	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) ↔ ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))))
249		fourierdlem91.fcn	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
250	248, 249	vtoclg 3500	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
251	55, 241, 250	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
252		nfv 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
253		fourierdlem91.w	. . . . . . . . . . . . 13 ⊢ 𝑊 = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
254		nfmpt1 5171	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑖 ∈ (0..^𝑀) ↦ 𝐿)
255	253, 254	nfcxfr 2899	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖𝑊
256		nfcv 2901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝐼‘(𝑆‘𝐽))
257	255, 256	nffv 6837	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(𝑊‘(𝐼‘(𝑆‘𝐽)))
258	257	nfel1 2917	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
259	252, 258	nfim 1903	. . . . . . . . 9 ⊢ Ⅎ𝑖((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
260	243	biimpar 478	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))
261	260	3adant2 1137	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))
262		fourierdlem91.l	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
263	261, 262	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
264		fveq2 6827	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑊‘𝑖) = (𝑊‘(𝐼‘(𝑆‘𝐽))))
265	264	eqcomd 2745	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) = (𝑊‘𝑖))
266	265	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑊‘(𝐼‘(𝑆‘𝐽))) = (𝑊‘𝑖))
267	260	simprd 496	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑖 ∈ (0..^𝑀))
268		elex 3452	. . . . . . . . . . . . . . . 16 ⊢ (𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) → 𝐿 ∈ V)
269	260, 262, 268	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝐿 ∈ V)
270	253	fvmpt2 6947	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝐿 ∈ V) → (𝑊‘𝑖) = 𝐿)
271	267, 269, 270	syl2anc 590	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑊‘𝑖) = 𝐿)
272	266, 271	eqtrd 2774	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑊‘(𝐼‘(𝑆‘𝐽))) = 𝐿)
273	272	3adant2 1137	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑊‘(𝐼‘(𝑆‘𝐽))) = 𝐿)
274	245, 237	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
275	274	eqcomd 2745	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
276	275	3ad2ant1 1139	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))
277	263, 273, 276	3eltr4d 2854	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
278	277	3exp 1125	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
279	262	2a1i 12	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1))))))
280	278, 279	impbid 213	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘(𝑖 + 1)))) ↔ ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
281	259, 280, 262	vtoclg1f 3514	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
282	55, 241, 281	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝑊‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
283		eqid 2739	. . . . . . 7 ⊢ if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) = if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1)))))
284		eqid 2739	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) ∪ {(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))})) = ((TopOpen‘ℂ_fld) ↾_t (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) ∪ {(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))}))
285	57, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284	fourierdlem33 46583	. . . . . 6 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝐸‘(𝑆‘(𝐽 + 1)))))
286	141	resabs1d 5960	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))))
287	286	oveq1d 7371	. . . . . 6 ⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝐸‘(𝑆‘(𝐽 + 1)))))
288	285, 287	eleqtrd 2841	. . . . 5 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝐸‘(𝑆‘(𝐽 + 1)))))
289	162, 164, 166, 170, 171, 175, 233, 288	limcperiod 46073	. . . 4 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)))
290	167	oveq2i 7367	. . . . . 6 ⊢ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
291	191, 192	pncan3d 11499	. . . . . 6 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘(𝐽 + 1)))
292	290, 291	eqtrid 2786	. . . . 5 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = (𝑆‘(𝐽 + 1)))
293	292	oveq2d 7372	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘(𝐽 + 1))))
294	289, 293	eleqtrd 2841	. . 3 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘(𝐽 + 1))))
295	167	oveq2i 7367	. . . . . . . . 9 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
296	295	a1i 11	. . . . . . . 8 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
297	17, 20	iccssred 13378	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
298		ax-resscn 11086	. . . . . . . . . . . . . . 15 ⊢ ℝ ⊆ ℂ
299	297, 298	sstrdi 3927	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℂ)
300	25, 44, 43	fourierdlem15 46565	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
301	300, 53	ffvelcdmd 7026	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐶[,]𝐷))
302	299, 301	sseldd 3916	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℂ)
303	192, 302	subcld 11496	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) ∈ ℂ)
304	83	recnd 11164	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℂ)
305	191, 303, 304	subsub23d 45735	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
306	124, 305	mpbird 258	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
307	306	eqcomd 2745	. . . . . . . . 9 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
308	307	oveq1d 7371	. . . . . . . 8 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
309	191, 303	subcld 11496	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) ∈ ℂ)
310	309, 192, 191	addsub12d 11519	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))))
311	191, 303, 191	sub32d 11528	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
312	191	subidd 11484	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = 0)
313	312	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
314		df-neg 11371	. . . . . . . . . . . 12 ⊢ -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
315	192, 302	negsubdi2d 11512	. . . . . . . . . . . 12 ⊢ (𝜑 → -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
316	314, 315	eqtr3id 2788	. . . . . . . . . . 11 ⊢ (𝜑 → (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
317	311, 313, 316	3eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
318	317	oveq2d 7372	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))))
319	192, 302	pncan3d 11499	. . . . . . . . 9 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))) = (𝑆‘𝐽))
320	310, 318, 319	3eqtrd 2778	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘𝐽))
321	296, 308, 320	3eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = (𝑆‘𝐽))
322	321, 292	oveq12d 7374	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
323	172, 322	eqtr3d 2776	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
324	323	reseq2d 5931	. . . 4 ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) = (𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))))
325	324	oveq1d 7371	. . 3 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘(𝐽 + 1))) = ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘(𝐽 + 1))))
326	294, 325	eleqtrd 2841	. 2 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘(𝐽 + 1))))
327	157, 326	eqeltrd 2839	1 ⊢ (𝜑 → if((𝐸‘(𝑆‘(𝐽 + 1))) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)), (𝑊‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝐸‘(𝑆‘(𝐽 + 1))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘(𝐽 + 1))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 {crab 3391 Vcvv 3431 ∪ cun 3881 ⊆ wss 3883 ifcif 4454 {csn 4555 {cpr 4557 class class class wbr 5072 ↦ cmpt 5153 dom cdm 5618 ran crn 5619 ↾ cres 5620 ℩cio 6439 ⟶wf 6481 ‘cfv 6485 Isom wiso 6486 (class class class)co 7356 ↑_m cmap 8763 supcsup 9343 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 +∞cpnf 11167 ℝ^*cxr 11169 < clt 11170 ≤ cle 11171 − cmin 11368 -cneg 11369 / cdiv 11798 ℕcn 12165 2c2 12227 ℤcz 12515 (,)cioo 13289 (,]cioc 13290 [,]cicc 13292 ...cfz 13452 ..^cfzo 13599 ⌊cfl 13740 ♯chash 14283 ↾_t crest 17374 TopOpenctopn 17375 ℂ_fldccnfld 21347 –cn→ccncf 24861 lim_ℂ climc 25847

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-se 5572 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-isom 6494 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-oadd 8399 df-er 8633 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-fi 9314 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-xnn0 12502 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-xneg 13054 df-xadd 13055 df-xmul 13056 df-ioo 13293 df-ioc 13294 df-ico 13295 df-icc 13296 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-struct 17108 df-slot 17143 df-ndx 17155 df-base 17171 df-plusg 17224 df-mulr 17225 df-starv 17226 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-rest 17376 df-topn 17377 df-topgen 17397 df-psmet 21339 df-xmet 21340 df-met 21341 df-bl 21342 df-mopn 21343 df-cnfld 21348 df-top 22877 df-topon 22894 df-topsp 22916 df-bases 22929 df-cld 23002 df-ntr 23003 df-cls 23004 df-nei 23081 df-lp 23119 df-cn 23210 df-cnp 23211 df-cmp 23370 df-xms 24303 df-ms 24304 df-cncf 24863 df-limc 25851

This theorem is referenced by: fourierdlem99 46648 fourierdlem100 46649 fourierdlem107 46656 fourierdlem109 46658

W3C validator