fourierdlem86

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

	Ref	Expression
Hypotheses	fourierdlem86.f	$⊢ φ \to F : ℝ ⟶ ℝ$
	fourierdlem86.xre	$⊢ φ \to X \in ℝ$
	fourierdlem86.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))\})$
	fourierdlem86.m	$⊢ φ \to M \in ℕ$
	fourierdlem86.v	$⊢ φ \to V \in P (M)$
	fourierdlem86.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem86.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
	fourierdlem86.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
	fourierdlem86.a	$⊢ φ \to A \in ℝ$
	fourierdlem86.b	$⊢ φ \to B \in ℝ$
	fourierdlem86.altb	$⊢ φ \to A < B$
	fourierdlem86.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
	fourierdlem86.n0	$⊢ φ \to \neg 0 \in [A, B]$
	fourierdlem86.c	$⊢ φ \to C \in ℝ$
	fourierdlem86.o	$⊢ O = (s \in [A, B] ⟼ (\frac{F (X + s) - C}{s}) (\frac{s}{2 \sin (\frac{s}{2})}))$
	fourierdlem86.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
	fourierdlem86.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
	fourierdlem86.n	$⊢ N = \|T\| - 1$
	fourierdlem86.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
	fourierdlem86.d	$⊢ D = (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
	fourierdlem86.e	$⊢ E = (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
	fourierdlem86.u	$⊢ U = (ι i \in (0 ..^M) \| (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1)))$
Assertion	fourierdlem86	$⊢ (φ \land j \in (0 ..^N)) \to ((D \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land E \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem86.f	$⊢ φ \to F : ℝ ⟶ ℝ$
2		fourierdlem86.xre	$⊢ φ \to X \in ℝ$
3		fourierdlem86.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))\})$
4		fourierdlem86.m	$⊢ φ \to M \in ℕ$
5		fourierdlem86.v	$⊢ φ \to V \in P (M)$
6		fourierdlem86.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(V (i), V (i + 1))}) : (V (i), V (i + 1)) \underset{cn}{⟶} ℂ$
7		fourierdlem86.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i))$
8		fourierdlem86.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(V (i), V (i + 1))}) {lim}_{ℂ} V (i + 1))$
9		fourierdlem86.a	$⊢ φ \to A \in ℝ$
10		fourierdlem86.b	$⊢ φ \to B \in ℝ$
11		fourierdlem86.altb	$⊢ φ \to A < B$
12		fourierdlem86.ab	$⊢ φ \to [A, B] \subseteq [- π, π]$
13		fourierdlem86.n0	$⊢ φ \to \neg 0 \in [A, B]$
14		fourierdlem86.c	$⊢ φ \to C \in ℝ$
15		fourierdlem86.o	$⊢ O = (s \in [A, B] ⟼ (\frac{F (X + s) - C}{s}) (\frac{s}{2 \sin (\frac{s}{2})}))$
16		fourierdlem86.q	$⊢ Q = (i \in (0 \dots M) ⟼ V (i) - X)$
17		fourierdlem86.t	$⊢ T = \{A, B\} \cup (ran Q \cap (A, B))$
18		fourierdlem86.n	$⊢ N = \|T\| - 1$
19		fourierdlem86.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), T))$
20		fourierdlem86.d	$⊢ D = (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
21		fourierdlem86.e	$⊢ E = (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
22		fourierdlem86.u	$⊢ U = (ι i \in (0 ..^M) \| (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1)))$
23	2	adantr	$⊢ (φ \land j \in (0 ..^N)) \to X \in ℝ$
24	4	adantr	$⊢ (φ \land j \in (0 ..^N)) \to M \in ℕ$
25	5	adantr	$⊢ (φ \land j \in (0 ..^N)) \to V \in P (M)$
26	9	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A \in ℝ$
27	10	adantr	$⊢ (φ \land j \in (0 ..^N)) \to B \in ℝ$
28	11	adantr	$⊢ (φ \land j \in (0 ..^N)) \to A < B$
29	12	adantr	$⊢ (φ \land j \in (0 ..^N)) \to [A, B] \subseteq [- π, π]$
30		simpr	$⊢ (φ \land j \in (0 ..^N)) \to j \in (0 ..^N)$
31		biid	$⊢ (((((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \land y \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (y), Q (y + 1))) \leftrightarrow (((((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \land y \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (y), Q (y + 1)))$
32	23 3 24 25 26 27 28 29 16 17 18 19 30 22 31	fourierdlem50	$⊢ (φ \land j \in (0 ..^N)) \to (U \in (0 ..^M) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1)))$
33	32	simpld	$⊢ (φ \land j \in (0 ..^N)) \to U \in (0 ..^M)$
34		id	$⊢ (φ \land j \in (0 ..^N)) \to (φ \land j \in (0 ..^N))$
35	32	simprd	$⊢ (φ \land j \in (0 ..^N)) \to (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1))$
36	34 33 35	jca31	$⊢ (φ \land j \in (0 ..^N)) \to (((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1)))$
37		nfv	$⊢ Ⅎ i (((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1)))$
38		nfv	$⊢ Ⅎ i S (j + 1) = Q (U + 1)$
39		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ U / i ⦌ L$
40		nfcv	$⊢ \underline{Ⅎ} i F (X + S (j + 1))$
41	38 39 40	nfif	$⊢ \underline{Ⅎ} i if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1)))$
42		nfcv	$⊢ \underline{Ⅎ} i -$
43		nfcv	$⊢ \underline{Ⅎ} i C$
44	41 42 43	nfov	$⊢ \underline{Ⅎ} i (if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C)$
45		nfcv	$⊢ \underline{Ⅎ} i \div$
46		nfcv	$⊢ \underline{Ⅎ} i S (j + 1)$
47	44 45 46	nfov	$⊢ \underline{Ⅎ} i (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)})$
48		nfcv	$⊢ \underline{Ⅎ} i \times$
49		nfcv	$⊢ \underline{Ⅎ} i (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
50	47 48 49	nfov	$⊢ \underline{Ⅎ} i (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
51	50	nfel1	$⊢ Ⅎ i (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
52		nfv	$⊢ Ⅎ i S (j) = Q (U)$
53		nfcsb1v	$⊢ \underline{Ⅎ} i ⦋ U / i ⦌ R$
54		nfcv	$⊢ \underline{Ⅎ} i F (X + S (j))$
55	52 53 54	nfif	$⊢ \underline{Ⅎ} i if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j)))$
56	55 42 43	nfov	$⊢ \underline{Ⅎ} i (if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C)$
57		nfcv	$⊢ \underline{Ⅎ} i S (j)$
58	56 45 57	nfov	$⊢ \underline{Ⅎ} i (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)})$
59		nfcv	$⊢ \underline{Ⅎ} i (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
60	58 48 59	nfov	$⊢ \underline{Ⅎ} i (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
61	60	nfel1	$⊢ Ⅎ i (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
62	51 61	nfan	$⊢ Ⅎ i ((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j)))$
63		nfv	$⊢ Ⅎ i ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
64	62 63	nfan	$⊢ Ⅎ i (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$
65	37 64	nfim	$⊢ Ⅎ i ((((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1))) \to (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ))$
66		eleq1	$⊢ i = U \to (i \in (0 ..^M) \leftrightarrow U \in (0 ..^M))$
67	66	anbi2d	$⊢ i = U \to (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \leftrightarrow ((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)))$
68		fveq2	$⊢ i = U \to Q (i) = Q (U)$
69		oveq1	$⊢ i = U \to i + 1 = U + 1$
70	69	fveq2d	$⊢ i = U \to Q (i + 1) = Q (U + 1)$
71	68 70	oveq12d	$⊢ i = U \to (Q (i), Q (i + 1)) = (Q (U), Q (U + 1))$
72	71	sseq2d	$⊢ i = U \to ((S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1)) \leftrightarrow (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1)))$
73	67 72	anbi12d	$⊢ i = U \to ((((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \leftrightarrow (((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1))))$
74	70	eqeq2d	$⊢ i = U \to (S (j + 1) = Q (i + 1) \leftrightarrow S (j + 1) = Q (U + 1))$
75		csbeq1a	$⊢ i = U \to L = ⦋ U / i ⦌ L$
76	74 75	ifbieq1d	$⊢ i = U \to if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) = if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1)))$
77	76	oveq1d	$⊢ i = U \to if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C = if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C$
78	77	oveq1d	$⊢ i = U \to \frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)} = \frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}$
79	78	oveq1d	$⊢ i = U \to (\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) = (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
80	79	eleq1d	$⊢ i = U \to ((\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \leftrightarrow (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)))$
81	68	eqeq2d	$⊢ i = U \to (S (j) = Q (i) \leftrightarrow S (j) = Q (U))$
82		csbeq1a	$⊢ i = U \to R = ⦋ U / i ⦌ R$
83	81 82	ifbieq1d	$⊢ i = U \to if (S (j) = Q (i), R, F (X + S (j))) = if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j)))$
84	83	oveq1d	$⊢ i = U \to if (S (j) = Q (i), R, F (X + S (j))) - C = if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C$
85	84	oveq1d	$⊢ i = U \to \frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)} = \frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}$
86	85	oveq1d	$⊢ i = U \to (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) = (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
87	86	eleq1d	$⊢ i = U \to ((\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j)) \leftrightarrow (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j)))$
88	80 87	anbi12d	$⊢ i = U \to (((\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \leftrightarrow ((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))))$
89	88	anbi1d	$⊢ i = U \to ((((\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ) \leftrightarrow (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ))$
90	73 89	imbi12d	$⊢ i = U \to (((((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \to (((\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)) \leftrightarrow ((((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1))) \to (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)))$
91		eqid	$⊢ (\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) = (\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})})$
92		eqid	$⊢ (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) = (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})})$
93		biid	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \leftrightarrow (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1)))$
94	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 91 92 93	fourierdlem76	$⊢ (((φ \land j \in (0 ..^N)) \land i \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (i), Q (i + 1))) \to (((\frac{if (S (j + 1) = Q (i + 1), L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (i), R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$
95	65 90 94	vtoclg1f	$⊢ U \in (0 ..^M) \to ((((φ \land j \in (0 ..^N)) \land U \in (0 ..^M)) \land (S (j), S (j + 1)) \subseteq (Q (U), Q (U + 1))) \to (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ))$
96	33 36 95	sylc	$⊢ (φ \land j \in (0 ..^N)) \to (((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$
97	96	simpld	$⊢ (φ \land j \in (0 ..^N)) \to ((\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j)))$
98	97	simpld	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{if (S (j + 1) = Q (U + 1), ⦋ U / i ⦌ L, F (X + S (j + 1))) - C}{S (j + 1)}) (\frac{S (j + 1)}{2 \sin (\frac{S (j + 1)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
99	20 98	eqeltrid	$⊢ (φ \land j \in (0 ..^N)) \to D \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1))$
100	97	simprd	$⊢ (φ \land j \in (0 ..^N)) \to (\frac{if (S (j) = Q (U), ⦋ U / i ⦌ R, F (X + S (j))) - C}{S (j)}) (\frac{S (j)}{2 \sin (\frac{S (j)}{2})}) \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
101	21 100	eqeltrid	$⊢ (φ \land j \in (0 ..^N)) \to E \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))$
102	96	simprd	$⊢ (φ \land j \in (0 ..^N)) \to ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ$
103	99 101 102	jca31	$⊢ (φ \land j \in (0 ..^N)) \to ((D \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j + 1)) \land E \in (({O ↾}_{(S (j), S (j + 1))}) {lim}_{ℂ} S (j))) \land ({O ↾}_{(S (j), S (j + 1))}) : (S (j), S (j + 1)) \underset{cn}{⟶} ℂ)$

Metamath Proof Explorer

Theorem fourierdlem86

Proof