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 46224

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 46138	. . . . . . . . . . . . 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 8863	. . . . . . . . . 10 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
10		fzossfz 13695	. . . . . . . . . 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 46173	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))})))
16	15	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17		fourierdlem89.c	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
18		fourierdlem89.d	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
19		elioore 13392	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℝ)
21		elioo4g 13423	. . . . . . . . . . . . . . . . . . . . 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 7412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
27	26	eleq1d 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3164	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3426	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4140	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
31		fourierdlem89.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = ((♯‘𝐻) − 1)
32		fourierdlem89.12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
33	32	fveq2i 6879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
34	33	oveq1i 7415	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
35	31, 34	eqtri 2758	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
36		fourierdlem89.s	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
37		isoeq5 7314	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
38	32, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
39	38	iotabii 6516	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
40	36, 39	eqtri 2758	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
41	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40	fourierdlem54 46189	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
42	41	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
43	42	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
44	42	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
45	25	fourierdlem2 46138	. . . . . . . . . . . . . . . 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 8863	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
51		fourierdlem89.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
52		elfzofz 13692	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
53	51, 52	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
54	50, 53	ffvelcdmd 7075	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
55	16, 54	ffvelcdmd 7075	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
56	10, 55	sselid 3956	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0...𝑀))
57	9, 56	ffvelcdmd 7075	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
58	57	rexrd 11285	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
60		fzofzp1 13780	. . . . . . . . . 10 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
61	55, 60	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
62	9, 61	ffvelcdmd 7075	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ)
63	62	rexrd 11285	. . . . . . 7 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
64	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
65	3, 2, 1	fourierdlem11 46147	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
66	65	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	65	simp2d 1143	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
68	66, 67	iccssred 13451	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
69	65	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 < 𝐵)
70	66, 67, 69, 13	fourierdlem17 46153	. . . . . . . . 9 ⊢ (𝜑 → 𝑍:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
71	66, 67, 69, 11, 12	fourierdlem4 46140	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
72	71, 54	ffvelcdmd 7075	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘(𝑆‘𝐽)) ∈ (𝐴(,]𝐵))
73	70, 72	ffvelcdmd 7075	. . . . . . . 8 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ (𝐴[,]𝐵))
74	68, 73	sseldd 3959	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
75	74	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
76	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
77	66	rexrd 11285	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
78		iocssre 13444	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
79	77, 67, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
80		fzofzp1 13780	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
81	51, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
82	50, 81	ffvelcdmd 7075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
83	71, 82	ffvelcdmd 7075	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ (𝐴(,]𝐵))
84	79, 83	sseldd 3959	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
85	47	simprrd 773	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
86		fveq2 6876	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘𝑖) = (𝑆‘𝐽))
87		oveq1 7412	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐽 → (𝑖 + 1) = (𝐽 + 1))
88	87	fveq2d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘(𝑖 + 1)) = (𝑆‘(𝐽 + 1)))
89	86, 88	breq12d 5132	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐽 → ((𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
90	89	rspccva 3600	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
91	85, 51, 90	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
92	54, 82	posdifd 11824	. . . . . . . . . . . . 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 7412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑗 + 1) = (𝐽 + 1))
98	97	fveq2d 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝐽 + 1)))
99	98	fveq2d 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐸‘(𝑆‘(𝐽 + 1))))
100		fveq2 6876	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑆‘𝑗) = (𝑆‘𝐽))
101	100	fveq2d 6880	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘𝑗)) = (𝐸‘(𝑆‘𝐽)))
102	101	fveq2d 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
103	99, 102	oveq12d 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
104	98, 100	oveq12d 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
105	103, 104	eqeq12d 2751	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → (((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
106	96, 105	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))))
107	11	oveq2i 7416	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 · 𝑇) = (𝑘 · (𝐵 − 𝐴))
108	107	oveq2i 7416	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵 − 𝐴)))
109	108	eleq1i 2825	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
110	109	rexbii 3083	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
111	110	rgenw 3055	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
112		rabbi 3446	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
113	111, 112	mpbi 230	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}
114	113	uneq2i 4140	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
115	114	fveq2i 6879	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
116	115	oveq1i 7415	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
117	35, 116	eqtri 2758	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
118		isoeq5 7314	. . . . . . . . . . . . . . . . . 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 6516	. . . . . . . . . . . . . . . 16 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
121	40, 120	eqtri 2758	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
122		eqid 2735	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
123	3, 11, 2, 1, 17, 18, 25, 117, 121, 12, 13, 122	fourierdlem65 46200	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
124	106, 123	vtoclg 3533	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
125	51, 94, 124	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
126	93, 125	breqtrrd 5147	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
127	74, 84	posdifd 11824	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))) ↔ 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽))))))
128	126, 127	mpbird 257	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
129		id 22	. . . . . . . . . . 11 ⊢ (𝜑 → 𝜑)
130	102, 99	oveq12d 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))))
131	100	fveq2d 6880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐼‘(𝑆‘𝑗)) = (𝐼‘(𝑆‘𝐽)))
132	131	fveq2d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
133	131	oveq1d 7420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
134	133	fveq2d 6880	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
135	132, 134	oveq12d 7423	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
136	130, 135	sseq12d 3992	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) ↔ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
137	96, 136	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
138		eqid 2735	. . . . . . . . . . . . . 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 46214	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
140	137, 139	vtoclg 3533	. . . . . . . . . . . 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 46146	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))) ∧ (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
144	143	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
145	144	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
146		neqne 2940	. . . . . . . 8 ⊢ (¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
147	146	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
148	76, 75, 145, 147	leneltd 11389	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑍‘(𝐸‘(𝑆‘𝐽))))
149	143	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
150	74, 84, 62, 128, 149	ltletrd 11395	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
151	150	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
152	59, 64, 75, 148, 151	eliood 45527	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
153		fvres 6895	. . . . 5 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
154	152, 153	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
155	154	eqcomd 2741	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
156	155	ifeq2da 4533	. 2 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))))
157		fourierdlem89.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
158		fdm 6715	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
159	157, 158	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 = ℝ)
160	159	feq2d 6692	. . . . . 6 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:ℝ⟶ℂ))
161	157, 160	mpbird 257	. . . . 5 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
162		ioosscn 13425	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ
163	162	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ)
164		ioossre 13424	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℝ
165	164, 159	sseqtrrid 4002	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ dom 𝐹)
166		fourierdlem89.u	. . . . . . 7 ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))
167	82, 84	resubcld 11665	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
168	166, 167	eqeltrid 2838	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ ℝ)
169	168	recnd 11263	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ ℂ)
170		eqid 2735	. . . . 5 ⊢ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}
171	74, 84, 168	iooshift 45551	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)})
172		ioossre 13424	. . . . . . 7 ⊢ (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ ℝ
173	172, 159	sseqtrrid 4002	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ dom 𝐹)
174	171, 173	eqsstrrd 3994	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} ⊆ dom 𝐹)
175		elioore 13392	. . . . . 6 ⊢ (𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑦 ∈ ℝ)
176	67, 66	resubcld 11665	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
177	11, 176	eqeltrid 2838	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
178	177	recnd 11263	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
179	66, 67	posdifd 11824	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
180	69, 179	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
181	180, 11	breqtrrdi 5161	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑇)
182	181	gt0ne0d 11801	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≠ 0)
183	169, 178, 182	divcan1d 12018	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈 / 𝑇) · 𝑇) = 𝑈)
184	183	eqcomd 2741	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = ((𝑈 / 𝑇) · 𝑇))
185	184	oveq2d 7421	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
186	185	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
187	186	fveq2d 6880	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))))
188	157	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
189	177	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
190	84	recnd 11263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
191	82	recnd 11263	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
192	190, 191	negsubdi2d 11610	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
193	192	eqcomd 2741	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) = -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))
194	193	oveq1d 7420	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
195	166	oveq1i 7415	. . . . . . . . . . . 12 ⊢ (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇)
196	195	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇))
197	12	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
198		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
199		oveq2 7413	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
200	199	oveq1d 7420	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
201	200	fveq2d 6880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
202	201	oveq1d 7420	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
203	198, 202	oveq12d 7423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
204	203	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
205	67, 82	resubcld 11665	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
206	205, 177, 182	redivcld 12069	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
207	206	flcld 13815	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
208	207	zred 12697	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
209	208, 177	remulcld 11265	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
210	82, 209	readdcld 11264	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
211	197, 204, 82, 210	fvmptd 6993	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
212	211	oveq1d 7420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))))
213	208	recnd 11263	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℂ)
214	213, 178	mulcld 11255	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℂ)
215	191, 214	pncan2d 11596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
216	212, 215	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
217	216, 214	eqeltrd 2834	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℂ)
218	217, 178, 182	divnegd 12030	. . . . . . . . . . 11 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
219	194, 196, 218	3eqtr4d 2780	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 / 𝑇) = -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
220	216	oveq1d 7420	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇))
221	213, 178, 182	divcan4d 12023	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
222	220, 221	eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
223	222, 207	eqeltrd 2834	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
224	223	znegcld 12699	. . . . . . . . . 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 45333	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))) = (𝐹‘𝑦))
231	187, 230	eqtrd 2770	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
232	175, 231	sylan2 593	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
233	6	simprrd 773	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
234		fveq2 6876	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘𝑖) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
235		oveq1 7412	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
236	235	fveq2d 6880	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
237	234, 236	breq12d 5132	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
238	237	rspccva 3600	. . . . . . . 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 7423	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
244	243	reseq2d 5966	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
245	243	oveq1d 7420	. . . . . . . . . . 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 3533	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
250	55, 240, 249	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
251		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
252		fourierdlem89.21	. . . . . . . . . . . . 13 ⊢ 𝑉 = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
253		nfmpt1 5220	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑖 ∈ (0..^𝑀) ↦ 𝑅)
254	252, 253	nfcxfr 2896	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖𝑉
255		nfcv 2898	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝐼‘(𝑆‘𝐽))
256	254, 255	nffv 6886	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽)))
257	256	nfel1 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))
258	251, 257	nfim 1896	. . . . . . . . 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 6876	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘𝑖) = (𝑉‘(𝐼‘(𝑆‘𝐽))))
264	263	eqcomd 2741	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
265	264	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
266	259	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑖 ∈ (0..^𝑀))
267		elex 3480	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) → 𝑅 ∈ V)
268	259, 261, 267	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑅 ∈ V)
269	252	fvmpt2 6997	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑅 ∈ V) → (𝑉‘𝑖) = 𝑅)
270	266, 268, 269	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘𝑖) = 𝑅)
271	265, 270	eqtrd 2770	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
272	271	3adant2 1131	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
273	244, 234	oveq12d 7423	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
274	273	eqcomd 2741	. . . . . . . . . . . . 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 3549	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))))
281	55, 240, 280	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
282		eqid 2735	. . . . . . 7 ⊢ if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
283		eqid 2735	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
284	57, 62, 239, 250, 281, 74, 84, 128, 142, 282, 283	fourierdlem32 46168	. . . . . 6 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
285	142	resabs1d 5995	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))))
286	285	oveq1d 7420	. . . . . 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 45657	. . . 4 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)))
289	166	oveq2i 7416	. . . . . . 7 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
290	289	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
291	17, 20	iccssred 13451	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
292		ax-resscn 11186	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
293	291, 292	sstrdi 3971	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℂ)
294	25, 44, 43	fourierdlem15 46151	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
295	294, 53	ffvelcdmd 7075	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐶[,]𝐷))
296	293, 295	sseldd 3959	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℂ)
297	191, 296	subcld 11594	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) ∈ ℂ)
298	74	recnd 11263	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℂ)
299	190, 297, 298	subsub23d 45316	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
300	125, 299	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
301	300	eqcomd 2741	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
302	301	oveq1d 7420	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
303	190, 297	subcld 11594	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) ∈ ℂ)
304	303, 191, 190	addsub12d 11617	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))))
305	190, 297, 190	sub32d 11626	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
306	190	subidd 11582	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = 0)
307	306	oveq1d 7420	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
308		df-neg 11469	. . . . . . . . . 10 ⊢ -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
309	191, 296	negsubdi2d 11610	. . . . . . . . . 10 ⊢ (𝜑 → -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
310	308, 309	eqtr3id 2784	. . . . . . . . 9 ⊢ (𝜑 → (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
311	305, 307, 310	3eqtrd 2774	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
312	311	oveq2d 7421	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))))
313	191, 296	pncan3d 11597	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))) = (𝑆‘𝐽))
314	304, 312, 313	3eqtrd 2774	. . . . . 6 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘𝐽))
315	290, 302, 314	3eqtrd 2774	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = (𝑆‘𝐽))
316	315	oveq2d 7421	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)) = ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
317	288, 316	eleqtrd 2836	. . 3 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
318	166	oveq2i 7416	. . . . . . . 8 ⊢ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
319	190, 191	pncan3d 11597	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘(𝐽 + 1)))
320	318, 319	eqtrid 2782	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = (𝑆‘(𝐽 + 1)))
321	315, 320	oveq12d 7423	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
322	171, 321	eqtr3d 2772	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
323	322	reseq2d 5966	. . . 4 ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) = (𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))))
324	323	oveq1d 7420	. . 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 1540 ∈ wcel 2108 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3415 Vcvv 3459 ∪ cun 3924 ⊆ wss 3926 ifcif 4500 {cpr 4603 class class class wbr 5119 ↦ cmpt 5201 dom cdm 5654 ran crn 5655 ↾ cres 5656 ℩cio 6482 ⟶wf 6527 ‘cfv 6531 Isom wiso 6532 (class class class)co 7405 ↑_m cmap 8840 supcsup 9452 ℂcc 11127 ℝcr 11128 0cc0 11129 1c1 11130 + caddc 11132 · cmul 11134 +∞cpnf 11266 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 − cmin 11466 -cneg 11467 / cdiv 11894 ℕcn 12240 2c2 12295 ℤcz 12588 (,)cioo 13362 (,]cioc 13363 [,)cico 13364 [,]cicc 13365 ...cfz 13524 ..^cfzo 13671 ⌊cfl 13807 ♯chash 14348 ↾_t crest 17434 TopOpenctopn 17435 ℂ_fldccnfld 21315 –cn→ccncf 24820 lim_ℂ climc 25815

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-inf2 9655 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-om 7862 df-1st 7988 df-2nd 7989 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-oadd 8484 df-er 8719 df-map 8842 df-pm 8843 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-dju 9915 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-xnn0 12575 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13366 df-ioc 13367 df-ico 13368 df-icc 13369 df-fz 13525 df-fzo 13672 df-fl 13809 df-seq 14020 df-exp 14080 df-hash 14349 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-struct 17166 df-slot 17201 df-ndx 17213 df-base 17229 df-plusg 17284 df-mulr 17285 df-starv 17286 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-rest 17436 df-topn 17437 df-topgen 17457 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-cnfld 21316 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-cld 22957 df-ntr 22958 df-cls 22959 df-nei 23036 df-lp 23074 df-cn 23165 df-cnp 23166 df-cmp 23325 df-xms 24259 df-ms 24260 df-cncf 24822 df-limc 25819

This theorem is referenced by: fourierdlem96 46231 fourierdlem100 46235 fourierdlem107 46242 fourierdlem109 46244

W3C validator