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

Metamath Proof Explorer

Theorem fourierdlem48

Proof