fourierdlem85

Description: Limit of the function G at the lower bounds of the partition intervals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem85.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem85.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem85.x	$⊢ φ \to X \in ran V$
	fourierdlem85.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem85.w	$⊢ φ \to W \in ℝ$
	fourierdlem85.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
	fourierdlem85.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem85.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
	fourierdlem85.n	$⊢ φ \to N \in ℝ$
	fourierdlem85.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
	fourierdlem85.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
	fourierdlem85.m	$⊢ φ \to M \in ℕ$
	fourierdlem85.v	$⊢ φ \to V \in P (M)$
	fourierdlem85.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem85.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem85.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem85.i	$⊢ I = ℝ D F$
	fourierdlem85.ifn	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
	fourierdlem85.e	$⊢ φ \to E \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
	fourierdlem85.a	$⊢ A = if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) S (Q (i))$
Assertion	fourierdlem85	$⊢ (φ \land i \in (0 ..^M)) \to A \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem85.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π + X \land p (m) = π + X) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem85.f	$⊢ φ \to F : ℝ ⟶ ℝ$
3		fourierdlem85.x	$⊢ φ \to X \in ran V$
4		fourierdlem85.y	$⊢ φ \to Y \in (({F ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
5		fourierdlem85.w	$⊢ φ \to W \in ℝ$
6		fourierdlem85.h	$⊢ H = (s \in [- π, π] ⟼ if (s = 0, 0, \frac{F (X + s) - if (0 < s, Y, W)}{s}))$
7		fourierdlem85.k	$⊢ K = (s \in [- π, π] ⟼ if (s = 0, 1, \frac{s}{2 \sin (\frac{s}{2})}))$
8		fourierdlem85.u	$⊢ U = (s \in [- π, π] ⟼ H (s) K (s))$
9		fourierdlem85.n	$⊢ φ \to N \in ℝ$
10		fourierdlem85.s	$⊢ S = (s \in [- π, π] ⟼ \sin (N + (\frac{1}{2})) s)$
11		fourierdlem85.g	$⊢ G = (s \in [- π, π] ⟼ U (s) S (s))$
12		fourierdlem85.m	$⊢ φ \to M \in ℕ$
13		fourierdlem85.v	$⊢ φ \to V \in P (M)$
14		fourierdlem85.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
15		fourierdlem85.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
16		fourierdlem85.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = - π \land p (m) = π) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
17		fourierdlem85.i	$⊢ I = ℝ D F$
18		fourierdlem85.ifn	$⊢ (φ \land i \in (0 ..^M)) \to ({I ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) ⟶ ℂ$
19		fourierdlem85.e	$⊢ φ \to E \in (({I ↾}_{(X, +∞)}) {lim}_{ℂ} X)$
20		fourierdlem85.a	$⊢ A = if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) S (Q (i))$
21		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ U (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s))$
22		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ S (s)) = (s \in (Q (i), Q (i + 1)) ⟼ S (s))$
23		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) = (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s))$
24		pire	$⊢ π \in ℝ$
25	24	renegcli	$⊢ - π \in ℝ$
26	25	rexri	$⊢ - π \in ℝ^{*}$
27	26	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to - π \in ℝ^{*}$
28	24	rexri	$⊢ π \in ℝ^{*}$
29	28	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to π \in ℝ^{*}$
30	24	a1i	$⊢ φ \to π \in ℝ$
31	30	renegcld	$⊢ φ \to - π \in ℝ$
32	1	fourierdlem2	$⊢ M \in ℕ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
33	12 32	syl	$⊢ φ \to (V \in P (M) \leftrightarrow (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1))))$
34	13 33	mpbid	$⊢ φ \to (V \in (ℝ^{(0 \dots M)}) \land ((V (0) = - π + X \land V (M) = π + X) \land \forall i \in (0 ..^M) V (i) < V (i + 1)))$
35	34	simpld	$⊢ φ \to V \in (ℝ^{(0 \dots M)})$
36		elmapi	$⊢ V \in (ℝ^{(0 \dots M)}) \to V : (0 \dots M) ⟶ ℝ$
37		frn	$⊢ V : (0 \dots M) ⟶ ℝ \to ran V \subseteq ℝ$
38	35 36 37	3syl	$⊢ φ \to ran V \subseteq ℝ$
39	38 3	sseldd	$⊢ φ \to X \in ℝ$
40	31 30 39 1 16 12 13 15	fourierdlem14	$⊢ φ \to Q \in O (M)$
41	16 12 40	fourierdlem15	$⊢ φ \to Q : (0 \dots M) ⟶ [- π, π]$
42	41	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ [- π, π]$
43	42	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to Q : (0 \dots M) ⟶ [- π, π]$
44		simplr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to i \in (0 ..^M)$
45	27 29 43 44	fourierdlem8	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
46		ioossicc	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1)]$
47	46	sseli	$⊢ s \in (Q (i), Q (i + 1)) \to s \in [Q (i), Q (i + 1)]$
48	47	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in [Q (i), Q (i + 1)]$
49	45 48	sseldd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to s \in [- π, π]$
50		ioossre	$⊢ (X, +∞) \subseteq ℝ$
51	50	a1i	$⊢ φ \to (X, +∞) \subseteq ℝ$
52	2 51	fssresd	$⊢ φ \to ({F ↾}_{(X, +∞)}) : (X, +∞) ⟶ ℝ$
53		ax-resscn	$⊢ ℝ \subseteq ℂ$
54	51 53	sstrdi	$⊢ φ \to (X, +∞) \subseteq ℂ$
55		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
56		pnfxr	$⊢ +∞ \in ℝ^{*}$
57	56	a1i	$⊢ φ \to +∞ \in ℝ^{*}$
58	39	ltpnfd	$⊢ φ \to X < +∞$
59	55 57 39 58	lptioo1cn	$⊢ φ \to X \in limPt (TopOpen (ℂ_{fld})) ((X, +∞))$
60	52 54 59 4	limcrecl	$⊢ φ \to Y \in ℝ$
61	2 39 60 5 6	fourierdlem9	$⊢ φ \to H : [- π, π] ⟶ ℝ$
62	53	a1i	$⊢ φ \to ℝ \subseteq ℂ$
63	61 62	fssd	$⊢ φ \to H : [- π, π] ⟶ ℂ$
64	63	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H : [- π, π] ⟶ ℂ$
65	64 49	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) \in ℂ$
66	7	fourierdlem43	$⊢ K : [- π, π] ⟶ ℝ$
67	66	a1i	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K : [- π, π] ⟶ ℝ$
68	67 49	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K (s) \in ℝ$
69	68	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to K (s) \in ℂ$
70	65 69	mulcld	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to H (s) K (s) \in ℂ$
71	8	fvmpt2	$⊢ (s \in [- π, π] \land H (s) K (s) \in ℂ) \to U (s) = H (s) K (s)$
72	49 70 71	syl2anc	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) = H (s) K (s)$
73	72 70	eqeltrd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to U (s) \in ℂ$
74	9 10	fourierdlem18	$⊢ φ \to S : [- π, π] \underset{cn}{⟶} ℝ$
75		cncff	$⊢ S : [- π, π] \underset{cn}{⟶} ℝ \to S : [- π, π] ⟶ ℝ$
76	74 75	syl	$⊢ φ \to S : [- π, π] ⟶ ℝ$
77	76	adantr	$⊢ (φ \land i \in (0 ..^M)) \to S : [- π, π] ⟶ ℝ$
78	77	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S : [- π, π] ⟶ ℝ$
79	78 49	ffvelrnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S (s) \in ℝ$
80	79	recnd	$⊢ ((φ \land i \in (0 ..^M)) \land s \in (Q (i), Q (i + 1))) \to S (s) \in ℂ$
81		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ H (s)) = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
82		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ K (s)) = (s \in (Q (i), Q (i + 1)) ⟼ K (s))$
83		eqid	$⊢ (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) = (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s))$
84		eqid	$⊢ if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) = if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)})$
85	39 1 2 3 4 5 6 12 13 14 15 16 17 18 19 84	fourierdlem75	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) \in (({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
86	61	adantr	$⊢ (φ \land i \in (0 ..^M)) \to H : [- π, π] ⟶ ℝ$
87	26	a1i	$⊢ (φ \land i \in (0 ..^M)) \to - π \in ℝ^{*}$
88	28	a1i	$⊢ (φ \land i \in (0 ..^M)) \to π \in ℝ^{*}$
89		simpr	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 ..^M)$
90	87 88 42 89	fourierdlem8	$⊢ (φ \land i \in (0 ..^M)) \to [Q (i), Q (i + 1)] \subseteq [- π, π]$
91	46 90	sstrid	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq [- π, π]$
92	86 91	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {H ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ H (s))$
93	92	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({H ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i)$
94	85 93	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s)) {lim}_{ℂ} Q (i))$
95		limcresi	$⊢ K {lim}_{ℂ} Q (i) \subseteq ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
96		ssid	$⊢ ℂ \subseteq ℂ$
97		cncfss	$⊢ (ℝ \subseteq ℂ \land ℂ \subseteq ℂ) \to [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
98	53 96 97	mp2an	$⊢ [- π, π] \underset{cn}{⟶} ℝ \subseteq [- π, π] \underset{cn}{⟶} ℂ$
99	7	fourierdlem62	$⊢ K : [- π, π] \underset{cn}{⟶} ℝ$
100	98 99	sselii	$⊢ K : [- π, π] \underset{cn}{⟶} ℂ$
101	100	a1i	$⊢ (φ \land i \in (0 ..^M)) \to K : [- π, π] \underset{cn}{⟶} ℂ$
102		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
103	102	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
104	42 103	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in [- π, π]$
105	101 104	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in (K {lim}_{ℂ} Q (i))$
106	95 105	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in (({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
107		cncff	$⊢ K : [- π, π] \underset{cn}{⟶} ℂ \to K : [- π, π] ⟶ ℂ$
108	100 107	mp1i	$⊢ (φ \land i \in (0 ..^M)) \to K : [- π, π] ⟶ ℂ$
109	108 91	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {K ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ K (s))$
110	109	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({K ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i)$
111	106 110	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ K (s)) {lim}_{ℂ} Q (i))$
112	81 82 83 65 69 94 111	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i))$
113	72	mpteq2dva	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s)) = (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s))$
114	113	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ H (s) K (s)) {lim}_{ℂ} Q (i)$
115	112 114	eleqtrrd	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s)) {lim}_{ℂ} Q (i))$
116		limcresi	$⊢ S {lim}_{ℂ} Q (i) \subseteq ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
117	74	adantr	$⊢ (φ \land i \in (0 ..^M)) \to S : [- π, π] \underset{cn}{⟶} ℝ$
118	117 104	cnlimci	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in (S {lim}_{ℂ} Q (i))$
119	116 118	sseldi	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in (({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
120	77 91	feqresmpt	$⊢ (φ \land i \in (0 ..^M)) \to {S ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ S (s))$
121	120	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to ({S ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i) = (s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i)$
122	119 121	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to S (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ S (s)) {lim}_{ℂ} Q (i))$
123	21 22 23 73 80 115 122	mullimc	$⊢ (φ \land i \in (0 ..^M)) \to if (V (i) = X, E, \frac{R - if (V (i) < X, W, Y)}{Q (i)}) K (Q (i)) S (Q (i)) \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i))$
124	20 123	eqeltrid	$⊢ (φ \land i \in (0 ..^M)) \to A \in ((s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i))$
125	11	reseq1i	$⊢ {G ↾}_{(Q (i), Q (i + 1))} = {(s \in [- π, π] ⟼ U (s) S (s)) ↾}_{(Q (i), Q (i + 1))}$
126	91	resmptd	$⊢ (φ \land i \in (0 ..^M)) \to {(s \in [- π, π] ⟼ U (s) S (s)) ↾}_{(Q (i), Q (i + 1))} = (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s))$
127	125 126	syl5req	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) = {G ↾}_{(Q (i), Q (i + 1))}$
128	127	oveq1d	$⊢ (φ \land i \in (0 ..^M)) \to (s \in (Q (i), Q (i + 1)) ⟼ U (s) S (s)) {lim}_{ℂ} Q (i) = ({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i)$
129	124 128	eleqtrd	$⊢ (φ \land i \in (0 ..^M)) \to A \in (({G ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$

Metamath Proof Explorer

Theorem fourierdlem85

Proof