Theorem fourierdlem94

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem94.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	fourierdlem94.t	⊢ 𝑇 = ( 2 · π )
	fourierdlem94.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
	fourierdlem94.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem94.p	⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
	fourierdlem94.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	fourierdlem94.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
	fourierdlem94.dvcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
	fourierdlem94.dvlb	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
	fourierdlem94.dvub	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
Assertion	fourierdlem94	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem94.f	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		fourierdlem94.t	⊢ 𝑇 = ( 2 · π )
3		fourierdlem94.per	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
4		fourierdlem94.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
5		fourierdlem94.p	⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
6		fourierdlem94.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7		fourierdlem94.q	⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
8		fourierdlem94.dvcn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
9		fourierdlem94.dvlb	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
10		fourierdlem94.dvub	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
11		pire	⊢ π ∈ ℝ
12	11	renegcli	⊢ - π ∈ ℝ
13	12	a1i	⊢ ( 𝜑 → - π ∈ ℝ )
14	11	a1i	⊢ ( 𝜑 → π ∈ ℝ )
15		negpilt0	⊢ - π < 0
16		pipos	⊢ 0 < π
17		0re	⊢ 0 ∈ ℝ
18	12 17 11	lttri	⊢ ( ( - π < 0 ∧ 0 < π ) → - π < π )
19	15 16 18	mp2an	⊢ - π < π
20	19	a1i	⊢ ( 𝜑 → - π < π )
21		picn	⊢ π ∈ ℂ
22	21	2timesi	⊢ ( 2 · π ) = ( π + π )
23	21 21	subnegi	⊢ ( π − - π ) = ( π + π )
24	22 2 23	3eqtr4i	⊢ 𝑇 = ( π − - π )
25		ssid	⊢ ℝ ⊆ ℝ
26	25	a1i	⊢ ( 𝜑 → ℝ ⊆ ℝ )
27		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → 𝑥 ∈ ℝ )
28		zre	⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℝ )
29	28	3ad2ant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
30		2re	⊢ 2 ∈ ℝ
31	30 11	remulcli	⊢ ( 2 · π ) ∈ ℝ
32	31	a1i	⊢ ( 𝜑 → ( 2 · π ) ∈ ℝ )
33	2 32	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
35	34	3adant2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → 𝑇 ∈ ℝ )
36	29 35	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
37	27 36	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝑥 + ( 𝑘 · 𝑇 ) ) ∈ ℝ )
38		simp1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → 𝜑 )
39		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℤ )
40		ax-resscn	⊢ ℝ ⊆ ℂ
41	40	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
42	1 41	fssd	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
43	42	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝐹 : ℝ ⟶ ℂ )
44	43	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
45	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
46		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑘 ∈ ℤ )
47		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
48		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ℝ ↔ 𝑦 ∈ ℝ ) )
49	48	anbi2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ↔ ( 𝜑 ∧ 𝑦 ∈ ℝ ) ) )
50		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
51	50	fveq2d	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) )
52		fveq2	⊢ ( 𝑥 = 𝑦 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
53	51 52	eqeq12d	⊢ ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) )
54	49 53	imbi12d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) ) ) )
55	54 3	chvarvv	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
56	55	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
57	44 45 46 47 56	fperiodmul	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
58	38 39 27 57	syl21anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℤ ) → ( 𝐹 ‘ ( 𝑥 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
59	40	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℂ )
60		ioossre	⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
61	60	a1i	⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
62	1 61	fssresd	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
63	62 41	fssd	⊢ ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
65	60	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
66	42	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℂ )
67	25	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ℝ ⊆ ℝ )
68		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
69	68	tgioo2	⊢ ( topGen ‘ ran (,) ) = ( ( TopOpen ‘ ℂfld ) ↾t ℝ )
70	68 69	dvres	⊢ ( ( ( ℝ ⊆ ℂ ∧ 𝐹 : ℝ ⟶ ℂ ) ∧ ( ℝ ⊆ ℝ ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
71	59 66 67 65 70	syl22anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
72	71	dmeqd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
73		ioontr	⊢ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
74	73	reseq2i	⊢ ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
75	74	dmeqi	⊢ dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
76	75	a1i	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( ( int ‘ ( topGen ‘ ran (,) ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
77		cncff	⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
78		fdm	⊢ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
79	8 77 78	3syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
80	72 76 79	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
81		dvcn	⊢ ( ( ( ℝ ⊆ ℂ ∧ ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ∧ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ ) ∧ dom ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
82	59 64 65 80 81	syl31anc	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
83	65 40	sstrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
84	5	fourierdlem2	⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
85	6 84	syl	⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
86	7 85	mpbid	⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
87	86	simpld	⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
88		elmapi	⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
89	87 88	syl	⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
90	89	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
91		elfzofz	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
92	91	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
93	90 92	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
94	93	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
95		fzofzp1	⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
96	95	adantl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
97	90 96	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
98	86	simprrd	⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
99	98	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
100	68 94 97 99	lptioo2cn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
101	62	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℝ )
102	41 42 26	dvbss	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) ⊆ ℝ )
103		dvfre	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
104	1 26 103	syl2anc	⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
105	86	simprd	⊢ ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = - π ∧ ( 𝑄 ‘ 𝑀 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
106	105	simplld	⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = - π )
107	105	simplrd	⊢ ( 𝜑 → ( 𝑄 ‘ 𝑀 ) = π )
108	8 77	syl	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
109	97	rexrd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
110	68 109 93 99	lptioo1cn	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ( ( limPt ‘ ( TopOpen ‘ ℂfld ) ) ‘ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
111	108 83 110 9 68	ellimciota	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
112	108 83 100 10 68	ellimciota	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑥 𝑥 ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
113	28	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → 𝑘 ∈ ℝ )
114	113 34	remulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( 𝑘 · 𝑇 ) ∈ ℝ )
115	43	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
116	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑇 ∈ ℝ )
117		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑘 ∈ ℤ )
118		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℝ )
119	3	ad4ant14	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
120	115 116 117 118 119	fperiodmul	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑡 ) )
121		eqid	⊢ ( ℝ D 𝐹 ) = ( ℝ D 𝐹 )
122	43 114 120 121	fperdvper	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) → ( ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
123	122	an32s	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) ∧ ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
124	123	simpld	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( 𝑡 + ( 𝑘 · 𝑇 ) ) ∈ dom ( ℝ D 𝐹 ) )
125	123	simprd	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) ∧ 𝑘 ∈ ℤ ) → ( ( ℝ D 𝐹 ) ‘ ( 𝑡 + ( 𝑘 · 𝑇 ) ) ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
126		fveq2	⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑖 ) )
127		oveq1	⊢ ( 𝑗 = 𝑖 → ( 𝑗 + 1 ) = ( 𝑖 + 1 ) )
128	127	fveq2d	⊢ ( 𝑗 = 𝑖 → ( 𝑄 ‘ ( 𝑗 + 1 ) ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
129	126 128	oveq12d	⊢ ( 𝑗 = 𝑖 → ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
130	129	cbvmptv	⊢ ( 𝑗 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑗 ) (,) ( 𝑄 ‘ ( 𝑗 + 1 ) ) ) ) = ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ↦ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
131		eqid	⊢ ( 𝑡 ∈ ℝ ↦ ( 𝑡 + ( ( ⌊ ‘ ( ( π − 𝑡 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑡 ∈ ℝ ↦ ( 𝑡 + ( ( ⌊ ‘ ( ( π − 𝑡 ) / 𝑇 ) ) · 𝑇 ) ) )
132	102 104 13 14 20 24 6 89 106 107 8 111 112 124 125 130 131	fourierdlem71	⊢ ( 𝜑 → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
133	132	adantr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
134		nfv	⊢ Ⅎ 𝑡 ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) )
135		nfra1	⊢ Ⅎ 𝑡 ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧
136	134 135	nfan	⊢ Ⅎ 𝑡 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
137	71 74	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) = ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
138	137	fveq1d	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) = ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) )
139		fvres	⊢ ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
140	138 139	sylan9eq	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) = ( ( ℝ D 𝐹 ) ‘ 𝑡 ) )
141	140	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
142	141	adantlr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) )
143		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
144		ssdmres	⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) ↔ dom ( ( ℝ D 𝐹 ) ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
145	79 144	sylibr	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) )
146	145	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom ( ℝ D 𝐹 ) )
147		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
148	146 147	sseldd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑡 ∈ dom ( ℝ D 𝐹 ) )
149		rspa	⊢ ( ( ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ∧ 𝑡 ∈ dom ( ℝ D 𝐹 ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
150	143 148 149	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 )
151	142 150	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) ∧ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
152	151	ex	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ( 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
153	136 152	ralrimi	⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 ) → ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
154	153	ex	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 → ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
155	154	reximdv	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ dom ( ℝ D 𝐹 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑡 ) ) ≤ 𝑧 → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 ) )
156	133 155	mpd	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∃ 𝑧 ∈ ℝ ∀ 𝑡 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( abs ‘ ( ( ℝ D ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) ‘ 𝑡 ) ) ≤ 𝑧 )
157	93 97 101 80 156	ioodvbdlimc2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ≠ ∅ )
158	64 83 100 157 68	ellimciota	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑦 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
159		oveq2	⊢ ( 𝑦 = 𝑥 → ( π − 𝑦 ) = ( π − 𝑥 ) )
160	159	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( π − 𝑦 ) / 𝑇 ) = ( ( π − 𝑥 ) / 𝑇 ) )
161	160	fveq2d	⊢ ( 𝑦 = 𝑥 → ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) )
162	161	oveq1d	⊢ ( 𝑦 = 𝑥 → ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
163	162	cbvmptv	⊢ ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
164		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
165		fveq2	⊢ ( 𝑧 = 𝑥 → ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) = ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) )
166	164 165	oveq12d	⊢ ( 𝑧 = 𝑥 → ( 𝑧 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) ) = ( 𝑥 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) )
167	166	cbvmptv	⊢ ( 𝑧 ∈ ℝ ↦ ( 𝑧 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( 𝑦 ∈ ℝ ↦ ( ( ⌊ ‘ ( ( π − 𝑦 ) / 𝑇 ) ) · 𝑇 ) ) ‘ 𝑥 ) ) )
168	13 14 20 5 24 6 7 26 1 37 58 82 158 4 163 167	fourierdlem49	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ )
169	93 97 101 80 156	ioodvbdlimc1	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ≠ ∅ )
170	64 83 110 169 68	ellimciota	⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ℩ 𝑦 𝑦 ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) ) ∈ ( ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) limℂ ( 𝑄 ‘ 𝑖 ) ) )
171		biid	⊢ ( ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) ↔ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ( ( 𝑄 ‘ 𝑖 ) [,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑘 ∈ ℤ ) ∧ 𝑤 = ( 𝑋 + ( 𝑘 · 𝑇 ) ) ) )
172	13 14 20 5 24 6 7 1 37 58 82 170 4 163 167 171	fourierdlem48	⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ )
173	168 172	jca	⊢ ( 𝜑 → ( ( ( 𝐹 ↾ ( -∞ (,) 𝑋 ) ) limℂ 𝑋 ) ≠ ∅ ∧ ( ( 𝐹 ↾ ( 𝑋 (,) +∞ ) ) limℂ 𝑋 ) ≠ ∅ ) )