fourierdlem90

Description: Given a piecewise continuous function, it is still continuous with respect to an open interval of the moved partition. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem90.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem90.t	$⊢ T = B - A$
	fourierdlem90.m	$⊢ φ \to M \in ℕ$
	fourierdlem90.q	$⊢ φ \to Q \in P (M)$
	fourierdlem90.f	$⊢ φ \to F : ℝ ⟶ ℂ$
	fourierdlem90.6	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
	fourierdlem90.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem90.c	$⊢ φ \to C \in ℝ$
	fourierdlem90.d	$⊢ φ \to D \in (C, +∞)$
	fourierdlem90.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
	fourierdlem90.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
	fourierdlem90.n	$⊢ N = \|H\| - 1$
	fourierdlem90.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
	fourierdlem90.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem90.J	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
	fourierdlem90.17	$⊢ φ \to J \in (0 ..^N)$
	fourierdlem90.u	$⊢ U = S (J + 1) - E (S (J + 1))$
	fourierdlem90.g	$⊢ G = {F ↾}_{(L (E (S (J))), E (S (J + 1)))}$
	fourierdlem90.r	$⊢ R = (y \in (L (E (S (J))) + U, E (S (J + 1)) + U) ⟼ G (y - U))$
	fourierdlem90.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
Assertion	fourierdlem90	$⊢ φ \to ({F ↾}_{(S (J), S (J + 1))}) : (S (J), S (J + 1)) \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem90.p	$⊢ P = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = A \land p (m) = B) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
2		fourierdlem90.t	$⊢ T = B - A$
3		fourierdlem90.m	$⊢ φ \to M \in ℕ$
4		fourierdlem90.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem90.f	$⊢ φ \to F : ℝ ⟶ ℂ$
6		fourierdlem90.6	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
7		fourierdlem90.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem90.c	$⊢ φ \to C \in ℝ$
9		fourierdlem90.d	$⊢ φ \to D \in (C, +∞)$
10		fourierdlem90.o	$⊢ O = (m \in ℕ ⟼ \{p \in (ℝ^{(0 \dots m)}) \| ((p (0) = C \land p (m) = D) \land \forall i \in (0 ..^m) p (i) < p (i + 1))\})$
11		fourierdlem90.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
12		fourierdlem90.n	$⊢ N = \|H\| - 1$
13		fourierdlem90.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
14		fourierdlem90.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
15		fourierdlem90.J	$⊢ L = (y \in (A, B] ⟼ if (y = B, A, y))$
16		fourierdlem90.17	$⊢ φ \to J \in (0 ..^N)$
17		fourierdlem90.u	$⊢ U = S (J + 1) - E (S (J + 1))$
18		fourierdlem90.g	$⊢ G = {F ↾}_{(L (E (S (J))), E (S (J + 1)))}$
19		fourierdlem90.r	$⊢ R = (y \in (L (E (S (J))) + U, E (S (J + 1)) + U) ⟼ G (y - U))$
20		fourierdlem90.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <))$
21	1 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
22	21	simp1d	$⊢ φ \to A \in ℝ$
23	21	simp2d	$⊢ φ \to B \in ℝ$
24	22 23	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
25	21	simp3d	$⊢ φ \to A < B$
26	22 23 25 15	fourierdlem17	$⊢ φ \to L : (A, B] ⟶ [A, B]$
27	22 23 25 2 14	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
28		elioore	$⊢ D \in (C, +∞) \to D \in ℝ$
29	9 28	syl	$⊢ φ \to D \in ℝ$
30		elioo4g	$⊢ D \in (C, +∞) \leftrightarrow ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
31	9 30	sylib	$⊢ φ \to ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
32	31	simprd	$⊢ φ \to (C < D \land D < +∞)$
33	32	simpld	$⊢ φ \to C < D$
34	2 1 3 4 8 29 33 10 11 12 13	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), H))$
35	34	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
36	35	simprd	$⊢ φ \to S \in O (N)$
37	35	simpld	$⊢ φ \to N \in ℕ$
38	10	fourierdlem2	$⊢ N \in ℕ \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
39	37 38	syl	$⊢ φ \to (S \in O (N) \leftrightarrow (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1))))$
40	36 39	mpbid	$⊢ φ \to (S \in (ℝ^{(0 \dots N)}) \land ((S (0) = C \land S (N) = D) \land \forall i \in (0 ..^N) S (i) < S (i + 1)))$
41	40	simpld	$⊢ φ \to S \in (ℝ^{(0 \dots N)})$
42		elmapi	$⊢ S \in (ℝ^{(0 \dots N)}) \to S : (0 \dots N) ⟶ ℝ$
43	41 42	syl	$⊢ φ \to S : (0 \dots N) ⟶ ℝ$
44		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
45	16 44	syl	$⊢ φ \to J \in (0 \dots N)$
46	43 45	ffvelrnd	$⊢ φ \to S (J) \in ℝ$
47	27 46	ffvelrnd	$⊢ φ \to E (S (J)) \in (A, B]$
48	26 47	ffvelrnd	$⊢ φ \to L (E (S (J))) \in [A, B]$
49	24 48	sseldd	$⊢ φ \to L (E (S (J))) \in ℝ$
50	22	rexrd	$⊢ φ \to A \in ℝ^{*}$
51		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
52	50 23 51	syl2anc	$⊢ φ \to (A, B] \subseteq ℝ$
53		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
54	16 53	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
55	43 54	ffvelrnd	$⊢ φ \to S (J + 1) \in ℝ$
56	27 55	ffvelrnd	$⊢ φ \to E (S (J + 1)) \in (A, B]$
57	52 56	sseldd	$⊢ φ \to E (S (J + 1)) \in ℝ$
58		eqid	$⊢ (L (E (S (J))), E (S (J + 1))) = (L (E (S (J))), E (S (J + 1)))$
59	55 57	resubcld	$⊢ φ \to S (J + 1) - E (S (J + 1)) \in ℝ$
60	17 59	eqeltrid	$⊢ φ \to U \in ℝ$
61		eqid	$⊢ (L (E (S (J))) + U, E (S (J + 1)) + U) = (L (E (S (J))) + U, E (S (J + 1)) + U)$
62		eleq1	$⊢ j = J \to (j \in (0 ..^N) \leftrightarrow J \in (0 ..^N))$
63	62	anbi2d	$⊢ j = J \to ((φ \land j \in (0 ..^N)) \leftrightarrow (φ \land J \in (0 ..^N)))$
64		fveq2	$⊢ j = J \to S (j) = S (J)$
65	64	fveq2d	$⊢ j = J \to E (S (j)) = E (S (J))$
66	65	fveq2d	$⊢ j = J \to L (E (S (j))) = L (E (S (J)))$
67		oveq1	$⊢ j = J \to j + 1 = J + 1$
68	67	fveq2d	$⊢ j = J \to S (j + 1) = S (J + 1)$
69	68	fveq2d	$⊢ j = J \to E (S (j + 1)) = E (S (J + 1))$
70	66 69	oveq12d	$⊢ j = J \to (L (E (S (j))), E (S (j + 1))) = (L (E (S (J))), E (S (J + 1)))$
71	64	fveq2d	$⊢ j = J \to I (S (j)) = I (S (J))$
72	71	fveq2d	$⊢ j = J \to Q (I (S (j))) = Q (I (S (J)))$
73	71	oveq1d	$⊢ j = J \to I (S (j)) + 1 = I (S (J)) + 1$
74	73	fveq2d	$⊢ j = J \to Q (I (S (j)) + 1) = Q (I (S (J)) + 1)$
75	72 74	oveq12d	$⊢ j = J \to (Q (I (S (j))), Q (I (S (j)) + 1)) = (Q (I (S (J))), Q (I (S (J)) + 1))$
76	70 75	sseq12d	$⊢ j = J \to ((L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1)) \leftrightarrow (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1)))$
77	63 76	imbi12d	$⊢ j = J \to (((φ \land j \in (0 ..^N)) \to (L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))) \leftrightarrow ((φ \land J \in (0 ..^N)) \to (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))))$
78	2	oveq2i	$⊢ k T = k (B - A)$
79	78	oveq2i	$⊢ y + k T = y + k (B - A)$
80	79	eleq1i	$⊢ y + k T \in ran Q \leftrightarrow y + k (B - A) \in ran Q$
81	80	rexbii	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q$
82	81	a1i	$⊢ y \in [C, D] \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q)$
83	82	rabbiia	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
84	83	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
85	11 84	eqtri	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}$
86		id	$⊢ y = x \to y = x$
87	2	eqcomi	$⊢ B - A = T$
88	87	oveq2i	$⊢ k (B - A) = k T$
89	88	a1i	$⊢ y = x \to k (B - A) = k T$
90	86 89	oveq12d	$⊢ y = x \to y + k (B - A) = x + k T$
91	90	eleq1d	$⊢ y = x \to (y + k (B - A) \in ran Q \leftrightarrow x + k T \in ran Q)$
92	91	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k (B - A) \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
93	92	cbvrabv	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
94	93	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
95	85 94	eqtri	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
96		eqid	$⊢ S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2}) = S (j) + if (S (j + 1) - S (j) < Q (1) - A, \frac{S (j + 1) - S (j)}{2}, \frac{Q (1) - A}{2})$
97	2 1 3 4 8 29 33 10 95 12 13 14 15 96 20	fourierdlem79	$⊢ (φ \land j \in (0 ..^N)) \to (L (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))$
98	77 97	vtoclg	$⊢ J \in (0 ..^N) \to ((φ \land J \in (0 ..^N)) \to (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1)))$
99	98	anabsi7	$⊢ (φ \land J \in (0 ..^N)) \to (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))$
100	16 99	mpdan	$⊢ φ \to (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))$
101	100	resabs1d	$⊢ φ \to {({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(L (E (S (J))), E (S (J + 1)))} = {F ↾}_{(L (E (S (J))), E (S (J + 1)))}$
102	101	eqcomd	$⊢ φ \to {F ↾}_{(L (E (S (J))), E (S (J + 1)))} = {({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(L (E (S (J))), E (S (J + 1)))}$
103	1 3 4 2 14 15 20	fourierdlem37	$⊢ φ \to (I : ℝ ⟶ (0 ..^M) \land (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq L (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq L (E (x))\}))$
104	103	simpld	$⊢ φ \to I : ℝ ⟶ (0 ..^M)$
105	104 46	ffvelrnd	$⊢ φ \to I (S (J)) \in (0 ..^M)$
106	105	ancli	$⊢ φ \to (φ \land I (S (J)) \in (0 ..^M))$
107		eleq1	$⊢ i = I (S (J)) \to (i \in (0 ..^M) \leftrightarrow I (S (J)) \in (0 ..^M))$
108	107	anbi2d	$⊢ i = I (S (J)) \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land I (S (J)) \in (0 ..^M)))$
109		fveq2	$⊢ i = I (S (J)) \to Q (i) = Q (I (S (J)))$
110		oveq1	$⊢ i = I (S (J)) \to i + 1 = I (S (J)) + 1$
111	110	fveq2d	$⊢ i = I (S (J)) \to Q (i + 1) = Q (I (S (J)) + 1)$
112	109 111	oveq12d	$⊢ i = I (S (J)) \to (Q (i), Q (i + 1)) = (Q (I (S (J))), Q (I (S (J)) + 1))$
113	112	reseq2d	$⊢ i = I (S (J)) \to {F ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}$
114	112	oveq1d	$⊢ i = I (S (J)) \to (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ = (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ$
115	113 114	eleq12d	$⊢ i = I (S (J)) \to (({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \leftrightarrow ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ)$
116	108 115	imbi12d	$⊢ i = I (S (J)) \to (((φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ) \leftrightarrow ((φ \land I (S (J)) \in (0 ..^M)) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ))$
117	116 7	vtoclg	$⊢ I (S (J)) \in (0 ..^M) \to ((φ \land I (S (J)) \in (0 ..^M)) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ)$
118	105 106 117	sylc	$⊢ φ \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ$
119		rescncf	$⊢ (L (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1)) \to (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ \to ({({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(L (E (S (J))), E (S (J + 1)))}) : (L (E (S (J))), E (S (J + 1))) \underset{cn}{⟶} ℂ)$
120	100 118 119	sylc	$⊢ φ \to ({({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(L (E (S (J))), E (S (J + 1)))}) : (L (E (S (J))), E (S (J + 1))) \underset{cn}{⟶} ℂ$
121	102 120	eqeltrd	$⊢ φ \to ({F ↾}_{(L (E (S (J))), E (S (J + 1)))}) : (L (E (S (J))), E (S (J + 1))) \underset{cn}{⟶} ℂ$
122	18 121	eqeltrid	$⊢ φ \to G : (L (E (S (J))), E (S (J + 1))) \underset{cn}{⟶} ℂ$
123	49 57 58 60 61 122 19	cncfshiftioo	$⊢ φ \to R : (L (E (S (J))) + U, E (S (J + 1)) + U) \underset{cn}{⟶} ℂ$
124	19	a1i	$⊢ φ \to R = (y \in (L (E (S (J))) + U, E (S (J + 1)) + U) ⟼ G (y - U))$
125	17	oveq2i	$⊢ L (E (S (J))) + U = L (E (S (J))) + S (J + 1) - E (S (J + 1))$
126	125	a1i	$⊢ φ \to L (E (S (J))) + U = L (E (S (J))) + S (J + 1) - E (S (J + 1))$
127	69 66	oveq12d	$⊢ j = J \to E (S (j + 1)) - L (E (S (j))) = E (S (J + 1)) - L (E (S (J)))$
128	68 64	oveq12d	$⊢ j = J \to S (j + 1) - S (j) = S (J + 1) - S (J)$
129	127 128	eqeq12d	$⊢ j = J \to (E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j) \leftrightarrow E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J))$
130	63 129	imbi12d	$⊢ j = J \to (((φ \land j \in (0 ..^N)) \to E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j)) \leftrightarrow ((φ \land J \in (0 ..^N)) \to E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J)))$
131	85	fveq2i	$⊢ \|H\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\|$
132	131	oveq1i	$⊢ \|H\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
133	12 132	eqtri	$⊢ N = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
134		isoeq5	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\} \to (f {Isom}_{<, <} ((0 \dots N), H) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
135	85 134	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots N), H) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
136	135	iotabii	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots N), H)) = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
137	13 136	eqtri	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
138		eqid	$⊢ S (j) + B - E (S (j)) = S (j) + B - E (S (j))$
139	1 2 3 4 8 9 10 133 137 14 15 138	fourierdlem65	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) - L (E (S (j))) = S (j + 1) - S (j)$
140	130 139	vtoclg	$⊢ J \in (0 ..^N) \to ((φ \land J \in (0 ..^N)) \to E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J))$
141	140	anabsi7	$⊢ (φ \land J \in (0 ..^N)) \to E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J)$
142	16 141	mpdan	$⊢ φ \to E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J)$
143	57	recnd	$⊢ φ \to E (S (J + 1)) \in ℂ$
144	55	recnd	$⊢ φ \to S (J + 1) \in ℂ$
145	8 29	iccssred	$⊢ φ \to [C, D] \subseteq ℝ$
146		ax-resscn	$⊢ ℝ \subseteq ℂ$
147	145 146	sstrdi	$⊢ φ \to [C, D] \subseteq ℂ$
148	10 37 36	fourierdlem15	$⊢ φ \to S : (0 \dots N) ⟶ [C, D]$
149	148 45	ffvelrnd	$⊢ φ \to S (J) \in [C, D]$
150	147 149	sseldd	$⊢ φ \to S (J) \in ℂ$
151	144 150	subcld	$⊢ φ \to S (J + 1) - S (J) \in ℂ$
152	49	recnd	$⊢ φ \to L (E (S (J))) \in ℂ$
153	143 151 152	subsub23d	$⊢ φ \to (E (S (J + 1)) - (S (J + 1) - S (J)) = L (E (S (J))) \leftrightarrow E (S (J + 1)) - L (E (S (J))) = S (J + 1) - S (J))$
154	142 153	mpbird	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) = L (E (S (J)))$
155	154	eqcomd	$⊢ φ \to L (E (S (J))) = E (S (J + 1)) - (S (J + 1) - S (J))$
156	155	oveq1d	$⊢ φ \to L (E (S (J))) + S (J + 1) - E (S (J + 1)) = (E (S (J + 1)) - (S (J + 1) - S (J))) + S (J + 1) - E (S (J + 1))$
157	143 151	subcld	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) \in ℂ$
158	157 144 143	addsub12d	$⊢ φ \to (E (S (J + 1)) - (S (J + 1) - S (J))) + S (J + 1) - E (S (J + 1)) = S (J + 1) + (E (S (J + 1)) - (S (J + 1) - S (J))) - E (S (J + 1))$
159	143 151 143	sub32d	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) - E (S (J + 1)) = E (S (J + 1)) - E (S (J + 1)) - (S (J + 1) - S (J))$
160	143	subidd	$⊢ φ \to E (S (J + 1)) - E (S (J + 1)) = 0$
161	160	oveq1d	$⊢ φ \to E (S (J + 1)) - E (S (J + 1)) - (S (J + 1) - S (J)) = 0 - (S (J + 1) - S (J))$
162		df-neg	$⊢ - (S (J + 1) - S (J)) = 0 - (S (J + 1) - S (J))$
163	144 150	negsubdi2d	$⊢ φ \to - (S (J + 1) - S (J)) = S (J) - S (J + 1)$
164	162 163	eqtr3id	$⊢ φ \to 0 - (S (J + 1) - S (J)) = S (J) - S (J + 1)$
165	159 161 164	3eqtrd	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) - E (S (J + 1)) = S (J) - S (J + 1)$
166	165	oveq2d	$⊢ φ \to S (J + 1) + (E (S (J + 1)) - (S (J + 1) - S (J))) - E (S (J + 1)) = S (J + 1) + S (J) - S (J + 1)$
167	144 150	pncan3d	$⊢ φ \to S (J + 1) + S (J) - S (J + 1) = S (J)$
168	158 166 167	3eqtrd	$⊢ φ \to (E (S (J + 1)) - (S (J + 1) - S (J))) + S (J + 1) - E (S (J + 1)) = S (J)$
169	126 156 168	3eqtrd	$⊢ φ \to L (E (S (J))) + U = S (J)$
170	17	oveq2i	$⊢ E (S (J + 1)) + U = E (S (J + 1)) + S (J + 1) - E (S (J + 1))$
171	143 144	pncan3d	$⊢ φ \to E (S (J + 1)) + S (J + 1) - E (S (J + 1)) = S (J + 1)$
172	170 171	eqtrid	$⊢ φ \to E (S (J + 1)) + U = S (J + 1)$
173	169 172	oveq12d	$⊢ φ \to (L (E (S (J))) + U, E (S (J + 1)) + U) = (S (J), S (J + 1))$
174	173	mpteq1d	$⊢ φ \to (y \in (L (E (S (J))) + U, E (S (J + 1)) + U) ⟼ G (y - U)) = (y \in (S (J), S (J + 1)) ⟼ G (y - U))$
175	5	feqmptd	$⊢ φ \to F = (y \in ℝ ⟼ F (y))$
176	175	reseq1d	$⊢ φ \to {F ↾}_{(S (J), S (J + 1))} = {(y \in ℝ ⟼ F (y)) ↾}_{(S (J), S (J + 1))}$
177		ioossre	$⊢ (S (J), S (J + 1)) \subseteq ℝ$
178	177	a1i	$⊢ φ \to (S (J), S (J + 1)) \subseteq ℝ$
179	178	resmptd	$⊢ φ \to {(y \in ℝ ⟼ F (y)) ↾}_{(S (J), S (J + 1))} = (y \in (S (J), S (J + 1)) ⟼ F (y))$
180	18	fveq1i	$⊢ G (y - U) = ({F ↾}_{(L (E (S (J))), E (S (J + 1)))}) (y - U)$
181	180	a1i	$⊢ (φ \land y \in (S (J), S (J + 1))) \to G (y - U) = ({F ↾}_{(L (E (S (J))), E (S (J + 1)))}) (y - U)$
182	49	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to L (E (S (J))) \in ℝ$
183	182	rexrd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to L (E (S (J))) \in ℝ^{*}$
184	57	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) \in ℝ$
185	184	rexrd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) \in ℝ^{*}$
186	178	sselda	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y \in ℝ$
187	60	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to U \in ℝ$
188	186 187	resubcld	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U \in ℝ$
189	46	rexrd	$⊢ φ \to S (J) \in ℝ^{*}$
190	189	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to S (J) \in ℝ^{*}$
191	55	rexrd	$⊢ φ \to S (J + 1) \in ℝ^{*}$
192	191	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to S (J + 1) \in ℝ^{*}$
193		simpr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y \in (S (J), S (J + 1))$
194		ioogtlb	$⊢ (S (J) \in ℝ^{} \land S (J + 1) \in ℝ^{} \land y \in (S (J), S (J + 1))) \to S (J) < y$
195	190 192 193 194	syl3anc	$⊢ (φ \land y \in (S (J), S (J + 1))) \to S (J) < y$
196	169	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to L (E (S (J))) + U = S (J)$
197	186	recnd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y \in ℂ$
198	187	recnd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to U \in ℂ$
199	197 198	npcand	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U + U = y$
200	195 196 199	3brtr4d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to L (E (S (J))) + U < y - U + U$
201	182 188 187	ltadd1d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to (L (E (S (J))) < y - U \leftrightarrow L (E (S (J))) + U < y - U + U)$
202	200 201	mpbird	$⊢ (φ \land y \in (S (J), S (J + 1))) \to L (E (S (J))) < y - U$
203		iooltub	$⊢ (S (J) \in ℝ^{} \land S (J + 1) \in ℝ^{} \land y \in (S (J), S (J + 1))) \to y < S (J + 1)$
204	190 192 193 203	syl3anc	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y < S (J + 1)$
205	172	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) + U = S (J + 1)$
206	204 199 205	3brtr4d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U + U < E (S (J + 1)) + U$
207	188 184 187	ltadd1d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to (y - U < E (S (J + 1)) \leftrightarrow y - U + U < E (S (J + 1)) + U)$
208	206 207	mpbird	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U < E (S (J + 1))$
209	183 185 188 202 208	eliood	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U \in (L (E (S (J))), E (S (J + 1)))$
210		fvres	$⊢ y - U \in (L (E (S (J))), E (S (J + 1))) \to ({F ↾}_{(L (E (S (J))), E (S (J + 1)))}) (y - U) = F (y - U)$
211	209 210	syl	$⊢ (φ \land y \in (S (J), S (J + 1))) \to ({F ↾}_{(L (E (S (J))), E (S (J + 1)))}) (y - U) = F (y - U)$
212	17	oveq2i	$⊢ y - U = y - (S (J + 1) - E (S (J + 1)))$
213	212	a1i	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U = y - (S (J + 1) - E (S (J + 1)))$
214	144	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to S (J + 1) \in ℂ$
215	143	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) \in ℂ$
216	197 214 215	subsub2d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - (S (J + 1) - E (S (J + 1))) = y + E (S (J + 1)) - S (J + 1)$
217	215 214	subcld	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) - S (J + 1) \in ℂ$
218	23 22	resubcld	$⊢ φ \to B - A \in ℝ$
219	2 218	eqeltrid	$⊢ φ \to T \in ℝ$
220	219	recnd	$⊢ φ \to T \in ℂ$
221	220	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to T \in ℂ$
222	22 23	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
223	25 222	mpbid	$⊢ φ \to 0 < B - A$
224	223 2	breqtrrdi	$⊢ φ \to 0 < T$
225	224	gt0ne0d	$⊢ φ \to T \neq 0$
226	225	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to T \neq 0$
227	217 221 226	divcan1d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to (\frac{E (S (J + 1)) - S (J + 1)}{T}) T = E (S (J + 1)) - S (J + 1)$
228	227	eqcomd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to E (S (J + 1)) - S (J + 1) = (\frac{E (S (J + 1)) - S (J + 1)}{T}) T$
229	228	oveq2d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y + E (S (J + 1)) - S (J + 1) = y + (\frac{E (S (J + 1)) - S (J + 1)}{T}) T$
230	213 216 229	3eqtrd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to y - U = y + (\frac{E (S (J + 1)) - S (J + 1)}{T}) T$
231	230	fveq2d	$⊢ (φ \land y \in (S (J), S (J + 1))) \to F (y - U) = F (y + (\frac{E (S (J + 1)) - S (J + 1)}{T}) T)$
232	5	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to F : ℝ ⟶ ℂ$
233	219	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to T \in ℝ$
234	14	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
235		id	$⊢ x = S (J + 1) \to x = S (J + 1)$
236		oveq2	$⊢ x = S (J + 1) \to B - x = B - S (J + 1)$
237	236	oveq1d	$⊢ x = S (J + 1) \to \frac{B - x}{T} = \frac{B - S (J + 1)}{T}$
238	237	fveq2d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (J + 1)}{T}⌋$
239	238	oveq1d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (J + 1)}{T}⌋ T$
240	235 239	oveq12d	$⊢ x = S (J + 1) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
241	240	adantl	$⊢ (φ \land x = S (J + 1)) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
242	23 55	resubcld	$⊢ φ \to B - S (J + 1) \in ℝ$
243	242 219 225	redivcld	$⊢ φ \to \frac{B - S (J + 1)}{T} \in ℝ$
244	243	flcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℤ$
245	244	zred	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℝ$
246	245 219	remulcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
247	55 246	readdcld	$⊢ φ \to S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
248	234 241 55 247	fvmptd	$⊢ φ \to E (S (J + 1)) = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
249	248	oveq1d	$⊢ φ \to E (S (J + 1)) - S (J + 1) = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T - S (J + 1)$
250	245	recnd	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℂ$
251	250 220	mulcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℂ$
252	144 251	pncan2d	$⊢ φ \to S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T - S (J + 1) = ⌊\frac{B - S (J + 1)}{T}⌋ T$
253	249 252	eqtrd	$⊢ φ \to E (S (J + 1)) - S (J + 1) = ⌊\frac{B - S (J + 1)}{T}⌋ T$
254	253	oveq1d	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} = \frac{⌊\frac{B - S (J + 1)}{T}⌋ T}{T}$
255	250 220 225	divcan4d	$⊢ φ \to \frac{⌊\frac{B - S (J + 1)}{T}⌋ T}{T} = ⌊\frac{B - S (J + 1)}{T}⌋$
256	254 255	eqtrd	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} = ⌊\frac{B - S (J + 1)}{T}⌋$
257	256 244	eqeltrd	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} \in ℤ$
258	257	adantr	$⊢ (φ \land y \in (S (J), S (J + 1))) \to \frac{E (S (J + 1)) - S (J + 1)}{T} \in ℤ$
259	6	adantlr	$⊢ ((φ \land y \in (S (J), S (J + 1))) \land x \in ℝ) \to F (x + T) = F (x)$
260	232 233 258 186 259	fperiodmul	$⊢ (φ \land y \in (S (J), S (J + 1))) \to F (y + (\frac{E (S (J + 1)) - S (J + 1)}{T}) T) = F (y)$
261	231 260	eqtrd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to F (y - U) = F (y)$
262	181 211 261	3eqtrrd	$⊢ (φ \land y \in (S (J), S (J + 1))) \to F (y) = G (y - U)$
263	262	mpteq2dva	$⊢ φ \to (y \in (S (J), S (J + 1)) ⟼ F (y)) = (y \in (S (J), S (J + 1)) ⟼ G (y - U))$
264	176 179 263	3eqtrrd	$⊢ φ \to (y \in (S (J), S (J + 1)) ⟼ G (y - U)) = {F ↾}_{(S (J), S (J + 1))}$
265	124 174 264	3eqtrd	$⊢ φ \to R = {F ↾}_{(S (J), S (J + 1))}$
266	173	oveq1d	$⊢ φ \to (L (E (S (J))) + U, E (S (J + 1)) + U) \underset{cn}{⟶} ℂ = (S (J), S (J + 1)) \underset{cn}{⟶} ℂ$
267	123 265 266	3eltr3d	$⊢ φ \to ({F ↾}_{(S (J), S (J + 1))}) : (S (J), S (J + 1)) \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem fourierdlem90

Proof