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

Metamath Proof Explorer

Theorem fourierdlem49

Proof