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 43626

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 43540	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
5	2, 4	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
6	1, 5	mpbid 231	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑄 ∈ (ℝ ↑_m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
7	6	simpld 494	. . . . . . . . . 10 ⊢ (𝜑 → 𝑄 ∈ (ℝ ↑_m (0...𝑀)))
8		elmapi 8595	. . . . . . . . . 10 ⊢ (𝑄 ∈ (ℝ ↑_m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9	7, 8	syl 17	. . . . . . . . 9 ⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
10		fzossfz 13334	. . . . . . . . . 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 43575	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼:ℝ⟶(0..^𝑀) ∧ (𝑥 ∈ ℝ → sup({𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (𝑄‘𝑖) ≤ (𝑍‘(𝐸‘𝑥))})))
16	15	simpld 494	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐼:ℝ⟶(0..^𝑀))
17		fourierdlem89.c	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 ∈ ℝ)
18		fourierdlem89.d	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐷 ∈ (𝐶(,)+∞))
19		elioore 13038	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐷 ∈ (𝐶(,)+∞) → 𝐷 ∈ ℝ)
20	18, 19	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐷 ∈ ℝ)
21		elioo4g 13068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐷 ∈ (𝐶(,)+∞) ↔ ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
22	18, 21	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐶 ∈ ℝ^* ∧ +∞ ∈ ℝ^* ∧ 𝐷 ∈ ℝ) ∧ (𝐶 < 𝐷 ∧ 𝐷 < +∞)))
23	22	simprd 495	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐶 < 𝐷 ∧ 𝐷 < +∞))
24	23	simpld 494	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐶 < 𝐷)
25		fourierdlem89.o	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
26		oveq1 7262	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = 𝑥 → (𝑦 + (𝑘 · 𝑇)) = (𝑥 + (𝑘 · 𝑇)))
27	26	eleq1d 2823	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = 𝑥 → ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
28	27	rexbidv 3225	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑥 → (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄))
29	28	cbvrabv 3416	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}
30	29	uneq2i 4090	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
31		fourierdlem89.n	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑁 = ((♯‘𝐻) − 1)
32		fourierdlem89.12	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})
33	32	fveq2i 6759	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯‘𝐻) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
34	33	oveq1i 7265	. . . . . . . . . . . . . . . . . . 19 ⊢ ((♯‘𝐻) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
35	31, 34	eqtri 2766	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1)
36		fourierdlem89.s	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
37		isoeq5 7172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐻 = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) → (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
38	32, 37	ax-mp 5	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
39	38	iotabii 6403	. . . . . . . . . . . . . . . . . . 19 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
40	36, 39	eqtri 2766	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})))
41	11, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40	fourierdlem54 43591	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))))
42	41	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)))
43	42	simprd 495	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁))
44	42	simpld 494	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑁 ∈ ℕ)
45	25	fourierdlem2 43540	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
46	44, 45	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))))
47	43, 46	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ∈ (ℝ ↑_m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))
48	47	simpld 494	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆 ∈ (ℝ ↑_m (0...𝑁)))
49		elmapi 8595	. . . . . . . . . . . . 13 ⊢ (𝑆 ∈ (ℝ ↑_m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
50	48, 49	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ)
51		fourierdlem89.j	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 ∈ (0..^𝑁))
52		elfzofz 13331	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
53	51, 52	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐽 ∈ (0...𝑁))
54	50, 53	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ)
55	16, 54	ffvelrnd 6944	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
56	10, 55	sselid 3915	. . . . . . . . 9 ⊢ (𝜑 → (𝐼‘(𝑆‘𝐽)) ∈ (0...𝑀))
57	9, 56	ffvelrnd 6944	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
58	57	rexrd 10956	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
59	58	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ^*)
60		fzofzp1 13412	. . . . . . . . . 10 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
61	55, 60	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝐼‘(𝑆‘𝐽)) + 1) ∈ (0...𝑀))
62	9, 61	ffvelrnd 6944	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ)
63	62	rexrd 10956	. . . . . . 7 ⊢ (𝜑 → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
64	63	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)) ∈ ℝ^*)
65	3, 2, 1	fourierdlem11 43549	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
66	65	simp1d 1140	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
67	65	simp2d 1141	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
68	66, 67	iccssred 13095	. . . . . . . 8 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ ℝ)
69	65	simp3d 1142	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 < 𝐵)
70	66, 67, 69, 13	fourierdlem17 43555	. . . . . . . . 9 ⊢ (𝜑 → 𝑍:(𝐴(,]𝐵)⟶(𝐴[,]𝐵))
71	66, 67, 69, 11, 12	fourierdlem4 43542	. . . . . . . . . 10 ⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵))
72	71, 54	ffvelrnd 6944	. . . . . . . . 9 ⊢ (𝜑 → (𝐸‘(𝑆‘𝐽)) ∈ (𝐴(,]𝐵))
73	70, 72	ffvelrnd 6944	. . . . . . . 8 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ (𝐴[,]𝐵))
74	68, 73	sseldd 3918	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
75	74	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℝ)
76	57	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ∈ ℝ)
77	66	rexrd 10956	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐴 ∈ ℝ^*)
78		iocssre 13088	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
79	77, 67, 78	syl2anc 583	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
80		fzofzp1 13412	. . . . . . . . . . . . . 14 ⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
81	51, 80	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
82	50, 81	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
83	71, 82	ffvelrnd 6944	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ (𝐴(,]𝐵))
84	79, 83	sseldd 3918	. . . . . . . . . 10 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
85	47	simprrd 770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
86		fveq2 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘𝑖) = (𝑆‘𝐽))
87		oveq1 7262	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 = 𝐽 → (𝑖 + 1) = (𝐽 + 1))
88	87	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝐽 → (𝑆‘(𝑖 + 1)) = (𝑆‘(𝐽 + 1)))
89	86, 88	breq12d 5083	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝐽 → ((𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))))
90	89	rspccva 3551	. . . . . . . . . . . . . 14 ⊢ ((∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)) ∧ 𝐽 ∈ (0..^𝑁)) → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
91	85, 51, 90	syl2anc 583	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))
92	54, 82	posdifd 11492	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑆‘𝐽) < (𝑆‘(𝐽 + 1)) ↔ 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
93	91, 92	mpbid 231	. . . . . . . . . . . 12 ⊢ (𝜑 → 0 < ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
94	51	ancli 548	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝜑 ∧ 𝐽 ∈ (0..^𝑁)))
95		eleq1 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑗 ∈ (0..^𝑁) ↔ 𝐽 ∈ (0..^𝑁)))
96	95	anbi2d 628	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ↔ (𝜑 ∧ 𝐽 ∈ (0..^𝑁))))
97		oveq1 7262	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑗 + 1) = (𝐽 + 1))
98	97	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝑆‘(𝑗 + 1)) = (𝑆‘(𝐽 + 1)))
99	98	fveq2d 6760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘(𝑗 + 1))) = (𝐸‘(𝑆‘(𝐽 + 1))))
100		fveq2 6756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝐽 → (𝑆‘𝑗) = (𝑆‘𝐽))
101	100	fveq2d 6760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝐽 → (𝐸‘(𝑆‘𝑗)) = (𝐸‘(𝑆‘𝐽)))
102	101	fveq2d 6760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝑍‘(𝐸‘(𝑆‘𝑗))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
103	99, 102	oveq12d 7273	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
104	98, 100	oveq12d 7273	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
105	103, 104	eqeq12d 2754	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → (((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
106	96, 105	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))))
107	11	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑘 · 𝑇) = (𝑘 · (𝐵 − 𝐴))
108	107	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 + (𝑘 · 𝑇)) = (𝑦 + (𝑘 · (𝐵 − 𝐴)))
109	108	eleq1i 2829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
110	109	rexbii 3177	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
111	110	rgenw 3075	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄)
112		rabbi 3309	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∀𝑦 ∈ (𝐶[,]𝐷)(∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
113	111, 112	mpbi 229	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}
114	113	uneq2i 4090	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}) = ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})
115	114	fveq2i 6759	. . . . . . . . . . . . . . . . 17 ⊢ (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) = (♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄}))
116	115	oveq1i 7265	. . . . . . . . . . . . . . . 16 ⊢ ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄})) − 1) = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
117	35, 116	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ 𝑁 = ((♯‘({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})) − 1)
118		isoeq5 7172	. . . . . . . . . . . . . . . . . 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 6403	. . . . . . . . . . . . . . . 16 ⊢ (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
121	40, 120	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐶, 𝐷} ∪ {𝑦 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑦 + (𝑘 · (𝐵 − 𝐴))) ∈ ran 𝑄})))
122		eqid 2738	. . . . . . . . . . . . . . 15 ⊢ ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗)))) = ((𝑆‘𝑗) + (𝐵 − (𝐸‘(𝑆‘𝑗))))
123	3, 11, 2, 1, 17, 18, 25, 117, 121, 12, 13, 122	fourierdlem65 43602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝑗 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝑗)))) = ((𝑆‘(𝑗 + 1)) − (𝑆‘𝑗)))
124	106, 123	vtoclg 3495	. . . . . . . . . . . . 13 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
125	51, 94, 124	sylc 65	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
126	93, 125	breqtrrd 5098	. . . . . . . . . . 11 ⊢ (𝜑 → 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))))
127	74, 84	posdifd 11492	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))) ↔ 0 < ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽))))))
128	126, 127	mpbird 256	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝐸‘(𝑆‘(𝐽 + 1))))
129		id 22	. . . . . . . . . . 11 ⊢ (𝜑 → 𝜑)
130	102, 99	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) = ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))))
131	100	fveq2d 6760	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → (𝐼‘(𝑆‘𝑗)) = (𝐼‘(𝑆‘𝐽)))
132	131	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘(𝐼‘(𝑆‘𝑗))) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
133	131	oveq1d 7270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 = 𝐽 → ((𝐼‘(𝑆‘𝑗)) + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
134	133	fveq2d 6760	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 = 𝐽 → (𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
135	132, 134	oveq12d 7273	. . . . . . . . . . . . . . 15 ⊢ (𝑗 = 𝐽 → ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
136	130, 135	sseq12d 3950	. . . . . . . . . . . . . 14 ⊢ (𝑗 = 𝐽 → (((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))) ↔ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
137	96, 136	imbi12d 344	. . . . . . . . . . . . 13 ⊢ (𝑗 = 𝐽 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1)))) ↔ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))))
138		eqid 2738	. . . . . . . . . . . . . 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 43616	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝑗)))(,)(𝐸‘(𝑆‘(𝑗 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝑗)))(,)(𝑄‘((𝐼‘(𝑆‘𝑗)) + 1))))
140	137, 139	vtoclg 3495	. . . . . . . . . . . 12 ⊢ (𝐽 ∈ (0..^𝑁) → ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
141	140	anabsi7 667	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐽 ∈ (0..^𝑁)) → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
142	129, 51, 141	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
143	57, 62, 74, 84, 128, 142	fourierdlem10 43548	. . . . . . . . 9 ⊢ (𝜑 → ((𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))) ∧ (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
144	143	simpld 494	. . . . . . . 8 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
145	144	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) ≤ (𝑍‘(𝐸‘(𝑆‘𝐽))))
146		neqne 2950	. . . . . . . 8 ⊢ (¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
147	146	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ≠ (𝑄‘(𝐼‘(𝑆‘𝐽))))
148	76, 75, 145, 147	leneltd 11059	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑍‘(𝐸‘(𝑆‘𝐽))))
149	143	simprd 495	. . . . . . . 8 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
150	74, 84, 62, 128, 149	ltletrd 11065	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
151	150	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
152	59, 64, 75, 148, 151	eliood 42926	. . . . 5 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
153		fvres 6775	. . . . 5 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
154	152, 153	syl 17	. . . 4 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
155	154	eqcomd 2744	. . 3 ⊢ ((𝜑 ∧ ¬ (𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽)))) → (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
156	155	ifeq2da 4488	. 2 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))))
157		fourierdlem89.f	. . . . . 6 ⊢ (𝜑 → 𝐹:ℝ⟶ℂ)
158		fdm 6593	. . . . . . . 8 ⊢ (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
159	157, 158	syl 17	. . . . . . 7 ⊢ (𝜑 → dom 𝐹 = ℝ)
160	159	feq2d 6570	. . . . . 6 ⊢ (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:ℝ⟶ℂ))
161	157, 160	mpbird 256	. . . . 5 ⊢ (𝜑 → 𝐹:dom 𝐹⟶ℂ)
162		ioosscn 13070	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ
163	162	a1i 11	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℂ)
164		ioossre 13069	. . . . . 6 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ ℝ
165	164, 159	sseqtrrid 3970	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) ⊆ dom 𝐹)
166		fourierdlem89.u	. . . . . . 7 ⊢ 𝑈 = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))
167	82, 84	resubcld 11333	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
168	166, 167	eqeltrid 2843	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ ℝ)
169	168	recnd 10934	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ ℂ)
170		eqid 2738	. . . . 5 ⊢ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}
171	74, 84, 168	iooshift 42950	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)})
172		ioossre 13069	. . . . . . 7 ⊢ (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ ℝ
173	172, 159	sseqtrrid 3970	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) ⊆ dom 𝐹)
174	171, 173	eqsstrrd 3956	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} ⊆ dom 𝐹)
175		elioore 13038	. . . . . 6 ⊢ (𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑦 ∈ ℝ)
176	67, 66	resubcld 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ)
177	11, 176	eqeltrid 2843	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑇 ∈ ℝ)
178	177	recnd 10934	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ∈ ℂ)
179	66, 67	posdifd 11492	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴)))
180	69, 179	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 0 < (𝐵 − 𝐴))
181	180, 11	breqtrrdi 5112	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 < 𝑇)
182	181	gt0ne0d 11469	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑇 ≠ 0)
183	169, 178, 182	divcan1d 11682	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑈 / 𝑇) · 𝑇) = 𝑈)
184	183	eqcomd 2744	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 = ((𝑈 / 𝑇) · 𝑇))
185	184	oveq2d 7271	. . . . . . . . 9 ⊢ (𝜑 → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
186	185	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑦 + 𝑈) = (𝑦 + ((𝑈 / 𝑇) · 𝑇)))
187	186	fveq2d 6760	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))))
188	157	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝐹:ℝ⟶ℂ)
189	177	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑇 ∈ ℝ)
190	84	recnd 10934	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
191	82	recnd 10934	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
192	190, 191	negsubdi2d 11278	. . . . . . . . . . . . 13 ⊢ (𝜑 → -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
193	192	eqcomd 2744	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) = -((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))
194	193	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
195	166	oveq1i 7265	. . . . . . . . . . . 12 ⊢ (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇)
196	195	a1i 11	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑈 / 𝑇) = (((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))) / 𝑇))
197	12	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))))
198		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
199		oveq2 7263	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
200	199	oveq1d 7270	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
201	200	fveq2d 6760	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
202	201	oveq1d 7270	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
203	198, 202	oveq12d 7273	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
204	203	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
205	67, 82	resubcld 11333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
206	205, 177, 182	redivcld 11733	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
207	206	flcld 13446	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
208	207	zred 12355	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
209	208, 177	remulcld 10936	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
210	82, 209	readdcld 10935	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
211	197, 204, 82, 210	fvmptd 6864	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
212	211	oveq1d 7270	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))))
213	208	recnd 10934	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℂ)
214	213, 178	mulcld 10926	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℂ)
215	191, 214	pncan2d 11264	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
216	212, 215	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
217	216, 214	eqeltrd 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℂ)
218	217, 178, 182	divnegd 11694	. . . . . . . . . . 11 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (-((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
219	194, 196, 218	3eqtr4d 2788	. . . . . . . . . 10 ⊢ (𝜑 → (𝑈 / 𝑇) = -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇))
220	216	oveq1d 7270	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇))
221	213, 178, 182	divcan4d 11687	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
222	220, 221	eqtrd 2778	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
223	222, 207	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
224	223	znegcld 12357	. . . . . . . . . 10 ⊢ (𝜑 → -(((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℤ)
225	219, 224	eqeltrd 2839	. . . . . . . . 9 ⊢ (𝜑 → (𝑈 / 𝑇) ∈ ℤ)
226	225	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝑈 / 𝑇) ∈ ℤ)
227		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
228		fourierdlem89.per	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
229	228	adantlr 711	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℝ) ∧ 𝑥 ∈ ℝ) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
230	188, 189, 226, 227, 229	fperiodmul 42733	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + ((𝑈 / 𝑇) · 𝑇))) = (𝐹‘𝑦))
231	187, 230	eqtrd 2778	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ ℝ) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
232	175, 231	sylan2 592	. . . . 5 ⊢ ((𝜑 ∧ 𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) → (𝐹‘(𝑦 + 𝑈)) = (𝐹‘𝑦))
233	6	simprrd 770	. . . . . . . 8 ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
234		fveq2 6756	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘𝑖) = (𝑄‘(𝐼‘(𝑆‘𝐽))))
235		oveq1 7262	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 + 1) = ((𝐼‘(𝑆‘𝐽)) + 1))
236	235	fveq2d 6760	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑄‘(𝑖 + 1)) = (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
237	234, 236	breq12d 5083	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
238	237	rspccva 3551	. . . . . . . 8 ⊢ ((∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)) ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
239	233, 55, 238	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → (𝑄‘(𝐼‘(𝑆‘𝐽))) < (𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))
240	55	ancli 548	. . . . . . . 8 ⊢ (𝜑 → (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
241		eleq1 2826	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑖 ∈ (0..^𝑀) ↔ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)))
242	241	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ↔ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))))
243	234, 236	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
244	243	reseq2d 5880	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))))
245	243	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ) = (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
246	244, 245	eleq12d 2833	. . . . . . . . . 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 3495	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ)))
250	55, 240, 249	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ∈ (((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))–cn→ℂ))
251		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))
252		fourierdlem89.21	. . . . . . . . . . . . 13 ⊢ 𝑉 = (𝑖 ∈ (0..^𝑀) ↦ 𝑅)
253		nfmpt1 5178	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑖 ∈ (0..^𝑀) ↦ 𝑅)
254	252, 253	nfcxfr 2904	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖𝑉
255		nfcv 2906	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖(𝐼‘(𝑆‘𝐽))
256	254, 255	nffv 6766	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽)))
257	256	nfel1 2922	. . . . . . . . . 10 ⊢ Ⅎ𝑖(𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))
258	251, 257	nfim 1900	. . . . . . . . 9 ⊢ Ⅎ𝑖((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
259	242	biimpar 477	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))
260	259	3adant2 1129	. . . . . . . . . . . . 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 6756	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘𝑖) = (𝑉‘(𝐼‘(𝑆‘𝐽))))
264	263	eqcomd 2744	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
265	264	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = (𝑉‘𝑖))
266	259	simprd 495	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑖 ∈ (0..^𝑀))
267		elex 3440	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) → 𝑅 ∈ V)
268	259, 261, 267	3syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → 𝑅 ∈ V)
269	252	fvmpt2 6868	. . . . . . . . . . . . . . 15 ⊢ ((𝑖 ∈ (0..^𝑀) ∧ 𝑅 ∈ V) → (𝑉‘𝑖) = 𝑅)
270	266, 268, 269	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘𝑖) = 𝑅)
271	265, 270	eqtrd 2778	. . . . . . . . . . . . 13 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
272	271	3adant2 1129	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) = 𝑅)
273	244, 234	oveq12d 7273	. . . . . . . . . . . . . 14 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)) = ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
274	273	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
275	274	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))
276	262, 272, 275	3eltr4d 2854	. . . . . . . . . . 11 ⊢ ((𝑖 = (𝐼‘(𝑆‘𝐽)) ∧ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ∧ (𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀))) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
277	276	3exp 1117	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))))
278	261	2a1i 12	. . . . . . . . . 10 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))) → ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖)))))
279	277, 278	impbid 211	. . . . . . . . 9 ⊢ (𝑖 = (𝐼‘(𝑆‘𝐽)) → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) lim_ℂ (𝑄‘𝑖))) ↔ ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))))
280	258, 279, 261	vtoclg1f 3494	. . . . . . . 8 ⊢ ((𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀) → ((𝜑 ∧ (𝐼‘(𝑆‘𝐽)) ∈ (0..^𝑀)) → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽))))))
281	55, 240, 280	sylc 65	. . . . . . 7 ⊢ (𝜑 → (𝑉‘(𝐼‘(𝑆‘𝐽))) ∈ ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) lim_ℂ (𝑄‘(𝐼‘(𝑆‘𝐽)))))
282		eqid 2738	. . . . . . 7 ⊢ if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) = if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽)))))
283		eqid 2738	. . . . . . 7 ⊢ ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) = ((TopOpen‘ℂ_fld) ↾_t ((𝑄‘(𝐼‘(𝑆‘𝐽)))[,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))
284	57, 62, 239, 250, 281, 74, 84, 128, 142, 282, 283	fourierdlem32 43570	. . . . . 6 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
285	142	resabs1d 5911	. . . . . . 7 ⊢ (𝜑 → ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) = (𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))))
286	285	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → (((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1)))) ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
287	284, 286	eleqtrd 2841	. . . . 5 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))) lim_ℂ (𝑍‘(𝐸‘(𝑆‘𝐽)))))
288	161, 163, 165, 169, 170, 174, 232, 287	limcperiod 43059	. . . 4 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)))
289	166	oveq2i 7266	. . . . . . 7 ⊢ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
290	289	a1i 11	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
291	17, 20	iccssred 13095	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℝ)
292		ax-resscn 10859	. . . . . . . . . . . . 13 ⊢ ℝ ⊆ ℂ
293	291, 292	sstrdi 3929	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶[,]𝐷) ⊆ ℂ)
294	25, 44, 43	fourierdlem15 43553	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
295	294, 53	ffvelrnd 6944	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝐽) ∈ (𝐶[,]𝐷))
296	293, 295	sseldd 3918	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑆‘𝐽) ∈ ℂ)
297	191, 296	subcld 11262	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) ∈ ℂ)
298	74	recnd 10934	. . . . . . . . . 10 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) ∈ ℂ)
299	190, 297, 298	subsub23d 42715	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))) ↔ ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑍‘(𝐸‘(𝑆‘𝐽)))) = ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
300	125, 299	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (𝑍‘(𝐸‘(𝑆‘𝐽))))
301	300	eqcomd 2744	. . . . . . 7 ⊢ (𝜑 → (𝑍‘(𝐸‘(𝑆‘𝐽))) = ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
302	301	oveq1d 7270	. . . . . 6 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))))
303	190, 297	subcld 11262	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) ∈ ℂ)
304	303, 191, 190	addsub12d 11285	. . . . . . 7 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))))
305	190, 297, 190	sub32d 11294	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
306	190	subidd 11250	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = 0)
307	306	oveq1d 7270	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − (𝐸‘(𝑆‘(𝐽 + 1)))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))))
308		df-neg 11138	. . . . . . . . . 10 ⊢ -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)))
309	191, 296	negsubdi2d 11278	. . . . . . . . . 10 ⊢ (𝜑 → -((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽)) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
310	308, 309	eqtr3id 2793	. . . . . . . . 9 ⊢ (𝜑 → (0 − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
311	305, 307, 310	3eqtrd 2782	. . . . . . . 8 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1)))) = ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1))))
312	311	oveq2d 7271	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) − (𝐸‘(𝑆‘(𝐽 + 1))))) = ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))))
313	191, 296	pncan3d 11265	. . . . . . 7 ⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((𝑆‘𝐽) − (𝑆‘(𝐽 + 1)))) = (𝑆‘𝐽))
314	304, 312, 313	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → (((𝐸‘(𝑆‘(𝐽 + 1))) − ((𝑆‘(𝐽 + 1)) − (𝑆‘𝐽))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘𝐽))
315	290, 302, 314	3eqtrd 2782	. . . . 5 ⊢ (𝜑 → ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈) = (𝑆‘𝐽))
316	315	oveq2d 7271	. . . 4 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ ((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)) = ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
317	288, 316	eleqtrd 2841	. . 3 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)))
318	166	oveq2i 7266	. . . . . . . 8 ⊢ ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1)))))
319	190, 191	pncan3d 11265	. . . . . . . 8 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + ((𝑆‘(𝐽 + 1)) − (𝐸‘(𝑆‘(𝐽 + 1))))) = (𝑆‘(𝐽 + 1)))
320	318, 319	syl5eq 2791	. . . . . . 7 ⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈) = (𝑆‘(𝐽 + 1)))
321	315, 320	oveq12d 7273	. . . . . 6 ⊢ (𝜑 → (((𝑍‘(𝐸‘(𝑆‘𝐽))) + 𝑈)(,)((𝐸‘(𝑆‘(𝐽 + 1))) + 𝑈)) = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
322	171, 321	eqtr3d 2780	. . . . 5 ⊢ (𝜑 → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)} = ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))))
323	322	reseq2d 5880	. . . 4 ⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) = (𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))))
324	323	oveq1d 7270	. . 3 ⊢ (𝜑 → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑍‘(𝐸‘(𝑆‘𝐽)))(,)(𝐸‘(𝑆‘(𝐽 + 1))))𝑥 = (𝑦 + 𝑈)}) lim_ℂ (𝑆‘𝐽)) = ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))
325	317, 324	eleqtrd 2841	. 2 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), ((𝐹 ↾ ((𝑄‘(𝐼‘(𝑆‘𝐽)))(,)(𝑄‘((𝐼‘(𝑆‘𝐽)) + 1))))‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))
326	156, 325	eqeltrd 2839	1 ⊢ (𝜑 → if((𝑍‘(𝐸‘(𝑆‘𝐽))) = (𝑄‘(𝐼‘(𝑆‘𝐽))), (𝑉‘(𝐼‘(𝑆‘𝐽))), (𝐹‘(𝑍‘(𝐸‘(𝑆‘𝐽))))) ∈ ((𝐹 ↾ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1)))) lim_ℂ (𝑆‘𝐽)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 Vcvv 3422 ∪ cun 3881 ⊆ wss 3883 ifcif 4456 {cpr 4560 class class class wbr 5070 ↦ cmpt 5153 dom cdm 5580 ran crn 5581 ↾ cres 5582 ℩cio 6374 ⟶wf 6414 ‘cfv 6418 Isom wiso 6419 (class class class)co 7255 ↑_m cmap 8573 supcsup 9129 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 +∞cpnf 10937 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 -cneg 11136 / cdiv 11562 ℕcn 11903 2c2 11958 ℤcz 12249 (,)cioo 13008 (,]cioc 13009 [,)cico 13010 [,]cicc 13011 ...cfz 13168 ..^cfzo 13311 ⌊cfl 13438 ♯chash 13972 ↾_t crest 17048 TopOpenctopn 17049 ℂ_fldccnfld 20510 –cn→ccncf 23945 lim_ℂ climc 24931

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-xnn0 12236 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-struct 16776 df-slot 16811 df-ndx 16823 df-base 16841 df-plusg 16901 df-mulr 16902 df-starv 16903 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-rest 17050 df-topn 17051 df-topgen 17071 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-cn 22286 df-cnp 22287 df-cmp 22446 df-xms 23381 df-ms 23382 df-cncf 23947 df-limc 24935

This theorem is referenced by: fourierdlem96 43633 fourierdlem100 43637 fourierdlem107 43644 fourierdlem109 43646

W3C validator