fourierdlem91

Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019)

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

Proof

Step	Hyp	Ref	Expression
1		fourierdlem91.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		fourierdlem91.t	$⊢ T = B - A$
3		fourierdlem91.m	$⊢ φ \to M \in ℕ$
4		fourierdlem91.q	$⊢ φ \to Q \in P (M)$
5		fourierdlem91.f	$⊢ φ \to F : ℝ ⟶ ℂ$
6		fourierdlem91.6	$⊢ (φ \land x \in ℝ) \to F (x + T) = F (x)$
7		fourierdlem91.fcn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
8		fourierdlem91.l	$⊢ (φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
9		fourierdlem91.c	$⊢ φ \to C \in ℝ$
10		fourierdlem91.d	$⊢ φ \to D \in (C, +∞)$
11		fourierdlem91.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))\})$
12		fourierdlem91.h	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}$
13		fourierdlem91.n	$⊢ N = \|H\| - 1$
14		fourierdlem91.s	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), H))$
15		fourierdlem91.e	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
16		fourierdlem91.J	$⊢ Z = (y \in (A, B] ⟼ if (y = B, A, y))$
17		fourierdlem91.17	$⊢ φ \to J \in (0 ..^N)$
18		fourierdlem91.u	$⊢ U = S (J + 1) - E (S (J + 1))$
19		fourierdlem91.i	$⊢ I = (x \in ℝ ⟼ sup (\{i \in (0 ..^M) \| Q (i) \leq Z (E (x))\} ℝ <))$
20		fourierdlem91.w	$⊢ W = (i \in (0 ..^M) ⟼ L)$
21	1	fourierdlem2	$⊢ M \in ℕ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
22	3 21	syl	$⊢ φ \to (Q \in P (M) \leftrightarrow (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))))$
23	4 22	mpbid	$⊢ φ \to (Q \in (ℝ^{(0 \dots M)}) \land ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1)))$
24	23	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
25		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
26	24 25	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
27		fzossfz	$⊢ (0 ..^M) \subseteq (0 \dots M)$
28	1 3 4 2 15 16 19	fourierdlem37	$⊢ φ \to (I : ℝ ⟶ (0 ..^M) \land (x \in ℝ \to sup (\{i \in (0 ..^M) \| Q (i) \leq Z (E (x))\} ℝ <) \in \{i \in (0 ..^M) \| Q (i) \leq Z (E (x))\}))$
29	28	simpld	$⊢ φ \to I : ℝ ⟶ (0 ..^M)$
30		elioore	$⊢ D \in (C, +∞) \to D \in ℝ$
31	10 30	syl	$⊢ φ \to D \in ℝ$
32		elioo4g	$⊢ D \in (C, +∞) \leftrightarrow ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
33	10 32	sylib	$⊢ φ \to ((C \in ℝ^{} \land +∞ \in ℝ^{} \land D \in ℝ) \land (C < D \land D < +∞))$
34	33	simprd	$⊢ φ \to (C < D \land D < +∞)$
35	34	simpld	$⊢ φ \to C < D$
36		oveq1	$⊢ y = x \to y + k T = x + k T$
37	36	eleq1d	$⊢ y = x \to (y + k T \in ran Q \leftrightarrow x + k T \in ran Q)$
38	37	rexbidv	$⊢ y = x \to (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ x + k T \in ran Q)$
39	38	cbvrabv	$⊢ \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
40	39	uneq2i	$⊢ \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\} = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
41	12	fveq2i	$⊢ \|H\| = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\|$
42	41	oveq1i	$⊢ \|H\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1$
43	13 42	eqtri	$⊢ N = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1$
44		isoeq5	$⊢ H = \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \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 T \in ran Q\}))$
45	12 44	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 T \in ran Q\})$
46	45	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 T \in ran Q\}))$
47	14 46	eqtri	$⊢ S = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}))$
48	2 1 3 4 9 31 35 11 40 43 47	fourierdlem54	$⊢ φ \to ((N \in ℕ \land S \in O (N)) \land S {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}))$
49	48	simpld	$⊢ φ \to (N \in ℕ \land S \in O (N))$
50	49	simprd	$⊢ φ \to S \in O (N)$
51	49	simpld	$⊢ φ \to N \in ℕ$
52	11	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))))$
53	51 52	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))))$
54	50 53	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)))$
55	54	simpld	$⊢ φ \to S \in (ℝ^{(0 \dots N)})$
56		elmapi	$⊢ S \in (ℝ^{(0 \dots N)}) \to S : (0 \dots N) ⟶ ℝ$
57	55 56	syl	$⊢ φ \to S : (0 \dots N) ⟶ ℝ$
58		elfzofz	$⊢ J \in (0 ..^N) \to J \in (0 \dots N)$
59	17 58	syl	$⊢ φ \to J \in (0 \dots N)$
60	57 59	ffvelrnd	$⊢ φ \to S (J) \in ℝ$
61	29 60	ffvelrnd	$⊢ φ \to I (S (J)) \in (0 ..^M)$
62	27 61	sselid	$⊢ φ \to I (S (J)) \in (0 \dots M)$
63	26 62	ffvelrnd	$⊢ φ \to Q (I (S (J))) \in ℝ$
64	63	rexrd	$⊢ φ \to Q (I (S (J))) \in ℝ^{*}$
65	64	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to Q (I (S (J))) \in ℝ^{*}$
66		fzofzp1	$⊢ I (S (J)) \in (0 ..^M) \to I (S (J)) + 1 \in (0 \dots M)$
67	61 66	syl	$⊢ φ \to I (S (J)) + 1 \in (0 \dots M)$
68	26 67	ffvelrnd	$⊢ φ \to Q (I (S (J)) + 1) \in ℝ$
69	68	rexrd	$⊢ φ \to Q (I (S (J)) + 1) \in ℝ^{*}$
70	69	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to Q (I (S (J)) + 1) \in ℝ^{*}$
71	1 3 4	fourierdlem11	$⊢ φ \to (A \in ℝ \land B \in ℝ \land A < B)$
72	71	simp1d	$⊢ φ \to A \in ℝ$
73	72	rexrd	$⊢ φ \to A \in ℝ^{*}$
74	71	simp2d	$⊢ φ \to B \in ℝ$
75		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
76	73 74 75	syl2anc	$⊢ φ \to (A, B] \subseteq ℝ$
77	71	simp3d	$⊢ φ \to A < B$
78	72 74 77 2 15	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
79		fzofzp1	$⊢ J \in (0 ..^N) \to J + 1 \in (0 \dots N)$
80	17 79	syl	$⊢ φ \to J + 1 \in (0 \dots N)$
81	57 80	ffvelrnd	$⊢ φ \to S (J + 1) \in ℝ$
82	78 81	ffvelrnd	$⊢ φ \to E (S (J + 1)) \in (A, B]$
83	76 82	sseldd	$⊢ φ \to E (S (J + 1)) \in ℝ$
84	83	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to E (S (J + 1)) \in ℝ$
85	72 74	iccssred	$⊢ φ \to [A, B] \subseteq ℝ$
86	72 74 77 16	fourierdlem17	$⊢ φ \to Z : (A, B] ⟶ [A, B]$
87	78 60	ffvelrnd	$⊢ φ \to E (S (J)) \in (A, B]$
88	86 87	ffvelrnd	$⊢ φ \to Z (E (S (J))) \in [A, B]$
89	85 88	sseldd	$⊢ φ \to Z (E (S (J))) \in ℝ$
90	54	simprrd	$⊢ φ \to \forall i \in (0 ..^N) S (i) < S (i + 1)$
91		fveq2	$⊢ i = J \to S (i) = S (J)$
92		oveq1	$⊢ i = J \to i + 1 = J + 1$
93	92	fveq2d	$⊢ i = J \to S (i + 1) = S (J + 1)$
94	91 93	breq12d	$⊢ i = J \to (S (i) < S (i + 1) \leftrightarrow S (J) < S (J + 1))$
95	94	rspccva	$⊢ (\forall i \in (0 ..^N) S (i) < S (i + 1) \land J \in (0 ..^N)) \to S (J) < S (J + 1)$
96	90 17 95	syl2anc	$⊢ φ \to S (J) < S (J + 1)$
97	60 81	posdifd	$⊢ φ \to (S (J) < S (J + 1) \leftrightarrow 0 < S (J + 1) - S (J))$
98	96 97	mpbid	$⊢ φ \to 0 < S (J + 1) - S (J)$
99		eleq1	$⊢ j = J \to (j \in (0 ..^N) \leftrightarrow J \in (0 ..^N))$
100	99	anbi2d	$⊢ j = J \to ((φ \land j \in (0 ..^N)) \leftrightarrow (φ \land J \in (0 ..^N)))$
101		oveq1	$⊢ j = J \to j + 1 = J + 1$
102	101	fveq2d	$⊢ j = J \to S (j + 1) = S (J + 1)$
103	102	fveq2d	$⊢ j = J \to E (S (j + 1)) = E (S (J + 1))$
104		fveq2	$⊢ j = J \to S (j) = S (J)$
105	104	fveq2d	$⊢ j = J \to E (S (j)) = E (S (J))$
106	105	fveq2d	$⊢ j = J \to Z (E (S (j))) = Z (E (S (J)))$
107	103 106	oveq12d	$⊢ j = J \to E (S (j + 1)) - Z (E (S (j))) = E (S (J + 1)) - Z (E (S (J)))$
108	102 104	oveq12d	$⊢ j = J \to S (j + 1) - S (j) = S (J + 1) - S (J)$
109	107 108	eqeq12d	$⊢ j = J \to (E (S (j + 1)) - Z (E (S (j))) = S (j + 1) - S (j) \leftrightarrow E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J))$
110	100 109	imbi12d	$⊢ j = J \to (((φ \land j \in (0 ..^N)) \to E (S (j + 1)) - Z (E (S (j))) = S (j + 1) - S (j)) \leftrightarrow ((φ \land J \in (0 ..^N)) \to E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J)))$
111	2	oveq2i	$⊢ k T = k (B - A)$
112	111	oveq2i	$⊢ y + k T = y + k (B - A)$
113	112	eleq1i	$⊢ y + k T \in ran Q \leftrightarrow y + k (B - A) \in ran Q$
114	113	rexbii	$⊢ \exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q$
115	114	rgenw	$⊢ \forall y \in [C, D] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q)$
116		rabbi	$⊢ \forall y \in [C, D] (\exists k \in ℤ y + k T \in ran Q \leftrightarrow \exists k \in ℤ y + k (B - A) \in ran Q) \leftrightarrow \{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\}$
117	115 116	mpbi	$⊢ \{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\}$
118	117	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\}$
119	118	fveq2i	$⊢ \|\{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\}\|$
120	119	oveq1i	$⊢ \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}\| - 1 = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
121	43 120	eqtri	$⊢ N = \|\{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}\| - 1$
122		isoeq5	$⊢ \{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\} \to (f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
123	118 122	ax-mp	$⊢ f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\}) \leftrightarrow f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\})$
124	123	iotabii	$⊢ (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k T \in ran Q\})) = (ι f \| f {Isom}_{<, <} ((0 \dots N), \{C, D\} \cup \{y \in [C, D] \| \exists k \in ℤ y + k (B - A) \in ran Q\}))$
125	47 124	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\}))$
126		eqid	$⊢ S (j) + B - E (S (j)) = S (j) + B - E (S (j))$
127	1 2 3 4 9 10 11 121 125 15 16 126	fourierdlem65	$⊢ (φ \land j \in (0 ..^N)) \to E (S (j + 1)) - Z (E (S (j))) = S (j + 1) - S (j)$
128	110 127	vtoclg	$⊢ J \in (0 ..^N) \to ((φ \land J \in (0 ..^N)) \to E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J))$
129	128	anabsi7	$⊢ (φ \land J \in (0 ..^N)) \to E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J)$
130	17 129	mpdan	$⊢ φ \to E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J)$
131	98 130	breqtrrd	$⊢ φ \to 0 < E (S (J + 1)) - Z (E (S (J)))$
132	89 83	posdifd	$⊢ φ \to (Z (E (S (J))) < E (S (J + 1)) \leftrightarrow 0 < E (S (J + 1)) - Z (E (S (J))))$
133	131 132	mpbird	$⊢ φ \to Z (E (S (J))) < E (S (J + 1))$
134	106 103	oveq12d	$⊢ j = J \to (Z (E (S (j))), E (S (j + 1))) = (Z (E (S (J))), E (S (J + 1)))$
135	104	fveq2d	$⊢ j = J \to I (S (j)) = I (S (J))$
136	135	fveq2d	$⊢ j = J \to Q (I (S (j))) = Q (I (S (J)))$
137	135	oveq1d	$⊢ j = J \to I (S (j)) + 1 = I (S (J)) + 1$
138	137	fveq2d	$⊢ j = J \to Q (I (S (j)) + 1) = Q (I (S (J)) + 1)$
139	136 138	oveq12d	$⊢ j = J \to (Q (I (S (j))), Q (I (S (j)) + 1)) = (Q (I (S (J))), Q (I (S (J)) + 1))$
140	134 139	sseq12d	$⊢ j = J \to ((Z (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1)) \leftrightarrow (Z (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1)))$
141	100 140	imbi12d	$⊢ j = J \to (((φ \land j \in (0 ..^N)) \to (Z (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))) \leftrightarrow ((φ \land J \in (0 ..^N)) \to (Z (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))))$
142	12 40	eqtri	$⊢ H = \{C, D\} \cup \{x \in [C, D] \| \exists k \in ℤ x + k T \in ran Q\}$
143		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})$
144	2 1 3 4 9 31 35 11 142 13 14 15 16 143 19	fourierdlem79	$⊢ (φ \land j \in (0 ..^N)) \to (Z (E (S (j))), E (S (j + 1))) \subseteq (Q (I (S (j))), Q (I (S (j)) + 1))$
145	141 144	vtoclg	$⊢ J \in (0 ..^N) \to ((φ \land J \in (0 ..^N)) \to (Z (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1)))$
146	145	anabsi7	$⊢ (φ \land J \in (0 ..^N)) \to (Z (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))$
147	17 146	mpdan	$⊢ φ \to (Z (E (S (J))), E (S (J + 1))) \subseteq (Q (I (S (J))), Q (I (S (J)) + 1))$
148	63 68 89 83 133 147	fourierdlem10	$⊢ φ \to (Q (I (S (J))) \leq Z (E (S (J))) \land E (S (J + 1)) \leq Q (I (S (J)) + 1))$
149	148	simpld	$⊢ φ \to Q (I (S (J))) \leq Z (E (S (J)))$
150	63 89 83 149 133	lelttrd	$⊢ φ \to Q (I (S (J))) < E (S (J + 1))$
151	150	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to Q (I (S (J))) < E (S (J + 1))$
152	68	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to Q (I (S (J)) + 1) \in ℝ$
153	148	simprd	$⊢ φ \to E (S (J + 1)) \leq Q (I (S (J)) + 1)$
154	153	adantr	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to E (S (J + 1)) \leq Q (I (S (J)) + 1)$
155		neqne	$⊢ \neg E (S (J + 1)) = Q (I (S (J)) + 1) \to E (S (J + 1)) \neq Q (I (S (J)) + 1)$
156	155	necomd	$⊢ \neg E (S (J + 1)) = Q (I (S (J)) + 1) \to Q (I (S (J)) + 1) \neq E (S (J + 1))$
157	156	adantl	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to Q (I (S (J)) + 1) \neq E (S (J + 1))$
158	84 152 154 157	leneltd	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to E (S (J + 1)) < Q (I (S (J)) + 1)$
159	65 70 84 151 158	eliood	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to E (S (J + 1)) \in (Q (I (S (J))), Q (I (S (J)) + 1))$
160		fvres	$⊢ E (S (J + 1)) \in (Q (I (S (J))), Q (I (S (J)) + 1)) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1))) = F (E (S (J + 1)))$
161	159 160	syl	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1))) = F (E (S (J + 1)))$
162	161	eqcomd	$⊢ (φ \land \neg E (S (J + 1)) = Q (I (S (J)) + 1)) \to F (E (S (J + 1))) = ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))$
163	162	ifeq2da	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), F (E (S (J + 1)))) = if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1))))$
164		fdm	$⊢ F : ℝ ⟶ ℂ \to dom F = ℝ$
165	5 164	syl	$⊢ φ \to dom F = ℝ$
166	165	feq2d	$⊢ φ \to (F : dom F ⟶ ℂ \leftrightarrow F : ℝ ⟶ ℂ)$
167	5 166	mpbird	$⊢ φ \to F : dom F ⟶ ℂ$
168		ioosscn	$⊢ (Z (E (S (J))), E (S (J + 1))) \subseteq ℂ$
169	168	a1i	$⊢ φ \to (Z (E (S (J))), E (S (J + 1))) \subseteq ℂ$
170		ioossre	$⊢ (Z (E (S (J))), E (S (J + 1))) \subseteq ℝ$
171	170 165	sseqtrrid	$⊢ φ \to (Z (E (S (J))), E (S (J + 1))) \subseteq dom F$
172	81 83	resubcld	$⊢ φ \to S (J + 1) - E (S (J + 1)) \in ℝ$
173	18 172	eqeltrid	$⊢ φ \to U \in ℝ$
174	173	recnd	$⊢ φ \to U \in ℂ$
175		eqid	$⊢ \{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\} = \{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}$
176	89 83 173	iooshift	$⊢ φ \to (Z (E (S (J))) + U, E (S (J + 1)) + U) = \{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}$
177		ioossre	$⊢ (Z (E (S (J))) + U, E (S (J + 1)) + U) \subseteq ℝ$
178	177 165	sseqtrrid	$⊢ φ \to (Z (E (S (J))) + U, E (S (J + 1)) + U) \subseteq dom F$
179	176 178	eqsstrrd	$⊢ φ \to \{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\} \subseteq dom F$
180		elioore	$⊢ y \in (Z (E (S (J))), E (S (J + 1))) \to y \in ℝ$
181	74 72	resubcld	$⊢ φ \to B - A \in ℝ$
182	2 181	eqeltrid	$⊢ φ \to T \in ℝ$
183	182	recnd	$⊢ φ \to T \in ℂ$
184	72 74	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
185	77 184	mpbid	$⊢ φ \to 0 < B - A$
186	185 2	breqtrrdi	$⊢ φ \to 0 < T$
187	186	gt0ne0d	$⊢ φ \to T \neq 0$
188	174 183 187	divcan1d	$⊢ φ \to (\frac{U}{T}) T = U$
189	188	eqcomd	$⊢ φ \to U = (\frac{U}{T}) T$
190	189	oveq2d	$⊢ φ \to y + U = y + (\frac{U}{T}) T$
191	190	adantr	$⊢ (φ \land y \in ℝ) \to y + U = y + (\frac{U}{T}) T$
192	191	fveq2d	$⊢ (φ \land y \in ℝ) \to F (y + U) = F (y + (\frac{U}{T}) T)$
193	5	adantr	$⊢ (φ \land y \in ℝ) \to F : ℝ ⟶ ℂ$
194	182	adantr	$⊢ (φ \land y \in ℝ) \to T \in ℝ$
195	83	recnd	$⊢ φ \to E (S (J + 1)) \in ℂ$
196	81	recnd	$⊢ φ \to S (J + 1) \in ℂ$
197	195 196	negsubdi2d	$⊢ φ \to - (E (S (J + 1)) - S (J + 1)) = S (J + 1) - E (S (J + 1))$
198	197	eqcomd	$⊢ φ \to S (J + 1) - E (S (J + 1)) = - (E (S (J + 1)) - S (J + 1))$
199	198	oveq1d	$⊢ φ \to \frac{S (J + 1) - E (S (J + 1))}{T} = \frac{- (E (S (J + 1)) - S (J + 1))}{T}$
200	18	oveq1i	$⊢ \frac{U}{T} = \frac{S (J + 1) - E (S (J + 1))}{T}$
201	200	a1i	$⊢ φ \to \frac{U}{T} = \frac{S (J + 1) - E (S (J + 1))}{T}$
202	15	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
203		id	$⊢ x = S (J + 1) \to x = S (J + 1)$
204		oveq2	$⊢ x = S (J + 1) \to B - x = B - S (J + 1)$
205	204	oveq1d	$⊢ x = S (J + 1) \to \frac{B - x}{T} = \frac{B - S (J + 1)}{T}$
206	205	fveq2d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - S (J + 1)}{T}⌋$
207	206	oveq1d	$⊢ x = S (J + 1) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - S (J + 1)}{T}⌋ T$
208	203 207	oveq12d	$⊢ x = S (J + 1) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
209	208	adantl	$⊢ (φ \land x = S (J + 1)) \to x + ⌊\frac{B - x}{T}⌋ T = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
210	74 81	resubcld	$⊢ φ \to B - S (J + 1) \in ℝ$
211	210 182 187	redivcld	$⊢ φ \to \frac{B - S (J + 1)}{T} \in ℝ$
212	211	flcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℤ$
213	212	zred	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℝ$
214	213 182	remulcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
215	81 214	readdcld	$⊢ φ \to S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℝ$
216	202 209 81 215	fvmptd	$⊢ φ \to E (S (J + 1)) = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T$
217	216	oveq1d	$⊢ φ \to E (S (J + 1)) - S (J + 1) = S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T - S (J + 1)$
218	212	zcnd	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ \in ℂ$
219	218 183	mulcld	$⊢ φ \to ⌊\frac{B - S (J + 1)}{T}⌋ T \in ℂ$
220	196 219	pncan2d	$⊢ φ \to S (J + 1) + ⌊\frac{B - S (J + 1)}{T}⌋ T - S (J + 1) = ⌊\frac{B - S (J + 1)}{T}⌋ T$
221	217 220	eqtrd	$⊢ φ \to E (S (J + 1)) - S (J + 1) = ⌊\frac{B - S (J + 1)}{T}⌋ T$
222	221 219	eqeltrd	$⊢ φ \to E (S (J + 1)) - S (J + 1) \in ℂ$
223	222 183 187	divnegd	$⊢ φ \to - \frac{E (S (J + 1)) - S (J + 1)}{T} = \frac{- (E (S (J + 1)) - S (J + 1))}{T}$
224	199 201 223	3eqtr4d	$⊢ φ \to \frac{U}{T} = - \frac{E (S (J + 1)) - S (J + 1)}{T}$
225	221	oveq1d	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} = \frac{⌊\frac{B - S (J + 1)}{T}⌋ T}{T}$
226	218 183 187	divcan4d	$⊢ φ \to \frac{⌊\frac{B - S (J + 1)}{T}⌋ T}{T} = ⌊\frac{B - S (J + 1)}{T}⌋$
227	225 226	eqtrd	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} = ⌊\frac{B - S (J + 1)}{T}⌋$
228	227 212	eqeltrd	$⊢ φ \to \frac{E (S (J + 1)) - S (J + 1)}{T} \in ℤ$
229	228	znegcld	$⊢ φ \to - \frac{E (S (J + 1)) - S (J + 1)}{T} \in ℤ$
230	224 229	eqeltrd	$⊢ φ \to \frac{U}{T} \in ℤ$
231	230	adantr	$⊢ (φ \land y \in ℝ) \to \frac{U}{T} \in ℤ$
232		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
233	6	adantlr	$⊢ ((φ \land y \in ℝ) \land x \in ℝ) \to F (x + T) = F (x)$
234	193 194 231 232 233	fperiodmul	$⊢ (φ \land y \in ℝ) \to F (y + (\frac{U}{T}) T) = F (y)$
235	192 234	eqtrd	$⊢ (φ \land y \in ℝ) \to F (y + U) = F (y)$
236	180 235	sylan2	$⊢ (φ \land y \in (Z (E (S (J))), E (S (J + 1)))) \to F (y + U) = F (y)$
237	23	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
238		fveq2	$⊢ i = I (S (J)) \to Q (i) = Q (I (S (J)))$
239		oveq1	$⊢ i = I (S (J)) \to i + 1 = I (S (J)) + 1$
240	239	fveq2d	$⊢ i = I (S (J)) \to Q (i + 1) = Q (I (S (J)) + 1)$
241	238 240	breq12d	$⊢ i = I (S (J)) \to (Q (i) < Q (i + 1) \leftrightarrow Q (I (S (J))) < Q (I (S (J)) + 1))$
242	241	rspccva	$⊢ (\forall i \in (0 ..^M) Q (i) < Q (i + 1) \land I (S (J)) \in (0 ..^M)) \to Q (I (S (J))) < Q (I (S (J)) + 1)$
243	237 61 242	syl2anc	$⊢ φ \to Q (I (S (J))) < Q (I (S (J)) + 1)$
244	61	ancli	$⊢ φ \to (φ \land I (S (J)) \in (0 ..^M))$
245		eleq1	$⊢ i = I (S (J)) \to (i \in (0 ..^M) \leftrightarrow I (S (J)) \in (0 ..^M))$
246	245	anbi2d	$⊢ i = I (S (J)) \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land I (S (J)) \in (0 ..^M)))$
247	238 240	oveq12d	$⊢ i = I (S (J)) \to (Q (i), Q (i + 1)) = (Q (I (S (J))), Q (I (S (J)) + 1))$
248	247	reseq2d	$⊢ i = I (S (J)) \to {F ↾}_{(Q (i), Q (i + 1))} = {F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}$
249	247	oveq1d	$⊢ i = I (S (J)) \to (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ = (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ$
250	248 249	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}{⟶} ℂ)$
251	246 250	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}{⟶} ℂ))$
252	251 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}{⟶} ℂ)$
253	61 244 252	sylc	$⊢ φ \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) : (Q (I (S (J))), Q (I (S (J)) + 1)) \underset{cn}{⟶} ℂ$
254		nfv	$⊢ Ⅎ i (φ \land I (S (J)) \in (0 ..^M))$
255		nfmpt1	$⊢ \underline{Ⅎ} i (i \in (0 ..^M) ⟼ L)$
256	20 255	nfcxfr	$⊢ \underline{Ⅎ} i W$
257		nfcv	$⊢ \underline{Ⅎ} i I (S (J))$
258	256 257	nffv	$⊢ \underline{Ⅎ} i W (I (S (J)))$
259	258	nfel1	$⊢ Ⅎ i W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))$
260	254 259	nfim	$⊢ Ⅎ i ((φ \land I (S (J)) \in (0 ..^M)) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1)))$
261	246	biimpar	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to (φ \land i \in (0 ..^M))$
262	261	3adant2	$⊢ (i = I (S (J)) \land ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \land (φ \land I (S (J)) \in (0 ..^M))) \to (φ \land i \in (0 ..^M))$
263	262 8	syl	$⊢ (i = I (S (J)) \land ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \land (φ \land I (S (J)) \in (0 ..^M))) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))$
264		fveq2	$⊢ i = I (S (J)) \to W (i) = W (I (S (J)))$
265	264	eqcomd	$⊢ i = I (S (J)) \to W (I (S (J))) = W (i)$
266	265	adantr	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to W (I (S (J))) = W (i)$
267	261	simprd	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to i \in (0 ..^M)$
268		elex	$⊢ L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)) \to L \in V$
269	261 8 268	3syl	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to L \in V$
270	20	fvmpt2	$⊢ (i \in (0 ..^M) \land L \in V) \to W (i) = L$
271	267 269 270	syl2anc	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to W (i) = L$
272	266 271	eqtrd	$⊢ (i = I (S (J)) \land (φ \land I (S (J)) \in (0 ..^M))) \to W (I (S (J))) = L$
273	272	3adant2	$⊢ (i = I (S (J)) \land ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \land (φ \land I (S (J)) \in (0 ..^M))) \to W (I (S (J))) = L$
274	248 240	oveq12d	$⊢ i = I (S (J)) \to ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1) = ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1)$
275	274	eqcomd	$⊢ i = I (S (J)) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1) = ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
276	275	3ad2ant1	$⊢ (i = I (S (J)) \land ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \land (φ \land I (S (J)) \in (0 ..^M))) \to ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1) = ({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1)$
277	263 273 276	3eltr4d	$⊢ (i = I (S (J)) \land ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \land (φ \land I (S (J)) \in (0 ..^M))) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))$
278	277	3exp	$⊢ i = I (S (J)) \to (((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \to ((φ \land I (S (J)) \in (0 ..^M)) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))))$
279	8	2a1i	$⊢ i = I (S (J)) \to (((φ \land I (S (J)) \in (0 ..^M)) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))) \to ((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))))$
280	278 279	impbid	$⊢ i = I (S (J)) \to (((φ \land i \in (0 ..^M)) \to L \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i + 1))) \leftrightarrow ((φ \land I (S (J)) \in (0 ..^M)) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))))$
281	260 280 8	vtoclg1f	$⊢ I (S (J)) \in (0 ..^M) \to ((φ \land I (S (J)) \in (0 ..^M)) \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1)))$
282	61 244 281	sylc	$⊢ φ \to W (I (S (J))) \in (({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) {lim}_{ℂ} Q (I (S (J)) + 1))$
283		eqid	$⊢ if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) = if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1))))$
284		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (I (S (J))), Q (I (S (J)) + 1)) \cup \{Q (I (S (J)) + 1)\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ((Q (I (S (J))), Q (I (S (J)) + 1)) \cup \{Q (I (S (J)) + 1)\})$
285	63 68 243 253 282 89 83 133 147 283 284	fourierdlem33	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) \in (({({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(Z (E (S (J))), E (S (J + 1)))}) {lim}_{ℂ} E (S (J + 1)))$
286	147	resabs1d	$⊢ φ \to {({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(Z (E (S (J))), E (S (J + 1)))} = {F ↾}_{(Z (E (S (J))), E (S (J + 1)))}$
287	286	oveq1d	$⊢ φ \to ({({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) ↾}_{(Z (E (S (J))), E (S (J + 1)))}) {lim}_{ℂ} E (S (J + 1)) = ({F ↾}_{(Z (E (S (J))), E (S (J + 1)))}) {lim}_{ℂ} E (S (J + 1))$
288	285 287	eleqtrd	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) \in (({F ↾}_{(Z (E (S (J))), E (S (J + 1)))}) {lim}_{ℂ} E (S (J + 1)))$
289	167 169 171 174 175 179 236 288	limcperiod	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) \in (({F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}}) {lim}_{ℂ} (E (S (J + 1)) + U))$
290	18	oveq2i	$⊢ E (S (J + 1)) + U = E (S (J + 1)) + S (J + 1) - E (S (J + 1))$
291	195 196	pncan3d	$⊢ φ \to E (S (J + 1)) + S (J + 1) - E (S (J + 1)) = S (J + 1)$
292	290 291	syl5eq	$⊢ φ \to E (S (J + 1)) + U = S (J + 1)$
293	292	oveq2d	$⊢ φ \to ({F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}}) {lim}_{ℂ} (E (S (J + 1)) + U) = ({F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}}) {lim}_{ℂ} S (J + 1)$
294	289 293	eleqtrd	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) \in (({F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}}) {lim}_{ℂ} S (J + 1))$
295	18	oveq2i	$⊢ Z (E (S (J))) + U = Z (E (S (J))) + S (J + 1) - E (S (J + 1))$
296	295	a1i	$⊢ φ \to Z (E (S (J))) + U = Z (E (S (J))) + S (J + 1) - E (S (J + 1))$
297	9 31	iccssred	$⊢ φ \to [C, D] \subseteq ℝ$
298		ax-resscn	$⊢ ℝ \subseteq ℂ$
299	297 298	sstrdi	$⊢ φ \to [C, D] \subseteq ℂ$
300	11 51 50	fourierdlem15	$⊢ φ \to S : (0 \dots N) ⟶ [C, D]$
301	300 59	ffvelrnd	$⊢ φ \to S (J) \in [C, D]$
302	299 301	sseldd	$⊢ φ \to S (J) \in ℂ$
303	196 302	subcld	$⊢ φ \to S (J + 1) - S (J) \in ℂ$
304	89	recnd	$⊢ φ \to Z (E (S (J))) \in ℂ$
305	195 303 304	subsub23d	$⊢ φ \to (E (S (J + 1)) - (S (J + 1) - S (J)) = Z (E (S (J))) \leftrightarrow E (S (J + 1)) - Z (E (S (J))) = S (J + 1) - S (J))$
306	130 305	mpbird	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) = Z (E (S (J)))$
307	306	eqcomd	$⊢ φ \to Z (E (S (J))) = E (S (J + 1)) - (S (J + 1) - S (J))$
308	307	oveq1d	$⊢ φ \to Z (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))$
309	195 303	subcld	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) \in ℂ$
310	309 196 195	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))$
311	195 303 195	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))$
312	195	subidd	$⊢ φ \to E (S (J + 1)) - E (S (J + 1)) = 0$
313	312	oveq1d	$⊢ φ \to E (S (J + 1)) - E (S (J + 1)) - (S (J + 1) - S (J)) = 0 - (S (J + 1) - S (J))$
314		df-neg	$⊢ - (S (J + 1) - S (J)) = 0 - (S (J + 1) - S (J))$
315	196 302	negsubdi2d	$⊢ φ \to - (S (J + 1) - S (J)) = S (J) - S (J + 1)$
316	314 315	eqtr3id	$⊢ φ \to 0 - (S (J + 1) - S (J)) = S (J) - S (J + 1)$
317	311 313 316	3eqtrd	$⊢ φ \to E (S (J + 1)) - (S (J + 1) - S (J)) - E (S (J + 1)) = S (J) - S (J + 1)$
318	317	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)$
319	196 302	pncan3d	$⊢ φ \to S (J + 1) + S (J) - S (J + 1) = S (J)$
320	310 318 319	3eqtrd	$⊢ φ \to (E (S (J + 1)) - (S (J + 1) - S (J))) + S (J + 1) - E (S (J + 1)) = S (J)$
321	296 308 320	3eqtrd	$⊢ φ \to Z (E (S (J))) + U = S (J)$
322	321 292	oveq12d	$⊢ φ \to (Z (E (S (J))) + U, E (S (J + 1)) + U) = (S (J), S (J + 1))$
323	176 322	eqtr3d	$⊢ φ \to \{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\} = (S (J), S (J + 1))$
324	323	reseq2d	$⊢ φ \to {F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}} = {F ↾}_{(S (J), S (J + 1))}$
325	324	oveq1d	$⊢ φ \to ({F ↾}_{\{x \in ℂ \| \exists y \in (Z (E (S (J))), E (S (J + 1))) x = y + U\}}) {lim}_{ℂ} S (J + 1) = ({F ↾}_{(S (J), S (J + 1))}) {lim}_{ℂ} S (J + 1)$
326	294 325	eleqtrd	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), ({F ↾}_{(Q (I (S (J))), Q (I (S (J)) + 1))}) (E (S (J + 1)))) \in (({F ↾}_{(S (J), S (J + 1))}) {lim}_{ℂ} S (J + 1))$
327	163 326	eqeltrd	$⊢ φ \to if (E (S (J + 1)) = Q (I (S (J)) + 1), W (I (S (J))), F (E (S (J + 1)))) \in (({F ↾}_{(S (J), S (J + 1))}) {lim}_{ℂ} S (J + 1))$

Metamath Proof Explorer

Theorem fourierdlem91

Proof