fourierdlem48

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

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

Proof

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

Metamath Proof Explorer

Theorem fourierdlem48

Proof