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