fourierdlem86 - Mathbox for Glauco Siliprandi

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

Theorem fourierdlem86 47171

Description: Continuity of 𝑂 and its limits with respect to the 𝑆 partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
fourierdlem86.f	⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
fourierdlem86.xre	⊢ (𝜑 → 𝑋 ∈ ℝ)
fourierdlem86.p	⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem86.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
fourierdlem86.v	⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
fourierdlem86.fcn	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
fourierdlem86.r	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
fourierdlem86.l	⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
fourierdlem86.a	⊢ (𝜑 → 𝐴 ∈ ℝ)
fourierdlem86.b	⊢ (𝜑 → 𝐵 ∈ ℝ)
fourierdlem86.altb	⊢ (𝜑 → 𝐴 < 𝐵)
fourierdlem86.ab	⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
fourierdlem86.n0	⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
fourierdlem86.c	⊢ (𝜑 → 𝐶 ∈ ℝ)
fourierdlem86.o	⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
fourierdlem86.q	⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
fourierdlem86.t	⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
fourierdlem86.n	⊢ 𝑁 = ((♯‘𝑇) − 1)
fourierdlem86.s	⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
fourierdlem86.d	⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
fourierdlem86.e	⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
fourierdlem86.u	⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))

**Assertion**
Ref	Expression
fourierdlem86	⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Distinct variable groups: 𝐴,𝑠 𝐵,𝑠 𝐶,𝑖,𝑠 𝑖,𝐹,𝑠 𝐿,𝑠 𝑖,𝑀,𝑚,𝑝 𝑗,𝑀,𝑠,𝑖 𝑓,𝑁 𝑖,𝑁,𝑠 𝑖,𝑂 𝑄,𝑖,𝑠 𝑅,𝑠 𝑆,𝑓 𝑆,𝑖,𝑠 𝑇,𝑓 𝑈,𝑖 𝑖,𝑉,𝑝 𝑗,𝑉,𝑠 𝑖,𝑋,𝑚,𝑝 𝑗,𝑋,𝑠 𝑓,𝑗,𝜑 𝜑,𝑖,𝑠 Allowed substitution hints: 𝜑(𝑚, 𝑝) 𝐴(𝑓, 𝑖, 𝑗, 𝑚, 𝑝) 𝐵(𝑓, 𝑖, 𝑗, 𝑚, 𝑝) 𝐶(𝑓, 𝑗, 𝑚, 𝑝) 𝐷(𝑓, 𝑖, 𝑗, 𝑚, 𝑠, 𝑝) 𝑃(𝑓, 𝑖, 𝑗, 𝑚, 𝑠, 𝑝) 𝑄(𝑓, 𝑗, 𝑚, 𝑝) 𝑅(𝑓, 𝑖, 𝑗, 𝑚, 𝑝) 𝑆(𝑗, 𝑚, 𝑝) 𝑇(𝑖, 𝑗, 𝑚, 𝑠, 𝑝) 𝑈(𝑓, 𝑗, 𝑚, 𝑠, 𝑝) 𝐸(𝑓, 𝑖, 𝑗, 𝑚, 𝑠, 𝑝) 𝐹(𝑓, 𝑗, 𝑚, 𝑝) 𝐿(𝑓, 𝑖, 𝑗, 𝑚, 𝑝) 𝑀(𝑓) 𝑁(𝑗, 𝑚, 𝑝) 𝑂(𝑓, 𝑗, 𝑚, 𝑠, 𝑝) 𝑉(𝑓, 𝑚) 𝑋(𝑓)

Proof of Theorem fourierdlem86 Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fourierdlem86.d	. . 3 ⊢ 𝐷 = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
2		fourierdlem86.xre	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ ℝ)
3	2	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑋 ∈ ℝ)
4		fourierdlem86.p	. . . . . . . 8 ⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑_m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
5		fourierdlem86.m	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ∈ ℕ)
6	5	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑀 ∈ ℕ)
7		fourierdlem86.v	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀))
8	7	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑉 ∈ (𝑃‘𝑀))
9		fourierdlem86.a	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℝ)
10	9	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 ∈ ℝ)
11		fourierdlem86.b	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℝ)
12	11	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐵 ∈ ℝ)
13		fourierdlem86.altb	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 < 𝐵)
14	13	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐴 < 𝐵)
15		fourierdlem86.ab	. . . . . . . . 9 ⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π))
16	15	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝐴[,]𝐵) ⊆ (-π[,]π))
17		fourierdlem86.q	. . . . . . . 8 ⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))
18		fourierdlem86.t	. . . . . . . 8 ⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))
19		fourierdlem86.n	. . . . . . . 8 ⊢ 𝑁 = ((♯‘𝑇) − 1)
20		fourierdlem86.s	. . . . . . . 8 ⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇))
21		simpr 490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑗 ∈ (0..^𝑁))
22		fourierdlem86.u	. . . . . . . 8 ⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
23		biid 264	. . . . . . . 8 ⊢ ((((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑦)(,)(𝑄‘(𝑦 + 1)))) ↔ (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑦 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑦)(,)(𝑄‘(𝑦 + 1)))))
24	3, 4, 6, 8, 10, 12, 14, 16, 17, 18, 19, 20, 21, 22, 23	fourierdlem50 47135	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))))
25	24	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝑈 ∈ (0..^𝑀))
26		id 23	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝜑 ∧ 𝑗 ∈ (0..^𝑁)))
27	24	simprd 501	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))
28	26, 25, 27	jca31 524	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))))
29		nfv 1947	. . . . . . . 8 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))
30		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1))
31		nfcsb1v 3871	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖⦋𝑈 / 𝑖⦌𝐿
32		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))
33	30, 31, 32	nfif 4513	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1)))))
34		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖 −
35		nfcv 2923	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖𝐶
36	33, 34, 35	nfov 7448	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶)
37		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖 /
38		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑆‘(𝑗 + 1))
39	36, 37, 38	nfov 7448	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1)))
40		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖 ·
41		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))
42	39, 40, 41	nfov 7448	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
43	42	nfel1 2939	. . . . . . . . . 10 ⊢ Ⅎ𝑖(((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1)))
44		nfv 1947	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝑆‘𝑗) = (𝑄‘𝑈)
45		nfcsb1v 3871	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖⦋𝑈 / 𝑖⦌𝑅
46		nfcv 2923	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑖(𝐹‘(𝑋 + (𝑆‘𝑗)))
47	44, 45, 46	nfif 4513	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑖if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗))))
48	47, 34, 35	nfov 7448	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶)
49		nfcv 2923	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑖(𝑆‘𝑗)
50	48, 37, 49	nfov 7448	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗))
51		nfcv 2923	. . . . . . . . . . . 12 ⊢ Ⅎ𝑖((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))
52	50, 40, 51	nfov 7448	. . . . . . . . . . 11 ⊢ Ⅎ𝑖(((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
53	52	nfel1 2939	. . . . . . . . . 10 ⊢ Ⅎ𝑖(((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))
54	43, 53	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑖((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
55		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)
56	54, 55	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑖(((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
57	29, 56	nfim 1929	. . . . . . 7 ⊢ Ⅎ𝑖((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
58		eleq1 2849	. . . . . . . . . 10 ⊢ (𝑖 = 𝑈 → (𝑖 ∈ (0..^𝑀) ↔ 𝑈 ∈ (0..^𝑀)))
59	58	anbi2d 642	. . . . . . . . 9 ⊢ (𝑖 = 𝑈 → (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ↔ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀))))
60		fveq2 6883	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑈 → (𝑄‘𝑖) = (𝑄‘𝑈))
61		oveq1 7425	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1))
62	61	fveq2d 6887	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1)))
63	60, 62	oveq12d 7436	. . . . . . . . . 10 ⊢ (𝑖 = 𝑈 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))
64	63	sseq2d 3963	. . . . . . . . 9 ⊢ (𝑖 = 𝑈 → (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))))
65	59, 64	anbi12d 644	. . . . . . . 8 ⊢ (𝑖 = 𝑈 → ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))))
66	62	eqeq2d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑈 → ((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)) ↔ (𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1))))
67		csbeq1a 3861	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑈 → 𝐿 = ⦋𝑈 / 𝑖⦌𝐿)
68	66, 67	ifbieq1d 4507	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑈 → if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) = if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))))
69	68	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑈 → (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) = (if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶))
70	69	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑈 → ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) = ((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))))
71	70	oveq1d 7433	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑈 → (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))))
72	71	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑖 = 𝑈 → ((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ↔ (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1)))))
73	60	eqeq2d 2772	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑈 → ((𝑆‘𝑗) = (𝑄‘𝑖) ↔ (𝑆‘𝑗) = (𝑄‘𝑈)))
74		csbeq1a 3861	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑈 → 𝑅 = ⦋𝑈 / 𝑖⦌𝑅)
75	73, 74	ifbieq1d 4507	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑈 → if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) = if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))))
76	75	oveq1d 7433	. . . . . . . . . . . . 13 ⊢ (𝑖 = 𝑈 → (if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) = (if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶))
77	76	oveq1d 7433	. . . . . . . . . . . 12 ⊢ (𝑖 = 𝑈 → ((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) = ((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)))
78	77	oveq1d 7433	. . . . . . . . . . 11 ⊢ (𝑖 = 𝑈 → (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) = (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))))
79	78	eleq1d 2846	. . . . . . . . . 10 ⊢ (𝑖 = 𝑈 → ((((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)) ↔ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))))
80	72, 79	anbi12d 644	. . . . . . . . 9 ⊢ (𝑖 = 𝑈 → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ↔ ((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))))
81	80	anbi1d 643	. . . . . . . 8 ⊢ (𝑖 = 𝑈 → ((((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)) ↔ (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))))
82	65, 81	imbi12d 347	. . . . . . 7 ⊢ (𝑖 = 𝑈 → (((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))) ↔ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))))
83		fourierdlem86.f	. . . . . . . 8 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
84		fourierdlem86.fcn	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) ∈ (((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))–cn→ℂ))
85		fourierdlem86.r	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘𝑖)))
86		fourierdlem86.l	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑉‘𝑖)(,)(𝑉‘(𝑖 + 1)))) lim_ℂ (𝑉‘(𝑖 + 1))))
87		fourierdlem86.n0	. . . . . . . 8 ⊢ (𝜑 → ¬ 0 ∈ (𝐴[,]𝐵))
88		fourierdlem86.c	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ ℝ)
89		fourierdlem86.o	. . . . . . . 8 ⊢ 𝑂 = (𝑠 ∈ (𝐴[,]𝐵) ↦ ((((𝐹‘(𝑋 + 𝑠)) − 𝐶) / 𝑠) · (𝑠 / (2 · (sin‘(𝑠 / 2))))))
90		eqid 2761	. . . . . . . 8 ⊢ (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) = (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2)))))
91		eqid 2761	. . . . . . . 8 ⊢ (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) = (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
92		biid 264	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ↔ (((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
93	83, 2, 4, 5, 7, 84, 85, 86, 9, 11, 13, 15, 87, 88, 89, 17, 18, 19, 20, 90, 91, 92	fourierdlem76 47161	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑖), 𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
94	57, 82, 93	vtoclg1f 3531	. . . . . 6 ⊢ (𝑈 ∈ (0..^𝑀) → ((((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) ∧ 𝑈 ∈ (0..^𝑀)) ∧ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))))
95	25, 28, 94	sylc 66	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))
96	95	simpld 500	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))))
97	96	simpld 500	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((if((𝑆‘(𝑗 + 1)) = (𝑄‘(𝑈 + 1)), ⦋𝑈 / 𝑖⦌𝐿, (𝐹‘(𝑋 + (𝑆‘(𝑗 + 1))))) − 𝐶) / (𝑆‘(𝑗 + 1))) · ((𝑆‘(𝑗 + 1)) / (2 · (sin‘((𝑆‘(𝑗 + 1)) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
98	1, 97	eqeltrid 2865	. 2 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))))
99		fourierdlem86.e	. . 3 ⊢ 𝐸 = (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2)))))
100	96	simprd 501	. . 3 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (((if((𝑆‘𝑗) = (𝑄‘𝑈), ⦋𝑈 / 𝑖⦌𝑅, (𝐹‘(𝑋 + (𝑆‘𝑗)))) − 𝐶) / (𝑆‘𝑗)) · ((𝑆‘𝑗) / (2 · (sin‘((𝑆‘𝑗) / 2))))) ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
101	99, 100	eqeltrid 2865	. 2 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗)))
102	95	simprd 501	. 2 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ))
103	98, 101, 102	jca31 524	1 ⊢ ((𝜑 ∧ 𝑗 ∈ (0..^𝑁)) → ((𝐷 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘(𝑗 + 1))) ∧ 𝐸 ∈ ((𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) lim_ℂ (𝑆‘𝑗))) ∧ (𝑂 ↾ ((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))) ∈ (((𝑆‘𝑗)(,)(𝑆‘(𝑗 + 1)))–cn→ℂ)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ∀wral 3077 {crab 3413 ⦋csb 3847 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ifcif 4482 {cpr 4586 class class class wbr 5103 ↦ cmpt 5186 ran crn 5652 ↾ cres 5653 ℩cio 6491 ⟶wf 6533 ‘cfv 6537 Isom wiso 6538 ℩crio 7374 (class class class)co 7418 ↑_m cmap 8840 ℂcc 11191 ℝcr 11192 0cc0 11193 1c1 11194 + caddc 11196 · cmul 11198 < clt 11336 − cmin 11534 -cneg 11535 / cdiv 11966 ℕcn 12328 2c2 12390 (,)cioo 13469 [,]cicc 13472 ...cfz 13632 ..^cfzo 13781 ♯chash 14467 sincsin 16222 πcpi 16225 –cn→ccncf 25190 lim_ℂ climc 26175

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7749 ax-inf2 9635 ax-cnex 11249 ax-resscn 11250 ax-1cn 11251 ax-icn 11252 ax-addcl 11253 ax-addrcl 11254 ax-mulcl 11255 ax-mulrcl 11256 ax-mulcom 11257 ax-addass 11258 ax-mulass 11259 ax-distr 11260 ax-i2m1 11261 ax-1ne0 11262 ax-1rid 11263 ax-rnegex 11264 ax-rrecex 11265 ax-cnre 11266 ax-pre-lttri 11267 ax-pre-lttrn 11268 ax-pre-ltadd 11269 ax-pre-mulgt0 11270 ax-pre-sup 11271 ax-addf 11272

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-int 4908 df-iun 4953 df-iin 4954 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7375 df-ov 7421 df-oprab 7422 df-mpo 7423 df-of 7691 df-om 7876 df-1st 7999 df-2nd 8000 df-supp 8171 df-frecs 8292 df-wrecs 8323 df-recs 8372 df-rdg 8411 df-1o 8469 df-2o 8470 df-er 8710 df-map 8842 df-pm 8843 df-ixp 8919 df-en 8967 df-dom 8968 df-sdom 8969 df-fin 8970 df-fsupp 9347 df-fi 9396 df-sup 9427 df-inf 9428 df-oi 9497 df-card 10013 df-pnf 11338 df-mnf 11339 df-xr 11340 df-ltxr 11341 df-le 11342 df-sub 11536 df-neg 11537 df-div 11967 df-nn 12329 df-2 12398 df-3 12399 df-4 12400 df-5 12401 df-6 12402 df-7 12403 df-8 12404 df-9 12405 df-n0 12600 df-z 12687 df-dec 12808 df-uz 12959 df-q 13069 df-rp 13114 df-xneg 13234 df-xadd 13235 df-xmul 13236 df-ioo 13473 df-ioc 13474 df-ico 13475 df-icc 13476 df-fz 13633 df-fzo 13782 df-fl 13925 df-mod 14003 df-seq 14138 df-exp 14198 df-fac 14411 df-bc 14440 df-hash 14468 df-shft 15213 df-cj 15259 df-re 15260 df-im 15261 df-sqrt 15395 df-abs 15396 df-limsup 15631 df-clim 15648 df-rlim 15649 df-sum 15847 df-ef 16226 df-sin 16228 df-cos 16229 df-pi 16231 df-struct 17318 df-sets 17335 df-slot 17353 df-ndx 17365 df-base 17381 df-ress 17402 df-plusg 17434 df-mulr 17435 df-starv 17436 df-sca 17437 df-vsca 17438 df-ip 17439 df-tset 17440 df-ple 17441 df-ds 17443 df-unif 17444 df-hom 17445 df-cco 17446 df-rest 17586 df-topn 17587 df-0g 17605 df-gsum 17606 df-topgen 17607 df-pt 17608 df-prds 17611 df-xrs 17667 df-qtop 17672 df-imas 17673 df-xps 17675 df-mre 17749 df-mrc 17750 df-acs 17752 df-mgm 18809 df-sgrp 18901 df-mnd 18917 df-submnd 18972 df-mulg 19271 df-cntz 19524 df-cmn 19989 df-psmet 21663 df-xmet 21664 df-met 21665 df-bl 21666 df-mopn 21667 df-fbas 21668 df-fg 21669 df-cnfld 21672 df-top 23205 df-topon 23222 df-topsp 23244 df-bases 23257 df-cld 23330 df-ntr 23331 df-cls 23332 df-nei 23409 df-lp 23447 df-perf 23448 df-cn 23538 df-cnp 23539 df-haus 23626 df-tx 23874 df-hmeo 24067 df-fil 24158 df-fm 24250 df-flim 24251 df-flf 24252 df-xms 24632 df-ms 24633 df-tms 24634 df-cncf 25192 df-limc 26179 df-dv 26180

This theorem is used by: fourierdlem103 47188 fourierdlem104 47189

W3C validator