fourierdlem48

Description: The given periodic function F has a right limit at every point in the reals. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem48.a	$⊢ φ \to A \in ℝ$
	fourierdlem48.b	$⊢ φ \to B \in ℝ$
	fourierdlem48.altb	$⊢ φ \to A < B$
	fourierdlem48.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))\})$
	fourierdlem48.t	$⊢ T = B - A$
	fourierdlem48.m	$⊢ φ \to M \in ℕ$
	fourierdlem48.q	$⊢ φ \to Q \in P (M)$
	fourierdlem48.f	$⊢ φ \to F : D ⟶ ℝ$
	fourierdlem48.dper	$⊢ (φ \land x \in D \land k \in ℤ) \to x + k T \in D$
	fourierdlem48.per	$⊢ (φ \land x \in D \land k \in ℤ) \to F (x + k T) = F (x)$
	fourierdlem48.cn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
	fourierdlem48.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
	fourierdlem48.x	$⊢ φ \to X \in ℝ$
	fourierdlem48.z	$⊢ Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem48.e	$⊢ E = (x \in ℝ ⟼ x + Z (x))$
	fourierdlem48.ch	$⊢ χ \leftrightarrow ((((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1))) \land k \in ℤ) \land y = X + k T)$
Assertion	fourierdlem48	$⊢ φ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem48.a	$⊢ φ \to A \in ℝ$
2		fourierdlem48.b	$⊢ φ \to B \in ℝ$
3		fourierdlem48.altb	$⊢ φ \to A < B$
4		fourierdlem48.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))\})$
5		fourierdlem48.t	$⊢ T = B - A$
6		fourierdlem48.m	$⊢ φ \to M \in ℕ$
7		fourierdlem48.q	$⊢ φ \to Q \in P (M)$
8		fourierdlem48.f	$⊢ φ \to F : D ⟶ ℝ$
9		fourierdlem48.dper	$⊢ (φ \land x \in D \land k \in ℤ) \to x + k T \in D$
10		fourierdlem48.per	$⊢ (φ \land x \in D \land k \in ℤ) \to F (x + k T) = F (x)$
11		fourierdlem48.cn	$⊢ (φ \land i \in (0 ..^M)) \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
12		fourierdlem48.r	$⊢ (φ \land i \in (0 ..^M)) \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
13		fourierdlem48.x	$⊢ φ \to X \in ℝ$
14		fourierdlem48.z	$⊢ Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
15		fourierdlem48.e	$⊢ E = (x \in ℝ ⟼ x + Z (x))$
16		fourierdlem48.ch	$⊢ χ \leftrightarrow ((((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1))) \land k \in ℤ) \land y = X + k T)$
17		simpl	$⊢ (φ \land E (X) = B) \to φ$
18		0zd	$⊢ φ \to 0 \in ℤ$
19	6	nnzd	$⊢ φ \to M \in ℤ$
20	6	nngt0d	$⊢ φ \to 0 < M$
21		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
22	18 19 20 21	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
23	22	adantr	$⊢ (φ \land E (X) = B) \to 0 \in (0 ..^M)$
24	2 13	resubcld	$⊢ φ \to B - X \in ℝ$
25	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
26	5 25	eqeltrid	$⊢ φ \to T \in ℝ$
27	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
28	3 27	mpbid	$⊢ φ \to 0 < B - A$
29	28 5	breqtrrdi	$⊢ φ \to 0 < T$
30	29	gt0ne0d	$⊢ φ \to T \neq 0$
31	24 26 30	redivcld	$⊢ φ \to \frac{B - X}{T} \in ℝ$
32	31	adantr	$⊢ (φ \land E (X) = B) \to \frac{B - X}{T} \in ℝ$
33	32	flcld	$⊢ (φ \land E (X) = B) \to ⌊\frac{B - X}{T}⌋ \in ℤ$
34		1zzd	$⊢ (φ \land E (X) = B) \to 1 \in ℤ$
35	33 34	zsubcld	$⊢ (φ \land E (X) = B) \to ⌊\frac{B - X}{T}⌋ - 1 \in ℤ$
36		id	$⊢ E (X) = B \to E (X) = B$
37	5	a1i	$⊢ E (X) = B \to T = B - A$
38	36 37	oveq12d	$⊢ E (X) = B \to E (X) - T = B - (B - A)$
39	2	recnd	$⊢ φ \to B \in ℂ$
40	1	recnd	$⊢ φ \to A \in ℂ$
41	39 40	nncand	$⊢ φ \to B - (B - A) = A$
42	38 41	sylan9eqr	$⊢ (φ \land E (X) = B) \to E (X) - T = A$
43	4	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))))$
44	6 43	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))))$
45	7 44	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)))$
46	45	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
47		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
48	46 47	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
49	6	nnnn0d	$⊢ φ \to M \in ℕ_{0}$
50		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
51	49 50	eleqtrdi	$⊢ φ \to M \in ℤ_{\geq 0}$
52		eluzfz1	$⊢ M \in ℤ_{\geq 0} \to 0 \in (0 \dots M)$
53	51 52	syl	$⊢ φ \to 0 \in (0 \dots M)$
54	48 53	ffvelrnd	$⊢ φ \to Q (0) \in ℝ$
55	54	rexrd	$⊢ φ \to Q (0) \in ℝ^{*}$
56		1zzd	$⊢ φ \to 1 \in ℤ$
57	18 19 56	3jca	$⊢ φ \to (0 \in ℤ \land M \in ℤ \land 1 \in ℤ)$
58		0le1	$⊢ 0 \leq 1$
59	58	a1i	$⊢ φ \to 0 \leq 1$
60	6	nnge1d	$⊢ φ \to 1 \leq M$
61	57 59 60	jca32	$⊢ φ \to ((0 \in ℤ \land M \in ℤ \land 1 \in ℤ) \land (0 \leq 1 \land 1 \leq M))$
62		elfz2	$⊢ 1 \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land 1 \in ℤ) \land (0 \leq 1 \land 1 \leq M))$
63	61 62	sylibr	$⊢ φ \to 1 \in (0 \dots M)$
64	48 63	ffvelrnd	$⊢ φ \to Q (1) \in ℝ$
65	64	rexrd	$⊢ φ \to Q (1) \in ℝ^{*}$
66	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
67	45	simprd	$⊢ φ \to ((Q (0) = A \land Q (M) = B) \land \forall i \in (0 ..^M) Q (i) < Q (i + 1))$
68	67	simplld	$⊢ φ \to Q (0) = A$
69	1	leidd	$⊢ φ \to A \leq A$
70	68 69	eqbrtrd	$⊢ φ \to Q (0) \leq A$
71	68	eqcomd	$⊢ φ \to A = Q (0)$
72		0re	$⊢ 0 \in ℝ$
73		eleq1	$⊢ i = 0 \to (i \in (0 ..^M) \leftrightarrow 0 \in (0 ..^M))$
74	73	anbi2d	$⊢ i = 0 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land 0 \in (0 ..^M)))$
75		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
76		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
77	76	fveq2d	$⊢ i = 0 \to Q (i + 1) = Q (0 + 1)$
78	75 77	breq12d	$⊢ i = 0 \to (Q (i) < Q (i + 1) \leftrightarrow Q (0) < Q (0 + 1))$
79	74 78	imbi12d	$⊢ i = 0 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)))$
80	45	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
81	80	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
82	79 81	vtoclg	$⊢ 0 \in ℝ \to ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1))$
83	72 82	ax-mp	$⊢ (φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)$
84	22 83	mpdan	$⊢ φ \to Q (0) < Q (0 + 1)$
85		1e0p1	$⊢ 1 = 0 + 1$
86	85	fveq2i	$⊢ Q (1) = Q (0 + 1)$
87	84 86	breqtrrdi	$⊢ φ \to Q (0) < Q (1)$
88	71 87	eqbrtrd	$⊢ φ \to A < Q (1)$
89	55 65 66 70 88	elicod	$⊢ φ \to A \in [Q (0), Q (1))$
90	86	oveq2i	$⊢ [Q (0), Q (1)) = [Q (0), Q (0 + 1))$
91	89 90	eleqtrdi	$⊢ φ \to A \in [Q (0), Q (0 + 1))$
92	91	adantr	$⊢ (φ \land E (X) = B) \to A \in [Q (0), Q (0 + 1))$
93	42 92	eqeltrd	$⊢ (φ \land E (X) = B) \to E (X) - T \in [Q (0), Q (0 + 1))$
94	15	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + Z (x))$
95		id	$⊢ x = X \to x = X$
96		fveq2	$⊢ x = X \to Z (x) = Z (X)$
97	95 96	oveq12d	$⊢ x = X \to x + Z (x) = X + Z (X)$
98	97	adantl	$⊢ (φ \land x = X) \to x + Z (x) = X + Z (X)$
99	14	a1i	$⊢ φ \to Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
100		oveq2	$⊢ x = X \to B - x = B - X$
101	100	oveq1d	$⊢ x = X \to \frac{B - x}{T} = \frac{B - X}{T}$
102	101	fveq2d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - X}{T}⌋$
103	102	oveq1d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - X}{T}⌋ T$
104	103	adantl	$⊢ (φ \land x = X) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - X}{T}⌋ T$
105	31	flcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℤ$
106	105	zred	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℝ$
107	106 26	remulcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T \in ℝ$
108	99 104 13 107	fvmptd	$⊢ φ \to Z (X) = ⌊\frac{B - X}{T}⌋ T$
109	108 107	eqeltrd	$⊢ φ \to Z (X) \in ℝ$
110	13 109	readdcld	$⊢ φ \to X + Z (X) \in ℝ$
111	94 98 13 110	fvmptd	$⊢ φ \to E (X) = X + Z (X)$
112	108	oveq2d	$⊢ φ \to X + Z (X) = X + ⌊\frac{B - X}{T}⌋ T$
113	111 112	eqtrd	$⊢ φ \to E (X) = X + ⌊\frac{B - X}{T}⌋ T$
114	113	oveq1d	$⊢ φ \to E (X) - T = X + ⌊\frac{B - X}{T}⌋ T - T$
115	13	recnd	$⊢ φ \to X \in ℂ$
116	107	recnd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T \in ℂ$
117	26	recnd	$⊢ φ \to T \in ℂ$
118	115 116 117	addsubassd	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T - T = X + ⌊\frac{B - X}{T}⌋ T - T$
119	105	zcnd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℂ$
120	119 117	mulsubfacd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T - T = (⌊\frac{B - X}{T}⌋ - 1) T$
121	120	oveq2d	$⊢ φ \to X + ⌊\frac{B - X}{T}⌋ T - T = X + (⌊\frac{B - X}{T}⌋ - 1) T$
122	114 118 121	3eqtrd	$⊢ φ \to E (X) - T = X + (⌊\frac{B - X}{T}⌋ - 1) T$
123	122	adantr	$⊢ (φ \land E (X) = B) \to E (X) - T = X + (⌊\frac{B - X}{T}⌋ - 1) T$
124		oveq1	$⊢ k = ⌊\frac{B - X}{T}⌋ - 1 \to k T = (⌊\frac{B - X}{T}⌋ - 1) T$
125	124	oveq2d	$⊢ k = ⌊\frac{B - X}{T}⌋ - 1 \to X + k T = X + (⌊\frac{B - X}{T}⌋ - 1) T$
126	125	eqeq2d	$⊢ k = ⌊\frac{B - X}{T}⌋ - 1 \to (E (X) - T = X + k T \leftrightarrow E (X) - T = X + (⌊\frac{B - X}{T}⌋ - 1) T)$
127	126	anbi2d	$⊢ k = ⌊\frac{B - X}{T}⌋ - 1 \to ((E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T) \leftrightarrow (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + (⌊\frac{B - X}{T}⌋ - 1) T))$
128	127	rspcev	$⊢ (⌊\frac{B - X}{T}⌋ - 1 \in ℤ \land (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + (⌊\frac{B - X}{T}⌋ - 1) T)) \to \exists k \in ℤ (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T)$
129	35 93 123 128	syl12anc	$⊢ (φ \land E (X) = B) \to \exists k \in ℤ (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T)$
130	75 77	oveq12d	$⊢ i = 0 \to [Q (i), Q (i + 1)) = [Q (0), Q (0 + 1))$
131	130	eleq2d	$⊢ i = 0 \to (E (X) - T \in [Q (i), Q (i + 1)) \leftrightarrow E (X) - T \in [Q (0), Q (0 + 1)))$
132	131	anbi1d	$⊢ i = 0 \to ((E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T) \leftrightarrow (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T))$
133	132	rexbidv	$⊢ i = 0 \to (\exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T) \leftrightarrow \exists k \in ℤ (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T))$
134	133	rspcev	$⊢ (0 \in (0 ..^M) \land \exists k \in ℤ (E (X) - T \in [Q (0), Q (0 + 1)) \land E (X) - T = X + k T)) \to \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T)$
135	23 129 134	syl2anc	$⊢ (φ \land E (X) = B) \to \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T)$
136		ovex	$⊢ E (X) - T \in V$
137		eleq1	$⊢ y = E (X) - T \to (y \in [Q (i), Q (i + 1)) \leftrightarrow E (X) - T \in [Q (i), Q (i + 1)))$
138		eqeq1	$⊢ y = E (X) - T \to (y = X + k T \leftrightarrow E (X) - T = X + k T)$
139	137 138	anbi12d	$⊢ y = E (X) - T \to ((y \in [Q (i), Q (i + 1)) \land y = X + k T) \leftrightarrow (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T))$
140	139	2rexbidv	$⊢ y = E (X) - T \to (\exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T) \leftrightarrow \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T))$
141	140	anbi2d	$⊢ y = E (X) - T \to ((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \leftrightarrow (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T)))$
142	141	imbi1d	$⊢ y = E (X) - T \to (((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset) \leftrightarrow ((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset))$
143		simpr	$⊢ (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)$
144		nfv	$⊢ Ⅎ i φ$
145		nfre1	$⊢ Ⅎ i \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)$
146	144 145	nfan	$⊢ Ⅎ i (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T))$
147		nfv	$⊢ Ⅎ k φ$
148		nfcv	$⊢ \underline{Ⅎ} k (0 ..^M)$
149		nfre1	$⊢ Ⅎ k \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)$
150	148 149	nfrex	$⊢ Ⅎ k \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)$
151	147 150	nfan	$⊢ Ⅎ k (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T))$
152		simp1	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to φ$
153		simp2l	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to i \in (0 ..^M)$
154		simp3l	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to y \in [Q (i), Q (i + 1))$
155	152 153 154	jca31	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1)))$
156		simp2r	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to k \in ℤ$
157		simp3r	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to y = X + k T$
158	16	biimpi	$⊢ χ \to ((((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1))) \land k \in ℤ) \land y = X + k T)$
159	158	simplld	$⊢ χ \to ((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1)))$
160	159	simplld	$⊢ χ \to φ$
161		frel	$⊢ F : D ⟶ ℝ \to Rel F$
162	160 8 161	3syl	$⊢ χ \to Rel F$
163		resindm	$⊢ Rel F \to {F ↾}_{((X, +∞) \cap dom F)} = {F ↾}_{(X, +∞)}$
164	163	eqcomd	$⊢ Rel F \to {F ↾}_{(X, +∞)} = {F ↾}_{((X, +∞) \cap dom F)}$
165	162 164	syl	$⊢ χ \to {F ↾}_{(X, +∞)} = {F ↾}_{((X, +∞) \cap dom F)}$
166		fdm	$⊢ F : D ⟶ ℝ \to dom F = D$
167	160 8 166	3syl	$⊢ χ \to dom F = D$
168	167	ineq2d	$⊢ χ \to (X, +∞) \cap dom F = (X, +∞) \cap D$
169	168	reseq2d	$⊢ χ \to {F ↾}_{((X, +∞) \cap dom F)} = {F ↾}_{((X, +∞) \cap D)}$
170	165 169	eqtrd	$⊢ χ \to {F ↾}_{(X, +∞)} = {F ↾}_{((X, +∞) \cap D)}$
171	170	oveq1d	$⊢ χ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X = ({F ↾}_{((X, +∞) \cap D)}) {lim}_{ℂ} X$
172	160 8	syl	$⊢ χ \to F : D ⟶ ℝ$
173		ax-resscn	$⊢ ℝ \subseteq ℂ$
174	173	a1i	$⊢ χ \to ℝ \subseteq ℂ$
175	172 174	fssd	$⊢ χ \to F : D ⟶ ℂ$
176		inss2	$⊢ (X, +∞) \cap D \subseteq D$
177	176	a1i	$⊢ χ \to (X, +∞) \cap D \subseteq D$
178	175 177	fssresd	$⊢ χ \to ({F ↾}_{((X, +∞) \cap D)}) : (X, +∞) \cap D ⟶ ℂ$
179		pnfxr	$⊢ +∞ \in ℝ^{*}$
180	179	a1i	$⊢ χ \to +∞ \in ℝ^{*}$
181	159	simplrd	$⊢ χ \to i \in (0 ..^M)$
182	48	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
183		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
184	183	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
185	182 184	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
186	160 181 185	syl2anc	$⊢ χ \to Q (i + 1) \in ℝ$
187	158	simplrd	$⊢ χ \to k \in ℤ$
188	187	zred	$⊢ χ \to k \in ℝ$
189	160 26	syl	$⊢ χ \to T \in ℝ$
190	188 189	remulcld	$⊢ χ \to k T \in ℝ$
191	186 190	resubcld	$⊢ χ \to Q (i + 1) - k T \in ℝ$
192	191	rexrd	$⊢ χ \to Q (i + 1) - k T \in ℝ^{*}$
193	191	ltpnfd	$⊢ χ \to Q (i + 1) - k T < +∞$
194	192 180 193	xrltled	$⊢ χ \to Q (i + 1) - k T \leq +∞$
195		iooss2	$⊢ (+∞ \in ℝ^{*} \land Q (i + 1) - k T \leq +∞) \to (X, Q (i + 1) - k T) \subseteq (X, +∞)$
196	180 194 195	syl2anc	$⊢ χ \to (X, Q (i + 1) - k T) \subseteq (X, +∞)$
197	187	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k \in ℤ$
198	197	zcnd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k \in ℂ$
199	189	recnd	$⊢ χ \to T \in ℂ$
200	199	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to T \in ℂ$
201	198 200	mulneg1d	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to (- k) T = - k T$
202	201	oveq2d	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k) T = w + k T + (- k T)$
203		elioore	$⊢ w \in (X, Q (i + 1) - k T) \to w \in ℝ$
204	203	recnd	$⊢ w \in (X, Q (i + 1) - k T) \to w \in ℂ$
205	204	adantl	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in ℂ$
206	198 200	mulcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k T \in ℂ$
207	205 206	addcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in ℂ$
208	207 206	negsubd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k T) = w + k T - k T$
209	205 206	pncand	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T - k T = w$
210	202 208 209	3eqtrrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w = w + k T + (- k) T$
211	160	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to φ$
212	159	simpld	$⊢ χ \to (φ \land i \in (0 ..^M))$
213		cncff	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ$
214		fdm	$⊢ ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) ⟶ ℂ \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
215	11 213 214	3syl	$⊢ (φ \land i \in (0 ..^M)) \to dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
216		ssdmres	$⊢ (Q (i), Q (i + 1)) \subseteq dom F \leftrightarrow dom ({F ↾}_{(Q (i), Q (i + 1))}) = (Q (i), Q (i + 1))$
217	215 216	sylibr	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq dom F$
218	8 166	syl	$⊢ φ \to dom F = D$
219	218	adantr	$⊢ (φ \land i \in (0 ..^M)) \to dom F = D$
220	217 219	sseqtrd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq D$
221	212 220	syl	$⊢ χ \to (Q (i), Q (i + 1)) \subseteq D$
222	221	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to (Q (i), Q (i + 1)) \subseteq D$
223		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
224	223	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
225	182 224	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
226	160 181 225	syl2anc	$⊢ χ \to Q (i) \in ℝ$
227	226	rexrd	$⊢ χ \to Q (i) \in ℝ^{*}$
228	227	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i) \in ℝ^{*}$
229	186	rexrd	$⊢ χ \to Q (i + 1) \in ℝ^{*}$
230	229	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i + 1) \in ℝ^{*}$
231	203	adantl	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in ℝ$
232	197	zred	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k \in ℝ$
233	211 26	syl	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to T \in ℝ$
234	232 233	remulcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k T \in ℝ$
235	231 234	readdcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in ℝ$
236	226	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i) \in ℝ$
237	160 13	syl	$⊢ χ \to X \in ℝ$
238	237 190	readdcld	$⊢ χ \to X + k T \in ℝ$
239	238	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to X + k T \in ℝ$
240	16	simprbi	$⊢ χ \to y = X + k T$
241	240	eqcomd	$⊢ χ \to X + k T = y$
242	159	simprd	$⊢ χ \to y \in [Q (i), Q (i + 1))$
243	241 242	eqeltrd	$⊢ χ \to X + k T \in [Q (i), Q (i + 1))$
244		icogelb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land X + k T \in [Q (i), Q (i + 1))) \to Q (i) \leq X + k T$
245	227 229 243 244	syl3anc	$⊢ χ \to Q (i) \leq X + k T$
246	245	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i) \leq X + k T$
247	211 13	syl	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to X \in ℝ$
248	247	rexrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to X \in ℝ^{*}$
249	186	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i + 1) \in ℝ$
250	249 234	resubcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i + 1) - k T \in ℝ$
251	250	rexrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i + 1) - k T \in ℝ^{*}$
252		simpr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in (X, Q (i + 1) - k T)$
253		ioogtlb	$⊢ (X \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land w \in (X, Q (i + 1) - k T)) \to X < w$
254	248 251 252 253	syl3anc	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to X < w$
255	247 231 234 254	ltadd1dd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to X + k T < w + k T$
256	236 239 235 246 255	lelttrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i) < w + k T$
257		iooltub	$⊢ (X \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land w \in (X, Q (i + 1) - k T)) \to w < Q (i + 1) - k T$
258	248 251 252 257	syl3anc	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w < Q (i + 1) - k T$
259	231 250 234 258	ltadd1dd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T < Q (i + 1) - k T + k T$
260	186	recnd	$⊢ χ \to Q (i + 1) \in ℂ$
261	190	recnd	$⊢ χ \to k T \in ℂ$
262	260 261	npcand	$⊢ χ \to Q (i + 1) - k T + k T = Q (i + 1)$
263	262	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to Q (i + 1) - k T + k T = Q (i + 1)$
264	259 263	breqtrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T < Q (i + 1)$
265	228 230 235 256 264	eliood	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in (Q (i), Q (i + 1))$
266	222 265	sseldd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in D$
267	197	znegcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to - k \in ℤ$
268		ovex	$⊢ w + k T \in V$
269		eleq1	$⊢ x = w + k T \to (x \in D \leftrightarrow w + k T \in D)$
270	269	3anbi2d	$⊢ x = w + k T \to ((φ \land x \in D \land - k \in ℤ) \leftrightarrow (φ \land w + k T \in D \land - k \in ℤ))$
271		oveq1	$⊢ x = w + k T \to x + (- k) T = w + k T + (- k) T$
272	271	eleq1d	$⊢ x = w + k T \to (x + (- k) T \in D \leftrightarrow w + k T + (- k) T \in D)$
273	270 272	imbi12d	$⊢ x = w + k T \to (((φ \land x \in D \land - k \in ℤ) \to x + (- k) T \in D) \leftrightarrow ((φ \land w + k T \in D \land - k \in ℤ) \to w + k T + (- k) T \in D))$
274		negex	$⊢ - k \in V$
275		eleq1	$⊢ j = - k \to (j \in ℤ \leftrightarrow - k \in ℤ)$
276	275	3anbi3d	$⊢ j = - k \to ((φ \land x \in D \land j \in ℤ) \leftrightarrow (φ \land x \in D \land - k \in ℤ))$
277		oveq1	$⊢ j = - k \to j T = (- k) T$
278	277	oveq2d	$⊢ j = - k \to x + j T = x + (- k) T$
279	278	eleq1d	$⊢ j = - k \to (x + j T \in D \leftrightarrow x + (- k) T \in D)$
280	276 279	imbi12d	$⊢ j = - k \to (((φ \land x \in D \land j \in ℤ) \to x + j T \in D) \leftrightarrow ((φ \land x \in D \land - k \in ℤ) \to x + (- k) T \in D))$
281		eleq1	$⊢ k = j \to (k \in ℤ \leftrightarrow j \in ℤ)$
282	281	3anbi3d	$⊢ k = j \to ((φ \land x \in D \land k \in ℤ) \leftrightarrow (φ \land x \in D \land j \in ℤ))$
283		oveq1	$⊢ k = j \to k T = j T$
284	283	oveq2d	$⊢ k = j \to x + k T = x + j T$
285	284	eleq1d	$⊢ k = j \to (x + k T \in D \leftrightarrow x + j T \in D)$
286	282 285	imbi12d	$⊢ k = j \to (((φ \land x \in D \land k \in ℤ) \to x + k T \in D) \leftrightarrow ((φ \land x \in D \land j \in ℤ) \to x + j T \in D))$
287	286 9	chvarvv	$⊢ (φ \land x \in D \land j \in ℤ) \to x + j T \in D$
288	274 280 287	vtocl	$⊢ (φ \land x \in D \land - k \in ℤ) \to x + (- k) T \in D$
289	268 273 288	vtocl	$⊢ (φ \land w + k T \in D \land - k \in ℤ) \to w + k T + (- k) T \in D$
290	211 266 267 289	syl3anc	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k) T \in D$
291	210 290	eqeltrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in D$
292	291	ralrimiva	$⊢ χ \to \forall w \in (X, Q (i + 1) - k T) w \in D$
293		dfss3	$⊢ (X, Q (i + 1) - k T) \subseteq D \leftrightarrow \forall w \in (X, Q (i + 1) - k T) w \in D$
294	292 293	sylibr	$⊢ χ \to (X, Q (i + 1) - k T) \subseteq D$
295	196 294	ssind	$⊢ χ \to (X, Q (i + 1) - k T) \subseteq (X, +∞) \cap D$
296		ioosscn	$⊢ (X, +∞) \subseteq ℂ$
297		ssinss1	$⊢ (X, +∞) \subseteq ℂ \to (X, +∞) \cap D \subseteq ℂ$
298	296 297	mp1i	$⊢ χ \to (X, +∞) \cap D \subseteq ℂ$
299		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
300		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) = TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})$
301	237	rexrd	$⊢ χ \to X \in ℝ^{*}$
302	237	leidd	$⊢ χ \to X \leq X$
303	240	oveq1d	$⊢ χ \to y - k T = X + k T - k T$
304	237	recnd	$⊢ χ \to X \in ℂ$
305	304 261	pncand	$⊢ χ \to X + k T - k T = X$
306	303 305	eqtr2d	$⊢ χ \to X = y - k T$
307		icossre	$⊢ (Q (i) \in ℝ \land Q (i + 1) \in ℝ^{*}) \to [Q (i), Q (i + 1)) \subseteq ℝ$
308	226 229 307	syl2anc	$⊢ χ \to [Q (i), Q (i + 1)) \subseteq ℝ$
309	308 242	sseldd	$⊢ χ \to y \in ℝ$
310		icoltub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land y \in [Q (i), Q (i + 1))) \to y < Q (i + 1)$
311	227 229 242 310	syl3anc	$⊢ χ \to y < Q (i + 1)$
312	309 186 190 311	ltsub1dd	$⊢ χ \to y - k T < Q (i + 1) - k T$
313	306 312	eqbrtrd	$⊢ χ \to X < Q (i + 1) - k T$
314	301 192 301 302 313	elicod	$⊢ χ \to X \in [X, Q (i + 1) - k T)$
315		snunioo1	$⊢ (X \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land X < Q (i + 1) - k T) \to (X, Q (i + 1) - k T) \cup \{X\} = [X, Q (i + 1) - k T)$
316	301 192 313 315	syl3anc	$⊢ χ \to (X, Q (i + 1) - k T) \cup \{X\} = [X, Q (i + 1) - k T)$
317	316	fveq2d	$⊢ χ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ((X, Q (i + 1) - k T) \cup \{X\}) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ([X, Q (i + 1) - k T))$
318	299	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
319		ovex	$⊢ (X, +∞) \in V$
320	319	inex1	$⊢ (X, +∞) \cap D \in V$
321		snex	$⊢ \{X\} \in V$
322	320 321	unex	$⊢ ((X, +∞) \cap D) \cup \{X\} \in V$
323		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land ((X, +∞) \cap D) \cup \{X\} \in V) \to TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) \in Top$
324	318 322 323	mp2an	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) \in Top$
325	324	a1i	$⊢ χ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) \in Top$
326		retop	$⊢ topGen (ran (.)) \in Top$
327	326	a1i	$⊢ χ \to topGen (ran (.)) \in Top$
328	322	a1i	$⊢ χ \to ((X, +∞) \cap D) \cup \{X\} \in V$
329		iooretop	$⊢ (−∞, Q (i + 1) - k T) \in topGen (ran (.))$
330	329	a1i	$⊢ χ \to (−∞, Q (i + 1) - k T) \in topGen (ran (.))$
331		elrestr	$⊢ (topGen (ran (.)) \in Top \land ((X, +∞) \cap D) \cup \{X\} \in V \land (−∞, Q (i + 1) - k T) \in topGen (ran (.))) \to (−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}) \in (topGen (ran (.)) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}))$
332	327 328 330 331	syl3anc	$⊢ χ \to (−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}) \in (topGen (ran (.)) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}))$
333		mnfxr	$⊢ −∞ \in ℝ^{*}$
334	333	a1i	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to −∞ \in ℝ^{*}$
335	192	adantr	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to Q (i + 1) - k T \in ℝ^{*}$
336		icossre	$⊢ (X \in ℝ \land Q (i + 1) - k T \in ℝ^{*}) \to [X, Q (i + 1) - k T) \subseteq ℝ$
337	237 192 336	syl2anc	$⊢ χ \to [X, Q (i + 1) - k T) \subseteq ℝ$
338	337	sselda	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x \in ℝ$
339	338	mnfltd	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to −∞ < x$
340	301	adantr	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to X \in ℝ^{*}$
341		simpr	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x \in [X, Q (i + 1) - k T)$
342		icoltub	$⊢ (X \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land x \in [X, Q (i + 1) - k T)) \to x < Q (i + 1) - k T$
343	340 335 341 342	syl3anc	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x < Q (i + 1) - k T$
344	334 335 338 339 343	eliood	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x \in (−∞, Q (i + 1) - k T)$
345		vsnid	$⊢ x \in \{x\}$
346	345	a1i	$⊢ x = X \to x \in \{x\}$
347		sneq	$⊢ x = X \to \{x\} = \{X\}$
348	346 347	eleqtrd	$⊢ x = X \to x \in \{X\}$
349		elun2	$⊢ x \in \{X\} \to x \in (((X, +∞) \cap D) \cup \{X\})$
350	348 349	syl	$⊢ x = X \to x \in (((X, +∞) \cap D) \cup \{X\})$
351	350	adantl	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land x = X) \to x \in (((X, +∞) \cap D) \cup \{X\})$
352	301	ad2antrr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to X \in ℝ^{*}$
353	179	a1i	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to +∞ \in ℝ^{*}$
354	338	adantr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in ℝ$
355	237	ad2antrr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to X \in ℝ$
356		icogelb	$⊢ (X \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land x \in [X, Q (i + 1) - k T)) \to X \leq x$
357	340 335 341 356	syl3anc	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to X \leq x$
358	357	adantr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to X \leq x$
359		neqne	$⊢ \neg x = X \to x \neq X$
360	359	adantl	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \neq X$
361	355 354 358 360	leneltd	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to X < x$
362	354	ltpnfd	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x < +∞$
363	352 353 354 361 362	eliood	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in (X, +∞)$
364	187	zcnd	$⊢ χ \to k \in ℂ$
365	364 199	mulneg1d	$⊢ χ \to (- k) T = - k T$
366	365	oveq2d	$⊢ χ \to w + k T + (- k) T = w + k T + (- k T)$
367	366	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k) T = w + k T + (- k T)$
368		ioosscn	$⊢ (X, Q (i + 1) - k T) \subseteq ℂ$
369	368	sseli	$⊢ w \in (X, Q (i + 1) - k T) \to w \in ℂ$
370	369	adantl	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in ℂ$
371	261	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k T \in ℂ$
372	370 371	addcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in ℂ$
373	372 371	negsubd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k T) = w + k T - k T$
374	370 371	pncand	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T - k T = w$
375	367 373 374	3eqtrrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w = w + k T + (- k) T$
376	190	adantr	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to k T \in ℝ$
377	231 376	readdcld	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in ℝ$
378	228 230 377 256 264	eliood	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in (Q (i), Q (i + 1))$
379	222 378	sseldd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in D$
380	275	3anbi3d	$⊢ j = - k \to ((φ \land w + k T \in D \land j \in ℤ) \leftrightarrow (φ \land w + k T \in D \land - k \in ℤ))$
381	277	oveq2d	$⊢ j = - k \to w + k T + j T = w + k T + (- k) T$
382	381	eleq1d	$⊢ j = - k \to (w + k T + j T \in D \leftrightarrow w + k T + (- k) T \in D)$
383	380 382	imbi12d	$⊢ j = - k \to (((φ \land w + k T \in D \land j \in ℤ) \to w + k T + j T \in D) \leftrightarrow ((φ \land w + k T \in D \land - k \in ℤ) \to w + k T + (- k) T \in D))$
384	269	3anbi2d	$⊢ x = w + k T \to ((φ \land x \in D \land j \in ℤ) \leftrightarrow (φ \land w + k T \in D \land j \in ℤ))$
385		oveq1	$⊢ x = w + k T \to x + j T = w + k T + j T$
386	385	eleq1d	$⊢ x = w + k T \to (x + j T \in D \leftrightarrow w + k T + j T \in D)$
387	384 386	imbi12d	$⊢ x = w + k T \to (((φ \land x \in D \land j \in ℤ) \to x + j T \in D) \leftrightarrow ((φ \land w + k T \in D \land j \in ℤ) \to w + k T + j T \in D))$
388	268 387 287	vtocl	$⊢ (φ \land w + k T \in D \land j \in ℤ) \to w + k T + j T \in D$
389	274 383 388	vtocl	$⊢ (φ \land w + k T \in D \land - k \in ℤ) \to w + k T + (- k) T \in D$
390	211 379 267 389	syl3anc	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w + k T + (- k) T \in D$
391	375 390	eqeltrd	$⊢ (χ \land w \in (X, Q (i + 1) - k T)) \to w \in D$
392	391	ralrimiva	$⊢ χ \to \forall w \in (X, Q (i + 1) - k T) w \in D$
393	392 293	sylibr	$⊢ χ \to (X, Q (i + 1) - k T) \subseteq D$
394	393	ad2antrr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to (X, Q (i + 1) - k T) \subseteq D$
395	192	ad2antrr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to Q (i + 1) - k T \in ℝ^{*}$
396	343	adantr	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x < Q (i + 1) - k T$
397	352 395 354 361 396	eliood	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in (X, Q (i + 1) - k T)$
398	394 397	sseldd	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in D$
399	363 398	elind	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in ((X, +∞) \cap D)$
400		elun1	$⊢ x \in ((X, +∞) \cap D) \to x \in (((X, +∞) \cap D) \cup \{X\})$
401	399 400	syl	$⊢ ((χ \land x \in [X, Q (i + 1) - k T)) \land \neg x = X) \to x \in (((X, +∞) \cap D) \cup \{X\})$
402	351 401	pm2.61dan	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x \in (((X, +∞) \cap D) \cup \{X\})$
403	344 402	elind	$⊢ (χ \land x \in [X, Q (i + 1) - k T)) \to x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))$
404	301	adantr	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to X \in ℝ^{*}$
405	192	adantr	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to Q (i + 1) - k T \in ℝ^{*}$
406		elinel1	$⊢ x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})) \to x \in (−∞, Q (i + 1) - k T)$
407		elioore	$⊢ x \in (−∞, Q (i + 1) - k T) \to x \in ℝ$
408	406 407	syl	$⊢ x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})) \to x \in ℝ$
409	408	rexrd	$⊢ x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})) \to x \in ℝ^{*}$
410	409	adantl	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to x \in ℝ^{*}$
411		elinel2	$⊢ x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})) \to x \in (((X, +∞) \cap D) \cup \{X\})$
412	237	adantr	$⊢ (χ \land x = X) \to X \in ℝ$
413	95	eqcomd	$⊢ x = X \to X = x$
414	413	adantl	$⊢ (χ \land x = X) \to X = x$
415	412 414	eqled	$⊢ (χ \land x = X) \to X \leq x$
416	415	adantlr	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land x = X) \to X \leq x$
417		simpll	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to χ$
418		simplr	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to x \in (((X, +∞) \cap D) \cup \{X\})$
419		id	$⊢ \neg x = X \to \neg x = X$
420		velsn	$⊢ x \in \{X\} \leftrightarrow x = X$
421	419 420	sylnibr	$⊢ \neg x = X \to \neg x \in \{X\}$
422	421	adantl	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to \neg x \in \{X\}$
423		elunnel2	$⊢ (x \in (((X, +∞) \cap D) \cup \{X\}) \land \neg x \in \{X\}) \to x \in ((X, +∞) \cap D)$
424	418 422 423	syl2anc	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to x \in ((X, +∞) \cap D)$
425		elinel1	$⊢ x \in ((X, +∞) \cap D) \to x \in (X, +∞)$
426	424 425	syl	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to x \in (X, +∞)$
427	237	adantr	$⊢ (χ \land x \in (X, +∞)) \to X \in ℝ$
428		elioore	$⊢ x \in (X, +∞) \to x \in ℝ$
429	428	adantl	$⊢ (χ \land x \in (X, +∞)) \to x \in ℝ$
430	301	adantr	$⊢ (χ \land x \in (X, +∞)) \to X \in ℝ^{*}$
431	179	a1i	$⊢ (χ \land x \in (X, +∞)) \to +∞ \in ℝ^{*}$
432		simpr	$⊢ (χ \land x \in (X, +∞)) \to x \in (X, +∞)$
433		ioogtlb	$⊢ (X \in ℝ^{} \land +∞ \in ℝ^{} \land x \in (X, +∞)) \to X < x$
434	430 431 432 433	syl3anc	$⊢ (χ \land x \in (X, +∞)) \to X < x$
435	427 429 434	ltled	$⊢ (χ \land x \in (X, +∞)) \to X \leq x$
436	417 426 435	syl2anc	$⊢ ((χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \land \neg x = X) \to X \leq x$
437	416 436	pm2.61dan	$⊢ (χ \land x \in (((X, +∞) \cap D) \cup \{X\})) \to X \leq x$
438	411 437	sylan2	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to X \leq x$
439	333	a1i	$⊢ (χ \land x \in (−∞, Q (i + 1) - k T)) \to −∞ \in ℝ^{*}$
440	192	adantr	$⊢ (χ \land x \in (−∞, Q (i + 1) - k T)) \to Q (i + 1) - k T \in ℝ^{*}$
441		simpr	$⊢ (χ \land x \in (−∞, Q (i + 1) - k T)) \to x \in (−∞, Q (i + 1) - k T)$
442		iooltub	$⊢ (−∞ \in ℝ^{} \land Q (i + 1) - k T \in ℝ^{} \land x \in (−∞, Q (i + 1) - k T)) \to x < Q (i + 1) - k T$
443	439 440 441 442	syl3anc	$⊢ (χ \land x \in (−∞, Q (i + 1) - k T)) \to x < Q (i + 1) - k T$
444	406 443	sylan2	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to x < Q (i + 1) - k T$
445	404 405 410 438 444	elicod	$⊢ (χ \land x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\}))) \to x \in [X, Q (i + 1) - k T)$
446	403 445	impbida	$⊢ χ \to (x \in [X, Q (i + 1) - k T) \leftrightarrow x \in ((−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})))$
447	446	eqrdv	$⊢ χ \to [X, Q (i + 1) - k T) = (−∞, Q (i + 1) - k T) \cap (((X, +∞) \cap D) \cup \{X\})$
448		ioossre	$⊢ (X, +∞) \subseteq ℝ$
449		ssinss1	$⊢ (X, +∞) \subseteq ℝ \to (X, +∞) \cap D \subseteq ℝ$
450	448 449	mp1i	$⊢ χ \to (X, +∞) \cap D \subseteq ℝ$
451	237	snssd	$⊢ χ \to \{X\} \subseteq ℝ$
452	450 451	unssd	$⊢ χ \to ((X, +∞) \cap D) \cup \{X\} \subseteq ℝ$
453		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
454	299 453	rerest	$⊢ ((X, +∞) \cap D) \cup \{X\} \subseteq ℝ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) = topGen (ran (.)) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})$
455	452 454	syl	$⊢ χ \to TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) = topGen (ran (.)) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})$
456	332 447 455	3eltr4d	$⊢ χ \to [X, Q (i + 1) - k T) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}))$
457		isopn3i	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}) \in Top \land [X, Q (i + 1) - k T) \in (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\}))) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ([X, Q (i + 1) - k T)) = [X, Q (i + 1) - k T)$
458	325 456 457	syl2anc	$⊢ χ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ([X, Q (i + 1) - k T)) = [X, Q (i + 1) - k T)$
459	317 458	eqtr2d	$⊢ χ \to [X, Q (i + 1) - k T) = int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ((X, Q (i + 1) - k T) \cup \{X\})$
460	314 459	eleqtrd	$⊢ χ \to X \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} (((X, +∞) \cap D) \cup \{X\})) ((X, Q (i + 1) - k T) \cup \{X\})$
461	178 295 298 299 300 460	limcres	$⊢ χ \to ({({F ↾}_{((X, +∞) \cap D)}) ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X = ({F ↾}_{((X, +∞) \cap D)}) {lim}_{ℂ} X$
462	295	resabs1d	$⊢ χ \to {({F ↾}_{((X, +∞) \cap D)}) ↾}_{(X, Q (i + 1) - k T)} = {F ↾}_{(X, Q (i + 1) - k T)}$
463	462	oveq1d	$⊢ χ \to ({({F ↾}_{((X, +∞) \cap D)}) ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X = ({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X$
464	173	a1i	$⊢ φ \to ℝ \subseteq ℂ$
465	8 464	fssd	$⊢ φ \to F : D ⟶ ℂ$
466	218	feq2d	$⊢ φ \to (F : dom F ⟶ ℂ \leftrightarrow F : D ⟶ ℂ)$
467	465 466	mpbird	$⊢ φ \to F : dom F ⟶ ℂ$
468	160 467	syl	$⊢ χ \to F : dom F ⟶ ℂ$
469	468	adantr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to F : dom F ⟶ ℂ$
470	368	a1i	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to (X, Q (i + 1) - k T) \subseteq ℂ$
471	393 167	sseqtrrd	$⊢ χ \to (X, Q (i + 1) - k T) \subseteq dom F$
472	471	adantr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to (X, Q (i + 1) - k T) \subseteq dom F$
473	261	adantr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to k T \in ℂ$
474		eqid	$⊢ \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} = \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}$
475		eqeq1	$⊢ z = w \to (z = x + k T \leftrightarrow w = x + k T)$
476	475	rexbidv	$⊢ z = w \to (\exists x \in (X, Q (i + 1) - k T) z = x + k T \leftrightarrow \exists x \in (X, Q (i + 1) - k T) w = x + k T)$
477	476	elrab	$⊢ w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \leftrightarrow (w \in ℂ \land \exists x \in (X, Q (i + 1) - k T) w = x + k T)$
478	477	simprbi	$⊢ w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \to \exists x \in (X, Q (i + 1) - k T) w = x + k T$
479	478	adantl	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}) \to \exists x \in (X, Q (i + 1) - k T) w = x + k T$
480		nfv	$⊢ Ⅎ x χ$
481		nfre1	$⊢ Ⅎ x \exists x \in (X, Q (i + 1) - k T) z = x + k T$
482		nfcv	$⊢ \underline{Ⅎ} x ℂ$
483	481 482	nfrabw	$⊢ \underline{Ⅎ} x \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}$
484	483	nfcri	$⊢ Ⅎ x w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}$
485	480 484	nfan	$⊢ Ⅎ x (χ \land w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\})$
486		nfv	$⊢ Ⅎ x w \in D$
487		simp3	$⊢ (χ \land x \in (X, Q (i + 1) - k T) \land w = x + k T) \to w = x + k T$
488		eleq1	$⊢ w = x \to (w \in (X, Q (i + 1) - k T) \leftrightarrow x \in (X, Q (i + 1) - k T))$
489	488	anbi2d	$⊢ w = x \to ((χ \land w \in (X, Q (i + 1) - k T)) \leftrightarrow (χ \land x \in (X, Q (i + 1) - k T)))$
490		oveq1	$⊢ w = x \to w + k T = x + k T$
491	490	eleq1d	$⊢ w = x \to (w + k T \in D \leftrightarrow x + k T \in D)$
492	489 491	imbi12d	$⊢ w = x \to (((χ \land w \in (X, Q (i + 1) - k T)) \to w + k T \in D) \leftrightarrow ((χ \land x \in (X, Q (i + 1) - k T)) \to x + k T \in D))$
493	492 266	chvarvv	$⊢ (χ \land x \in (X, Q (i + 1) - k T)) \to x + k T \in D$
494	493	3adant3	$⊢ (χ \land x \in (X, Q (i + 1) - k T) \land w = x + k T) \to x + k T \in D$
495	487 494	eqeltrd	$⊢ (χ \land x \in (X, Q (i + 1) - k T) \land w = x + k T) \to w \in D$
496	495	3exp	$⊢ χ \to (x \in (X, Q (i + 1) - k T) \to (w = x + k T \to w \in D))$
497	496	adantr	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}) \to (x \in (X, Q (i + 1) - k T) \to (w = x + k T \to w \in D))$
498	485 486 497	rexlimd	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}) \to (\exists x \in (X, Q (i + 1) - k T) w = x + k T \to w \in D)$
499	479 498	mpd	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}) \to w \in D$
500	499	ralrimiva	$⊢ χ \to \forall w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} w \in D$
501		dfss3	$⊢ \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \subseteq D \leftrightarrow \forall w \in \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} w \in D$
502	500 501	sylibr	$⊢ χ \to \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \subseteq D$
503	502 167	sseqtrrd	$⊢ χ \to \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \subseteq dom F$
504	503	adantr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} \subseteq dom F$
505	160	adantr	$⊢ (χ \land x \in (X, Q (i + 1) - k T)) \to φ$
506	393	sselda	$⊢ (χ \land x \in (X, Q (i + 1) - k T)) \to x \in D$
507	187	adantr	$⊢ (χ \land x \in (X, Q (i + 1) - k T)) \to k \in ℤ$
508	505 506 507 10	syl3anc	$⊢ (χ \land x \in (X, Q (i + 1) - k T)) \to F (x + k T) = F (x)$
509	508	adantlr	$⊢ ((χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \land x \in (X, Q (i + 1) - k T)) \to F (x + k T) = F (x)$
510		simpr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)$
511	469 470 472 473 474 504 509 510	limcperiod	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to w \in (({F ↾}_{\{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}}) {lim}_{ℂ} (X + k T))$
512	262	eqcomd	$⊢ χ \to Q (i + 1) = Q (i + 1) - k T + k T$
513	240 512	oveq12d	$⊢ χ \to (y, Q (i + 1)) = (X + k T, Q (i + 1) - k T + k T)$
514	237 191 190	iooshift	$⊢ χ \to (X + k T, Q (i + 1) - k T + k T) = \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}$
515	513 514	eqtr2d	$⊢ χ \to \{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\} = (y, Q (i + 1))$
516	515	reseq2d	$⊢ χ \to {F ↾}_{\{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}} = {F ↾}_{(y, Q (i + 1))}$
517	516 241	oveq12d	$⊢ χ \to ({F ↾}_{\{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}}) {lim}_{ℂ} (X + k T) = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
518	517	adantr	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to ({F ↾}_{\{z \in ℂ \| \exists x \in (X, Q (i + 1) - k T) z = x + k T\}}) {lim}_{ℂ} (X + k T) = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
519	511 518	eleqtrd	$⊢ (χ \land w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)) \to w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)$
520	468	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to F : dom F ⟶ ℂ$
521		ioosscn	$⊢ (y, Q (i + 1)) \subseteq ℂ$
522	521	a1i	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to (y, Q (i + 1)) \subseteq ℂ$
523		icogelb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land y \in [Q (i), Q (i + 1))) \to Q (i) \leq y$
524	227 229 242 523	syl3anc	$⊢ χ \to Q (i) \leq y$
525		iooss1	$⊢ (Q (i) \in ℝ^{*} \land Q (i) \leq y) \to (y, Q (i + 1)) \subseteq (Q (i), Q (i + 1))$
526	227 524 525	syl2anc	$⊢ χ \to (y, Q (i + 1)) \subseteq (Q (i), Q (i + 1))$
527	526 221	sstrd	$⊢ χ \to (y, Q (i + 1)) \subseteq D$
528	527 167	sseqtrrd	$⊢ χ \to (y, Q (i + 1)) \subseteq dom F$
529	528	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to (y, Q (i + 1)) \subseteq dom F$
530	364	negcld	$⊢ χ \to - k \in ℂ$
531	530 199	mulcld	$⊢ χ \to (- k) T \in ℂ$
532	531	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to (- k) T \in ℂ$
533		eqid	$⊢ \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} = \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}$
534		eqeq1	$⊢ z = w \to (z = x + (- k) T \leftrightarrow w = x + (- k) T)$
535	534	rexbidv	$⊢ z = w \to (\exists x \in (y, Q (i + 1)) z = x + (- k) T \leftrightarrow \exists x \in (y, Q (i + 1)) w = x + (- k) T)$
536	535	elrab	$⊢ w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \leftrightarrow (w \in ℂ \land \exists x \in (y, Q (i + 1)) w = x + (- k) T)$
537	536	simprbi	$⊢ w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \to \exists x \in (y, Q (i + 1)) w = x + (- k) T$
538	537	adantl	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}) \to \exists x \in (y, Q (i + 1)) w = x + (- k) T$
539		nfre1	$⊢ Ⅎ x \exists x \in (y, Q (i + 1)) z = x + (- k) T$
540	539 482	nfrabw	$⊢ \underline{Ⅎ} x \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}$
541	540	nfcri	$⊢ Ⅎ x w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}$
542	480 541	nfan	$⊢ Ⅎ x (χ \land w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\})$
543		simp3	$⊢ (χ \land x \in (y, Q (i + 1)) \land w = x + (- k) T) \to w = x + (- k) T$
544	160	adantr	$⊢ (χ \land x \in (y, Q (i + 1))) \to φ$
545	527	sselda	$⊢ (χ \land x \in (y, Q (i + 1))) \to x \in D$
546	187	adantr	$⊢ (χ \land x \in (y, Q (i + 1))) \to k \in ℤ$
547	546	znegcld	$⊢ (χ \land x \in (y, Q (i + 1))) \to - k \in ℤ$
548	544 545 547 288	syl3anc	$⊢ (χ \land x \in (y, Q (i + 1))) \to x + (- k) T \in D$
549	548	3adant3	$⊢ (χ \land x \in (y, Q (i + 1)) \land w = x + (- k) T) \to x + (- k) T \in D$
550	543 549	eqeltrd	$⊢ (χ \land x \in (y, Q (i + 1)) \land w = x + (- k) T) \to w \in D$
551	550	3exp	$⊢ χ \to (x \in (y, Q (i + 1)) \to (w = x + (- k) T \to w \in D))$
552	551	adantr	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}) \to (x \in (y, Q (i + 1)) \to (w = x + (- k) T \to w \in D))$
553	542 486 552	rexlimd	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}) \to (\exists x \in (y, Q (i + 1)) w = x + (- k) T \to w \in D)$
554	538 553	mpd	$⊢ (χ \land w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}) \to w \in D$
555	554	ralrimiva	$⊢ χ \to \forall w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} w \in D$
556		dfss3	$⊢ \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \subseteq D \leftrightarrow \forall w \in \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} w \in D$
557	555 556	sylibr	$⊢ χ \to \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \subseteq D$
558	557 167	sseqtrrd	$⊢ χ \to \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \subseteq dom F$
559	558	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} \subseteq dom F$
560	160	ad2antrr	$⊢ ((χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \land x \in (y, Q (i + 1))) \to φ$
561	545	adantlr	$⊢ ((χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \land x \in (y, Q (i + 1))) \to x \in D$
562	547	adantlr	$⊢ ((χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \land x \in (y, Q (i + 1))) \to - k \in ℤ$
563	278	fveq2d	$⊢ j = - k \to F (x + j T) = F (x + (- k) T)$
564	563	eqeq1d	$⊢ j = - k \to (F (x + j T) = F (x) \leftrightarrow F (x + (- k) T) = F (x))$
565	276 564	imbi12d	$⊢ j = - k \to (((φ \land x \in D \land j \in ℤ) \to F (x + j T) = F (x)) \leftrightarrow ((φ \land x \in D \land - k \in ℤ) \to F (x + (- k) T) = F (x)))$
566	284	fveq2d	$⊢ k = j \to F (x + k T) = F (x + j T)$
567	566	eqeq1d	$⊢ k = j \to (F (x + k T) = F (x) \leftrightarrow F (x + j T) = F (x))$
568	282 567	imbi12d	$⊢ k = j \to (((φ \land x \in D \land k \in ℤ) \to F (x + k T) = F (x)) \leftrightarrow ((φ \land x \in D \land j \in ℤ) \to F (x + j T) = F (x)))$
569	568 10	chvarvv	$⊢ (φ \land x \in D \land j \in ℤ) \to F (x + j T) = F (x)$
570	274 565 569	vtocl	$⊢ (φ \land x \in D \land - k \in ℤ) \to F (x + (- k) T) = F (x)$
571	560 561 562 570	syl3anc	$⊢ ((χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \land x \in (y, Q (i + 1))) \to F (x + (- k) T) = F (x)$
572		simpr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)$
573	520 522 529 532 533 559 571 572	limcperiod	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to w \in (({F ↾}_{\{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}}) {lim}_{ℂ} (y + (- k) T))$
574	365	oveq2d	$⊢ χ \to y + (- k) T = y + (- k T)$
575	309	recnd	$⊢ χ \to y \in ℂ$
576	575 261	negsubd	$⊢ χ \to y + (- k T) = y - k T$
577	306	eqcomd	$⊢ χ \to y - k T = X$
578	574 576 577	3eqtrd	$⊢ χ \to y + (- k) T = X$
579	578	eqcomd	$⊢ χ \to X = y + (- k) T$
580	365	oveq2d	$⊢ χ \to Q (i + 1) + (- k) T = Q (i + 1) + (- k T)$
581	260 261	negsubd	$⊢ χ \to Q (i + 1) + (- k T) = Q (i + 1) - k T$
582	580 581	eqtr2d	$⊢ χ \to Q (i + 1) - k T = Q (i + 1) + (- k) T$
583	579 582	oveq12d	$⊢ χ \to (X, Q (i + 1) - k T) = (y + (- k) T, Q (i + 1) + (- k) T)$
584	188	renegcld	$⊢ χ \to - k \in ℝ$
585	584 189	remulcld	$⊢ χ \to (- k) T \in ℝ$
586	309 186 585	iooshift	$⊢ χ \to (y + (- k) T, Q (i + 1) + (- k) T) = \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}$
587	583 586	eqtr2d	$⊢ χ \to \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} = (X, Q (i + 1) - k T)$
588	587	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to \{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\} = (X, Q (i + 1) - k T)$
589	588	reseq2d	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to {F ↾}_{\{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}} = {F ↾}_{(X, Q (i + 1) - k T)}$
590	578	adantr	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to y + (- k) T = X$
591	589 590	oveq12d	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to ({F ↾}_{\{z \in ℂ \| \exists x \in (y, Q (i + 1)) z = x + (- k) T\}}) {lim}_{ℂ} (y + (- k) T) = ({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X$
592	573 591	eleqtrd	$⊢ (χ \land w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)) \to w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X)$
593	519 592	impbida	$⊢ χ \to (w \in (({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X) \leftrightarrow w \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y))$
594	593	eqrdv	$⊢ χ \to ({F ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
595	463 594	eqtrd	$⊢ χ \to ({({F ↾}_{((X, +∞) \cap D)}) ↾}_{(X, Q (i + 1) - k T)}) {lim}_{ℂ} X = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
596	171 461 595	3eqtr2d	$⊢ χ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
597	160 181 81	syl2anc	$⊢ χ \to Q (i) < Q (i + 1)$
598	160 181 11	syl2anc	$⊢ χ \to ({F ↾}_{(Q (i), Q (i + 1))}) : (Q (i), Q (i + 1)) \underset{cn}{⟶} ℂ$
599	160 181 12	syl2anc	$⊢ χ \to R \in (({F ↾}_{(Q (i), Q (i + 1))}) {lim}_{ℂ} Q (i))$
600		eqid	$⊢ if (y = Q (i), R, ({F ↾}_{(Q (i), Q (i + 1))}) (y)) = if (y = Q (i), R, ({F ↾}_{(Q (i), Q (i + 1))}) (y))$
601		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} [Q (i), Q (i + 1)) = TopOpen (ℂ_{fld}) ↾_{𝑡} [Q (i), Q (i + 1))$
602	226 186 597 598 599 309 186 311 526 600 601	fourierdlem32	$⊢ χ \to if (y = Q (i), R, ({F ↾}_{(Q (i), Q (i + 1))}) (y)) \in (({({F ↾}_{(Q (i), Q (i + 1))}) ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)$
603	526	resabs1d	$⊢ χ \to {({F ↾}_{(Q (i), Q (i + 1))}) ↾}_{(y, Q (i + 1))} = {F ↾}_{(y, Q (i + 1))}$
604	603	oveq1d	$⊢ χ \to ({({F ↾}_{(Q (i), Q (i + 1))}) ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y = ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y$
605	602 604	eleqtrd	$⊢ χ \to if (y = Q (i), R, ({F ↾}_{(Q (i), Q (i + 1))}) (y)) \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y)$
606		ne0i	$⊢ if (y = Q (i), R, ({F ↾}_{(Q (i), Q (i + 1))}) (y)) \in (({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y) \to ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y \neq \emptyset$
607	605 606	syl	$⊢ χ \to ({F ↾}_{(y, Q (i + 1))}) {lim}_{ℂ} y \neq \emptyset$
608	596 607	eqnetrd	$⊢ χ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
609	16 608	sylbir	$⊢ ((((φ \land i \in (0 ..^M)) \land y \in [Q (i), Q (i + 1))) \land k \in ℤ) \land y = X + k T) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
610	155 156 157 609	syl21anc	$⊢ (φ \land (i \in (0 ..^M) \land k \in ℤ) \land (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
611	610	3exp	$⊢ φ \to ((i \in (0 ..^M) \land k \in ℤ) \to ((y \in [Q (i), Q (i + 1)) \land y = X + k T) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset))$
612	611	adantr	$⊢ (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ((i \in (0 ..^M) \land k \in ℤ) \to ((y \in [Q (i), Q (i + 1)) \land y = X + k T) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset))$
613	146 151 612	rexlim2d	$⊢ (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to (\exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$
614	143 613	mpd	$⊢ (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
615	136 142 614	vtocl	$⊢ (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) - T \in [Q (i), Q (i + 1)) \land E (X) - T = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
616	17 135 615	syl2anc	$⊢ (φ \land E (X) = B) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
617		iocssre	$⊢ (A \in ℝ^{*} \land B \in ℝ) \to (A, B] \subseteq ℝ$
618	66 2 617	syl2anc	$⊢ φ \to (A, B] \subseteq ℝ$
619		ovex	$⊢ ⌊\frac{B - x}{T}⌋ T \in V$
620	14	fvmpt2	$⊢ (x \in ℝ \land ⌊\frac{B - x}{T}⌋ T \in V) \to Z (x) = ⌊\frac{B - x}{T}⌋ T$
621	619 620	mpan2	$⊢ x \in ℝ \to Z (x) = ⌊\frac{B - x}{T}⌋ T$
622	621	oveq2d	$⊢ x \in ℝ \to x + Z (x) = x + ⌊\frac{B - x}{T}⌋ T$
623	622	mpteq2ia	$⊢ (x \in ℝ ⟼ x + Z (x)) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
624	15 623	eqtri	$⊢ E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
625	1 2 3 5 624	fourierdlem4	$⊢ φ \to E : ℝ ⟶ (A, B]$
626	625 13	ffvelrnd	$⊢ φ \to E (X) \in (A, B]$
627	618 626	sseldd	$⊢ φ \to E (X) \in ℝ$
628	627	adantr	$⊢ (φ \land E (X) \neq B) \to E (X) \in ℝ$
629		simpl	$⊢ (φ \land E (X) \neq B) \to φ$
630		simpr	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to E (X) \in ran Q$
631		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
632	48 631	syl	$⊢ φ \to Q Fn (0 \dots M)$
633	632	ad2antrr	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to Q Fn (0 \dots M)$
634		fvelrnb	$⊢ Q Fn (0 \dots M) \to (E (X) \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = E (X))$
635	633 634	syl	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to (E (X) \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = E (X))$
636	630 635	mpbid	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to \exists j \in (0 \dots M) Q (j) = E (X)$
637		1zzd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 1 \in ℤ$
638		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
639	638	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j \in ℤ$
640	639	zred	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j \in ℝ$
641		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
642	641	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 0 \leq j$
643		id	$⊢ Q (j) = E (X) \to Q (j) = E (X)$
644	643	eqcomd	$⊢ Q (j) = E (X) \to E (X) = Q (j)$
645	644	ad2antlr	$⊢ ((φ \land Q (j) = E (X)) \land j = 0) \to E (X) = Q (j)$
646		fveq2	$⊢ j = 0 \to Q (j) = Q (0)$
647	646	adantl	$⊢ ((φ \land Q (j) = E (X)) \land j = 0) \to Q (j) = Q (0)$
648	45	simprld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
649	648	simpld	$⊢ φ \to Q (0) = A$
650	649	ad2antrr	$⊢ ((φ \land Q (j) = E (X)) \land j = 0) \to Q (0) = A$
651	645 647 650	3eqtrd	$⊢ ((φ \land Q (j) = E (X)) \land j = 0) \to E (X) = A$
652	651	adantllr	$⊢ (((φ \land E (X) \in (A, B]) \land Q (j) = E (X)) \land j = 0) \to E (X) = A$
653	652	adantllr	$⊢ ((((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \land j = 0) \to E (X) = A$
654	1	adantr	$⊢ (φ \land E (X) \in (A, B]) \to A \in ℝ$
655	66	adantr	$⊢ (φ \land E (X) \in (A, B]) \to A \in ℝ^{*}$
656	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
657	656	adantr	$⊢ (φ \land E (X) \in (A, B]) \to B \in ℝ^{*}$
658		simpr	$⊢ (φ \land E (X) \in (A, B]) \to E (X) \in (A, B]$
659		iocgtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land E (X) \in (A, B]) \to A < E (X)$
660	655 657 658 659	syl3anc	$⊢ (φ \land E (X) \in (A, B]) \to A < E (X)$
661	654 660	gtned	$⊢ (φ \land E (X) \in (A, B]) \to E (X) \neq A$
662	661	neneqd	$⊢ (φ \land E (X) \in (A, B]) \to \neg E (X) = A$
663	662	ad3antrrr	$⊢ ((((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \land j = 0) \to \neg E (X) = A$
664	653 663	pm2.65da	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to \neg j = 0$
665	664	neqned	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j \neq 0$
666	640 642 665	ne0gt0d	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 0 < j$
667		0zd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 0 \in ℤ$
668		zltp1le	$⊢ (0 \in ℤ \land j \in ℤ) \to (0 < j \leftrightarrow 0 + 1 \leq j)$
669	667 639 668	syl2anc	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to (0 < j \leftrightarrow 0 + 1 \leq j)$
670	666 669	mpbid	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 0 + 1 \leq j$
671	85 670	eqbrtrid	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 1 \leq j$
672		eluz2	$⊢ j \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land j \in ℤ \land 1 \leq j)$
673	637 639 671 672	syl3anbrc	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j \in ℤ_{\geq 1}$
674		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
675	673 674	eleqtrrdi	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j \in ℕ$
676		nnm1nn0	$⊢ j \in ℕ \to j - 1 \in ℕ_{0}$
677	675 676	syl	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \in ℕ_{0}$
678	677 50	eleqtrdi	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \in ℤ_{\geq 0}$
679	19	ad3antrrr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to M \in ℤ$
680		peano2zm	$⊢ j \in ℤ \to j - 1 \in ℤ$
681	638 680	syl	$⊢ j \in (0 \dots M) \to j - 1 \in ℤ$
682	681	zred	$⊢ j \in (0 \dots M) \to j - 1 \in ℝ$
683	638	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
684		elfzel2	$⊢ j \in (0 \dots M) \to M \in ℤ$
685	684	zred	$⊢ j \in (0 \dots M) \to M \in ℝ$
686	683	ltm1d	$⊢ j \in (0 \dots M) \to j - 1 < j$
687		elfzle2	$⊢ j \in (0 \dots M) \to j \leq M$
688	682 683 685 686 687	ltletrd	$⊢ j \in (0 \dots M) \to j - 1 < M$
689	688	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 < M$
690		elfzo2	$⊢ j - 1 \in (0 ..^M) \leftrightarrow (j - 1 \in ℤ_{\geq 0} \land M \in ℤ \land j - 1 < M)$
691	678 679 689 690	syl3anbrc	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \in (0 ..^M)$
692	48	ad3antrrr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q : (0 \dots M) ⟶ ℝ$
693	639 680	syl	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \in ℤ$
694	667 679 693	3jca	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to (0 \in ℤ \land M \in ℤ \land j - 1 \in ℤ)$
695	677	nn0ge0d	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to 0 \leq j - 1$
696	682 685 688	ltled	$⊢ j \in (0 \dots M) \to j - 1 \leq M$
697	696	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \leq M$
698	694 695 697	jca32	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to ((0 \in ℤ \land M \in ℤ \land j - 1 \in ℤ) \land (0 \leq j - 1 \land j - 1 \leq M))$
699		elfz2	$⊢ j - 1 \in (0 \dots M) \leftrightarrow ((0 \in ℤ \land M \in ℤ \land j - 1 \in ℤ) \land (0 \leq j - 1 \land j - 1 \leq M))$
700	698 699	sylibr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to j - 1 \in (0 \dots M)$
701	692 700	ffvelrnd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1) \in ℝ$
702	701	rexrd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1) \in ℝ^{*}$
703	48	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ$
704	703	rexrd	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ^{*}$
705	704	adantlr	$⊢ ((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \to Q (j) \in ℝ^{*}$
706	705	adantr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j) \in ℝ^{*}$
707	618	sselda	$⊢ (φ \land E (X) \in (A, B]) \to E (X) \in ℝ$
708	707	rexrd	$⊢ (φ \land E (X) \in (A, B]) \to E (X) \in ℝ^{*}$
709	708	ad2antrr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \in ℝ^{*}$
710		simplll	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to φ$
711		ovex	$⊢ j - 1 \in V$
712		eleq1	$⊢ i = j - 1 \to (i \in (0 ..^M) \leftrightarrow j - 1 \in (0 ..^M))$
713	712	anbi2d	$⊢ i = j - 1 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j - 1 \in (0 ..^M)))$
714		fveq2	$⊢ i = j - 1 \to Q (i) = Q (j - 1)$
715		oveq1	$⊢ i = j - 1 \to i + 1 = j - 1 + 1$
716	715	fveq2d	$⊢ i = j - 1 \to Q (i + 1) = Q (j - 1 + 1)$
717	714 716	breq12d	$⊢ i = j - 1 \to (Q (i) < Q (i + 1) \leftrightarrow Q (j - 1) < Q (j - 1 + 1))$
718	713 717	imbi12d	$⊢ i = j - 1 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land j - 1 \in (0 ..^M)) \to Q (j - 1) < Q (j - 1 + 1)))$
719	711 718 81	vtocl	$⊢ (φ \land j - 1 \in (0 ..^M)) \to Q (j - 1) < Q (j - 1 + 1)$
720	710 691 719	syl2anc	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1) < Q (j - 1 + 1)$
721	638	zcnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
722		1cnd	$⊢ j \in (0 \dots M) \to 1 \in ℂ$
723	721 722	npcand	$⊢ j \in (0 \dots M) \to j - 1 + 1 = j$
724	723	eqcomd	$⊢ j \in (0 \dots M) \to j = j - 1 + 1$
725	724	fveq2d	$⊢ j \in (0 \dots M) \to Q (j) = Q (j - 1 + 1)$
726	725	eqcomd	$⊢ j \in (0 \dots M) \to Q (j - 1 + 1) = Q (j)$
727	726	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1 + 1) = Q (j)$
728	720 727	breqtrd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1) < Q (j)$
729		simpr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j) = E (X)$
730	728 729	breqtrd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to Q (j - 1) < E (X)$
731	627	leidd	$⊢ φ \to E (X) \leq E (X)$
732	731	ad2antrr	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \leq E (X)$
733	644	adantl	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) = Q (j)$
734	732 733	breqtrd	$⊢ ((φ \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \leq Q (j)$
735	734	adantllr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \leq Q (j)$
736	702 706 709 730 735	eliocd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \in (Q (j - 1), Q (j)]$
737	725	oveq2d	$⊢ j \in (0 \dots M) \to (Q (j - 1), Q (j)] = (Q (j - 1), Q (j - 1 + 1)]$
738	737	ad2antlr	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to (Q (j - 1), Q (j)] = (Q (j - 1), Q (j - 1 + 1)]$
739	736 738	eleqtrd	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to E (X) \in (Q (j - 1), Q (j - 1 + 1)]$
740	714 716	oveq12d	$⊢ i = j - 1 \to (Q (i), Q (i + 1)] = (Q (j - 1), Q (j - 1 + 1)]$
741	740	eleq2d	$⊢ i = j - 1 \to (E (X) \in (Q (i), Q (i + 1)] \leftrightarrow E (X) \in (Q (j - 1), Q (j - 1 + 1)])$
742	741	rspcev	$⊢ (j - 1 \in (0 ..^M) \land E (X) \in (Q (j - 1), Q (j - 1 + 1)]) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
743	691 739 742	syl2anc	$⊢ (((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \land Q (j) = E (X)) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
744	743	ex	$⊢ ((φ \land E (X) \in (A, B]) \land j \in (0 \dots M)) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)])$
745	744	adantlr	$⊢ (((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \land j \in (0 \dots M)) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)])$
746	745	rexlimdva	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to (\exists j \in (0 \dots M) Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)])$
747	636 746	mpd	$⊢ ((φ \land E (X) \in (A, B]) \land E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
748	6	ad2antrr	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to M \in ℕ$
749	48	ad2antrr	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to Q : (0 \dots M) ⟶ ℝ$
750		iocssicc	$⊢ (A, B] \subseteq [A, B]$
751	649	eqcomd	$⊢ φ \to A = Q (0)$
752	648	simprd	$⊢ φ \to Q (M) = B$
753	752	eqcomd	$⊢ φ \to B = Q (M)$
754	751 753	oveq12d	$⊢ φ \to [A, B] = [Q (0), Q (M)]$
755	750 754	sseqtrid	$⊢ φ \to (A, B] \subseteq [Q (0), Q (M)]$
756	755	sselda	$⊢ (φ \land E (X) \in (A, B]) \to E (X) \in [Q (0), Q (M)]$
757	756	adantr	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to E (X) \in [Q (0), Q (M)]$
758		simpr	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to \neg E (X) \in ran Q$
759		fveq2	$⊢ k = j \to Q (k) = Q (j)$
760	759	breq1d	$⊢ k = j \to (Q (k) < E (X) \leftrightarrow Q (j) < E (X))$
761	760	cbvrabv	$⊢ \{k \in (0 ..^M) \| Q (k) < E (X)\} = \{j \in (0 ..^M) \| Q (j) < E (X)\}$
762	761	supeq1i	$⊢ sup (\{k \in (0 ..^M) \| Q (k) < E (X)\} ℝ <) = sup (\{j \in (0 ..^M) \| Q (j) < E (X)\} ℝ <)$
763	748 749 757 758 762	fourierdlem25	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1))$
764		ioossioc	$⊢ (Q (i), Q (i + 1)) \subseteq (Q (i), Q (i + 1)]$
765	764	sseli	$⊢ E (X) \in (Q (i), Q (i + 1)) \to E (X) \in (Q (i), Q (i + 1)]$
766	765	a1i	$⊢ (((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \land i \in (0 ..^M)) \to (E (X) \in (Q (i), Q (i + 1)) \to E (X) \in (Q (i), Q (i + 1)])$
767	766	reximdva	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to (\exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)])$
768	763 767	mpd	$⊢ ((φ \land E (X) \in (A, B]) \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
769	747 768	pm2.61dan	$⊢ (φ \land E (X) \in (A, B]) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
770	626 769	mpdan	$⊢ φ \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
771		fveq2	$⊢ i = j \to Q (i) = Q (j)$
772		oveq1	$⊢ i = j \to i + 1 = j + 1$
773	772	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
774	771 773	oveq12d	$⊢ i = j \to (Q (i), Q (i + 1)] = (Q (j), Q (j + 1)]$
775	774	eleq2d	$⊢ i = j \to (E (X) \in (Q (i), Q (i + 1)] \leftrightarrow E (X) \in (Q (j), Q (j + 1)])$
776	775	cbvrexvw	$⊢ \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)] \leftrightarrow \exists j \in (0 ..^M) E (X) \in (Q (j), Q (j + 1)]$
777	770 776	sylib	$⊢ φ \to \exists j \in (0 ..^M) E (X) \in (Q (j), Q (j + 1)]$
778	777	adantr	$⊢ (φ \land E (X) \neq B) \to \exists j \in (0 ..^M) E (X) \in (Q (j), Q (j + 1)]$
779		elfzonn0	$⊢ j \in (0 ..^M) \to j \in ℕ_{0}$
780		1nn0	$⊢ 1 \in ℕ_{0}$
781	780	a1i	$⊢ j \in (0 ..^M) \to 1 \in ℕ_{0}$
782	779 781	nn0addcld	$⊢ j \in (0 ..^M) \to j + 1 \in ℕ_{0}$
783	782 50	eleqtrdi	$⊢ j \in (0 ..^M) \to j + 1 \in ℤ_{\geq 0}$
784	783	adantr	$⊢ (j \in (0 ..^M) \land E (X) = Q (j + 1)) \to j + 1 \in ℤ_{\geq 0}$
785	784	3ad2antl2	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 \in ℤ_{\geq 0}$
786	19	ad2antrr	$⊢ ((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \to M \in ℤ$
787	786	3ad2antl1	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to M \in ℤ$
788	779	nn0red	$⊢ j \in (0 ..^M) \to j \in ℝ$
789	788	adantr	$⊢ (j \in (0 ..^M) \land E (X) = Q (j + 1)) \to j \in ℝ$
790	789	3ad2antl2	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j \in ℝ$
791		1red	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to 1 \in ℝ$
792	790 791	readdcld	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 \in ℝ$
793	787	zred	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to M \in ℝ$
794		elfzop1le2	$⊢ j \in (0 ..^M) \to j + 1 \leq M$
795	794	adantr	$⊢ (j \in (0 ..^M) \land E (X) = Q (j + 1)) \to j + 1 \leq M$
796	795	3ad2antl2	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 \leq M$
797		simplr	$⊢ ((φ \land E (X) = Q (j + 1)) \land M = j + 1) \to E (X) = Q (j + 1)$
798		fveq2	$⊢ M = j + 1 \to Q (M) = Q (j + 1)$
799	798	eqcomd	$⊢ M = j + 1 \to Q (j + 1) = Q (M)$
800	799	adantl	$⊢ ((φ \land E (X) = Q (j + 1)) \land M = j + 1) \to Q (j + 1) = Q (M)$
801	752	ad2antrr	$⊢ ((φ \land E (X) = Q (j + 1)) \land M = j + 1) \to Q (M) = B$
802	797 800 801	3eqtrd	$⊢ ((φ \land E (X) = Q (j + 1)) \land M = j + 1) \to E (X) = B$
803	802	adantllr	$⊢ (((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \land M = j + 1) \to E (X) = B$
804		simpllr	$⊢ (((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \land M = j + 1) \to E (X) \neq B$
805	804	neneqd	$⊢ (((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \land M = j + 1) \to \neg E (X) = B$
806	803 805	pm2.65da	$⊢ ((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \to \neg M = j + 1$
807	806	neqned	$⊢ ((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \to M \neq j + 1$
808	807	3ad2antl1	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to M \neq j + 1$
809	792 793 796 808	leneltd	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 < M$
810		elfzo2	$⊢ j + 1 \in (0 ..^M) \leftrightarrow (j + 1 \in ℤ_{\geq 0} \land M \in ℤ \land j + 1 < M)$
811	785 787 809 810	syl3anbrc	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 \in (0 ..^M)$
812	48	adantr	$⊢ (φ \land j \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
813		fzofzp1	$⊢ j \in (0 ..^M) \to j + 1 \in (0 \dots M)$
814	813	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j + 1 \in (0 \dots M)$
815	812 814	ffvelrnd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ$
816	815	rexrd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ^{*}$
817	816	adantlr	$⊢ ((φ \land E (X) \neq B) \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ^{*}$
818	817	3adant3	$⊢ ((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j + 1) \in ℝ^{*}$
819	818	adantr	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to Q (j + 1) \in ℝ^{*}$
820		simpl1l	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to φ$
821	820 48	syl	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to Q : (0 \dots M) ⟶ ℝ$
822		fzofzp1	$⊢ j + 1 \in (0 ..^M) \to j + 1 + 1 \in (0 \dots M)$
823	811 822	syl	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to j + 1 + 1 \in (0 \dots M)$
824	821 823	ffvelrnd	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to Q (j + 1 + 1) \in ℝ$
825	824	rexrd	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to Q (j + 1 + 1) \in ℝ^{*}$
826	627	rexrd	$⊢ φ \to E (X) \in ℝ^{*}$
827	826	ad2antrr	$⊢ ((φ \land E (X) \neq B) \land E (X) = Q (j + 1)) \to E (X) \in ℝ^{*}$
828	827	3ad2antl1	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to E (X) \in ℝ^{*}$
829	815	leidd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \leq Q (j + 1)$
830	829	adantr	$⊢ ((φ \land j \in (0 ..^M)) \land E (X) = Q (j + 1)) \to Q (j + 1) \leq Q (j + 1)$
831		id	$⊢ E (X) = Q (j + 1) \to E (X) = Q (j + 1)$
832	831	eqcomd	$⊢ E (X) = Q (j + 1) \to Q (j + 1) = E (X)$
833	832	adantl	$⊢ ((φ \land j \in (0 ..^M)) \land E (X) = Q (j + 1)) \to Q (j + 1) = E (X)$
834	830 833	breqtrd	$⊢ ((φ \land j \in (0 ..^M)) \land E (X) = Q (j + 1)) \to Q (j + 1) \leq E (X)$
835	834	adantllr	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M)) \land E (X) = Q (j + 1)) \to Q (j + 1) \leq E (X)$
836	835	3adantl3	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to Q (j + 1) \leq E (X)$
837		simpr	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to E (X) = Q (j + 1)$
838		simpr	$⊢ ((φ \land j + 1 \in (0 ..^M)) \land E (X) = Q (j + 1)) \to E (X) = Q (j + 1)$
839		ovex	$⊢ j + 1 \in V$
840		eleq1	$⊢ i = j + 1 \to (i \in (0 ..^M) \leftrightarrow j + 1 \in (0 ..^M))$
841	840	anbi2d	$⊢ i = j + 1 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j + 1 \in (0 ..^M)))$
842		fveq2	$⊢ i = j + 1 \to Q (i) = Q (j + 1)$
843		oveq1	$⊢ i = j + 1 \to i + 1 = j + 1 + 1$
844	843	fveq2d	$⊢ i = j + 1 \to Q (i + 1) = Q (j + 1 + 1)$
845	842 844	breq12d	$⊢ i = j + 1 \to (Q (i) < Q (i + 1) \leftrightarrow Q (j + 1) < Q (j + 1 + 1))$
846	841 845	imbi12d	$⊢ i = j + 1 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land j + 1 \in (0 ..^M)) \to Q (j + 1) < Q (j + 1 + 1)))$
847	839 846 81	vtocl	$⊢ (φ \land j + 1 \in (0 ..^M)) \to Q (j + 1) < Q (j + 1 + 1)$
848	847	adantr	$⊢ ((φ \land j + 1 \in (0 ..^M)) \land E (X) = Q (j + 1)) \to Q (j + 1) < Q (j + 1 + 1)$
849	838 848	eqbrtrd	$⊢ ((φ \land j + 1 \in (0 ..^M)) \land E (X) = Q (j + 1)) \to E (X) < Q (j + 1 + 1)$
850	820 811 837 849	syl21anc	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to E (X) < Q (j + 1 + 1)$
851	819 825 828 836 850	elicod	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to E (X) \in [Q (j + 1), Q (j + 1 + 1))$
852	842 844	oveq12d	$⊢ i = j + 1 \to [Q (i), Q (i + 1)) = [Q (j + 1), Q (j + 1 + 1))$
853	852	eleq2d	$⊢ i = j + 1 \to (E (X) \in [Q (i), Q (i + 1)) \leftrightarrow E (X) \in [Q (j + 1), Q (j + 1 + 1)))$
854	853	rspcev	$⊢ (j + 1 \in (0 ..^M) \land E (X) \in [Q (j + 1), Q (j + 1 + 1))) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
855	811 851 854	syl2anc	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land E (X) = Q (j + 1)) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
856		simpl2	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to j \in (0 ..^M)$
857		id	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)])$
858	857	3adant1r	$⊢ ((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)])$
859		elfzofz	$⊢ j \in (0 ..^M) \to j \in (0 \dots M)$
860	859	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j \in (0 \dots M)$
861	812 860	ffvelrnd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \in ℝ$
862	861	rexrd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) \in ℝ^{*}$
863	862	adantr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg E (X) = Q (j + 1)) \to Q (j) \in ℝ^{*}$
864	863	3adantl3	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to Q (j) \in ℝ^{*}$
865	816	adantr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg E (X) = Q (j + 1)) \to Q (j + 1) \in ℝ^{*}$
866	865	3adantl3	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to Q (j + 1) \in ℝ^{*}$
867	826	adantr	$⊢ (φ \land \neg E (X) = Q (j + 1)) \to E (X) \in ℝ^{*}$
868	867	3ad2antl1	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) \in ℝ^{*}$
869	861	3adant3	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j) \in ℝ$
870	627	3ad2ant1	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to E (X) \in ℝ$
871	862	3adant3	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j) \in ℝ^{*}$
872	816	3adant3	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j + 1) \in ℝ^{*}$
873		simp3	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to E (X) \in (Q (j), Q (j + 1)]$
874		iocgtlb	$⊢ (Q (j) \in ℝ^{} \land Q (j + 1) \in ℝ^{} \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j) < E (X)$
875	871 872 873 874	syl3anc	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j) < E (X)$
876	869 870 875	ltled	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to Q (j) \leq E (X)$
877	876	adantr	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to Q (j) \leq E (X)$
878	870	adantr	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) \in ℝ$
879	815	adantr	$⊢ ((φ \land j \in (0 ..^M)) \land \neg E (X) = Q (j + 1)) \to Q (j + 1) \in ℝ$
880	879	3adantl3	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to Q (j + 1) \in ℝ$
881		iocleub	$⊢ (Q (j) \in ℝ^{} \land Q (j + 1) \in ℝ^{} \land E (X) \in (Q (j), Q (j + 1)]) \to E (X) \leq Q (j + 1)$
882	871 872 873 881	syl3anc	$⊢ (φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to E (X) \leq Q (j + 1)$
883	882	adantr	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) \leq Q (j + 1)$
884		neqne	$⊢ \neg E (X) = Q (j + 1) \to E (X) \neq Q (j + 1)$
885	884	necomd	$⊢ \neg E (X) = Q (j + 1) \to Q (j + 1) \neq E (X)$
886	885	adantl	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to Q (j + 1) \neq E (X)$
887	878 880 883 886	leneltd	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) < Q (j + 1)$
888	864 866 868 877 887	elicod	$⊢ ((φ \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) \in [Q (j), Q (j + 1))$
889	858 888	sylan	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to E (X) \in [Q (j), Q (j + 1))$
890	771 773	oveq12d	$⊢ i = j \to [Q (i), Q (i + 1)) = [Q (j), Q (j + 1))$
891	890	eleq2d	$⊢ i = j \to (E (X) \in [Q (i), Q (i + 1)) \leftrightarrow E (X) \in [Q (j), Q (j + 1)))$
892	891	rspcev	$⊢ (j \in (0 ..^M) \land E (X) \in [Q (j), Q (j + 1))) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
893	856 889 892	syl2anc	$⊢ (((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \land \neg E (X) = Q (j + 1)) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
894	855 893	pm2.61dan	$⊢ ((φ \land E (X) \neq B) \land j \in (0 ..^M) \land E (X) \in (Q (j), Q (j + 1)]) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
895	894	rexlimdv3a	$⊢ (φ \land E (X) \neq B) \to (\exists j \in (0 ..^M) E (X) \in (Q (j), Q (j + 1)] \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1)))$
896	778 895	mpd	$⊢ (φ \land E (X) \neq B) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
897		simpr	$⊢ ((φ \land E (X) \neq B) \land E (X) \in [Q (i), Q (i + 1))) \to E (X) \in [Q (i), Q (i + 1))$
898		oveq1	$⊢ k = ⌊\frac{B - X}{T}⌋ \to k T = ⌊\frac{B - X}{T}⌋ T$
899	898	oveq2d	$⊢ k = ⌊\frac{B - X}{T}⌋ \to X + k T = X + ⌊\frac{B - X}{T}⌋ T$
900	899	eqeq2d	$⊢ k = ⌊\frac{B - X}{T}⌋ \to (E (X) = X + k T \leftrightarrow E (X) = X + ⌊\frac{B - X}{T}⌋ T)$
901	900	rspcev	$⊢ (⌊\frac{B - X}{T}⌋ \in ℤ \land E (X) = X + ⌊\frac{B - X}{T}⌋ T) \to \exists k \in ℤ E (X) = X + k T$
902	105 113 901	syl2anc	$⊢ φ \to \exists k \in ℤ E (X) = X + k T$
903	902	ad2antrr	$⊢ ((φ \land E (X) \neq B) \land E (X) \in [Q (i), Q (i + 1))) \to \exists k \in ℤ E (X) = X + k T$
904		r19.42v	$⊢ \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T) \leftrightarrow (E (X) \in [Q (i), Q (i + 1)) \land \exists k \in ℤ E (X) = X + k T)$
905	897 903 904	sylanbrc	$⊢ ((φ \land E (X) \neq B) \land E (X) \in [Q (i), Q (i + 1))) \to \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T)$
906	905	ex	$⊢ (φ \land E (X) \neq B) \to (E (X) \in [Q (i), Q (i + 1)) \to \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T))$
907	906	reximdv	$⊢ (φ \land E (X) \neq B) \to (\exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1)) \to \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T))$
908	896 907	mpd	$⊢ (φ \land E (X) \neq B) \to \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T)$
909	629 908	jca	$⊢ (φ \land E (X) \neq B) \to (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T))$
910		eleq1	$⊢ y = E (X) \to (y \in [Q (i), Q (i + 1)) \leftrightarrow E (X) \in [Q (i), Q (i + 1)))$
911		eqeq1	$⊢ y = E (X) \to (y = X + k T \leftrightarrow E (X) = X + k T)$
912	910 911	anbi12d	$⊢ y = E (X) \to ((y \in [Q (i), Q (i + 1)) \land y = X + k T) \leftrightarrow (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T))$
913	912	2rexbidv	$⊢ y = E (X) \to (\exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T) \leftrightarrow \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T))$
914	913	anbi2d	$⊢ y = E (X) \to ((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \leftrightarrow (φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T)))$
915	914	imbi1d	$⊢ y = E (X) \to (((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (y \in [Q (i), Q (i + 1)) \land y = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset) \leftrightarrow ((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset))$
916	915 614	vtoclg	$⊢ E (X) \in ℝ \to ((φ \land \exists i \in (0 ..^M) \exists k \in ℤ (E (X) \in [Q (i), Q (i + 1)) \land E (X) = X + k T)) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset)$
917	628 909 916	sylc	$⊢ (φ \land E (X) \neq B) \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$
918	616 917	pm2.61dane	$⊢ φ \to ({F ↾}_{(X, +∞)}) {lim}_{ℂ} X \neq \emptyset$

Metamath Proof Explorer

Theorem fourierdlem48

Proof