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

Metamath Proof Explorer

Theorem fourierdlem48

Proof