fourierdlem89 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem89 46381

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

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

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

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

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

Step	Hyp	Ref	Expression
1		fourierdlem89.q	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2		fourierdlem89.m	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑀 ∈ ℕ)
3		fourierdlem89.p	. . . . . . . . . . . . . 14 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
4	3	fourierdlem2 46295	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 232	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		elmapi 8784	. . . . . . . . . 10 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
10		fzossfz 13592	. . . . . . . . . 10 ⊢ (0..^𝑀) ⊆ (0...𝑀)
11		fourierdlem89.t	. . . . . . . . . . . . 13 ⊢ 𝑇 = (𝐵 − 𝐴)
12		fourierdlem89.e	. . . . . . . . . . . . 13 ⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))
13		fourierdlem89.z	. . . . . . . . . . . . 13 ⊢ 𝑍 = (𝑦 ∈ (𝐴(,]𝐵) ↦ if(𝑦 = 𝐵, 𝐴, 𝑦))
14		fourierdlem89.20	. . . . . . . . . . . . 13 ⊢ 𝐼 = (𝑥 ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ))
15	3, 2, 1, 11, 12, 13, 14	fourierdlem37 46330	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))})))
16	15	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17		fourierdlem89.c	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
18		fourierdlem89.d	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
19		elioore 13289	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℝ)
21		elioo4g 13320	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (𝐶(,)+∞) ↔ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
22	18, 21	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
23	22	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 < 𝐷 ∧ 𝐷 < +∞))
24	23	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 < 𝐷)
25		fourierdlem89.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		oveq1 7363	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
27	26	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3158	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3407	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4115	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
31		fourierdlem89.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = ((♯‘𝐻) − 1)
32		fourierdlem89.12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
33	32	fveq2i 6835	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
34	33	oveq1i 7366	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
35	31, 34	eqtri 2757	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
36		fourierdlem89.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 6475	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
40	36, 39	eqtri 2757	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
41	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40	fourierdlem54 46346	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
42	41	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
43	42	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
44	42	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
45	25	fourierdlem2 46295	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
46	44, 45	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
47	43, 46	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
48	47	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
49		elmapi 8784	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
51		fourierdlem89.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
52		elfzofz 13589	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
53	51, 52	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
54	50, 53	ffvelcdmd 7028	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
55	16, 54	ffvelcdmd 7028	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
56	10, 55	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0...𝑀))
57	9, 56	ffvelcdmd 7028	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
58	57	rexrd 11180	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
60		fzofzp1 13678	. . . . . . . . . 10 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
61	55, 60	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
62	9, 61	ffvelcdmd 7028	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ)
63	62	rexrd 11180	. . . . . . 7 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
64	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
65	3, 2, 1	fourierdlem11 46304	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
66	65	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	65	simp2d 1143	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
68	66, 67	iccssred 13348	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
69	65	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 < 𝐵)
70	66, 67, 69, 13	fourierdlem17 46310	. . . . . . . . 9 ⊢ (𝜑 → 𝑍:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
71	66, 67, 69, 11, 12	fourierdlem4 46297	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
72	71, 54	ffvelcdmd 7028	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘(𝑆‘𝐽)) ∈ (𝐴(,]𝐵))
73	70, 72	ffvelcdmd 7028	. . . . . . . 8 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ (𝐴[,]𝐵))
74	68, 73	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
75	74	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
76	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
77	66	rexrd 11180	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
78		iocssre 13341	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
79	77, 67, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
80		fzofzp1 13678	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
81	51, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
82	50, 81	ffvelcdmd 7028	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
83	71, 82	ffvelcdmd 7028	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ (𝐴(,]𝐵))
84	79, 83	sseldd 3932	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
85	47	simprrd 773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
86		fveq2 6832	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘𝑖) = (𝑆‘𝐽))
87		oveq1 7363	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐽 → (𝑖 + 1) = (𝐽 + 1))
88	87	fveq2d 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘(𝑖 + 1)) = (𝑆‘(𝐽 + 1)))
89	86, 88	breq12d 5109	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐽 → ((𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
90	89	rspccva 3573	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
91	85, 51, 90	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
92	54, 82	posdifd 11722	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽) < (𝑆‘(𝐽 + 1)) ↔ 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
93	91, 92	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
94	51	ancli 548	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (0..^𝑁)))
95		eleq1 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑗 ∈ (0..^𝑁) ↔ 𝐽 ∈ (0..^𝑁)))
96	95	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (0..^𝑁))))
97		oveq1 7363	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑗 + 1) = (𝐽 + 1))
98	97	fveq2d 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝐽 + 1)))
99	98	fveq2d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐸‘(𝑆‘(𝐽 + 1))))
100		fveq2 6832	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑆‘𝑗) = (𝑆‘𝐽))
101	100	fveq2d 6836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘𝑗)) = (𝐸‘(𝑆‘𝐽)))
102	101	fveq2d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
103	99, 102	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
104	98, 100	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
105	103, 104	eqeq12d 2750	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → (((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
106	96, 105	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))))
107	11	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 · 𝑇) = (𝑘 · (𝐵 − 𝐴))
108	107	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵 − 𝐴)))
109	108	eleq1i 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
110	109	rexbii 3081	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
111	110	rgenw 3053	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
112		rabbi 3427	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
113	111, 112	mpbi 230	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}
114	113	uneq2i 4115	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
115	114	fveq2i 6835	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
116	115	oveq1i 7366	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
117	35, 116	eqtri 2757	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
118		isoeq5 7265	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))))
119	114, 118	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
120	119	iotabii 6475	. . . . . . . . . . . . . . . 16 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
121	40, 120	eqtri 2757	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
122		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
123	3, 11, 2, 1, 17, 18, 25, 117, 121, 12, 13, 122	fourierdlem65 46357	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
124	106, 123	vtoclg 3509	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
125	51, 94, 124	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
126	93, 125	breqtrrd 5124	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
127	74, 84	posdifd 11722	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))) ↔ 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽))))))
128	126, 127	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
129		id 22	. . . . . . . . . . 11 ⊢ (𝜑 → 𝜑)
130	102, 99	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))))
131	100	fveq2d 6836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐼‘(𝑆‘𝑗)) = (𝐼‘(𝑆‘𝐽)))
132	131	fveq2d 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
133	131	oveq1d 7371	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
134	133	fveq2d 6836	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
135	132, 134	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
136	130, 135	sseq12d 3965	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) ↔ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
137	96, 136	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
138		eqid 2734	. . . . . . . . . . . . . 14 ⊢ ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2))) = ((𝑆‘𝑗) + if(((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) < ((𝑄‘1) − 𝐴), (((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) / 2), (((𝑄‘1) − 𝐴) / 2)))
139	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40, 12, 13, 138, 14	fourierdlem79 46371	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
140	137, 139	vtoclg 3509	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
141	140	anabsi7 671	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
142	129, 51, 141	syl2anc 584	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
143	57, 62, 74, 84, 128, 142	fourierdlem10 46303	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))) ∧ (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
144	143	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
145	144	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
146		neqne 2938	. . . . . . . 8 ⊢ (¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
147	146	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
148	76, 75, 145, 147	leneltd 11285	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑍‘(𝐸‘(𝑆‘𝐽))))
149	143	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
150	74, 84, 62, 128, 149	ltletrd 11291	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
151	150	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
152	59, 64, 75, 148, 151	eliood 45686	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
153		fvres 6851	. . . . 5 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
154	152, 153	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
155	154	eqcomd 2740	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
156	155	ifeq2da 4510	. 2 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))))
157		fourierdlem89.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
158		fdm 6669	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
159	157, 158	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 = ℝ)
160	159	feq2d 6644	. . . . . 6 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:ℝ⟶ℂ))
161	157, 160	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
162		ioosscn 13322	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ
163	162	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ)
164		ioossre 13321	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℝ
165	164, 159	sseqtrrid 3975	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ dom 𝐹)
166		fourierdlem89.u	. . . . . . 7 ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))
167	82, 84	resubcld 11563	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
168	166, 167	eqeltrid 2838	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ ℝ)
169	168	recnd 11158	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ ℂ)
170		eqid 2734	. . . . 5 ⊢ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}
171	74, 84, 168	iooshift 45710	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)})
172		ioossre 13321	. . . . . . 7 ⊢ (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ ℝ
173	172, 159	sseqtrrid 3975	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ dom 𝐹)
174	171, 173	eqsstrrd 3967	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} ⊆ dom 𝐹)
175		elioore 13289	. . . . . 6 ⊢ (𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑦 ∈ ℝ)
176	67, 66	resubcld 11563	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
177	11, 176	eqeltrid 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
178	177	recnd 11158	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
179	66, 67	posdifd 11722	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
180	69, 179	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
181	180, 11	breqtrrdi 5138	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑇)
182	181	gt0ne0d 11699	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≠ 0)
183	169, 178, 182	divcan1d 11916	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈 / 𝑇) · 𝑇) = 𝑈)
184	183	eqcomd 2740	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = ((𝑈 / 𝑇) · 𝑇))
185	184	oveq2d 7372	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
186	185	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
187	186	fveq2d 6836	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))))
188	157	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
189	177	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
190	84	recnd 11158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
191	82	recnd 11158	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
192	190, 191	negsubdi2d 11506	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
193	192	eqcomd 2740	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) = -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))
194	193	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
195	166	oveq1i 7366	. . . . . . . . . . . 12 ⊢ (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇)
196	195	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇))
197	12	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
198		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
199		oveq2 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
200	199	oveq1d 7371	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
201	200	fveq2d 6836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
202	201	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
203	198, 202	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
204	203	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
205	67, 82	resubcld 11563	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
206	205, 177, 182	redivcld 11967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
207	206	flcld 13716	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
208	207	zred 12594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
209	208, 177	remulcld 11160	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
210	82, 209	readdcld 11159	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
211	197, 204, 82, 210	fvmptd 6946	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
212	211	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))))
213	208	recnd 11158	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℂ)
214	213, 178	mulcld 11150	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℂ)
215	191, 214	pncan2d 11492	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
216	212, 215	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
217	216, 214	eqeltrd 2834	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℂ)
218	217, 178, 182	divnegd 11928	. . . . . . . . . . 11 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
219	194, 196, 218	3eqtr4d 2779	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 / 𝑇) = -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
220	216	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇))
221	213, 178, 182	divcan4d 11921	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
222	220, 221	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
223	222, 207	eqeltrd 2834	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
224	223	znegcld 12596	. . . . . . . . . 10 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
225	219, 224	eqeltrd 2834	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 / 𝑇) ∈ ℤ)
226	225	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑈 / 𝑇) ∈ ℤ)
227		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
228		fourierdlem89.per	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
229	228	adantlr 715	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
230	188, 189, 226, 227, 229	fperiodmul 45494	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))) = (𝐹‘𝑦))
231	187, 230	eqtrd 2769	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
232	175, 231	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
233	6	simprrd 773	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
234		fveq2 6832	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘𝑖) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
235		oveq1 7363	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
236	235	fveq2d 6836	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
237	234, 236	breq12d 5109	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
238	237	rspccva 3573	. . . . . . . 8 ⊢ ((∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
239	233, 55, 238	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
240	55	ancli 548	. . . . . . . 8 ⊢ (𝜑 → (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
241		eleq1 2822	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 ∈ (0..^𝑀) ↔ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
242	241	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))))
243	234, 236	oveq12d 7374	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
244	243	reseq2d 5936	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
245	243	oveq1d 7371	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) = (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
246	244, 245	eleq12d 2828	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) ↔ (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
247	242, 246	imbi12d 344	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ)) ↔ ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))))
248		fourierdlem89.fcn	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
249	247, 248	vtoclg 3509	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
250	55, 240, 249	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
251		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
252		fourierdlem89.21	. . . . . . . . . . . . 13 ⊢ 𝑉 = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
253		nfmpt1 5195	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑖 ∈ (0..^𝑀) ↦ 𝑅)
254	252, 253	nfcxfr 2894	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖𝑉
255		nfcv 2896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝐼‘(𝑆‘𝐽))
256	254, 255	nffv 6842	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽)))
257	256	nfel1 2913	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))
258	251, 257	nfim 1897	. . . . . . . . 9 ⊢ Ⅎ𝑖((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
259	242	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))
260	259	3adant2 1131	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))
261		fourierdlem89.limc	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
262	260, 261	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
263		fveq2 6832	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘𝑖) = (𝑉‘(𝐼‘(𝑆‘𝐽))))
264	263	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
265	264	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
266	259	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑖 ∈ (0..^𝑀))
267		elex 3459	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) → 𝑅 ∈ V)
268	259, 261, 267	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑅 ∈ V)
269	252	fvmpt2 6950	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑅 ∈ V) → (𝑉‘𝑖) = 𝑅)
270	266, 268, 269	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘𝑖) = 𝑅)
271	265, 270	eqtrd 2769	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
272	271	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
273	244, 234	oveq12d 7374	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
274	273	eqcomd 2740	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
275	274	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
276	262, 272, 275	3eltr4d 2849	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
277	276	3exp 1119	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))))
278	261	2a1i 12	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))))
279	277, 278	impbid 212	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ↔ ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))))
280	258, 279, 261	vtoclg1f 3524	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))))
281	55, 240, 280	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
282		eqid 2734	. . . . . . 7 ⊢ if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
283		eqid 2734	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
284	57, 62, 239, 250, 281, 74, 84, 128, 142, 282, 283	fourierdlem32 46325	. . . . . 6 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
285	142	resabs1d 5965	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))))
286	285	oveq1d 7371	. . . . . 6 ⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
287	284, 286	eleqtrd 2836	. . . . 5 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
288	161, 163, 165, 169, 170, 174, 232, 287	limcperiod 45816	. . . 4 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)))
289	166	oveq2i 7367	. . . . . . 7 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
290	289	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
291	17, 20	iccssred 13348	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
292		ax-resscn 11081	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
293	291, 292	sstrdi 3944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℂ)
294	25, 44, 43	fourierdlem15 46308	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
295	294, 53	ffvelcdmd 7028	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐶[,]𝐷))
296	293, 295	sseldd 3932	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℂ)
297	191, 296	subcld 11490	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) ∈ ℂ)
298	74	recnd 11158	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℂ)
299	190, 297, 298	subsub23d 45477	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
300	125, 299	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
301	300	eqcomd 2740	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
302	301	oveq1d 7371	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
303	190, 297	subcld 11490	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) ∈ ℂ)
304	303, 191, 190	addsub12d 11513	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))))
305	190, 297, 190	sub32d 11522	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
306	190	subidd 11478	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = 0)
307	306	oveq1d 7371	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
308		df-neg 11365	. . . . . . . . . 10 ⊢ -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
309	191, 296	negsubdi2d 11506	. . . . . . . . . 10 ⊢ (𝜑 → -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
310	308, 309	eqtr3id 2783	. . . . . . . . 9 ⊢ (𝜑 → (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
311	305, 307, 310	3eqtrd 2773	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
312	311	oveq2d 7372	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))))
313	191, 296	pncan3d 11493	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))) = (𝑆‘𝐽))
314	304, 312, 313	3eqtrd 2773	. . . . . 6 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘𝐽))
315	290, 302, 314	3eqtrd 2773	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = (𝑆‘𝐽))
316	315	oveq2d 7372	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)) = ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
317	288, 316	eleqtrd 2836	. . 3 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
318	166	oveq2i 7367	. . . . . . . 8 ⊢ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
319	190, 191	pncan3d 11493	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘(𝐽 + 1)))
320	318, 319	eqtrid 2781	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = (𝑆‘(𝐽 + 1)))
321	315, 320	oveq12d 7374	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
322	171, 321	eqtr3d 2771	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
323	322	reseq2d 5936	. . . 4 ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) = (𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))))
324	323	oveq1d 7371	. . 3 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)) = ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))
325	317, 324	eleqtrd 2836	. 2 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))
326	156, 325	eqeltrd 2834	1 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2930 ∀wral 3049 ∃wrex 3058 {crab 3397 Vcvv 3438 ∪ cun 3897 ⊆ wss 3899 ifcif 4477 {cpr 4580 class class class wbr 5096 ↦ cmpt 5177 dom cdm 5622 ran crn 5623 ↾ cres 5624 ℩cio 6444 ⟶wf 6486 ‘cfv 6490 Isom wiso 6491 (class class class)co 7356 ↑_m cmap 8761 supcsup 9341 ℂcc 11022 ℝcr 11023 0cc0 11024 1c1 11025 + caddc 11027 · cmul 11029 +∞cpnf 11161 ℝ^*cxr 11163 < clt 11164 ≤ cle 11165 − cmin 11362 -cneg 11363 / cdiv 11792 ℕcn 12143 2c2 12198 ℤcz 12486 (,)cioo 13259 (,]cioc 13260 [,)cico 13261 [,]cicc 13262 ...cfz 13421 ..^cfzo 13568 ⌊cfl 13708 ♯chash 14251 ↾_t crest 17338 TopOpenctopn 17339 ℂ_fldccnfld 21307 –cn→ccncf 24823 lim_ℂ climc 25817

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-inf2 9548 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-tp 4583 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-iin 4947 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 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 8763 df-pm 8764 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-fi 9312 df-sup 9343 df-inf 9344 df-oi 9413 df-dju 9811 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-4 12208 df-5 12209 df-6 12210 df-7 12211 df-8 12212 df-9 12213 df-n0 12400 df-xnn0 12473 df-z 12487 df-dec 12606 df-uz 12750 df-q 12860 df-rp 12904 df-xneg 13024 df-xadd 13025 df-xmul 13026 df-ioo 13263 df-ioc 13264 df-ico 13265 df-icc 13266 df-fz 13422 df-fzo 13569 df-fl 13710 df-seq 13923 df-exp 13983 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-struct 17072 df-slot 17107 df-ndx 17119 df-base 17135 df-plusg 17188 df-mulr 17189 df-starv 17190 df-tset 17194 df-ple 17195 df-ds 17197 df-unif 17198 df-rest 17340 df-topn 17341 df-topgen 17361 df-psmet 21299 df-xmet 21300 df-met 21301 df-bl 21302 df-mopn 21303 df-cnfld 21308 df-top 22836 df-topon 22853 df-topsp 22875 df-bases 22888 df-cld 22961 df-ntr 22962 df-cls 22963 df-nei 23040 df-lp 23078 df-cn 23169 df-cnp 23170 df-cmp 23329 df-xms 24262 df-ms 24263 df-cncf 24825 df-limc 25821

This theorem is referenced by: fourierdlem96 46388 fourierdlem100 46392 fourierdlem107 46399 fourierdlem109 46401

W3C validator