fourierdlem41

Description: Lemma used to prove that every real is a limit point for the domain of the derivative of the periodic function to be approximated. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem41.a	$⊢ φ \to A \in ℝ$
	fourierdlem41.b	$⊢ φ \to B \in ℝ$
	fourierdlem41.altb	$⊢ φ \to A < B$
	fourierdlem41.t	$⊢ T = B - A$
	fourierdlem41.dper	$⊢ (φ \land x \in D \land k \in ℤ) \to x + k T \in D$
	fourierdlem41.x	$⊢ φ \to X \in ℝ$
	fourierdlem41.z	$⊢ Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
	fourierdlem41.e	$⊢ E = (x \in ℝ ⟼ x + Z (x))$
	fourierdlem41.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))\})$
	fourierdlem41.m	$⊢ φ \to M \in ℕ$
	fourierdlem41.q	$⊢ φ \to Q \in P (M)$
	fourierdlem41.qssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq D$
Assertion	fourierdlem41	$⊢ φ \to (\exists y \in ℝ (y < X \land (y, X) \subseteq D) \land \exists y \in ℝ (X < y \land (X, y) \subseteq D))$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem41.a	$⊢ φ \to A \in ℝ$
2		fourierdlem41.b	$⊢ φ \to B \in ℝ$
3		fourierdlem41.altb	$⊢ φ \to A < B$
4		fourierdlem41.t	$⊢ T = B - A$
5		fourierdlem41.dper	$⊢ (φ \land x \in D \land k \in ℤ) \to x + k T \in D$
6		fourierdlem41.x	$⊢ φ \to X \in ℝ$
7		fourierdlem41.z	$⊢ Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
8		fourierdlem41.e	$⊢ E = (x \in ℝ ⟼ x + Z (x))$
9		fourierdlem41.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))\})$
10		fourierdlem41.m	$⊢ φ \to M \in ℕ$
11		fourierdlem41.q	$⊢ φ \to Q \in P (M)$
12		fourierdlem41.qssd	$⊢ (φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq D$
13		simpr	$⊢ (φ \land E (X) \in ran Q) \to E (X) \in ran Q$
14	9	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))))$
15	10 14	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))))$
16	11 15	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)))$
17	16	simpld	$⊢ φ \to Q \in (ℝ^{(0 \dots M)})$
18		elmapi	$⊢ Q \in (ℝ^{(0 \dots M)}) \to Q : (0 \dots M) ⟶ ℝ$
19		ffn	$⊢ Q : (0 \dots M) ⟶ ℝ \to Q Fn (0 \dots M)$
20	17 18 19	3syl	$⊢ φ \to Q Fn (0 \dots M)$
21	20	adantr	$⊢ (φ \land E (X) \in ran Q) \to Q Fn (0 \dots M)$
22		fvelrnb	$⊢ Q Fn (0 \dots M) \to (E (X) \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = E (X))$
23	21 22	syl	$⊢ (φ \land E (X) \in ran Q) \to (E (X) \in ran Q \leftrightarrow \exists j \in (0 \dots M) Q (j) = E (X))$
24	13 23	mpbid	$⊢ (φ \land E (X) \in ran Q) \to \exists j \in (0 \dots M) Q (j) = E (X)$
25		0zd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to 0 \in ℤ$
26		elfzelz	$⊢ j \in (0 \dots M) \to j \in ℤ$
27	26	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j \in ℤ$
28		1zzd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to 1 \in ℤ$
29	27 28	zsubcld	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 \in ℤ$
30		simpll	$⊢ ((φ \land j \in (0 \dots M)) \land \neg 0 < j) \to φ$
31		elfzle1	$⊢ j \in (0 \dots M) \to 0 \leq j$
32	31	anim1i	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to (0 \leq j \land \neg 0 < j)$
33		0red	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to 0 \in ℝ$
34	26	zred	$⊢ j \in (0 \dots M) \to j \in ℝ$
35	34	adantr	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to j \in ℝ$
36	33 35	eqleltd	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to (0 = j \leftrightarrow (0 \leq j \land \neg 0 < j))$
37	32 36	mpbird	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to 0 = j$
38	37	eqcomd	$⊢ (j \in (0 \dots M) \land \neg 0 < j) \to j = 0$
39	38	adantll	$⊢ ((φ \land j \in (0 \dots M)) \land \neg 0 < j) \to j = 0$
40		fveq2	$⊢ j = 0 \to Q (j) = Q (0)$
41	16	simprld	$⊢ φ \to (Q (0) = A \land Q (M) = B)$
42	41	simpld	$⊢ φ \to Q (0) = A$
43	40 42	sylan9eqr	$⊢ (φ \land j = 0) \to Q (j) = A$
44	30 39 43	syl2anc	$⊢ ((φ \land j \in (0 \dots M)) \land \neg 0 < j) \to Q (j) = A$
45	44	3adantl3	$⊢ ((φ \land j \in (0 \dots M) \land Q (j) = E (X)) \land \neg 0 < j) \to Q (j) = A$
46		simpr	$⊢ (φ \land Q (j) = E (X)) \to Q (j) = E (X)$
47	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
48	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
49		eqid	$⊢ (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
50	1 2 3 4 49	fourierdlem4	$⊢ φ \to (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T) : ℝ ⟶ (A, B]$
51	8	a1i	$⊢ φ \to E = (x \in ℝ ⟼ x + Z (x))$
52		simpr	$⊢ (φ \land x \in ℝ) \to x \in ℝ$
53	2	adantr	$⊢ (φ \land x \in ℝ) \to B \in ℝ$
54	53 52	resubcld	$⊢ (φ \land x \in ℝ) \to B - x \in ℝ$
55	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
56	4 55	eqeltrid	$⊢ φ \to T \in ℝ$
57	56	adantr	$⊢ (φ \land x \in ℝ) \to T \in ℝ$
58		0red	$⊢ φ \to 0 \in ℝ$
59	1 2	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
60	3 59	mpbid	$⊢ φ \to 0 < B - A$
61	4	eqcomi	$⊢ B - A = T$
62	61	a1i	$⊢ φ \to B - A = T$
63	60 62	breqtrd	$⊢ φ \to 0 < T$
64	58 63	gtned	$⊢ φ \to T \neq 0$
65	64	adantr	$⊢ (φ \land x \in ℝ) \to T \neq 0$
66	54 57 65	redivcld	$⊢ (φ \land x \in ℝ) \to \frac{B - x}{T} \in ℝ$
67	66	flcld	$⊢ (φ \land x \in ℝ) \to ⌊\frac{B - x}{T}⌋ \in ℤ$
68	67	zred	$⊢ (φ \land x \in ℝ) \to ⌊\frac{B - x}{T}⌋ \in ℝ$
69	68 57	remulcld	$⊢ (φ \land x \in ℝ) \to ⌊\frac{B - x}{T}⌋ T \in ℝ$
70	7	fvmpt2	$⊢ (x \in ℝ \land ⌊\frac{B - x}{T}⌋ T \in ℝ) \to Z (x) = ⌊\frac{B - x}{T}⌋ T$
71	52 69 70	syl2anc	$⊢ (φ \land x \in ℝ) \to Z (x) = ⌊\frac{B - x}{T}⌋ T$
72	71	oveq2d	$⊢ (φ \land x \in ℝ) \to x + Z (x) = x + ⌊\frac{B - x}{T}⌋ T$
73	72	mpteq2dva	$⊢ φ \to (x \in ℝ ⟼ x + Z (x)) = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
74	51 73	eqtrd	$⊢ φ \to E = (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T)$
75	74	feq1d	$⊢ φ \to (E : ℝ ⟶ (A, B] \leftrightarrow (x \in ℝ ⟼ x + ⌊\frac{B - x}{T}⌋ T) : ℝ ⟶ (A, B])$
76	50 75	mpbird	$⊢ φ \to E : ℝ ⟶ (A, B]$
77	76 6	ffvelrnd	$⊢ φ \to E (X) \in (A, B]$
78		iocgtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land E (X) \in (A, B]) \to A < E (X)$
79	47 48 77 78	syl3anc	$⊢ φ \to A < E (X)$
80	1 79	gtned	$⊢ φ \to E (X) \neq A$
81	80	adantr	$⊢ (φ \land Q (j) = E (X)) \to E (X) \neq A$
82	46 81	eqnetrd	$⊢ (φ \land Q (j) = E (X)) \to Q (j) \neq A$
83	82	adantr	$⊢ ((φ \land Q (j) = E (X)) \land \neg 0 < j) \to Q (j) \neq A$
84	83	3adantl2	$⊢ ((φ \land j \in (0 \dots M) \land Q (j) = E (X)) \land \neg 0 < j) \to Q (j) \neq A$
85	84	neneqd	$⊢ ((φ \land j \in (0 \dots M) \land Q (j) = E (X)) \land \neg 0 < j) \to \neg Q (j) = A$
86	45 85	condan	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to 0 < j$
87		zltlem1	$⊢ (0 \in ℤ \land j \in ℤ) \to (0 < j \leftrightarrow 0 \leq j - 1)$
88	25 27 87	syl2anc	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to (0 < j \leftrightarrow 0 \leq j - 1)$
89	86 88	mpbid	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to 0 \leq j - 1$
90		eluz2	$⊢ j - 1 \in ℤ_{\geq 0} \leftrightarrow (0 \in ℤ \land j - 1 \in ℤ \land 0 \leq j - 1)$
91	25 29 89 90	syl3anbrc	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 \in ℤ_{\geq 0}$
92		elfzel2	$⊢ j \in (0 \dots M) \to M \in ℤ$
93	92	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to M \in ℤ$
94		1red	$⊢ j \in (0 \dots M) \to 1 \in ℝ$
95	34 94	resubcld	$⊢ j \in (0 \dots M) \to j - 1 \in ℝ$
96	92	zred	$⊢ j \in (0 \dots M) \to M \in ℝ$
97	34	ltm1d	$⊢ j \in (0 \dots M) \to j - 1 < j$
98		elfzle2	$⊢ j \in (0 \dots M) \to j \leq M$
99	95 34 96 97 98	ltletrd	$⊢ j \in (0 \dots M) \to j - 1 < M$
100	99	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 < M$
101		elfzo2	$⊢ j - 1 \in (0 ..^M) \leftrightarrow (j - 1 \in ℤ_{\geq 0} \land M \in ℤ \land j - 1 < M)$
102	91 93 100 101	syl3anbrc	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 \in (0 ..^M)$
103	17 18	syl	$⊢ φ \to Q : (0 \dots M) ⟶ ℝ$
104	103	3ad2ant1	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q : (0 \dots M) ⟶ ℝ$
105	95 96 99	ltled	$⊢ j \in (0 \dots M) \to j - 1 \leq M$
106	105	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 \leq M$
107	25 93 29 89 106	elfzd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to j - 1 \in (0 \dots M)$
108	104 107	ffvelrnd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1) \in ℝ$
109	108	rexrd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1) \in ℝ^{*}$
110	34	recnd	$⊢ j \in (0 \dots M) \to j \in ℂ$
111		1cnd	$⊢ j \in (0 \dots M) \to 1 \in ℂ$
112	110 111	npcand	$⊢ j \in (0 \dots M) \to j - 1 + 1 = j$
113	112	fveq2d	$⊢ j \in (0 \dots M) \to Q (j - 1 + 1) = Q (j)$
114	113	adantl	$⊢ (φ \land j \in (0 \dots M)) \to Q (j - 1 + 1) = Q (j)$
115	103	ffvelrnda	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ$
116	115	rexrd	$⊢ (φ \land j \in (0 \dots M)) \to Q (j) \in ℝ^{*}$
117	114 116	eqeltrd	$⊢ (φ \land j \in (0 \dots M)) \to Q (j - 1 + 1) \in ℝ^{*}$
118	117	3adant3	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1 + 1) \in ℝ^{*}$
119		id	$⊢ x = X \to x = X$
120		fveq2	$⊢ x = X \to Z (x) = Z (X)$
121	119 120	oveq12d	$⊢ x = X \to x + Z (x) = X + Z (X)$
122	121	adantl	$⊢ (φ \land x = X) \to x + Z (x) = X + Z (X)$
123	7	a1i	$⊢ φ \to Z = (x \in ℝ ⟼ ⌊\frac{B - x}{T}⌋ T)$
124		oveq2	$⊢ x = X \to B - x = B - X$
125	124	oveq1d	$⊢ x = X \to \frac{B - x}{T} = \frac{B - X}{T}$
126	125	fveq2d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ = ⌊\frac{B - X}{T}⌋$
127	126	oveq1d	$⊢ x = X \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - X}{T}⌋ T$
128	127	adantl	$⊢ (φ \land x = X) \to ⌊\frac{B - x}{T}⌋ T = ⌊\frac{B - X}{T}⌋ T$
129	2 6	resubcld	$⊢ φ \to B - X \in ℝ$
130	129 56 64	redivcld	$⊢ φ \to \frac{B - X}{T} \in ℝ$
131	130	flcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℤ$
132	131	zred	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℝ$
133	132 56	remulcld	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T \in ℝ$
134	123 128 6 133	fvmptd	$⊢ φ \to Z (X) = ⌊\frac{B - X}{T}⌋ T$
135	134 133	eqeltrd	$⊢ φ \to Z (X) \in ℝ$
136	6 135	readdcld	$⊢ φ \to X + Z (X) \in ℝ$
137	51 122 6 136	fvmptd	$⊢ φ \to E (X) = X + Z (X)$
138	137 136	eqeltrd	$⊢ φ \to E (X) \in ℝ$
139	138	rexrd	$⊢ φ \to E (X) \in ℝ^{*}$
140	139	3ad2ant1	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \in ℝ^{*}$
141		simp1	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to φ$
142		ovex	$⊢ j - 1 \in V$
143		eleq1	$⊢ i = j - 1 \to (i \in (0 ..^M) \leftrightarrow j - 1 \in (0 ..^M))$
144	143	anbi2d	$⊢ i = j - 1 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j - 1 \in (0 ..^M)))$
145		fveq2	$⊢ i = j - 1 \to Q (i) = Q (j - 1)$
146		oveq1	$⊢ i = j - 1 \to i + 1 = j - 1 + 1$
147	146	fveq2d	$⊢ i = j - 1 \to Q (i + 1) = Q (j - 1 + 1)$
148	145 147	breq12d	$⊢ i = j - 1 \to (Q (i) < Q (i + 1) \leftrightarrow Q (j - 1) < Q (j - 1 + 1))$
149	144 148	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)))$
150	16	simprrd	$⊢ φ \to \forall i \in (0 ..^M) Q (i) < Q (i + 1)$
151	150	r19.21bi	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)$
152	142 149 151	vtocl	$⊢ (φ \land j - 1 \in (0 ..^M)) \to Q (j - 1) < Q (j - 1 + 1)$
153	141 102 152	syl2anc	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1) < Q (j - 1 + 1)$
154	113	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1 + 1) = Q (j)$
155	153 154	breqtrd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1) < Q (j)$
156		simp3	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j) = E (X)$
157	155 156	breqtrd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j - 1) < E (X)$
158	138	leidd	$⊢ φ \to E (X) \leq E (X)$
159	158	adantr	$⊢ (φ \land Q (j) = E (X)) \to E (X) \leq E (X)$
160	46	eqcomd	$⊢ (φ \land Q (j) = E (X)) \to E (X) = Q (j)$
161	159 160	breqtrd	$⊢ (φ \land Q (j) = E (X)) \to E (X) \leq Q (j)$
162	161	3adant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \leq Q (j)$
163	112	eqcomd	$⊢ j \in (0 \dots M) \to j = j - 1 + 1$
164	163	fveq2d	$⊢ j \in (0 \dots M) \to Q (j) = Q (j - 1 + 1)$
165	164	3ad2ant2	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j) = Q (j - 1 + 1)$
166	162 165	breqtrd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \leq Q (j - 1 + 1)$
167	109 118 140 157 166	eliocd	$⊢ (φ \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \in (Q (j - 1), Q (j - 1 + 1)]$
168	145 147	oveq12d	$⊢ i = j - 1 \to (Q (i), Q (i + 1)] = (Q (j - 1), Q (j - 1 + 1)]$
169	168	eleq2d	$⊢ i = j - 1 \to (E (X) \in (Q (i), Q (i + 1)] \leftrightarrow E (X) \in (Q (j - 1), Q (j - 1 + 1)])$
170	169	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)]$
171	102 167 170	syl2anc	$⊢ (φ \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)]$
172	171	3exp	$⊢ φ \to (j \in (0 \dots M) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]))$
173	172	adantr	$⊢ (φ \land E (X) \in ran Q) \to (j \in (0 \dots M) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]))$
174	173	rexlimdv	$⊢ (φ \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)])$
175	24 174	mpd	$⊢ (φ \land E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
176	10	adantr	$⊢ (φ \land \neg E (X) \in ran Q) \to M \in ℕ$
177	103	adantr	$⊢ (φ \land \neg E (X) \in ran Q) \to Q : (0 \dots M) ⟶ ℝ$
178		iocssicc	$⊢ (Q (0), Q (M)] \subseteq [Q (0), Q (M)]$
179	41	simprd	$⊢ φ \to Q (M) = B$
180	42 179	oveq12d	$⊢ φ \to (Q (0), Q (M)] = (A, B]$
181	77 180	eleqtrrd	$⊢ φ \to E (X) \in (Q (0), Q (M)]$
182	178 181	sselid	$⊢ φ \to E (X) \in [Q (0), Q (M)]$
183	182	adantr	$⊢ (φ \land \neg E (X) \in ran Q) \to E (X) \in [Q (0), Q (M)]$
184		simpr	$⊢ (φ \land \neg E (X) \in ran Q) \to \neg E (X) \in ran Q$
185		fveq2	$⊢ k = j \to Q (k) = Q (j)$
186	185	breq1d	$⊢ k = j \to (Q (k) < E (X) \leftrightarrow Q (j) < E (X))$
187	186	cbvrabv	$⊢ \{k \in (0 ..^M) \| Q (k) < E (X)\} = \{j \in (0 ..^M) \| Q (j) < E (X)\}$
188	187	supeq1i	$⊢ sup (\{k \in (0 ..^M) \| Q (k) < E (X)\} ℝ <) = sup (\{j \in (0 ..^M) \| Q (j) < E (X)\} ℝ <)$
189	176 177 183 184 188	fourierdlem25	$⊢ (φ \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1))$
190		ioossioc	$⊢ (Q (i), Q (i + 1)) \subseteq (Q (i), Q (i + 1)]$
191	190	a1i	$⊢ ((φ \land \neg E (X) \in ran Q) \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq (Q (i), Q (i + 1)]$
192	191	sseld	$⊢ ((φ \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)])$
193	192	reximdva	$⊢ (φ \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)])$
194	189 193	mpd	$⊢ (φ \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
195	175 194	pm2.61dan	$⊢ φ \to \exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)]$
196	103	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
197		elfzofz	$⊢ i \in (0 ..^M) \to i \in (0 \dots M)$
198	197	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i \in (0 \dots M)$
199	196 198	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ$
200	199	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) \in ℝ$
201	135	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Z (X) \in ℝ$
202	200 201	resubcld	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) - Z (X) \in ℝ$
203	138	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to E (X) \in ℝ$
204	200	rexrd	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) \in ℝ^{*}$
205		fzofzp1	$⊢ i \in (0 ..^M) \to i + 1 \in (0 \dots M)$
206	205	adantl	$⊢ (φ \land i \in (0 ..^M)) \to i + 1 \in (0 \dots M)$
207	196 206	ffvelrnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ$
208	207	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℝ^{*}$
209	208	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i + 1) \in ℝ^{*}$
210		simp3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to E (X) \in (Q (i), Q (i + 1)]$
211		iocgtlb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) < E (X)$
212	204 209 210 211	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) < E (X)$
213	200 203 201 212	ltsub1dd	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) - Z (X) < E (X) - Z (X)$
214	137	oveq1d	$⊢ φ \to E (X) - Z (X) = X + Z (X) - Z (X)$
215	6	recnd	$⊢ φ \to X \in ℂ$
216	135	recnd	$⊢ φ \to Z (X) \in ℂ$
217	215 216	pncand	$⊢ φ \to X + Z (X) - Z (X) = X$
218	214 217	eqtrd	$⊢ φ \to E (X) - Z (X) = X$
219	218	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to E (X) - Z (X) = X$
220	213 219	breqtrd	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to Q (i) - Z (X) < X$
221		elioore	$⊢ y \in (Q (i) - Z (X), X) \to y \in ℝ$
222	134	oveq2d	$⊢ φ \to y + Z (X) = y + ⌊\frac{B - X}{T}⌋ T$
223	132	recnd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ \in ℂ$
224	56	recnd	$⊢ φ \to T \in ℂ$
225	223 224	mulneg1d	$⊢ φ \to (- ⌊\frac{B - X}{T}⌋) T = - ⌊\frac{B - X}{T}⌋ T$
226	222 225	oveq12d	$⊢ φ \to y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T = y + ⌊\frac{B - X}{T}⌋ T + (- ⌊\frac{B - X}{T}⌋ T)$
227	226	adantr	$⊢ (φ \land y \in ℝ) \to y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T = y + ⌊\frac{B - X}{T}⌋ T + (- ⌊\frac{B - X}{T}⌋ T)$
228		simpr	$⊢ (φ \land y \in ℝ) \to y \in ℝ$
229	133	adantr	$⊢ (φ \land y \in ℝ) \to ⌊\frac{B - X}{T}⌋ T \in ℝ$
230	228 229	readdcld	$⊢ (φ \land y \in ℝ) \to y + ⌊\frac{B - X}{T}⌋ T \in ℝ$
231	230	recnd	$⊢ (φ \land y \in ℝ) \to y + ⌊\frac{B - X}{T}⌋ T \in ℂ$
232	229	recnd	$⊢ (φ \land y \in ℝ) \to ⌊\frac{B - X}{T}⌋ T \in ℂ$
233	231 232	negsubd	$⊢ (φ \land y \in ℝ) \to y + ⌊\frac{B - X}{T}⌋ T + (- ⌊\frac{B - X}{T}⌋ T) = y + ⌊\frac{B - X}{T}⌋ T - ⌊\frac{B - X}{T}⌋ T$
234	228	recnd	$⊢ (φ \land y \in ℝ) \to y \in ℂ$
235	234 232	pncand	$⊢ (φ \land y \in ℝ) \to y + ⌊\frac{B - X}{T}⌋ T - ⌊\frac{B - X}{T}⌋ T = y$
236	227 233 235	3eqtrrd	$⊢ (φ \land y \in ℝ) \to y = y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T$
237	221 236	sylan2	$⊢ (φ \land y \in (Q (i) - Z (X), X)) \to y = y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T$
238	237	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) + (- ⌊\frac{B - X}{T}⌋) T$
239		simpl1	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \land y \in (Q (i) - Z (X), X)) \to φ$
240	12	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to (Q (i), Q (i + 1)) \subseteq D$
241	240	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), Q (i + 1)) \subseteq D$
242	204	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) \in ℝ^{*}$
243	209	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 + 1) \in ℝ^{*}$
244	221	adantl	$⊢ (φ \land y \in (Q (i) - Z (X), X)) \to y \in ℝ$
245	135	adantr	$⊢ (φ \land y \in (Q (i) - Z (X), X)) \to Z (X) \in ℝ$
246	244 245	readdcld	$⊢ (φ \land y \in (Q (i) - Z (X), X)) \to y + Z (X) \in ℝ$
247	246	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) \in ℝ$
248	135	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Z (X) \in ℝ$
249	199 248	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - Z (X) \in ℝ$
250	249	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) - Z (X) \in ℝ^{*}$
251	250	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Q (i) - Z (X) \in ℝ^{*}$
252	6	rexrd	$⊢ φ \to X \in ℝ^{*}$
253	252	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to X \in ℝ^{*}$
254		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to y \in (Q (i) - Z (X), X)$
255		ioogtlb	$⊢ (Q (i) - Z (X) \in ℝ^{} \land X \in ℝ^{} \land y \in (Q (i) - Z (X), X)) \to Q (i) - Z (X) < y$
256	251 253 254 255	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Q (i) - Z (X) < y$
257	199	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Q (i) \in ℝ$
258	135	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Z (X) \in ℝ$
259	221	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to y \in ℝ$
260	257 258 259	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))$
261	256 260	mpbid	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Q (i) < y + Z (X)$
262	261	3adantl3	$⊢ ((φ \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) < y + Z (X)$
263	239 138	syl	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \land y \in (Q (i) - Z (X), X)) \to E (X) \in ℝ$
264	207	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to Q (i + 1) \in ℝ$
265	264	3adantl3	$⊢ ((φ \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 + 1) \in ℝ$
266	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to X \in ℝ$
267		iooltub	$⊢ (Q (i) - Z (X) \in ℝ^{} \land X \in ℝ^{} \land y \in (Q (i) - Z (X), X)) \to y < X$
268	251 253 254 267	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to y < X$
269	259 266 258 268	ltadd1dd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to y + Z (X) < X + Z (X)$
270	137	eqcomd	$⊢ φ \to X + Z (X) = E (X)$
271	270	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to X + Z (X) = E (X)$
272	269 271	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (Q (i) - Z (X), X)) \to y + Z (X) < E (X)$
273	272	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) < E (X)$
274		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)$
275	204 209 210 274	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to E (X) \leq Q (i + 1)$
276	275	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \land y \in (Q (i) - Z (X), X)) \to E (X) \leq Q (i + 1)$
277	247 263 265 273 276	ltletrd	$⊢ ((φ \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) < Q (i + 1)$
278	242 243 247 262 277	eliood	$⊢ ((φ \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), Q (i + 1))$
279	241 278	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$
280	239 130	syl	$⊢ ((φ \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 ℝ$
281	280	flcld	$⊢ ((φ \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 ℤ$
282	281	znegcld	$⊢ ((φ \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 ℤ$
283		negex	$⊢ - ⌊\frac{B - X}{T}⌋ \in V$
284		eleq1	$⊢ k = - ⌊\frac{B - X}{T}⌋ \to (k \in ℤ \leftrightarrow - ⌊\frac{B - X}{T}⌋ \in ℤ)$
285	284	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 ℤ))$
286		oveq1	$⊢ k = - ⌊\frac{B - X}{T}⌋ \to k T = (- ⌊\frac{B - X}{T}⌋) T$
287	286	oveq2d	$⊢ k = - ⌊\frac{B - X}{T}⌋ \to y + Z (X) + k T = y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T$
288	287	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)$
289	285 288	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))$
290		ovex	$⊢ y + Z (X) \in V$
291		eleq1	$⊢ x = y + Z (X) \to (x \in D \leftrightarrow y + Z (X) \in D)$
292	291	3anbi2d	$⊢ x = y + Z (X) \to ((φ \land x \in D \land k \in ℤ) \leftrightarrow (φ \land y + Z (X) \in D \land k \in ℤ))$
293		oveq1	$⊢ x = y + Z (X) \to x + k T = y + Z (X) + k T$
294	293	eleq1d	$⊢ x = y + Z (X) \to (x + k T \in D \leftrightarrow y + Z (X) + k T \in D)$
295	292 294	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))$
296	290 295 5	vtocl	$⊢ (φ \land y + Z (X) \in D \land k \in ℤ) \to y + Z (X) + k T \in D$
297	283 289 296	vtocl	$⊢ (φ \land y + Z (X) \in D \land - ⌊\frac{B - X}{T}⌋ \in ℤ) \to y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T \in D$
298	239 279 282 297	syl3anc	$⊢ ((φ \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$
299	238 298	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$
300	299	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$
301		dfss3	$⊢ (Q (i) - Z (X), X) \subseteq D \leftrightarrow \forall y \in (Q (i) - Z (X), X) y \in D$
302	300 301	sylibr	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to (Q (i) - Z (X), X) \subseteq D$
303		breq1	$⊢ y = Q (i) - Z (X) \to (y < X \leftrightarrow Q (i) - Z (X) < X)$
304		oveq1	$⊢ y = Q (i) - Z (X) \to (y, X) = (Q (i) - Z (X), X)$
305	304	sseq1d	$⊢ y = Q (i) - Z (X) \to ((y, X) \subseteq D \leftrightarrow (Q (i) - Z (X), X) \subseteq D)$
306	303 305	anbi12d	$⊢ y = Q (i) - Z (X) \to ((y < X \land (y, X) \subseteq D) \leftrightarrow (Q (i) - Z (X) < X \land (Q (i) - Z (X), X) \subseteq D))$
307	306	rspcev	$⊢ (Q (i) - Z (X) \in ℝ \land (Q (i) - Z (X) < X \land (Q (i) - Z (X), X) \subseteq D)) \to \exists y \in ℝ (y < X \land (y, X) \subseteq D)$
308	202 220 302 307	syl12anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in (Q (i), Q (i + 1)]) \to \exists y \in ℝ (y < X \land (y, X) \subseteq D)$
309	308	3exp	$⊢ φ \to (i \in (0 ..^M) \to (E (X) \in (Q (i), Q (i + 1)] \to \exists y \in ℝ (y < X \land (y, X) \subseteq D)))$
310	309	rexlimdv	$⊢ φ \to (\exists i \in (0 ..^M) E (X) \in (Q (i), Q (i + 1)] \to \exists y \in ℝ (y < X \land (y, X) \subseteq D))$
311	195 310	mpd	$⊢ φ \to \exists y \in ℝ (y < X \land (y, X) \subseteq D)$
312		0zd	$⊢ φ \to 0 \in ℤ$
313	10	nnzd	$⊢ φ \to M \in ℤ$
314		1zzd	$⊢ φ \to 1 \in ℤ$
315		0le1	$⊢ 0 \leq 1$
316	315	a1i	$⊢ φ \to 0 \leq 1$
317	10	nnge1d	$⊢ φ \to 1 \leq M$
318	312 313 314 316 317	elfzd	$⊢ φ \to 1 \in (0 \dots M)$
319	103 318	ffvelrnd	$⊢ φ \to Q (1) \in ℝ$
320	135 56	resubcld	$⊢ φ \to Z (X) - T \in ℝ$
321	319 320	resubcld	$⊢ φ \to Q (1) - (Z (X) - T) \in ℝ$
322	321	adantr	$⊢ (φ \land E (X) = B) \to Q (1) - (Z (X) - T) \in ℝ$
323	1	recnd	$⊢ φ \to A \in ℂ$
324	323 224	pncand	$⊢ φ \to A + T - T = A$
325	324	adantr	$⊢ (φ \land E (X) = B) \to A + T - T = A$
326	4	oveq2i	$⊢ A + T = A + B - A$
327	326	a1i	$⊢ (φ \land E (X) = B) \to A + T = A + B - A$
328	2	recnd	$⊢ φ \to B \in ℂ$
329	323 328	pncan3d	$⊢ φ \to A + B - A = B$
330	329	adantr	$⊢ (φ \land E (X) = B) \to A + B - A = B$
331		id	$⊢ E (X) = B \to E (X) = B$
332	331	eqcomd	$⊢ E (X) = B \to B = E (X)$
333	332	adantl	$⊢ (φ \land E (X) = B) \to B = E (X)$
334	327 330 333	3eqtrrd	$⊢ (φ \land E (X) = B) \to E (X) = A + T$
335	334	oveq1d	$⊢ (φ \land E (X) = B) \to E (X) - T = A + T - T$
336	42	adantr	$⊢ (φ \land E (X) = B) \to Q (0) = A$
337	325 335 336	3eqtr4rd	$⊢ (φ \land E (X) = B) \to Q (0) = E (X) - T$
338	337	oveq1d	$⊢ (φ \land E (X) = B) \to Q (0) - (Z (X) - T) = E (X) - T - (Z (X) - T)$
339	138	recnd	$⊢ φ \to E (X) \in ℂ$
340	339 216 224	nnncan2d	$⊢ φ \to E (X) - T - (Z (X) - T) = E (X) - Z (X)$
341	340	adantr	$⊢ (φ \land E (X) = B) \to E (X) - T - (Z (X) - T) = E (X) - Z (X)$
342	218	adantr	$⊢ (φ \land E (X) = B) \to E (X) - Z (X) = X$
343	338 341 342	3eqtrrd	$⊢ (φ \land E (X) = B) \to X = Q (0) - (Z (X) - T)$
344	42 1	eqeltrd	$⊢ φ \to Q (0) \in ℝ$
345	10	nngt0d	$⊢ φ \to 0 < M$
346		fzolb	$⊢ 0 \in (0 ..^M) \leftrightarrow (0 \in ℤ \land M \in ℤ \land 0 < M)$
347	312 313 345 346	syl3anbrc	$⊢ φ \to 0 \in (0 ..^M)$
348		0re	$⊢ 0 \in ℝ$
349		eleq1	$⊢ i = 0 \to (i \in (0 ..^M) \leftrightarrow 0 \in (0 ..^M))$
350	349	anbi2d	$⊢ i = 0 \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land 0 \in (0 ..^M)))$
351		fveq2	$⊢ i = 0 \to Q (i) = Q (0)$
352		oveq1	$⊢ i = 0 \to i + 1 = 0 + 1$
353	352	fveq2d	$⊢ i = 0 \to Q (i + 1) = Q (0 + 1)$
354	351 353	breq12d	$⊢ i = 0 \to (Q (i) < Q (i + 1) \leftrightarrow Q (0) < Q (0 + 1))$
355	350 354	imbi12d	$⊢ i = 0 \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)))$
356	355 151	vtoclg	$⊢ 0 \in ℝ \to ((φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1))$
357	348 356	ax-mp	$⊢ (φ \land 0 \in (0 ..^M)) \to Q (0) < Q (0 + 1)$
358	347 357	mpdan	$⊢ φ \to Q (0) < Q (0 + 1)$
359		0p1e1	$⊢ 0 + 1 = 1$
360	359	fveq2i	$⊢ Q (0 + 1) = Q (1)$
361	360	a1i	$⊢ φ \to Q (0 + 1) = Q (1)$
362	358 361	breqtrd	$⊢ φ \to Q (0) < Q (1)$
363	344 319 320 362	ltsub1dd	$⊢ φ \to Q (0) - (Z (X) - T) < Q (1) - (Z (X) - T)$
364	363	adantr	$⊢ (φ \land E (X) = B) \to Q (0) - (Z (X) - T) < Q (1) - (Z (X) - T)$
365	343 364	eqbrtrd	$⊢ (φ \land E (X) = B) \to X < Q (1) - (Z (X) - T)$
366		elioore	$⊢ y \in (X, Q (1) - (Z (X) - T)) \to y \in ℝ$
367	134	eqcomd	$⊢ φ \to ⌊\frac{B - X}{T}⌋ T = Z (X)$
368	367	negeqd	$⊢ φ \to - ⌊\frac{B - X}{T}⌋ T = - Z (X)$
369	225 368	eqtrd	$⊢ φ \to (- ⌊\frac{B - X}{T}⌋) T = - Z (X)$
370	224	mulid2d	$⊢ φ \to 1 T = T$
371	369 370	oveq12d	$⊢ φ \to (- ⌊\frac{B - X}{T}⌋) T + 1 T = - Z (X) + T$
372	223	negcld	$⊢ φ \to - ⌊\frac{B - X}{T}⌋ \in ℂ$
373		1cnd	$⊢ φ \to 1 \in ℂ$
374	372 373 224	adddird	$⊢ φ \to (- ⌊\frac{B - X}{T}⌋ + 1) T = (- ⌊\frac{B - X}{T}⌋) T + 1 T$
375	216 224	negsubdid	$⊢ φ \to - (Z (X) - T) = - Z (X) + T$
376	371 374 375	3eqtr4d	$⊢ φ \to (- ⌊\frac{B - X}{T}⌋ + 1) T = - (Z (X) - T)$
377	376	oveq2d	$⊢ φ \to y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T = y + (Z (X) - T) + (- (Z (X) - T))$
378	377	adantr	$⊢ (φ \land y \in ℝ) \to y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T = y + (Z (X) - T) + (- (Z (X) - T))$
379	320	adantr	$⊢ (φ \land y \in ℝ) \to Z (X) - T \in ℝ$
380	228 379	readdcld	$⊢ (φ \land y \in ℝ) \to y + Z (X) - T \in ℝ$
381	380	recnd	$⊢ (φ \land y \in ℝ) \to y + Z (X) - T \in ℂ$
382	379	recnd	$⊢ (φ \land y \in ℝ) \to Z (X) - T \in ℂ$
383	381 382	negsubd	$⊢ (φ \land y \in ℝ) \to y + (Z (X) - T) + (- (Z (X) - T)) = y + (Z (X) - T) - (Z (X) - T)$
384	234 382	pncand	$⊢ (φ \land y \in ℝ) \to y + (Z (X) - T) - (Z (X) - T) = y$
385	378 383 384	3eqtrrd	$⊢ (φ \land y \in ℝ) \to y = y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T$
386	366 385	sylan2	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y = y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T$
387	386	adantlr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y = y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T$
388		simpll	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to φ$
389	361	eqcomd	$⊢ φ \to Q (1) = Q (0 + 1)$
390	389	oveq2d	$⊢ φ \to (Q (0), Q (1)) = (Q (0), Q (0 + 1))$
391	351 353	oveq12d	$⊢ i = 0 \to (Q (i), Q (i + 1)) = (Q (0), Q (0 + 1))$
392	391	sseq1d	$⊢ i = 0 \to ((Q (i), Q (i + 1)) \subseteq D \leftrightarrow (Q (0), Q (0 + 1)) \subseteq D)$
393	350 392	imbi12d	$⊢ i = 0 \to (((φ \land i \in (0 ..^M)) \to (Q (i), Q (i + 1)) \subseteq D) \leftrightarrow ((φ \land 0 \in (0 ..^M)) \to (Q (0), Q (0 + 1)) \subseteq D))$
394	393 12	vtoclg	$⊢ 0 \in ℝ \to ((φ \land 0 \in (0 ..^M)) \to (Q (0), Q (0 + 1)) \subseteq D)$
395	348 394	ax-mp	$⊢ (φ \land 0 \in (0 ..^M)) \to (Q (0), Q (0 + 1)) \subseteq D$
396	347 395	mpdan	$⊢ φ \to (Q (0), Q (0 + 1)) \subseteq D$
397	390 396	eqsstrd	$⊢ φ \to (Q (0), Q (1)) \subseteq D$
398	397	ad2antrr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to (Q (0), Q (1)) \subseteq D$
399	42 47	eqeltrd	$⊢ φ \to Q (0) \in ℝ^{*}$
400	399	ad2antrr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to Q (0) \in ℝ^{*}$
401	319	rexrd	$⊢ φ \to Q (1) \in ℝ^{*}$
402	401	ad2antrr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to Q (1) \in ℝ^{*}$
403	366 380	sylan2	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T \in ℝ$
404	403	adantlr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T \in ℝ$
405	339 215 216	subaddd	$⊢ φ \to (E (X) - X = Z (X) \leftrightarrow X + Z (X) = E (X))$
406	270 405	mpbird	$⊢ φ \to E (X) - X = Z (X)$
407		oveq1	$⊢ E (X) = B \to E (X) - X = B - X$
408	406 407	sylan9req	$⊢ (φ \land E (X) = B) \to Z (X) = B - X$
409	408	oveq1d	$⊢ (φ \land E (X) = B) \to Z (X) - T = B - X - T$
410	409	oveq2d	$⊢ (φ \land E (X) = B) \to X + Z (X) - T = X + (B - X) - T$
411	129	recnd	$⊢ φ \to B - X \in ℂ$
412	215 411 224	addsubassd	$⊢ φ \to X + (B - X) - T = X + (B - X) - T$
413	412	eqcomd	$⊢ φ \to X + (B - X) - T = X + (B - X) - T$
414	413	adantr	$⊢ (φ \land E (X) = B) \to X + (B - X) - T = X + (B - X) - T$
415	328 224 323	subsub23d	$⊢ φ \to (B - T = A \leftrightarrow B - A = T)$
416	62 415	mpbird	$⊢ φ \to B - T = A$
417	215 328	pncan3d	$⊢ φ \to X + B - X = B$
418	417	oveq1d	$⊢ φ \to X + (B - X) - T = B - T$
419	416 418 42	3eqtr4d	$⊢ φ \to X + (B - X) - T = Q (0)$
420	419	adantr	$⊢ (φ \land E (X) = B) \to X + (B - X) - T = Q (0)$
421	410 414 420	3eqtrrd	$⊢ (φ \land E (X) = B) \to Q (0) = X + Z (X) - T$
422	421	adantr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to Q (0) = X + Z (X) - T$
423	6	adantr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to X \in ℝ$
424	366	adantl	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y \in ℝ$
425	320	adantr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to Z (X) - T \in ℝ$
426	252	adantr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to X \in ℝ^{*}$
427	321	rexrd	$⊢ φ \to Q (1) - (Z (X) - T) \in ℝ^{*}$
428	427	adantr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to Q (1) - (Z (X) - T) \in ℝ^{*}$
429		simpr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y \in (X, Q (1) - (Z (X) - T))$
430		ioogtlb	$⊢ (X \in ℝ^{} \land Q (1) - (Z (X) - T) \in ℝ^{} \land y \in (X, Q (1) - (Z (X) - T))) \to X < y$
431	426 428 429 430	syl3anc	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to X < y$
432	423 424 425 431	ltadd1dd	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to X + Z (X) - T < y + Z (X) - T$
433	432	adantlr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to X + Z (X) - T < y + Z (X) - T$
434	422 433	eqbrtrd	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to Q (0) < y + Z (X) - T$
435		iooltub	$⊢ (X \in ℝ^{} \land Q (1) - (Z (X) - T) \in ℝ^{} \land y \in (X, Q (1) - (Z (X) - T))) \to y < Q (1) - (Z (X) - T)$
436	426 428 429 435	syl3anc	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y < Q (1) - (Z (X) - T)$
437	319	adantr	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to Q (1) \in ℝ$
438	424 425 437	ltaddsubd	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to (y + Z (X) - T < Q (1) \leftrightarrow y < Q (1) - (Z (X) - T))$
439	436 438	mpbird	$⊢ (φ \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T < Q (1)$
440	439	adantlr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T < Q (1)$
441	400 402 404 434 440	eliood	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T \in (Q (0), Q (1))$
442	398 441	sseldd	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y + Z (X) - T \in D$
443	131	znegcld	$⊢ φ \to - ⌊\frac{B - X}{T}⌋ \in ℤ$
444	443	peano2zd	$⊢ φ \to - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ$
445	444	ad2antrr	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ$
446		ovex	$⊢ - ⌊\frac{B - X}{T}⌋ + 1 \in V$
447		eleq1	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to (k \in ℤ \leftrightarrow - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ)$
448	447	3anbi3d	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to ((φ \land y + Z (X) - T \in D \land k \in ℤ) \leftrightarrow (φ \land y + Z (X) - T \in D \land - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ))$
449		oveq1	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to k T = (- ⌊\frac{B - X}{T}⌋ + 1) T$
450	449	oveq2d	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to y + (Z (X) - T) + k T = y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T$
451	450	eleq1d	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to (y + (Z (X) - T) + k T \in D \leftrightarrow y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T \in D)$
452	448 451	imbi12d	$⊢ k = - ⌊\frac{B - X}{T}⌋ + 1 \to (((φ \land y + Z (X) - T \in D \land k \in ℤ) \to y + (Z (X) - T) + k T \in D) \leftrightarrow ((φ \land y + Z (X) - T \in D \land - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ) \to y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T \in D))$
453		ovex	$⊢ y + Z (X) - T \in V$
454		eleq1	$⊢ x = y + Z (X) - T \to (x \in D \leftrightarrow y + Z (X) - T \in D)$
455	454	3anbi2d	$⊢ x = y + Z (X) - T \to ((φ \land x \in D \land k \in ℤ) \leftrightarrow (φ \land y + Z (X) - T \in D \land k \in ℤ))$
456		oveq1	$⊢ x = y + Z (X) - T \to x + k T = y + (Z (X) - T) + k T$
457	456	eleq1d	$⊢ x = y + Z (X) - T \to (x + k T \in D \leftrightarrow y + (Z (X) - T) + k T \in D)$
458	455 457	imbi12d	$⊢ x = y + Z (X) - T \to (((φ \land x \in D \land k \in ℤ) \to x + k T \in D) \leftrightarrow ((φ \land y + Z (X) - T \in D \land k \in ℤ) \to y + (Z (X) - T) + k T \in D))$
459	453 458 5	vtocl	$⊢ (φ \land y + Z (X) - T \in D \land k \in ℤ) \to y + (Z (X) - T) + k T \in D$
460	446 452 459	vtocl	$⊢ (φ \land y + Z (X) - T \in D \land - ⌊\frac{B - X}{T}⌋ + 1 \in ℤ) \to y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T \in D$
461	388 442 445 460	syl3anc	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y + (Z (X) - T) + (- ⌊\frac{B - X}{T}⌋ + 1) T \in D$
462	387 461	eqeltrd	$⊢ ((φ \land E (X) = B) \land y \in (X, Q (1) - (Z (X) - T))) \to y \in D$
463	462	ralrimiva	$⊢ (φ \land E (X) = B) \to \forall y \in (X, Q (1) - (Z (X) - T)) y \in D$
464		dfss3	$⊢ (X, Q (1) - (Z (X) - T)) \subseteq D \leftrightarrow \forall y \in (X, Q (1) - (Z (X) - T)) y \in D$
465	463 464	sylibr	$⊢ (φ \land E (X) = B) \to (X, Q (1) - (Z (X) - T)) \subseteq D$
466		breq2	$⊢ y = Q (1) - (Z (X) - T) \to (X < y \leftrightarrow X < Q (1) - (Z (X) - T))$
467		oveq2	$⊢ y = Q (1) - (Z (X) - T) \to (X, y) = (X, Q (1) - (Z (X) - T))$
468	467	sseq1d	$⊢ y = Q (1) - (Z (X) - T) \to ((X, y) \subseteq D \leftrightarrow (X, Q (1) - (Z (X) - T)) \subseteq D)$
469	466 468	anbi12d	$⊢ y = Q (1) - (Z (X) - T) \to ((X < y \land (X, y) \subseteq D) \leftrightarrow (X < Q (1) - (Z (X) - T) \land (X, Q (1) - (Z (X) - T)) \subseteq D))$
470	469	rspcev	$⊢ (Q (1) - (Z (X) - T) \in ℝ \land (X < Q (1) - (Z (X) - T) \land (X, Q (1) - (Z (X) - T)) \subseteq D)) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
471	322 365 465 470	syl12anc	$⊢ (φ \land E (X) = B) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
472	24	adantlr	$⊢ ((φ \land E (X) \neq B) \land E (X) \in ran Q) \to \exists j \in (0 \dots M) Q (j) = E (X)$
473		simp2	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to j \in (0 \dots M)$
474	34	3ad2ant2	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to j \in ℝ$
475	96	3ad2ant2	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to M \in ℝ$
476	98	3ad2ant2	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to j \leq M$
477		id	$⊢ Q (j) = E (X) \to Q (j) = E (X)$
478	477	eqcomd	$⊢ Q (j) = E (X) \to E (X) = Q (j)$
479	478	adantr	$⊢ (Q (j) = E (X) \land M = j) \to E (X) = Q (j)$
480	479	3ad2antl3	$⊢ (((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \land M = j) \to E (X) = Q (j)$
481		fveq2	$⊢ M = j \to Q (M) = Q (j)$
482	481	eqcomd	$⊢ M = j \to Q (j) = Q (M)$
483	482	adantl	$⊢ (((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \land M = j) \to Q (j) = Q (M)$
484	179	ad2antrr	$⊢ ((φ \land E (X) \neq B) \land M = j) \to Q (M) = B$
485	484	3ad2antl1	$⊢ (((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \land M = j) \to Q (M) = B$
486	480 483 485	3eqtrd	$⊢ (((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \land M = j) \to E (X) = B$
487		neneq	$⊢ E (X) \neq B \to \neg E (X) = B$
488	487	ad2antlr	$⊢ ((φ \land E (X) \neq B) \land M = j) \to \neg E (X) = B$
489	488	3ad2antl1	$⊢ (((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \land M = j) \to \neg E (X) = B$
490	486 489	pm2.65da	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to \neg M = j$
491	490	neqned	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to M \neq j$
492	474 475 476 491	leneltd	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to j < M$
493		elfzfzo	$⊢ j \in (0 ..^M) \leftrightarrow (j \in (0 \dots M) \land j < M)$
494	473 492 493	sylanbrc	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to j \in (0 ..^M)$
495	116	adantlr	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M)) \to Q (j) \in ℝ^{*}$
496	495	3adant3	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j) \in ℝ^{*}$
497		simp1l	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to φ$
498	103	adantr	$⊢ (φ \land j \in (0 ..^M)) \to Q : (0 \dots M) ⟶ ℝ$
499		fzofzp1	$⊢ j \in (0 ..^M) \to j + 1 \in (0 \dots M)$
500	499	adantl	$⊢ (φ \land j \in (0 ..^M)) \to j + 1 \in (0 \dots M)$
501	498 500	ffvelrnd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ$
502	501	rexrd	$⊢ (φ \land j \in (0 ..^M)) \to Q (j + 1) \in ℝ^{*}$
503	497 494 502	syl2anc	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j + 1) \in ℝ^{*}$
504	140	3adant1r	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \in ℝ^{*}$
505	46 159	eqbrtrd	$⊢ (φ \land Q (j) = E (X)) \to Q (j) \leq E (X)$
506	505	adantlr	$⊢ ((φ \land E (X) \neq B) \land Q (j) = E (X)) \to Q (j) \leq E (X)$
507	506	3adant2	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j) \leq E (X)$
508	478	3ad2ant3	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) = Q (j)$
509		eleq1	$⊢ i = j \to (i \in (0 ..^M) \leftrightarrow j \in (0 ..^M))$
510	509	anbi2d	$⊢ i = j \to ((φ \land i \in (0 ..^M)) \leftrightarrow (φ \land j \in (0 ..^M)))$
511		fveq2	$⊢ i = j \to Q (i) = Q (j)$
512		oveq1	$⊢ i = j \to i + 1 = j + 1$
513	512	fveq2d	$⊢ i = j \to Q (i + 1) = Q (j + 1)$
514	511 513	breq12d	$⊢ i = j \to (Q (i) < Q (i + 1) \leftrightarrow Q (j) < Q (j + 1))$
515	510 514	imbi12d	$⊢ i = j \to (((φ \land i \in (0 ..^M)) \to Q (i) < Q (i + 1)) \leftrightarrow ((φ \land j \in (0 ..^M)) \to Q (j) < Q (j + 1)))$
516	515 151	chvarvv	$⊢ (φ \land j \in (0 ..^M)) \to Q (j) < Q (j + 1)$
517	497 494 516	syl2anc	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to Q (j) < Q (j + 1)$
518	508 517	eqbrtrd	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) < Q (j + 1)$
519	496 503 504 507 518	elicod	$⊢ ((φ \land E (X) \neq B) \land j \in (0 \dots M) \land Q (j) = E (X)) \to E (X) \in [Q (j), Q (j + 1))$
520	511 513	oveq12d	$⊢ i = j \to [Q (i), Q (i + 1)) = [Q (j), Q (j + 1))$
521	520	eleq2d	$⊢ i = j \to (E (X) \in [Q (i), Q (i + 1)) \leftrightarrow E (X) \in [Q (j), Q (j + 1)))$
522	521	rspcev	$⊢ (j \in (0 ..^M) \land E (X) \in [Q (j), Q (j + 1))) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
523	494 519 522	syl2anc	$⊢ ((φ \land E (X) \neq 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))$
524	523	3exp	$⊢ (φ \land E (X) \neq B) \to (j \in (0 \dots M) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))))$
525	524	adantr	$⊢ ((φ \land E (X) \neq B) \land E (X) \in ran Q) \to (j \in (0 \dots M) \to (Q (j) = E (X) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))))$
526	525	rexlimdv	$⊢ ((φ \land E (X) \neq 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)))$
527	472 526	mpd	$⊢ ((φ \land E (X) \neq B) \land E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
528		ioossico	$⊢ (Q (i), Q (i + 1)) \subseteq [Q (i), Q (i + 1))$
529		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land E (X) \in (Q (i), Q (i + 1))) \to E (X) \in (Q (i), Q (i + 1))$
530	528 529	sselid	$⊢ ((φ \land i \in (0 ..^M)) \land E (X) \in (Q (i), Q (i + 1))) \to E (X) \in [Q (i), Q (i + 1))$
531	530	ex	$⊢ (φ \land i \in (0 ..^M)) \to (E (X) \in (Q (i), Q (i + 1)) \to E (X) \in [Q (i), Q (i + 1)))$
532	531	adantlr	$⊢ ((φ \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)))$
533	532	reximdva	$⊢ (φ \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)))$
534	189 533	mpd	$⊢ (φ \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
535	534	adantlr	$⊢ ((φ \land E (X) \neq B) \land \neg E (X) \in ran Q) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
536	527 535	pm2.61dan	$⊢ (φ \land E (X) \neq B) \to \exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1))$
537	207 248	resubcld	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - Z (X) \in ℝ$
538	537	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i + 1) - Z (X) \in ℝ$
539	218	eqcomd	$⊢ φ \to X = E (X) - Z (X)$
540	539	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to X = E (X) - Z (X)$
541	138	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to E (X) \in ℝ$
542	207	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ$
543	135	3ad2ant1	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Z (X) \in ℝ$
544	199	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i) \in ℝ^{*}$
545	544	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i) \in ℝ^{*}$
546	208	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i + 1) \in ℝ^{*}$
547		simp3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to E (X) \in [Q (i), Q (i + 1))$
548		icoltub	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land E (X) \in [Q (i), Q (i + 1))) \to E (X) < Q (i + 1)$
549	545 546 547 548	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to E (X) < Q (i + 1)$
550	541 542 543 549	ltsub1dd	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to E (X) - Z (X) < Q (i + 1) - Z (X)$
551	540 550	eqbrtrd	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to X < Q (i + 1) - Z (X)$
552		elioore	$⊢ y \in (X, Q (i + 1) - Z (X)) \to y \in ℝ$
553	552 236	sylan2	$⊢ (φ \land y \in (X, Q (i + 1) - Z (X))) \to y = y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T$
554	553	3ad2antl1	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y = y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T$
555		simpl1	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to φ$
556	12	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to (Q (i), Q (i + 1)) \subseteq D$
557	556	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to (Q (i), Q (i + 1)) \subseteq D$
558	545	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i) \in ℝ^{*}$
559	546	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i + 1) \in ℝ^{*}$
560	552	adantl	$⊢ (φ \land y \in (X, Q (i + 1) - Z (X))) \to y \in ℝ$
561	135	adantr	$⊢ (φ \land y \in (X, Q (i + 1) - Z (X))) \to Z (X) \in ℝ$
562	560 561	readdcld	$⊢ (φ \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) \in ℝ$
563	562	3ad2antl1	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) \in ℝ$
564	199	3adant3	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i) \in ℝ$
565	564	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i) \in ℝ$
566	555 138	syl	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to E (X) \in ℝ$
567		icogelb	$⊢ (Q (i) \in ℝ^{} \land Q (i + 1) \in ℝ^{} \land E (X) \in [Q (i), Q (i + 1))) \to Q (i) \leq E (X)$
568	545 546 547 567	syl3anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to Q (i) \leq E (X)$
569	568	adantr	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i) \leq E (X)$
570	137	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to E (X) = X + Z (X)$
571	6	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to X \in ℝ$
572	552	adantl	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to y \in ℝ$
573	135	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to Z (X) \in ℝ$
574	252	ad2antrr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to X \in ℝ^{*}$
575	537	rexrd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - Z (X) \in ℝ^{*}$
576	575	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i + 1) - Z (X) \in ℝ^{*}$
577		simpr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to y \in (X, Q (i + 1) - Z (X))$
578		ioogtlb	$⊢ (X \in ℝ^{} \land Q (i + 1) - Z (X) \in ℝ^{} \land y \in (X, Q (i + 1) - Z (X))) \to X < y$
579	574 576 577 578	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to X < y$
580	571 572 573 579	ltadd1dd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to X + Z (X) < y + Z (X)$
581	570 580	eqbrtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to E (X) < y + Z (X)$
582	581	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to E (X) < y + Z (X)$
583	565 566 563 569 582	lelttrd	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i) < y + Z (X)$
584	537	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i + 1) - Z (X) \in ℝ$
585		iooltub	$⊢ (X \in ℝ^{} \land Q (i + 1) - Z (X) \in ℝ^{} \land y \in (X, Q (i + 1) - Z (X))) \to y < Q (i + 1) - Z (X)$
586	574 576 577 585	syl3anc	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to y < Q (i + 1) - Z (X)$
587	572 584 573 586	ltadd1dd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) < Q (i + 1) - Z (X) + Z (X)$
588	207	recnd	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) \in ℂ$
589	216	adantr	$⊢ (φ \land i \in (0 ..^M)) \to Z (X) \in ℂ$
590	588 589	npcand	$⊢ (φ \land i \in (0 ..^M)) \to Q (i + 1) - Z (X) + Z (X) = Q (i + 1)$
591	590	adantr	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to Q (i + 1) - Z (X) + Z (X) = Q (i + 1)$
592	587 591	breqtrd	$⊢ ((φ \land i \in (0 ..^M)) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) < Q (i + 1)$
593	592	3adantl3	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) < Q (i + 1)$
594	558 559 563 583 593	eliood	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) \in (Q (i), Q (i + 1))$
595	557 594	sseldd	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) \in D$
596	555 443	syl	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to - ⌊\frac{B - X}{T}⌋ \in ℤ$
597	555 595 596 297	syl3anc	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y + Z (X) + (- ⌊\frac{B - X}{T}⌋) T \in D$
598	554 597	eqeltrd	$⊢ ((φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \land y \in (X, Q (i + 1) - Z (X))) \to y \in D$
599	598	ralrimiva	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to \forall y \in (X, Q (i + 1) - Z (X)) y \in D$
600		dfss3	$⊢ (X, Q (i + 1) - Z (X)) \subseteq D \leftrightarrow \forall y \in (X, Q (i + 1) - Z (X)) y \in D$
601	599 600	sylibr	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to (X, Q (i + 1) - Z (X)) \subseteq D$
602		breq2	$⊢ y = Q (i + 1) - Z (X) \to (X < y \leftrightarrow X < Q (i + 1) - Z (X))$
603		oveq2	$⊢ y = Q (i + 1) - Z (X) \to (X, y) = (X, Q (i + 1) - Z (X))$
604	603	sseq1d	$⊢ y = Q (i + 1) - Z (X) \to ((X, y) \subseteq D \leftrightarrow (X, Q (i + 1) - Z (X)) \subseteq D)$
605	602 604	anbi12d	$⊢ y = Q (i + 1) - Z (X) \to ((X < y \land (X, y) \subseteq D) \leftrightarrow (X < Q (i + 1) - Z (X) \land (X, Q (i + 1) - Z (X)) \subseteq D))$
606	605	rspcev	$⊢ (Q (i + 1) - Z (X) \in ℝ \land (X < Q (i + 1) - Z (X) \land (X, Q (i + 1) - Z (X)) \subseteq D)) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
607	538 551 601 606	syl12anc	$⊢ (φ \land i \in (0 ..^M) \land E (X) \in [Q (i), Q (i + 1))) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
608	607	3exp	$⊢ φ \to (i \in (0 ..^M) \to (E (X) \in [Q (i), Q (i + 1)) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)))$
609	608	adantr	$⊢ (φ \land E (X) \neq B) \to (i \in (0 ..^M) \to (E (X) \in [Q (i), Q (i + 1)) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)))$
610	609	rexlimdv	$⊢ (φ \land E (X) \neq B) \to (\exists i \in (0 ..^M) E (X) \in [Q (i), Q (i + 1)) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D))$
611	536 610	mpd	$⊢ (φ \land E (X) \neq B) \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
612	471 611	pm2.61dane	$⊢ φ \to \exists y \in ℝ (X < y \land (X, y) \subseteq D)$
613	311 612	jca	$⊢ φ \to (\exists y \in ℝ (y < X \land (y, X) \subseteq D) \land \exists y \in ℝ (X < y \land (X, y) \subseteq D))$

Metamath Proof Explorer

Theorem fourierdlem41

Proof