fourierdlem49

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

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

Proof

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

Metamath Proof Explorer

Theorem fourierdlem49

Proof