fourierdlem89

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

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

Proof

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

Metamath Proof Explorer

Theorem fourierdlem89

Proof