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

Metamath Proof Explorer

Theorem fourierdlem49

Proof