fourierdlem42

Description: The set of points in a moved partition are finite. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 29-Sep-2020)

	Ref	Expression
Hypotheses	fourierdlem42.b	$⊢ φ \to B \in ℝ$
	fourierdlem42.c	$⊢ φ \to C \in ℝ$
	fourierdlem42.bc	$⊢ φ \to B < C$
	fourierdlem42.t	$⊢ T = C - B$
	fourierdlem42.a	$⊢ φ \to A \subseteq [B, C]$
	fourierdlem42.af	$⊢ φ \to A \in Fin$
	fourierdlem42.ba	$⊢ φ \to B \in A$
	fourierdlem42.ca	$⊢ φ \to C \in A$
	fourierdlem42.d	$⊢ D = abs \circ -$
	fourierdlem42.i	$⊢ I = (A \times A) ∖ I$
	fourierdlem42.r	$⊢ R = ran ({D ↾}_{I})$
	fourierdlem42.e	$⊢ E = sup (R ℝ <)$
	fourierdlem42.x	$⊢ φ \to X \in ℝ$
	fourierdlem42.y	$⊢ φ \to Y \in ℝ$
	fourierdlem42.j	$⊢ J = topGen (ran (.))$
	fourierdlem42.k	$⊢ K = J ↾_{𝑡} [X, Y]$
	fourierdlem42.h	$⊢ H = \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\}$
	fourierdlem42.15	$⊢ ψ \leftrightarrow ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A))$
Assertion	fourierdlem42	$⊢ φ \to H \in Fin$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem42.b	$⊢ φ \to B \in ℝ$
2		fourierdlem42.c	$⊢ φ \to C \in ℝ$
3		fourierdlem42.bc	$⊢ φ \to B < C$
4		fourierdlem42.t	$⊢ T = C - B$
5		fourierdlem42.a	$⊢ φ \to A \subseteq [B, C]$
6		fourierdlem42.af	$⊢ φ \to A \in Fin$
7		fourierdlem42.ba	$⊢ φ \to B \in A$
8		fourierdlem42.ca	$⊢ φ \to C \in A$
9		fourierdlem42.d	$⊢ D = abs \circ -$
10		fourierdlem42.i	$⊢ I = (A \times A) ∖ I$
11		fourierdlem42.r	$⊢ R = ran ({D ↾}_{I})$
12		fourierdlem42.e	$⊢ E = sup (R ℝ <)$
13		fourierdlem42.x	$⊢ φ \to X \in ℝ$
14		fourierdlem42.y	$⊢ φ \to Y \in ℝ$
15		fourierdlem42.j	$⊢ J = topGen (ran (.))$
16		fourierdlem42.k	$⊢ K = J ↾_{𝑡} [X, Y]$
17		fourierdlem42.h	$⊢ H = \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\}$
18		fourierdlem42.15	$⊢ ψ \leftrightarrow ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A))$
19	15 16	icccmp	$⊢ (X \in ℝ \land Y \in ℝ) \to K \in Comp$
20	13 14 19	syl2anc	$⊢ φ \to K \in Comp$
21	20	adantr	$⊢ (φ \land \neg H \in Fin) \to K \in Comp$
22		ssrab2	$⊢ \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\} \subseteq [X, Y]$
23	22	a1i	$⊢ φ \to \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\} \subseteq [X, Y]$
24	17 23	eqsstrid	$⊢ φ \to H \subseteq [X, Y]$
25		retop	$⊢ topGen (ran (.)) \in Top$
26	15 25	eqeltri	$⊢ J \in Top$
27	13 14	iccssred	$⊢ φ \to [X, Y] \subseteq ℝ$
28		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
29	15	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
30	28 29	eqtr4i	$⊢ ℝ = ⋃ J$
31	30	restuni	$⊢ (J \in Top \land [X, Y] \subseteq ℝ) \to [X, Y] = ⋃ (J ↾_{𝑡} [X, Y])$
32	26 27 31	sylancr	$⊢ φ \to [X, Y] = ⋃ (J ↾_{𝑡} [X, Y])$
33	16	unieqi	$⊢ ⋃ K = ⋃ (J ↾_{𝑡} [X, Y])$
34	33	eqcomi	$⊢ ⋃ (J ↾_{𝑡} [X, Y]) = ⋃ K$
35	32 34	eqtrdi	$⊢ φ \to [X, Y] = ⋃ K$
36	24 35	sseqtrd	$⊢ φ \to H \subseteq ⋃ K$
37	36	adantr	$⊢ (φ \land \neg H \in Fin) \to H \subseteq ⋃ K$
38		simpr	$⊢ (φ \land \neg H \in Fin) \to \neg H \in Fin$
39		eqid	$⊢ ⋃ K = ⋃ K$
40	39	bwth	$⊢ (K \in Comp \land H \subseteq ⋃ K \land \neg H \in Fin) \to \exists x \in ⋃ K x \in limPt (K) (H)$
41	21 37 38 40	syl3anc	$⊢ (φ \land \neg H \in Fin) \to \exists x \in ⋃ K x \in limPt (K) (H)$
42	24 27	sstrd	$⊢ φ \to H \subseteq ℝ$
43	42	ad2antrr	$⊢ ((φ \land x \in ⋃ K) \land x \in limPt (J) (H)) \to H \subseteq ℝ$
44		ne0i	$⊢ x \in limPt (J) (H) \to limPt (J) (H) \neq \emptyset$
45	44	adantl	$⊢ ((φ \land x \in ⋃ K) \land x \in limPt (J) (H)) \to limPt (J) (H) \neq \emptyset$
46		absf	$⊢ abs : ℂ ⟶ ℝ$
47		ffn	$⊢ abs : ℂ ⟶ ℝ \to abs Fn ℂ$
48	46 47	ax-mp	$⊢ abs Fn ℂ$
49		subf	$⊢ - : ℂ \times ℂ ⟶ ℂ$
50		ffn	$⊢ - : ℂ \times ℂ ⟶ ℂ \to - Fn (ℂ \times ℂ)$
51	49 50	ax-mp	$⊢ - Fn (ℂ \times ℂ)$
52		frn	$⊢ - : ℂ \times ℂ ⟶ ℂ \to ran - \subseteq ℂ$
53	49 52	ax-mp	$⊢ ran - \subseteq ℂ$
54		fnco	$⊢ (abs Fn ℂ \land - Fn (ℂ \times ℂ) \land ran - \subseteq ℂ) \to (abs \circ -) Fn (ℂ \times ℂ)$
55	48 51 53 54	mp3an	$⊢ (abs \circ -) Fn (ℂ \times ℂ)$
56	9	fneq1i	$⊢ D Fn (ℂ \times ℂ) \leftrightarrow (abs \circ -) Fn (ℂ \times ℂ)$
57	55 56	mpbir	$⊢ D Fn (ℂ \times ℂ)$
58	1 2	iccssred	$⊢ φ \to [B, C] \subseteq ℝ$
59		ax-resscn	$⊢ ℝ \subseteq ℂ$
60	58 59	sstrdi	$⊢ φ \to [B, C] \subseteq ℂ$
61	5 60	sstrd	$⊢ φ \to A \subseteq ℂ$
62		xpss12	$⊢ (A \subseteq ℂ \land A \subseteq ℂ) \to A \times A \subseteq ℂ \times ℂ$
63	61 61 62	syl2anc	$⊢ φ \to A \times A \subseteq ℂ \times ℂ$
64	63	ssdifssd	$⊢ φ \to (A \times A) ∖ I \subseteq ℂ \times ℂ$
65	10 64	eqsstrid	$⊢ φ \to I \subseteq ℂ \times ℂ$
66		fnssres	$⊢ (D Fn (ℂ \times ℂ) \land I \subseteq ℂ \times ℂ) \to ({D ↾}_{I}) Fn I$
67	57 65 66	sylancr	$⊢ φ \to ({D ↾}_{I}) Fn I$
68		fvres	$⊢ x \in I \to ({D ↾}_{I}) (x) = D (x)$
69	68	adantl	$⊢ (φ \land x \in I) \to ({D ↾}_{I}) (x) = D (x)$
70	9	fveq1i	$⊢ D (x) = (abs \circ -) (x)$
71	70	a1i	$⊢ (φ \land x \in I) \to D (x) = (abs \circ -) (x)$
72		ffun	$⊢ - : ℂ \times ℂ ⟶ ℂ \to Fun -$
73	49 72	ax-mp	$⊢ Fun -$
74	65	sselda	$⊢ (φ \land x \in I) \to x \in (ℂ \times ℂ)$
75	49	fdmi	$⊢ dom - = ℂ \times ℂ$
76	74 75	eleqtrrdi	$⊢ (φ \land x \in I) \to x \in dom -$
77		fvco	$⊢ (Fun - \land x \in dom -) \to (abs \circ -) (x) = \|- (x)\|$
78	73 76 77	sylancr	$⊢ (φ \land x \in I) \to (abs \circ -) (x) = \|- (x)\|$
79	69 71 78	3eqtrd	$⊢ (φ \land x \in I) \to ({D ↾}_{I}) (x) = \|- (x)\|$
80	49	a1i	$⊢ (φ \land x \in I) \to - : ℂ \times ℂ ⟶ ℂ$
81	80 74	ffvelrnd	$⊢ (φ \land x \in I) \to - (x) \in ℂ$
82	81	abscld	$⊢ (φ \land x \in I) \to \|- (x)\| \in ℝ$
83	79 82	eqeltrd	$⊢ (φ \land x \in I) \to ({D ↾}_{I}) (x) \in ℝ$
84		elxp2	$⊢ x \in (ℂ \times ℂ) \leftrightarrow \exists y \in ℂ \exists z \in ℂ x = ⟨y, z⟩$
85	74 84	sylib	$⊢ (φ \land x \in I) \to \exists y \in ℂ \exists z \in ℂ x = ⟨y, z⟩$
86		fveq2	$⊢ x = ⟨y, z⟩ \to - (x) = - (⟨y, z⟩)$
87	86	3ad2ant3	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to - (x) = - (⟨y, z⟩)$
88		df-ov	$⊢ y - z = - (⟨y, z⟩)$
89		simp1l	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to φ$
90		simpr	$⊢ (x \in I \land x = ⟨y, z⟩) \to x = ⟨y, z⟩$
91		simpl	$⊢ (x \in I \land x = ⟨y, z⟩) \to x \in I$
92	90 91	eqeltrrd	$⊢ (x \in I \land x = ⟨y, z⟩) \to ⟨y, z⟩ \in I$
93	92	adantll	$⊢ ((φ \land x \in I) \land x = ⟨y, z⟩) \to ⟨y, z⟩ \in I$
94	93	3adant2	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to ⟨y, z⟩ \in I$
95	61	adantr	$⊢ (φ \land ⟨y, z⟩ \in I) \to A \subseteq ℂ$
96	10	eleq2i	$⊢ ⟨y, z⟩ \in I \leftrightarrow ⟨y, z⟩ \in ((A \times A) ∖ I)$
97		eldif	$⊢ ⟨y, z⟩ \in ((A \times A) ∖ I) \leftrightarrow (⟨y, z⟩ \in (A \times A) \land \neg ⟨y, z⟩ \in I)$
98	96 97	sylbb	$⊢ ⟨y, z⟩ \in I \to (⟨y, z⟩ \in (A \times A) \land \neg ⟨y, z⟩ \in I)$
99	98	simpld	$⊢ ⟨y, z⟩ \in I \to ⟨y, z⟩ \in (A \times A)$
100		opelxp	$⊢ ⟨y, z⟩ \in (A \times A) \leftrightarrow (y \in A \land z \in A)$
101	99 100	sylib	$⊢ ⟨y, z⟩ \in I \to (y \in A \land z \in A)$
102	101	adantl	$⊢ (φ \land ⟨y, z⟩ \in I) \to (y \in A \land z \in A)$
103	102	simpld	$⊢ (φ \land ⟨y, z⟩ \in I) \to y \in A$
104	95 103	sseldd	$⊢ (φ \land ⟨y, z⟩ \in I) \to y \in ℂ$
105	102	simprd	$⊢ (φ \land ⟨y, z⟩ \in I) \to z \in A$
106	95 105	sseldd	$⊢ (φ \land ⟨y, z⟩ \in I) \to z \in ℂ$
107	98	simprd	$⊢ ⟨y, z⟩ \in I \to \neg ⟨y, z⟩ \in I$
108		df-br	$⊢ y I z \leftrightarrow ⟨y, z⟩ \in I$
109	107 108	sylnibr	$⊢ ⟨y, z⟩ \in I \to \neg y I z$
110		vex	$⊢ z \in V$
111	110	ideq	$⊢ y I z \leftrightarrow y = z$
112	109 111	sylnib	$⊢ ⟨y, z⟩ \in I \to \neg y = z$
113	112	neqned	$⊢ ⟨y, z⟩ \in I \to y \neq z$
114	113	adantl	$⊢ (φ \land ⟨y, z⟩ \in I) \to y \neq z$
115	104 106 114	subne0d	$⊢ (φ \land ⟨y, z⟩ \in I) \to y - z \neq 0$
116	89 94 115	syl2anc	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to y - z \neq 0$
117	88 116	eqnetrrid	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to - (⟨y, z⟩) \neq 0$
118	87 117	eqnetrd	$⊢ ((φ \land x \in I) \land (y \in ℂ \land z \in ℂ) \land x = ⟨y, z⟩) \to - (x) \neq 0$
119	118	3exp	$⊢ (φ \land x \in I) \to ((y \in ℂ \land z \in ℂ) \to (x = ⟨y, z⟩ \to - (x) \neq 0))$
120	119	rexlimdvv	$⊢ (φ \land x \in I) \to (\exists y \in ℂ \exists z \in ℂ x = ⟨y, z⟩ \to - (x) \neq 0)$
121	85 120	mpd	$⊢ (φ \land x \in I) \to - (x) \neq 0$
122		absgt0	$⊢ - (x) \in ℂ \to (- (x) \neq 0 \leftrightarrow 0 < \|- (x)\|)$
123	81 122	syl	$⊢ (φ \land x \in I) \to (- (x) \neq 0 \leftrightarrow 0 < \|- (x)\|)$
124	121 123	mpbid	$⊢ (φ \land x \in I) \to 0 < \|- (x)\|$
125	79	eqcomd	$⊢ (φ \land x \in I) \to \|- (x)\| = ({D ↾}_{I}) (x)$
126	124 125	breqtrd	$⊢ (φ \land x \in I) \to 0 < ({D ↾}_{I}) (x)$
127	83 126	elrpd	$⊢ (φ \land x \in I) \to ({D ↾}_{I}) (x) \in ℝ^{+}$
128	127	ralrimiva	$⊢ φ \to \forall x \in I ({D ↾}_{I}) (x) \in ℝ^{+}$
129		fnfvrnss	$⊢ (({D ↾}_{I}) Fn I \land \forall x \in I ({D ↾}_{I}) (x) \in ℝ^{+}) \to ran ({D ↾}_{I}) \subseteq ℝ^{+}$
130	67 128 129	syl2anc	$⊢ φ \to ran ({D ↾}_{I}) \subseteq ℝ^{+}$
131	11 130	eqsstrid	$⊢ φ \to R \subseteq ℝ^{+}$
132		ltso	$⊢ < Or ℝ$
133	132	a1i	$⊢ φ \to < Or ℝ$
134		xpfi	$⊢ (A \in Fin \land A \in Fin) \to A \times A \in Fin$
135	6 6 134	syl2anc	$⊢ φ \to A \times A \in Fin$
136		diffi	$⊢ A \times A \in Fin \to (A \times A) ∖ I \in Fin$
137	135 136	syl	$⊢ φ \to (A \times A) ∖ I \in Fin$
138	10 137	eqeltrid	$⊢ φ \to I \in Fin$
139		fnfi	$⊢ (({D ↾}_{I}) Fn I \land I \in Fin) \to {D ↾}_{I} \in Fin$
140	67 138 139	syl2anc	$⊢ φ \to {D ↾}_{I} \in Fin$
141		rnfi	$⊢ {D ↾}_{I} \in Fin \to ran ({D ↾}_{I}) \in Fin$
142	140 141	syl	$⊢ φ \to ran ({D ↾}_{I}) \in Fin$
143	11 142	eqeltrid	$⊢ φ \to R \in Fin$
144	11	a1i	$⊢ φ \to R = ran ({D ↾}_{I})$
145	9	a1i	$⊢ φ \to D = abs \circ -$
146	145	reseq1d	$⊢ φ \to {D ↾}_{I} = {(abs \circ -) ↾}_{I}$
147	146	fveq1d	$⊢ φ \to ({D ↾}_{I}) (⟨B, C⟩) = ({(abs \circ -) ↾}_{I}) (⟨B, C⟩)$
148		opelxp	$⊢ ⟨B, C⟩ \in (A \times A) \leftrightarrow (B \in A \land C \in A)$
149	7 8 148	sylanbrc	$⊢ φ \to ⟨B, C⟩ \in (A \times A)$
150	1 3	ltned	$⊢ φ \to B \neq C$
151	150	neneqd	$⊢ φ \to \neg B = C$
152		ideqg	$⊢ C \in A \to (B I C \leftrightarrow B = C)$
153	8 152	syl	$⊢ φ \to (B I C \leftrightarrow B = C)$
154	151 153	mtbird	$⊢ φ \to \neg B I C$
155		df-br	$⊢ B I C \leftrightarrow ⟨B, C⟩ \in I$
156	154 155	sylnib	$⊢ φ \to \neg ⟨B, C⟩ \in I$
157	149 156	eldifd	$⊢ φ \to ⟨B, C⟩ \in ((A \times A) ∖ I)$
158	157 10	eleqtrrdi	$⊢ φ \to ⟨B, C⟩ \in I$
159		fvres	$⊢ ⟨B, C⟩ \in I \to ({(abs \circ -) ↾}_{I}) (⟨B, C⟩) = (abs \circ -) (⟨B, C⟩)$
160	158 159	syl	$⊢ φ \to ({(abs \circ -) ↾}_{I}) (⟨B, C⟩) = (abs \circ -) (⟨B, C⟩)$
161	1	recnd	$⊢ φ \to B \in ℂ$
162	2	recnd	$⊢ φ \to C \in ℂ$
163		opelxp	$⊢ ⟨B, C⟩ \in (ℂ \times ℂ) \leftrightarrow (B \in ℂ \land C \in ℂ)$
164	161 162 163	sylanbrc	$⊢ φ \to ⟨B, C⟩ \in (ℂ \times ℂ)$
165	164 75	eleqtrrdi	$⊢ φ \to ⟨B, C⟩ \in dom -$
166		fvco	$⊢ (Fun - \land ⟨B, C⟩ \in dom -) \to (abs \circ -) (⟨B, C⟩) = \|- (⟨B, C⟩)\|$
167	73 165 166	sylancr	$⊢ φ \to (abs \circ -) (⟨B, C⟩) = \|- (⟨B, C⟩)\|$
168		df-ov	$⊢ B - C = - (⟨B, C⟩)$
169	168	eqcomi	$⊢ - (⟨B, C⟩) = B - C$
170	169	a1i	$⊢ φ \to - (⟨B, C⟩) = B - C$
171	170	fveq2d	$⊢ φ \to \|- (⟨B, C⟩)\| = \|B - C\|$
172	167 171	eqtrd	$⊢ φ \to (abs \circ -) (⟨B, C⟩) = \|B - C\|$
173	147 160 172	3eqtrrd	$⊢ φ \to \|B - C\| = ({D ↾}_{I}) (⟨B, C⟩)$
174		fnfvelrn	$⊢ (({D ↾}_{I}) Fn I \land ⟨B, C⟩ \in I) \to ({D ↾}_{I}) (⟨B, C⟩) \in ran ({D ↾}_{I})$
175	67 158 174	syl2anc	$⊢ φ \to ({D ↾}_{I}) (⟨B, C⟩) \in ran ({D ↾}_{I})$
176	173 175	eqeltrd	$⊢ φ \to \|B - C\| \in ran ({D ↾}_{I})$
177		ne0i	$⊢ \|B - C\| \in ran ({D ↾}_{I}) \to ran ({D ↾}_{I}) \neq \emptyset$
178	176 177	syl	$⊢ φ \to ran ({D ↾}_{I}) \neq \emptyset$
179	144 178	eqnetrd	$⊢ φ \to R \neq \emptyset$
180		resss	$⊢ {D ↾}_{I} \subseteq D$
181		rnss	$⊢ {D ↾}_{I} \subseteq D \to ran ({D ↾}_{I}) \subseteq ran D$
182	180 181	ax-mp	$⊢ ran ({D ↾}_{I}) \subseteq ran D$
183	9	rneqi	$⊢ ran D = ran (abs \circ -)$
184		rncoss	$⊢ ran (abs \circ -) \subseteq ran abs$
185		frn	$⊢ abs : ℂ ⟶ ℝ \to ran abs \subseteq ℝ$
186	46 185	ax-mp	$⊢ ran abs \subseteq ℝ$
187	184 186	sstri	$⊢ ran (abs \circ -) \subseteq ℝ$
188	183 187	eqsstri	$⊢ ran D \subseteq ℝ$
189	182 188	sstri	$⊢ ran ({D ↾}_{I}) \subseteq ℝ$
190	11 189	eqsstri	$⊢ R \subseteq ℝ$
191	190	a1i	$⊢ φ \to R \subseteq ℝ$
192		fiinfcl	$⊢ (< Or ℝ \land (R \in Fin \land R \neq \emptyset \land R \subseteq ℝ)) \to sup (R ℝ <) \in R$
193	133 143 179 191 192	syl13anc	$⊢ φ \to sup (R ℝ <) \in R$
194	131 193	sseldd	$⊢ φ \to sup (R ℝ <) \in ℝ^{+}$
195	12 194	eqeltrid	$⊢ φ \to E \in ℝ^{+}$
196	195	ad2antrr	$⊢ ((φ \land x \in ⋃ K) \land x \in limPt (J) (H)) \to E \in ℝ^{+}$
197	15 43 45 196	lptre2pt	$⊢ ((φ \land x \in ⋃ K) \land x \in limPt (J) (H)) \to \exists y \in H \exists z \in H (y \neq z \land \|y - z\| < E)$
198		simpll	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to φ$
199	42	sselda	$⊢ (φ \land y \in H) \to y \in ℝ$
200	199	adantrr	$⊢ (φ \land (y \in H \land z \in H)) \to y \in ℝ$
201	200	adantr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to y \in ℝ$
202	42	sselda	$⊢ (φ \land z \in H) \to z \in ℝ$
203	202	adantrl	$⊢ (φ \land (y \in H \land z \in H)) \to z \in ℝ$
204	203	adantr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to z \in ℝ$
205		simpr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to y \neq z$
206	201 204 205	3jca	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to (y \in ℝ \land z \in ℝ \land y \neq z)$
207	17	eleq2i	$⊢ y \in H \leftrightarrow y \in \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\}$
208		oveq1	$⊢ x = y \to x + k T = y + k T$
209	208	eleq1d	$⊢ x = y \to (x + k T \in A \leftrightarrow y + k T \in A)$
210	209	rexbidv	$⊢ x = y \to (\exists k \in ℤ x + k T \in A \leftrightarrow \exists k \in ℤ y + k T \in A)$
211		oveq1	$⊢ k = j \to k T = j T$
212	211	oveq2d	$⊢ k = j \to y + k T = y + j T$
213	212	eleq1d	$⊢ k = j \to (y + k T \in A \leftrightarrow y + j T \in A)$
214	213	cbvrexvw	$⊢ \exists k \in ℤ y + k T \in A \leftrightarrow \exists j \in ℤ y + j T \in A$
215	210 214	bitrdi	$⊢ x = y \to (\exists k \in ℤ x + k T \in A \leftrightarrow \exists j \in ℤ y + j T \in A)$
216	215	elrab	$⊢ y \in \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\} \leftrightarrow (y \in [X, Y] \land \exists j \in ℤ y + j T \in A)$
217	207 216	sylbb	$⊢ y \in H \to (y \in [X, Y] \land \exists j \in ℤ y + j T \in A)$
218	217	simprd	$⊢ y \in H \to \exists j \in ℤ y + j T \in A$
219	218	adantr	$⊢ (y \in H \land z \in H) \to \exists j \in ℤ y + j T \in A$
220	17	eleq2i	$⊢ z \in H \leftrightarrow z \in \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\}$
221		oveq1	$⊢ x = z \to x + k T = z + k T$
222	221	eleq1d	$⊢ x = z \to (x + k T \in A \leftrightarrow z + k T \in A)$
223	222	rexbidv	$⊢ x = z \to (\exists k \in ℤ x + k T \in A \leftrightarrow \exists k \in ℤ z + k T \in A)$
224	223	elrab	$⊢ z \in \{x \in [X, Y] \| \exists k \in ℤ x + k T \in A\} \leftrightarrow (z \in [X, Y] \land \exists k \in ℤ z + k T \in A)$
225	220 224	sylbb	$⊢ z \in H \to (z \in [X, Y] \land \exists k \in ℤ z + k T \in A)$
226	225	simprd	$⊢ z \in H \to \exists k \in ℤ z + k T \in A$
227	226	adantl	$⊢ (y \in H \land z \in H) \to \exists k \in ℤ z + k T \in A$
228		reeanv	$⊢ \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A) \leftrightarrow (\exists j \in ℤ y + j T \in A \land \exists k \in ℤ z + k T \in A)$
229	219 227 228	sylanbrc	$⊢ (y \in H \land z \in H) \to \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)$
230	229	ad2antlr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)$
231		simplll	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land y < z) \to φ$
232		simpl1	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land y < z) \to y \in ℝ$
233		simpl2	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land y < z) \to z \in ℝ$
234		simpr	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land y < z) \to y < z$
235	232 233 234	3jca	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land y < z) \to (y \in ℝ \land z \in ℝ \land y < z)$
236	235	adantll	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land y < z) \to (y \in ℝ \land z \in ℝ \land y < z)$
237	236	adantlr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land y < z) \to (y \in ℝ \land z \in ℝ \land y < z)$
238		simplr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land y < z) \to \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)$
239		eleq1	$⊢ b = z \to (b \in ℝ \leftrightarrow z \in ℝ)$
240		breq2	$⊢ b = z \to (y < b \leftrightarrow y < z)$
241	239 240	3anbi23d	$⊢ b = z \to ((y \in ℝ \land b \in ℝ \land y < b) \leftrightarrow (y \in ℝ \land z \in ℝ \land y < z))$
242	241	anbi2d	$⊢ b = z \to ((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \leftrightarrow (φ \land (y \in ℝ \land z \in ℝ \land y < z)))$
243		oveq1	$⊢ b = z \to b + k T = z + k T$
244	243	eleq1d	$⊢ b = z \to (b + k T \in A \leftrightarrow z + k T \in A)$
245	244	anbi2d	$⊢ b = z \to ((y + j T \in A \land b + k T \in A) \leftrightarrow (y + j T \in A \land z + k T \in A))$
246	245	2rexbidv	$⊢ b = z \to (\exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A))$
247	242 246	anbi12d	$⊢ b = z \to (((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A)) \leftrightarrow ((φ \land (y \in ℝ \land z \in ℝ \land y < z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)))$
248		oveq2	$⊢ b = z \to y - b = y - z$
249	248	fveq2d	$⊢ b = z \to \|y - b\| = \|y - z\|$
250	249	breq2d	$⊢ b = z \to (E \leq \|y - b\| \leftrightarrow E \leq \|y - z\|)$
251	247 250	imbi12d	$⊢ b = z \to ((((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A)) \to E \leq \|y - b\|) \leftrightarrow (((φ \land (y \in ℝ \land z \in ℝ \land y < z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \to E \leq \|y - z\|))$
252		eleq1	$⊢ a = y \to (a \in ℝ \leftrightarrow y \in ℝ)$
253		breq1	$⊢ a = y \to (a < b \leftrightarrow y < b)$
254	252 253	3anbi13d	$⊢ a = y \to ((a \in ℝ \land b \in ℝ \land a < b) \leftrightarrow (y \in ℝ \land b \in ℝ \land y < b))$
255	254	anbi2d	$⊢ a = y \to ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \leftrightarrow (φ \land (y \in ℝ \land b \in ℝ \land y < b)))$
256		oveq1	$⊢ a = y \to a + j T = y + j T$
257	256	eleq1d	$⊢ a = y \to (a + j T \in A \leftrightarrow y + j T \in A)$
258	257	anbi1d	$⊢ a = y \to ((a + j T \in A \land b + k T \in A) \leftrightarrow (y + j T \in A \land b + k T \in A))$
259	258	2rexbidv	$⊢ a = y \to (\exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A))$
260	255 259	anbi12d	$⊢ a = y \to (((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)) \leftrightarrow ((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A)))$
261		oveq1	$⊢ a = y \to a - b = y - b$
262	261	fveq2d	$⊢ a = y \to \|a - b\| = \|y - b\|$
263	262	breq2d	$⊢ a = y \to (E \leq \|a - b\| \leftrightarrow E \leq \|y - b\|)$
264	260 263	imbi12d	$⊢ a = y \to ((((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)) \to E \leq \|a - b\|) \leftrightarrow (((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A)) \to E \leq \|y - b\|))$
265	18	simprbi	$⊢ ψ \to \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)$
266	18	biimpi	$⊢ ψ \to ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A))$
267	266	simpld	$⊢ ψ \to (φ \land (a \in ℝ \land b \in ℝ \land a < b))$
268	267	simpld	$⊢ ψ \to φ$
269	268 1	syl	$⊢ ψ \to B \in ℝ$
270	269	adantr	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to B \in ℝ$
271	268 2	syl	$⊢ ψ \to C \in ℝ$
272	271	adantr	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to C \in ℝ$
273	268 5	syl	$⊢ ψ \to A \subseteq [B, C]$
274	273	sselda	$⊢ (ψ \land b + k T \in A) \to b + k T \in [B, C]$
275	274	adantrl	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T \in [B, C]$
276	273	sselda	$⊢ (ψ \land a + j T \in A) \to a + j T \in [B, C]$
277	276	adantrr	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T \in [B, C]$
278	270 272 275 277	iccsuble	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \leq C - B$
279	278 4	breqtrrdi	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \leq T$
280	279	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \leq T$
281	280	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg k \leq j) \to b + k T - (a + j T) \leq T$
282		simpr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to \neg k \leq j$
283		zre	$⊢ j \in ℤ \to j \in ℝ$
284	283	adantr	$⊢ (j \in ℤ \land k \in ℤ) \to j \in ℝ$
285	284	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to j \in ℝ$
286		zre	$⊢ k \in ℤ \to k \in ℝ$
287	286	adantl	$⊢ (j \in ℤ \land k \in ℤ) \to k \in ℝ$
288	287	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to k \in ℝ$
289	285 288	ltnled	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to (j < k \leftrightarrow \neg k \leq j)$
290	282 289	mpbird	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to j < k$
291	2 1	resubcld	$⊢ φ \to C - B \in ℝ$
292	4 291	eqeltrid	$⊢ φ \to T \in ℝ$
293	268 292	syl	$⊢ ψ \to T \in ℝ$
294	293	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to T \in ℝ$
295	287	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k \in ℝ$
296	284	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j \in ℝ$
297	295 296	resubcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k - j \in ℝ$
298	293	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to T \in ℝ$
299	297 298	remulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T \in ℝ$
300	299	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to (k - j) T \in ℝ$
301	267	simprd	$⊢ ψ \to (a \in ℝ \land b \in ℝ \land a < b)$
302	301	simp2d	$⊢ ψ \to b \in ℝ$
303	302	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b \in ℝ$
304	286	adantl	$⊢ (ψ \land k \in ℤ) \to k \in ℝ$
305	293	adantr	$⊢ (ψ \land k \in ℤ) \to T \in ℝ$
306	304 305	remulcld	$⊢ (ψ \land k \in ℤ) \to k T \in ℝ$
307	306	adantrl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k T \in ℝ$
308	303 307	readdcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b + k T \in ℝ$
309	301	simp1d	$⊢ ψ \to a \in ℝ$
310	309	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to a \in ℝ$
311	283	adantl	$⊢ (ψ \land j \in ℤ) \to j \in ℝ$
312	293	adantr	$⊢ (ψ \land j \in ℤ) \to T \in ℝ$
313	311 312	remulcld	$⊢ (ψ \land j \in ℤ) \to j T \in ℝ$
314	313	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j T \in ℝ$
315	310 314	readdcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to a + j T \in ℝ$
316	308 315	resubcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b + k T - (a + j T) \in ℝ$
317	316	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to b + k T - (a + j T) \in ℝ$
318	293	recnd	$⊢ ψ \to T \in ℂ$
319	318	mulid2d	$⊢ ψ \to 1 T = T$
320	319	eqcomd	$⊢ ψ \to T = 1 T$
321	320	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to T = 1 T$
322		simpr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to j < k$
323		zltlem1	$⊢ (j \in ℤ \land k \in ℤ) \to (j < k \leftrightarrow j \leq k - 1)$
324	323	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to (j < k \leftrightarrow j \leq k - 1)$
325	322 324	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to j \leq k - 1$
326	284	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to j \in ℝ$
327		peano2rem	$⊢ k \in ℝ \to k - 1 \in ℝ$
328	295 327	syl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k - 1 \in ℝ$
329	328	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to k - 1 \in ℝ$
330		1re	$⊢ 1 \in ℝ$
331		resubcl	$⊢ (1 \in ℝ \land j \in ℝ) \to 1 - j \in ℝ$
332	330 326 331	sylancr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to 1 - j \in ℝ$
333		simpr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to j \leq k - 1$
334	326 329 332 333	leadd1dd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to j + 1 - j \leq (k - 1) + 1 - j$
335		zcn	$⊢ j \in ℤ \to j \in ℂ$
336	335	adantr	$⊢ (j \in ℤ \land k \in ℤ) \to j \in ℂ$
337		1cnd	$⊢ (j \in ℤ \land k \in ℤ) \to 1 \in ℂ$
338	336 337	pncan3d	$⊢ (j \in ℤ \land k \in ℤ) \to j + 1 - j = 1$
339	338	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to j + 1 - j = 1$
340		zcn	$⊢ k \in ℤ \to k \in ℂ$
341	340	adantl	$⊢ (j \in ℤ \land k \in ℤ) \to k \in ℂ$
342	341 337 336	npncand	$⊢ (j \in ℤ \land k \in ℤ) \to (k - 1) + 1 - j = k - j$
343	342	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to (k - 1) + 1 - j = k - j$
344	334 339 343	3brtr3d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j \leq k - 1) \to 1 \leq k - j$
345	325 344	syldan	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to 1 \leq k - j$
346	330	a1i	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to 1 \in ℝ$
347	297	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to k - j \in ℝ$
348	1 2	posdifd	$⊢ φ \to (B < C \leftrightarrow 0 < C - B)$
349	3 348	mpbid	$⊢ φ \to 0 < C - B$
350	349 4	breqtrrdi	$⊢ φ \to 0 < T$
351	292 350	elrpd	$⊢ φ \to T \in ℝ^{+}$
352	268 351	syl	$⊢ ψ \to T \in ℝ^{+}$
353	352	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to T \in ℝ^{+}$
354	346 347 353	lemul1d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to (1 \leq k - j \leftrightarrow 1 T \leq (k - j) T)$
355	345 354	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to 1 T \leq (k - j) T$
356	321 355	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to T \leq (k - j) T$
357	302 309	resubcld	$⊢ ψ \to b - a \in ℝ$
358	301	simp3d	$⊢ ψ \to a < b$
359	309 302	posdifd	$⊢ ψ \to (a < b \leftrightarrow 0 < b - a)$
360	358 359	mpbid	$⊢ ψ \to 0 < b - a$
361	357 360	elrpd	$⊢ ψ \to b - a \in ℝ^{+}$
362	361	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a \in ℝ^{+}$
363	299 362	ltaddrp2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T < b - a + (k - j) T$
364	302	recnd	$⊢ ψ \to b \in ℂ$
365	364	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b \in ℂ$
366	306	recnd	$⊢ (ψ \land k \in ℤ) \to k T \in ℂ$
367	366	adantrl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k T \in ℂ$
368	309	recnd	$⊢ ψ \to a \in ℂ$
369	368	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to a \in ℂ$
370	313	recnd	$⊢ (ψ \land j \in ℤ) \to j T \in ℂ$
371	370	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j T \in ℂ$
372	365 367 369 371	addsub4d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b + k T - (a + j T) = (b - a) + k T - j T$
373	340	ad2antll	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k \in ℂ$
374	335	ad2antrl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j \in ℂ$
375	318	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to T \in ℂ$
376	373 374 375	subdird	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T = k T - j T$
377	376	eqcomd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k T - j T = (k - j) T$
378	377	oveq2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + k T - j T = b - a + (k - j) T$
379	372 378	eqtr2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a + (k - j) T = b + k T - (a + j T)$
380	363 379	breqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T < b + k T - (a + j T)$
381	380	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to (k - j) T < b + k T - (a + j T)$
382	294 300 317 356 381	lelttrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to T < b + k T - (a + j T)$
383	294 317	ltnled	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to (T < b + k T - (a + j T) \leftrightarrow \neg b + k T - (a + j T) \leq T)$
384	382 383	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land j < k) \to \neg b + k T - (a + j T) \leq T$
385	290 384	syldan	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land \neg k \leq j) \to \neg b + k T - (a + j T) \leq T$
386	385	3adantl3	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg k \leq j) \to \neg b + k T - (a + j T) \leq T$
387	281 386	condan	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to k \leq j$
388	190 193	sseldi	$⊢ φ \to sup (R ℝ <) \in ℝ$
389	12 388	eqeltrid	$⊢ φ \to E \in ℝ$
390	268 389	syl	$⊢ ψ \to E \in ℝ$
391	390	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \in ℝ$
392	391	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to E \in ℝ$
393	293	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to T \in ℝ$
394	393	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to T \in ℝ$
395	284 287	resubcld	$⊢ (j \in ℤ \land k \in ℤ) \to j - k \in ℝ$
396	395	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j - k \in ℝ$
397	396 298	remulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k) T \in ℝ$
398	397	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T \in ℝ$
399	398	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to (j - k) T \in ℝ$
400		id	$⊢ φ \to φ$
401	7 8	jca	$⊢ φ \to (B \in A \land C \in A)$
402	400 401 3	3jca	$⊢ φ \to (φ \land (B \in A \land C \in A) \land B < C)$
403		eleq1	$⊢ d = C \to (d \in A \leftrightarrow C \in A)$
404	403	anbi2d	$⊢ d = C \to ((B \in A \land d \in A) \leftrightarrow (B \in A \land C \in A))$
405		breq2	$⊢ d = C \to (B < d \leftrightarrow B < C)$
406	404 405	3anbi23d	$⊢ d = C \to ((φ \land (B \in A \land d \in A) \land B < d) \leftrightarrow (φ \land (B \in A \land C \in A) \land B < C))$
407		oveq1	$⊢ d = C \to d - B = C - B$
408	407	breq2d	$⊢ d = C \to (E \leq d - B \leftrightarrow E \leq C - B)$
409	406 408	imbi12d	$⊢ d = C \to (((φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B) \leftrightarrow ((φ \land (B \in A \land C \in A) \land B < C) \to E \leq C - B))$
410		simp2l	$⊢ (φ \land (B \in A \land d \in A) \land B < d) \to B \in A$
411		eleq1	$⊢ c = B \to (c \in A \leftrightarrow B \in A)$
412	411	anbi1d	$⊢ c = B \to ((c \in A \land d \in A) \leftrightarrow (B \in A \land d \in A))$
413		breq1	$⊢ c = B \to (c < d \leftrightarrow B < d)$
414	412 413	3anbi23d	$⊢ c = B \to ((φ \land (c \in A \land d \in A) \land c < d) \leftrightarrow (φ \land (B \in A \land d \in A) \land B < d))$
415		oveq2	$⊢ c = B \to d - c = d - B$
416	415	breq2d	$⊢ c = B \to (E \leq d - c \leftrightarrow E \leq d - B)$
417	414 416	imbi12d	$⊢ c = B \to (((φ \land (c \in A \land d \in A) \land c < d) \to E \leq d - c) \leftrightarrow ((φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B))$
418	190	a1i	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to R \subseteq ℝ$
419		0re	$⊢ 0 \in ℝ$
420	11	eleq2i	$⊢ y \in R \leftrightarrow y \in ran ({D ↾}_{I})$
421	420	biimpi	$⊢ y \in R \to y \in ran ({D ↾}_{I})$
422	421	adantl	$⊢ (φ \land y \in R) \to y \in ran ({D ↾}_{I})$
423	67	adantr	$⊢ (φ \land y \in R) \to ({D ↾}_{I}) Fn I$
424		fvelrnb	$⊢ ({D ↾}_{I}) Fn I \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
425	423 424	syl	$⊢ (φ \land y \in R) \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
426	422 425	mpbid	$⊢ (φ \land y \in R) \to \exists x \in I ({D ↾}_{I}) (x) = y$
427	127	rpge0d	$⊢ (φ \land x \in I) \to 0 \leq ({D ↾}_{I}) (x)$
428	427	3adant3	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to 0 \leq ({D ↾}_{I}) (x)$
429		simp3	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to ({D ↾}_{I}) (x) = y$
430	428 429	breqtrd	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to 0 \leq y$
431	430	3exp	$⊢ φ \to (x \in I \to (({D ↾}_{I}) (x) = y \to 0 \leq y))$
432	431	adantr	$⊢ (φ \land y \in R) \to (x \in I \to (({D ↾}_{I}) (x) = y \to 0 \leq y))$
433	432	rexlimdv	$⊢ (φ \land y \in R) \to (\exists x \in I ({D ↾}_{I}) (x) = y \to 0 \leq y)$
434	426 433	mpd	$⊢ (φ \land y \in R) \to 0 \leq y$
435	434	ralrimiva	$⊢ φ \to \forall y \in R 0 \leq y$
436		breq1	$⊢ x = 0 \to (x \leq y \leftrightarrow 0 \leq y)$
437	436	ralbidv	$⊢ x = 0 \to (\forall y \in R x \leq y \leftrightarrow \forall y \in R 0 \leq y)$
438	437	rspcev	$⊢ (0 \in ℝ \land \forall y \in R 0 \leq y) \to \exists x \in ℝ \forall y \in R x \leq y$
439	419 435 438	sylancr	$⊢ φ \to \exists x \in ℝ \forall y \in R x \leq y$
440	439	3ad2ant1	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \exists x \in ℝ \forall y \in R x \leq y$
441		pm3.22	$⊢ (c \in A \land d \in A) \to (d \in A \land c \in A)$
442		opelxp	$⊢ ⟨d, c⟩ \in (A \times A) \leftrightarrow (d \in A \land c \in A)$
443	441 442	sylibr	$⊢ (c \in A \land d \in A) \to ⟨d, c⟩ \in (A \times A)$
444	443	3ad2ant2	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in (A \times A)$
445	5 58	sstrd	$⊢ φ \to A \subseteq ℝ$
446	445	sselda	$⊢ (φ \land c \in A) \to c \in ℝ$
447	446	adantrr	$⊢ (φ \land (c \in A \land d \in A)) \to c \in ℝ$
448	447	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \in ℝ$
449		simp3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c < d$
450	448 449	gtned	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d \neq c$
451	450	neneqd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \neg d = c$
452		df-br	$⊢ d I c \leftrightarrow ⟨d, c⟩ \in I$
453		vex	$⊢ c \in V$
454	453	ideq	$⊢ d I c \leftrightarrow d = c$
455	452 454	bitr3i	$⊢ ⟨d, c⟩ \in I \leftrightarrow d = c$
456	451 455	sylnibr	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \neg ⟨d, c⟩ \in I$
457	444 456	eldifd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in ((A \times A) ∖ I)$
458	457 10	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in I$
459	448 449	ltned	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \neq d$
460	146	3ad2ant1	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to {D ↾}_{I} = {(abs \circ -) ↾}_{I}$
461	460	fveq1d	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({D ↾}_{I}) (⟨d, c⟩) = ({(abs \circ -) ↾}_{I}) (⟨d, c⟩)$
462	443	3ad2ant2	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in (A \times A)$
463		necom	$⊢ c \neq d \leftrightarrow d \neq c$
464	463	biimpi	$⊢ c \neq d \to d \neq c$
465	464	neneqd	$⊢ c \neq d \to \neg d = c$
466	465	3ad2ant3	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to \neg d = c$
467	466 455	sylnibr	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to \neg ⟨d, c⟩ \in I$
468	462 467	eldifd	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in ((A \times A) ∖ I)$
469	468 10	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in I$
470		fvres	$⊢ ⟨d, c⟩ \in I \to ({(abs \circ -) ↾}_{I}) (⟨d, c⟩) = (abs \circ -) (⟨d, c⟩)$
471	469 470	syl	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({(abs \circ -) ↾}_{I}) (⟨d, c⟩) = (abs \circ -) (⟨d, c⟩)$
472		simp1	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to φ$
473	472 469	jca	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (φ \land ⟨d, c⟩ \in I)$
474		eleq1	$⊢ x = ⟨d, c⟩ \to (x \in I \leftrightarrow ⟨d, c⟩ \in I)$
475	474	anbi2d	$⊢ x = ⟨d, c⟩ \to ((φ \land x \in I) \leftrightarrow (φ \land ⟨d, c⟩ \in I))$
476		eleq1	$⊢ x = ⟨d, c⟩ \to (x \in dom - \leftrightarrow ⟨d, c⟩ \in dom -)$
477	475 476	imbi12d	$⊢ x = ⟨d, c⟩ \to (((φ \land x \in I) \to x \in dom -) \leftrightarrow ((φ \land ⟨d, c⟩ \in I) \to ⟨d, c⟩ \in dom -))$
478	477 76	vtoclg	$⊢ ⟨d, c⟩ \in I \to ((φ \land ⟨d, c⟩ \in I) \to ⟨d, c⟩ \in dom -)$
479	469 473 478	sylc	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in dom -$
480		fvco	$⊢ (Fun - \land ⟨d, c⟩ \in dom -) \to (abs \circ -) (⟨d, c⟩) = \|- (⟨d, c⟩)\|$
481	73 479 480	sylancr	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (abs \circ -) (⟨d, c⟩) = \|- (⟨d, c⟩)\|$
482		df-ov	$⊢ d - c = - (⟨d, c⟩)$
483	482	eqcomi	$⊢ - (⟨d, c⟩) = d - c$
484	483	fveq2i	$⊢ \|- (⟨d, c⟩)\| = \|d - c\|$
485	481 484	eqtrdi	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (abs \circ -) (⟨d, c⟩) = \|d - c\|$
486	461 471 485	3eqtrd	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({D ↾}_{I}) (⟨d, c⟩) = \|d - c\|$
487	459 486	syld3an3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ({D ↾}_{I}) (⟨d, c⟩) = \|d - c\|$
488	445	sselda	$⊢ (φ \land d \in A) \to d \in ℝ$
489	488	adantrl	$⊢ (φ \land (c \in A \land d \in A)) \to d \in ℝ$
490	489	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d \in ℝ$
491	448 490 449	ltled	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \leq d$
492	448 490 491	abssubge0d	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \|d - c\| = d - c$
493	487 492	eqtrd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ({D ↾}_{I}) (⟨d, c⟩) = d - c$
494		fveq2	$⊢ x = ⟨d, c⟩ \to ({D ↾}_{I}) (x) = ({D ↾}_{I}) (⟨d, c⟩)$
495	494	eqeq1d	$⊢ x = ⟨d, c⟩ \to (({D ↾}_{I}) (x) = d - c \leftrightarrow ({D ↾}_{I}) (⟨d, c⟩) = d - c)$
496	495	rspcev	$⊢ (⟨d, c⟩ \in I \land ({D ↾}_{I}) (⟨d, c⟩) = d - c) \to \exists x \in I ({D ↾}_{I}) (x) = d - c$
497	458 493 496	syl2anc	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \exists x \in I ({D ↾}_{I}) (x) = d - c$
498	489 447	resubcld	$⊢ (φ \land (c \in A \land d \in A)) \to d - c \in ℝ$
499		elex	$⊢ d - c \in ℝ \to d - c \in V$
500	498 499	syl	$⊢ (φ \land (c \in A \land d \in A)) \to d - c \in V$
501	500	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in V$
502		simp1	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to φ$
503		eleq1	$⊢ y = d - c \to (y \in ran ({D ↾}_{I}) \leftrightarrow d - c \in ran ({D ↾}_{I}))$
504		eqeq2	$⊢ y = d - c \to (({D ↾}_{I}) (x) = y \leftrightarrow ({D ↾}_{I}) (x) = d - c)$
505	504	rexbidv	$⊢ y = d - c \to (\exists x \in I ({D ↾}_{I}) (x) = y \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c)$
506	503 505	bibi12d	$⊢ y = d - c \to ((y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y) \leftrightarrow (d - c \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c))$
507	506	imbi2d	$⊢ y = d - c \to ((φ \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)) \leftrightarrow (φ \to (d - c \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c)))$
508	67 424	syl	$⊢ φ \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
509	507 508	vtoclg	$⊢ d - c \in V \to (φ \to (d - c \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c))$
510	501 502 509	sylc	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to (d - c \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c)$
511	497 510	mpbird	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in ran ({D ↾}_{I})$
512	511 11	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in R$
513		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall y \in R x \leq y \land d - c \in R) \to sup (R ℝ <) \leq d - c$
514	418 440 512 513	syl3anc	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to sup (R ℝ <) \leq d - c$
515	12 514	eqbrtrid	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to E \leq d - c$
516	417 515	vtoclg	$⊢ B \in A \to ((φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B)$
517	410 516	mpcom	$⊢ (φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B$
518	409 517	vtoclg	$⊢ C \in A \to ((φ \land (B \in A \land C \in A) \land B < C) \to E \leq C - B)$
519	8 402 518	sylc	$⊢ φ \to E \leq C - B$
520	519 4	breqtrrdi	$⊢ φ \to E \leq T$
521	268 520	syl	$⊢ ψ \to E \leq T$
522	521	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq T$
523	522	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to E \leq T$
524	364	adantr	$⊢ (ψ \land k \in ℤ) \to b \in ℂ$
525	524 366	pncan2d	$⊢ (ψ \land k \in ℤ) \to b + k T - b = k T$
526	525	oveq1d	$⊢ (ψ \land k \in ℤ) \to \frac{b + k T - b}{T} = \frac{k T}{T}$
527	340	adantl	$⊢ (ψ \land k \in ℤ) \to k \in ℂ$
528	318	adantr	$⊢ (ψ \land k \in ℤ) \to T \in ℂ$
529	419	a1i	$⊢ φ \to 0 \in ℝ$
530	529 350	gtned	$⊢ φ \to T \neq 0$
531	268 530	syl	$⊢ ψ \to T \neq 0$
532	531	adantr	$⊢ (ψ \land k \in ℤ) \to T \neq 0$
533	527 528 532	divcan4d	$⊢ (ψ \land k \in ℤ) \to \frac{k T}{T} = k$
534	526 533	eqtr2d	$⊢ (ψ \land k \in ℤ) \to k = \frac{b + k T - b}{T}$
535	534	adantrl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k = \frac{b + k T - b}{T}$
536	535	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k = \frac{b + k T - b}{T}$
537		oveq1	$⊢ a + j T = b + k T \to a + j T - b = b + k T - b$
538	537	oveq1d	$⊢ a + j T = b + k T \to \frac{a + j T - b}{T} = \frac{b + k T - b}{T}$
539	538	adantl	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to \frac{a + j T - b}{T} = \frac{b + k T - b}{T}$
540	368	adantr	$⊢ (ψ \land j \in ℤ) \to a \in ℂ$
541	364	adantr	$⊢ (ψ \land j \in ℤ) \to b \in ℂ$
542	540 370 541	addsubd	$⊢ (ψ \land j \in ℤ) \to a + j T - b = a - b + j T$
543	540 541	subcld	$⊢ (ψ \land j \in ℤ) \to a - b \in ℂ$
544	543 370	addcomd	$⊢ (ψ \land j \in ℤ) \to a - b + j T = j T + a - b$
545	542 544	eqtrd	$⊢ (ψ \land j \in ℤ) \to a + j T - b = j T + a - b$
546	545	oveq1d	$⊢ (ψ \land j \in ℤ) \to \frac{a + j T - b}{T} = \frac{j T + a - b}{T}$
547	318	adantr	$⊢ (ψ \land j \in ℤ) \to T \in ℂ$
548	531	adantr	$⊢ (ψ \land j \in ℤ) \to T \neq 0$
549	370 543 547 548	divdird	$⊢ (ψ \land j \in ℤ) \to \frac{j T + a - b}{T} = (\frac{j T}{T}) + (\frac{a - b}{T})$
550	335	adantl	$⊢ (ψ \land j \in ℤ) \to j \in ℂ$
551	550 547 548	divcan4d	$⊢ (ψ \land j \in ℤ) \to \frac{j T}{T} = j$
552	551	oveq1d	$⊢ (ψ \land j \in ℤ) \to (\frac{j T}{T}) + (\frac{a - b}{T}) = j + (\frac{a - b}{T})$
553	546 549 552	3eqtrd	$⊢ (ψ \land j \in ℤ) \to \frac{a + j T - b}{T} = j + (\frac{a - b}{T})$
554	553	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to \frac{a + j T - b}{T} = j + (\frac{a - b}{T})$
555	554	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to \frac{a + j T - b}{T} = j + (\frac{a - b}{T})$
556	536 539 555	3eqtr2d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k = j + (\frac{a - b}{T})$
557	309 302	resubcld	$⊢ ψ \to a - b \in ℝ$
558	309 302	sublt0d	$⊢ ψ \to (a - b < 0 \leftrightarrow a < b)$
559	358 558	mpbird	$⊢ ψ \to a - b < 0$
560	557 352 559	divlt0gt0d	$⊢ ψ \to \frac{a - b}{T} < 0$
561	560	adantr	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} < 0$
562	335	subidd	$⊢ j \in ℤ \to j - j = 0$
563	562	eqcomd	$⊢ j \in ℤ \to 0 = j - j$
564	563	adantl	$⊢ (ψ \land j \in ℤ) \to 0 = j - j$
565	561 564	breqtrd	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} < j - j$
566	557 293 531	redivcld	$⊢ ψ \to \frac{a - b}{T} \in ℝ$
567	566	adantr	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} \in ℝ$
568	311 567 311	ltaddsub2d	$⊢ (ψ \land j \in ℤ) \to (j + (\frac{a - b}{T}) < j \leftrightarrow \frac{a - b}{T} < j - j)$
569	565 568	mpbird	$⊢ (ψ \land j \in ℤ) \to j + (\frac{a - b}{T}) < j$
570	569	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j + (\frac{a - b}{T}) < j$
571	570	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to j + (\frac{a - b}{T}) < j$
572	556 571	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k < j$
573	320	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T = 1 T$
574		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k < j$
575		simplr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \in ℤ$
576		simpll	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to j \in ℤ$
577		zltp1le	$⊢ (k \in ℤ \land j \in ℤ) \to (k < j \leftrightarrow k + 1 \leq j)$
578	575 576 577	syl2anc	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to (k < j \leftrightarrow k + 1 \leq j)$
579	574 578	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k + 1 \leq j$
580	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \in ℝ$
581	330	a1i	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to 1 \in ℝ$
582	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to j \in ℝ$
583	580 581 582	leaddsub2d	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to (k + 1 \leq j \leftrightarrow 1 \leq j - k)$
584	579 583	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to 1 \leq j - k$
585	584	adantll	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 \leq j - k$
586	330	a1i	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 \in ℝ$
587	395	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to j - k \in ℝ$
588	352	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T \in ℝ^{+}$
589	586 587 588	lemul1d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to (1 \leq j - k \leftrightarrow 1 T \leq (j - k) T)$
590	585 589	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 T \leq (j - k) T$
591	573 590	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T \leq (j - k) T$
592	572 591	syldan	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to T \leq (j - k) T$
593	592	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \land a + j T = b + k T) \to T \leq (j - k) T$
594	593	3adantll3	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to T \leq (j - k) T$
595	392 394 399 523 594	letrd	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to E \leq (j - k) T$
596		oveq2	$⊢ a + j T = b + k T \to b + k T - (a + j T) = b + k T - (b + k T)$
597	596	oveq1d	$⊢ a + j T = b + k T \to (b + k T) - (a + j T) + (j - k) T = (b + k T) - (b + k T) + (j - k) T$
598	597	adantl	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T = b + k T) \to (b + k T) - (a + j T) + (j - k) T = (b + k T) - (b + k T) + (j - k) T$
599	268 445	syl	$⊢ ψ \to A \subseteq ℝ$
600	599	sselda	$⊢ (ψ \land b + k T \in A) \to b + k T \in ℝ$
601	600	adantrl	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℝ$
602	601	recnd	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℂ$
603	602	subidd	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (b + k T) = 0$
604	603	oveq1d	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to (b + k T) - (b + k T) + (j - k) T = 0 + (j - k) T$
605	604	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T = b + k T) \to (b + k T) - (b + k T) + (j - k) T = 0 + (j - k) T$
606	598 605	eqtrd	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T = b + k T) \to (b + k T) - (a + j T) + (j - k) T = 0 + (j - k) T$
607	606	3adantl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land a + j T = b + k T) \to (b + k T) - (a + j T) + (j - k) T = 0 + (j - k) T$
608	607	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to (b + k T) - (a + j T) + (j - k) T = 0 + (j - k) T$
609	374 373	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j - k \in ℂ$
610	609 375	mulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k) T \in ℂ$
611	610	addid2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to 0 + (j - k) T = (j - k) T$
612	611	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to 0 + (j - k) T = (j - k) T$
613	612	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to 0 + (j - k) T = (j - k) T$
614	608 613	eqtr2d	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to (j - k) T = (b + k T) - (a + j T) + (j - k) T$
615	595 614	breqtrd	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T = b + k T) \to E \leq (b + k T) - (a + j T) + (j - k) T$
616	615	adantlr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land a + j T = b + k T) \to E \leq (b + k T) - (a + j T) + (j - k) T$
617	391	ad3antrrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to E \in ℝ$
618	599	sselda	$⊢ (ψ \land a + j T \in A) \to a + j T \in ℝ$
619	618	adantrr	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T \in ℝ$
620	601 619	resubcld	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \in ℝ$
621	620	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \in ℝ$
622	621	ad3antrrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to b + k T - (a + j T) \in ℝ$
623	621 398	readdcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (b + k T) - (a + j T) + (j - k) T \in ℝ$
624	623	ad3antrrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to (b + k T) - (a + j T) + (j - k) T \in ℝ$
625	268	adantr	$⊢ (ψ \land k \leq j) \to φ$
626	625	3ad2antl1	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to φ$
627	626	ad2antrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to φ$
628		simpl3	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to (a + j T \in A \land b + k T \in A)$
629	628	ad2antrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to (a + j T \in A \land b + k T \in A)$
630		simplr	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to a + j T \leq b + k T$
631	619	ad2antrr	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to a + j T \in ℝ$
632	601	ad2antrr	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to b + k T \in ℝ$
633	631 632	lenltd	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to (a + j T \leq b + k T \leftrightarrow \neg b + k T < a + j T)$
634	630 633	mpbid	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg b + k T < a + j T$
635		eqcom	$⊢ a + j T = b + k T \leftrightarrow b + k T = a + j T$
636	635	notbii	$⊢ \neg a + j T = b + k T \leftrightarrow \neg b + k T = a + j T$
637	636	biimpi	$⊢ \neg a + j T = b + k T \to \neg b + k T = a + j T$
638	637	adantl	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg b + k T = a + j T$
639		ioran	$⊢ \neg (b + k T < a + j T \lor b + k T = a + j T) \leftrightarrow (\neg b + k T < a + j T \land \neg b + k T = a + j T)$
640	634 638 639	sylanbrc	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg (b + k T < a + j T \lor b + k T = a + j T)$
641	632 631	leloed	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to (b + k T \leq a + j T \leftrightarrow (b + k T < a + j T \lor b + k T = a + j T))$
642	640 641	mtbird	$⊢ (((ψ \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg b + k T \leq a + j T$
643	642	3adantll2	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg b + k T \leq a + j T$
644	643	adantllr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to \neg b + k T \leq a + j T$
645	619	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to a + j T \in ℝ$
646	645	3adantl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to a + j T \in ℝ$
647	646	ad2antrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to a + j T \in ℝ$
648	601	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to b + k T \in ℝ$
649	648	3adantl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to b + k T \in ℝ$
650	649	ad2antrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to b + k T \in ℝ$
651	647 650	ltnled	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to (a + j T < b + k T \leftrightarrow \neg b + k T \leq a + j T)$
652	644 651	mpbird	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to a + j T < b + k T$
653		simp2l	$⊢ (φ \land (a + j T \in A \land b + k T \in A) \land a + j T < b + k T) \to a + j T \in A$
654		eleq1	$⊢ c = a + j T \to (c \in A \leftrightarrow a + j T \in A)$
655	654	anbi1d	$⊢ c = a + j T \to ((c \in A \land b + k T \in A) \leftrightarrow (a + j T \in A \land b + k T \in A))$
656		breq1	$⊢ c = a + j T \to (c < b + k T \leftrightarrow a + j T < b + k T)$
657	655 656	3anbi23d	$⊢ c = a + j T \to ((φ \land (c \in A \land b + k T \in A) \land c < b + k T) \leftrightarrow (φ \land (a + j T \in A \land b + k T \in A) \land a + j T < b + k T))$
658		oveq2	$⊢ c = a + j T \to b + k T - c = b + k T - (a + j T)$
659	658	breq2d	$⊢ c = a + j T \to (E \leq b + k T - c \leftrightarrow E \leq b + k T - (a + j T))$
660	657 659	imbi12d	$⊢ c = a + j T \to (((φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to E \leq b + k T - c) \leftrightarrow ((φ \land (a + j T \in A \land b + k T \in A) \land a + j T < b + k T) \to E \leq b + k T - (a + j T)))$
661		simp2r	$⊢ (φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to b + k T \in A$
662		eleq1	$⊢ d = b + k T \to (d \in A \leftrightarrow b + k T \in A)$
663	662	anbi2d	$⊢ d = b + k T \to ((c \in A \land d \in A) \leftrightarrow (c \in A \land b + k T \in A))$
664		breq2	$⊢ d = b + k T \to (c < d \leftrightarrow c < b + k T)$
665	663 664	3anbi23d	$⊢ d = b + k T \to ((φ \land (c \in A \land d \in A) \land c < d) \leftrightarrow (φ \land (c \in A \land b + k T \in A) \land c < b + k T))$
666		oveq1	$⊢ d = b + k T \to d - c = b + k T - c$
667	666	breq2d	$⊢ d = b + k T \to (E \leq d - c \leftrightarrow E \leq b + k T - c)$
668	665 667	imbi12d	$⊢ d = b + k T \to (((φ \land (c \in A \land d \in A) \land c < d) \to E \leq d - c) \leftrightarrow ((φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to E \leq b + k T - c))$
669	668 515	vtoclg	$⊢ b + k T \in A \to ((φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to E \leq b + k T - c)$
670	661 669	mpcom	$⊢ (φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to E \leq b + k T - c$
671	660 670	vtoclg	$⊢ a + j T \in A \to ((φ \land (a + j T \in A \land b + k T \in A) \land a + j T < b + k T) \to E \leq b + k T - (a + j T))$
672	653 671	mpcom	$⊢ (φ \land (a + j T \in A \land b + k T \in A) \land a + j T < b + k T) \to E \leq b + k T - (a + j T)$
673	627 629 652 672	syl3anc	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to E \leq b + k T - (a + j T)$
674	395	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to j - k \in ℝ$
675	293	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to T \in ℝ$
676		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to k \leq j$
677	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to j \in ℝ$
678	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to k \in ℝ$
679	677 678	subge0d	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to (0 \leq j - k \leftrightarrow k \leq j)$
680	676 679	mpbird	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to 0 \leq j - k$
681	680	adantll	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq j - k$
682	352	rpge0d	$⊢ ψ \to 0 \leq T$
683	682	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq T$
684	674 675 681 683	mulge0d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq (j - k) T$
685	684	3adantl3	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to 0 \leq (j - k) T$
686	621	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to b + k T - (a + j T) \in ℝ$
687	398	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to (j - k) T \in ℝ$
688	686 687	addge01d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to (0 \leq (j - k) T \leftrightarrow b + k T - (a + j T) \leq (b + k T) - (a + j T) + (j - k) T)$
689	685 688	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to b + k T - (a + j T) \leq (b + k T) - (a + j T) + (j - k) T$
690	689	ad2antrr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to b + k T - (a + j T) \leq (b + k T) - (a + j T) + (j - k) T$
691	617 622 624 673 690	letrd	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \land \neg a + j T = b + k T) \to E \leq (b + k T) - (a + j T) + (j - k) T$
692	616 691	pm2.61dan	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \to E \leq (b + k T) - (a + j T) + (j - k) T$
693	372 378	eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b + k T - (a + j T) = b - a + (k - j) T$
694	693	oveq1d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b + k T) - (a + j T) + (j - k) T = (b - a) + (k - j) T + (j - k) T$
695	365 369	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a \in ℂ$
696	373 374	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k - j \in ℂ$
697	696 375	mulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T \in ℂ$
698	695 697 610	addassd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = (b - a) + (k - j) T + (j - k) T$
699	341 336 336 341	subadd4b	$⊢ (j \in ℤ \land k \in ℤ) \to (k - j) + j - k = (k - k) + j - j$
700	699	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) + j - k = (k - k) + j - j$
701	700	oveq1d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - j) + j - k) T = ((k - k) + j - j) T$
702	696 609 375	adddird	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - j) + j - k) T = (k - j) T + (j - k) T$
703	340	subidd	$⊢ k \in ℤ \to k - k = 0$
704	703	adantl	$⊢ (j \in ℤ \land k \in ℤ) \to k - k = 0$
705	562	adantr	$⊢ (j \in ℤ \land k \in ℤ) \to j - j = 0$
706	704 705	oveq12d	$⊢ (j \in ℤ \land k \in ℤ) \to (k - k) + j - j = 0 + 0$
707		00id	$⊢ 0 + 0 = 0$
708	706 707	eqtrdi	$⊢ (j \in ℤ \land k \in ℤ) \to (k - k) + j - j = 0$
709	708	oveq1d	$⊢ (j \in ℤ \land k \in ℤ) \to ((k - k) + j - j) T = 0 \cdot T$
710	709	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - k) + j - j) T = 0 \cdot T$
711	701 702 710	3eqtr3d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T + (j - k) T = 0 \cdot T$
712	711	oveq2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = b - a + 0 \cdot T$
713	318	mul02d	$⊢ ψ \to 0 \cdot T = 0$
714	713	oveq2d	$⊢ ψ \to b - a + 0 \cdot T = b - a + 0$
715	364 368	subcld	$⊢ ψ \to b - a \in ℂ$
716	715	addid1d	$⊢ ψ \to b - a + 0 = b - a$
717	714 716	eqtrd	$⊢ ψ \to b - a + 0 \cdot T = b - a$
718	717	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a + 0 \cdot T = b - a$
719	712 718	eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = b - a$
720	694 698 719	3eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b + k T) - (a + j T) + (j - k) T = b - a$
721	720	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (b + k T) - (a + j T) + (j - k) T = b - a$
722	721	ad2antrr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \to (b + k T) - (a + j T) + (j - k) T = b - a$
723	692 722	breqtrd	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land a + j T \leq b + k T) \to E \leq b - a$
724		simpll	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land \neg a + j T \leq b + k T) \to (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A))$
725		simpr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg a + j T \leq b + k T) \to \neg a + j T \leq b + k T$
726	601	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℝ$
727	726	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg a + j T \leq b + k T) \to b + k T \in ℝ$
728	619	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j T \in ℝ$
729	728	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg a + j T \leq b + k T) \to a + j T \in ℝ$
730	727 729	ltnled	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg a + j T \leq b + k T) \to (b + k T < a + j T \leftrightarrow \neg a + j T \leq b + k T)$
731	725 730	mpbird	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land \neg a + j T \leq b + k T) \to b + k T < a + j T$
732	731	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land \neg a + j T \leq b + k T) \to b + k T < a + j T$
733	535	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to k = \frac{b + k T - b}{T}$
734	733	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to k = \frac{b + k T - b}{T}$
735	600	3adant2	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b + k T \in ℝ$
736	302	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b \in ℝ$
737	735 736	resubcld	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b + k T - b \in ℝ$
738	293	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to T \in ℝ$
739	531	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to T \neq 0$
740	737 738 739	redivcld	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to \frac{b + k T - b}{T} \in ℝ$
741	740	3adant3l	$⊢ (ψ \land k \in ℤ \land (a + j T \in A \land b + k T \in A)) \to \frac{b + k T - b}{T} \in ℝ$
742	741	3adant2l	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to \frac{b + k T - b}{T} \in ℝ$
743	742	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to \frac{b + k T - b}{T} \in ℝ$
744	618	3adant2	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T \in ℝ$
745	302	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to b \in ℝ$
746	744 745	resubcld	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T - b \in ℝ$
747	293	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to T \in ℝ$
748	531	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to T \neq 0$
749	746 747 748	redivcld	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to \frac{a + j T - b}{T} \in ℝ$
750	749	3adant3r	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + k T \in A)) \to \frac{a + j T - b}{T} \in ℝ$
751	750	3adant2r	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to \frac{a + j T - b}{T} \in ℝ$
752	751	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to \frac{a + j T - b}{T} \in ℝ$
753	284	3ad2ant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j \in ℝ$
754	753	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to j \in ℝ$
755	726	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T \in ℝ$
756	302	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b \in ℝ$
757	756	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b \in ℝ$
758	755 757	resubcld	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T - b \in ℝ$
759	728	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to a + j T \in ℝ$
760	759 757	resubcld	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to a + j T - b \in ℝ$
761	352	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to T \in ℝ^{+}$
762	761	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to T \in ℝ^{+}$
763	601	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T \in ℝ$
764	619	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to a + j T \in ℝ$
765	302	ad2antrr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b \in ℝ$
766		simpr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T < a + j T$
767	763 764 765 766	ltsub1dd	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T - b < a + j T - b$
768	767	3adantl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b + k T - b < a + j T - b$
769	758 760 762 768	ltdiv1dd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to \frac{b + k T - b}{T} < \frac{a + j T - b}{T}$
770	554 570	eqbrtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to \frac{a + j T - b}{T} < j$
771	770	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to \frac{a + j T - b}{T} < j$
772	771	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to \frac{a + j T - b}{T} < j$
773	743 752 754 769 772	lttrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to \frac{b + k T - b}{T} < j$
774	734 773	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to k < j$
775	774	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land b + k T < a + j T) \to k < j$
776	732 775	syldan	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land \neg a + j T \leq b + k T) \to k < j$
777	391	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to E \in ℝ$
778	393	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to T \in ℝ$
779	623	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to (b + k T) - (a + j T) + (j - k) T \in ℝ$
780	522	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to E \leq T$
781		peano2rem	$⊢ j \in ℝ \to j - 1 \in ℝ$
782	753 781	syl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j - 1 \in ℝ$
783	287	3ad2ant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to k \in ℝ$
784	782 783	resubcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j - 1 - k \in ℝ$
785	784 393	remulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - 1 - k) T \in ℝ$
786	785	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to (j - 1 - k) T \in ℝ$
787	753	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to j \in ℝ$
788	330	a1i	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to 1 \in ℝ$
789	787 788	resubcld	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to j - 1 \in ℝ$
790	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \in ℝ$
791	790	3ad2antl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to k \in ℝ$
792	789 791	resubcld	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to j - 1 - k \in ℝ$
793	682	adantr	$⊢ (ψ \land k < j - 1) \to 0 \leq T$
794	793	3ad2antl1	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to 0 \leq T$
795	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j \in ℝ$
796	330	a1i	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \in ℝ$
797	795 796	resubcld	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j - 1 \in ℝ$
798		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k < j - 1$
799		simplr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \in ℤ$
800		simpll	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j \in ℤ$
801		1zzd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \in ℤ$
802	800 801	zsubcld	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j - 1 \in ℤ$
803		zltlem1	$⊢ (k \in ℤ \land j - 1 \in ℤ) \to (k < j - 1 \leftrightarrow k \leq j - 1 - 1)$
804	799 802 803	syl2anc	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to (k < j - 1 \leftrightarrow k \leq j - 1 - 1)$
805	798 804	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \leq j - 1 - 1$
806	790 797 796 805	lesubd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \leq j - 1 - k$
807	806	3ad2antl2	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to 1 \leq j - 1 - k$
808	778 792 794 807	lemulge12d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to T \leq (j - 1 - k) T$
809	336 337 341	sub32d	$⊢ (j \in ℤ \land k \in ℤ) \to j - 1 - k = j - k - 1$
810	809	oveq1d	$⊢ (j \in ℤ \land k \in ℤ) \to (j - 1 - k) T = (j - k - 1) T$
811	810	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - 1 - k) T = (j - k - 1) T$
812		1cnd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to 1 \in ℂ$
813	609 812 375	subdird	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k - 1) T = (j - k) T - 1 T$
814	319	oveq2d	$⊢ ψ \to (j - k) T - 1 T = (j - k) T - T$
815	814	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k) T - 1 T = (j - k) T - T$
816	811 813 815	3eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - 1 - k) T = (j - k) T - T$
817	816	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - 1 - k) T = (j - k) T - T$
818	728 726	resubcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j T - (b + k T) \in ℝ$
819	270 272 277 275	iccsuble	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T - (b + k T) \leq C - B$
820	819 4	breqtrrdi	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T - (b + k T) \leq T$
821	820	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j T - (b + k T) \leq T$
822	818 393 398 821	lesub2dd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T - T \leq (j - k) T - (a + j T - (b + k T))$
823	817 822	eqbrtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - 1 - k) T \leq (j - k) T - (a + j T - (b + k T))$
824	610	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T \in ℂ$
825	728	recnd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j T \in ℂ$
826	602	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℂ$
827	824 825 826	subsub2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T - (a + j T - (b + k T)) = (j - k) T + (b + k T) - (a + j T)$
828	621	recnd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \in ℂ$
829	824 828	addcomd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T + (b + k T) - (a + j T) = (b + k T) - (a + j T) + (j - k) T$
830	827 829	eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T - (a + j T - (b + k T)) = (b + k T) - (a + j T) + (j - k) T$
831	823 830	breqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - 1 - k) T \leq (b + k T) - (a + j T) + (j - k) T$
832	831	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to (j - 1 - k) T \leq (b + k T) - (a + j T) + (j - k) T$
833	778 786 779 808 832	letrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to T \leq (b + k T) - (a + j T) + (j - k) T$
834	777 778 779 780 833	letrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to E \leq (b + k T) - (a + j T) + (j - k) T$
835	721	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to (b + k T) - (a + j T) + (j - k) T = b - a$
836	834 835	breqtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j - 1) \to E \leq b - a$
837	836	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land k < j - 1) \to E \leq b - a$
838	837	adantlr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land b + k T < a + j T) \land k < j - 1) \to E \leq b - a$
839		simplll	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land b + k T < a + j T) \land \neg k < j - 1) \to (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A))$
840		simpll2	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land \neg k < j - 1) \to (j \in ℤ \land k \in ℤ)$
841		simplr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land \neg k < j - 1) \to k < j$
842		simpr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land \neg k < j - 1) \to \neg k < j - 1$
843	581 582 580 584	lesubd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \leq j - 1$
844	843	3adant3	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k \leq j - 1$
845		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to \neg k < j - 1$
846	284 781	syl	$⊢ (j \in ℤ \land k \in ℤ) \to j - 1 \in ℝ$
847	846	adantr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to j - 1 \in ℝ$
848	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to k \in ℝ$
849	847 848	lenltd	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to (j - 1 \leq k \leftrightarrow \neg k < j - 1)$
850	845 849	mpbird	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to j - 1 \leq k$
851	850	3adant2	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to j - 1 \leq k$
852	580	3adant3	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k \in ℝ$
853	846	3ad2ant1	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to j - 1 \in ℝ$
854	852 853	letri3d	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to (k = j - 1 \leftrightarrow (k \leq j - 1 \land j - 1 \leq k))$
855	844 851 854	mpbir2and	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k = j - 1$
856	840 841 842 855	syl3anc	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land \neg k < j - 1) \to k = j - 1$
857	856	adantlr	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land b + k T < a + j T) \land \neg k < j - 1) \to k = j - 1$
858		simpl1	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to ψ$
859		simpl2l	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to j \in ℤ$
860		simpl3l	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to a + j T \in A$
861		oveq1	$⊢ k = j - 1 \to k T = (j - 1) T$
862	861	oveq2d	$⊢ k = j - 1 \to b + k T = b + (j - 1) T$
863	862	eqcomd	$⊢ k = j - 1 \to b + (j - 1) T = b + k T$
864	863	adantl	$⊢ (b + k T \in A \land k = j - 1) \to b + (j - 1) T = b + k T$
865		simpl	$⊢ (b + k T \in A \land k = j - 1) \to b + k T \in A$
866	864 865	eqeltrd	$⊢ (b + k T \in A \land k = j - 1) \to b + (j - 1) T \in A$
867	866	adantll	$⊢ ((a + j T \in A \land b + k T \in A) \land k = j - 1) \to b + (j - 1) T \in A$
868	867	3ad2antl3	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to b + (j - 1) T \in A$
869	860 868	jca	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to (a + j T \in A \land b + (j - 1) T \in A)$
870		id	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to (ψ \land j \in ℤ \land a + j T \in A)$
871	870	3adant3r	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (ψ \land j \in ℤ \land a + j T \in A)$
872	744	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T \in ℝ$
873	271	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to C \in ℝ$
874	873	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to C \in ℝ$
875	269	adantr	$⊢ (ψ \land a + j T \in A) \to B \in ℝ$
876	271	adantr	$⊢ (ψ \land a + j T \in A) \to C \in ℝ$
877		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (a + j T \in [B, C] \leftrightarrow (a + j T \in ℝ \land B \leq a + j T \land a + j T \leq C))$
878	875 876 877	syl2anc	$⊢ (ψ \land a + j T \in A) \to (a + j T \in [B, C] \leftrightarrow (a + j T \in ℝ \land B \leq a + j T \land a + j T \leq C))$
879	276 878	mpbid	$⊢ (ψ \land a + j T \in A) \to (a + j T \in ℝ \land B \leq a + j T \land a + j T \leq C)$
880	879	simp3d	$⊢ (ψ \land a + j T \in A) \to a + j T \leq C$
881	880	3adant2	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T \leq C$
882	881	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T \leq C$
883		nne	$⊢ \neg C \neq a + j T \leftrightarrow C = a + j T$
884	540 370	pncand	$⊢ (ψ \land j \in ℤ) \to a + j T - j T = a$
885	884	eqcomd	$⊢ (ψ \land j \in ℤ) \to a = a + j T - j T$
886	885	adantr	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a = a + j T - j T$
887		oveq1	$⊢ C = a + j T \to C - j T = a + j T - j T$
888	887	eqcomd	$⊢ C = a + j T \to a + j T - j T = C - j T$
889	888	adantl	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a + j T - j T = C - j T$
890	4	oveq2i	$⊢ B + T = B + C - B$
891	268 161	syl	$⊢ ψ \to B \in ℂ$
892	268 162	syl	$⊢ ψ \to C \in ℂ$
893	891 892	pncan3d	$⊢ ψ \to B + C - B = C$
894	890 893	eqtr2id	$⊢ ψ \to C = B + T$
895	894	oveq1d	$⊢ ψ \to C - j T = B + T - j T$
896	895	adantr	$⊢ (ψ \land j \in ℤ) \to C - j T = B + T - j T$
897	891	adantr	$⊢ (ψ \land j \in ℤ) \to B \in ℂ$
898	897 370 547	subsub3d	$⊢ (ψ \land j \in ℤ) \to B - (j T - T) = B + T - j T$
899	550 547	mulsubfacd	$⊢ (ψ \land j \in ℤ) \to j T - T = (j - 1) T$
900	899	oveq2d	$⊢ (ψ \land j \in ℤ) \to B - (j T - T) = B - (j - 1) T$
901	896 898 900	3eqtr2d	$⊢ (ψ \land j \in ℤ) \to C - j T = B - (j - 1) T$
902	901	adantr	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to C - j T = B - (j - 1) T$
903	886 889 902	3eqtrd	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a = B - (j - 1) T$
904	903	3adantl3	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land C = a + j T) \to a = B - (j - 1) T$
905	904	adantlr	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land C = a + j T) \to a = B - (j - 1) T$
906		oveq1	$⊢ b + (j - 1) T = B \to b + (j - 1) T - (j - 1) T = B - (j - 1) T$
907	906	eqcomd	$⊢ b + (j - 1) T = B \to B - (j - 1) T = b + (j - 1) T - (j - 1) T$
908	907	ad2antlr	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land C = a + j T) \to B - (j - 1) T = b + (j - 1) T - (j - 1) T$
909	364	ad2antrr	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to b \in ℂ$
910		1cnd	$⊢ (ψ \land j \in ℤ) \to 1 \in ℂ$
911	550 910	subcld	$⊢ (ψ \land j \in ℤ) \to j - 1 \in ℂ$
912	911 547	mulcld	$⊢ (ψ \land j \in ℤ) \to (j - 1) T \in ℂ$
913	912	adantr	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to (j - 1) T \in ℂ$
914	909 913	pncand	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to b + (j - 1) T - (j - 1) T = b$
915	914	3adantl3	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to b + (j - 1) T - (j - 1) T = b$
916	915	adantr	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land C = a + j T) \to b + (j - 1) T - (j - 1) T = b$
917	905 908 916	3eqtrd	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land C = a + j T) \to a = b$
918	883 917	sylan2b	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land \neg C \neq a + j T) \to a = b$
919	309 358	ltned	$⊢ ψ \to a \neq b$
920	919	neneqd	$⊢ ψ \to \neg a = b$
921	920	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to \neg a = b$
922	921	ad2antrr	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land \neg C \neq a + j T) \to \neg a = b$
923	918 922	condan	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to C \neq a + j T$
924	872 874 882 923	leneltd	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T < C$
925	871 924	sylan	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to a + j T < C$
926	268	ad2antrr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to φ$
927		simplr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to a + j T \in A$
928	926 8	syl	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to C \in A$
929		simpr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to a + j T < C$
930		simp2l	$⊢ (φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to a + j T \in A$
931	654	anbi1d	$⊢ c = a + j T \to ((c \in A \land C \in A) \leftrightarrow (a + j T \in A \land C \in A))$
932		breq1	$⊢ c = a + j T \to (c < C \leftrightarrow a + j T < C)$
933	931 932	3anbi23d	$⊢ c = a + j T \to ((φ \land (c \in A \land C \in A) \land c < C) \leftrightarrow (φ \land (a + j T \in A \land C \in A) \land a + j T < C))$
934		oveq2	$⊢ c = a + j T \to C - c = C - (a + j T)$
935	934	breq2d	$⊢ c = a + j T \to (E \leq C - c \leftrightarrow E \leq C - (a + j T))$
936	933 935	imbi12d	$⊢ c = a + j T \to (((φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c) \leftrightarrow ((φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to E \leq C - (a + j T)))$
937		simp2r	$⊢ (φ \land (c \in A \land C \in A) \land c < C) \to C \in A$
938	403	anbi2d	$⊢ d = C \to ((c \in A \land d \in A) \leftrightarrow (c \in A \land C \in A))$
939		breq2	$⊢ d = C \to (c < d \leftrightarrow c < C)$
940	938 939	3anbi23d	$⊢ d = C \to ((φ \land (c \in A \land d \in A) \land c < d) \leftrightarrow (φ \land (c \in A \land C \in A) \land c < C))$
941		oveq1	$⊢ d = C \to d - c = C - c$
942	941	breq2d	$⊢ d = C \to (E \leq d - c \leftrightarrow E \leq C - c)$
943	940 942	imbi12d	$⊢ d = C \to (((φ \land (c \in A \land d \in A) \land c < d) \to E \leq d - c) \leftrightarrow ((φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c))$
944	943 515	vtoclg	$⊢ C \in A \to ((φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c)$
945	937 944	mpcom	$⊢ (φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c$
946	936 945	vtoclg	$⊢ a + j T \in A \to ((φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to E \leq C - (a + j T))$
947	930 946	mpcom	$⊢ (φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to E \leq C - (a + j T)$
948	926 927 928 929 947	syl121anc	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to E \leq C - (a + j T)$
949	948	adantlrr	$⊢ ((ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \land a + j T < C) \to E \leq C - (a + j T)$
950	949	3adantl2	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land a + j T < C) \to E \leq C - (a + j T)$
951	950	adantlr	$⊢ (((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \land a + j T < C) \to E \leq C - (a + j T)$
952	892	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to C \in ℂ$
953	599	sselda	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in ℝ$
954	953	recnd	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in ℂ$
955	952 954	npcand	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - (b + (j - 1) T)) + b + (j - 1) T = C$
956	955	eqcomd	$⊢ (ψ \land b + (j - 1) T \in A) \to C = (C - (b + (j - 1) T)) + b + (j - 1) T$
957	956	oveq1d	$⊢ (ψ \land b + (j - 1) T \in A) \to C - (a + j T) = (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T)$
958	957	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C - (a + j T) = (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T)$
959	958	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C - (a + j T) = (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T)$
960	959	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to C - (a + j T) = (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T)$
961		oveq2	$⊢ b + (j - 1) T = B \to C - (b + (j - 1) T) = C - B$
962	961	oveq1d	$⊢ b + (j - 1) T = B \to (C - (b + (j - 1) T)) + b + (j - 1) T = (C - B) + b + (j - 1) T$
963	962	oveq1d	$⊢ b + (j - 1) T = B \to (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T) = (C - B) + (b + (j - 1) T) - (a + j T)$
964	963	adantl	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to (C - (b + (j - 1) T)) + (b + (j - 1) T) - (a + j T) = (C - B) + (b + (j - 1) T) - (a + j T)$
965	4	eqcomi	$⊢ C - B = T$
966	965	oveq1i	$⊢ (C - B) + b + (j - 1) T = T + b + (j - 1) T$
967	966	a1i	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - B) + b + (j - 1) T = T + b + (j - 1) T$
968	318	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to T \in ℂ$
969	968 954	addcomd	$⊢ (ψ \land b + (j - 1) T \in A) \to T + b + (j - 1) T = b + (j - 1) T + T$
970	967 969	eqtrd	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - B) + b + (j - 1) T = b + (j - 1) T + T$
971	970	oveq1d	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - B) + (b + (j - 1) T) - (a + j T) = (b + (j - 1) T) + T - (a + j T)$
972	971	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (C - B) + (b + (j - 1) T) - (a + j T) = (b + (j - 1) T) + T - (a + j T)$
973	972	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (C - B) + (b + (j - 1) T) - (a + j T) = (b + (j - 1) T) + T - (a + j T)$
974	973	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to (C - B) + (b + (j - 1) T) - (a + j T) = (b + (j - 1) T) + T - (a + j T)$
975	954	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℂ$
976	975	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℂ$
977	976	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to b + (j - 1) T \in ℂ$
978	318	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to T \in ℂ$
979	978	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to T \in ℂ$
980	618	adantrr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℝ$
981	980	recnd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℂ$
982	981	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℂ$
983	982	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to a + j T \in ℂ$
984	977 979 983	addsubd	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to (b + (j - 1) T) + T - (a + j T) = (b + (j - 1) T) - (a + j T) + T$
985	974 984	eqtrd	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to (C - B) + (b + (j - 1) T) - (a + j T) = (b + (j - 1) T) - (a + j T) + T$
986	960 964 985	3eqtrd	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to C - (a + j T) = (b + (j - 1) T) - (a + j T) + T$
987	986	adantr	$⊢ (((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \land a + j T < C) \to C - (a + j T) = (b + (j - 1) T) - (a + j T) + T$
988	951 987	breqtrd	$⊢ (((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \land a + j T < C) \to E \leq (b + (j - 1) T) - (a + j T) + T$
989	925 988	mpdan	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land b + (j - 1) T = B) \to E \leq (b + (j - 1) T) - (a + j T) + T$
990		simpl1	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land \neg b + (j - 1) T = B) \to ψ$
991		simpl3r	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land \neg b + (j - 1) T = B) \to b + (j - 1) T \in A$
992		simpr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land \neg b + (j - 1) T = B) \to \neg b + (j - 1) T = B$
993	269	3ad2ant1	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B \in ℝ$
994	953	3adant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to b + (j - 1) T \in ℝ$
995	273	sselda	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in [B, C]$
996	269	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to B \in ℝ$
997	271	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to C \in ℝ$
998		elicc2	$⊢ (B \in ℝ \land C \in ℝ) \to (b + (j - 1) T \in [B, C] \leftrightarrow (b + (j - 1) T \in ℝ \land B \leq b + (j - 1) T \land b + (j - 1) T \leq C))$
999	996 997 998	syl2anc	$⊢ (ψ \land b + (j - 1) T \in A) \to (b + (j - 1) T \in [B, C] \leftrightarrow (b + (j - 1) T \in ℝ \land B \leq b + (j - 1) T \land b + (j - 1) T \leq C))$
1000	995 999	mpbid	$⊢ (ψ \land b + (j - 1) T \in A) \to (b + (j - 1) T \in ℝ \land B \leq b + (j - 1) T \land b + (j - 1) T \leq C)$
1001	1000	simp2d	$⊢ (ψ \land b + (j - 1) T \in A) \to B \leq b + (j - 1) T$
1002	1001	3adant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B \leq b + (j - 1) T$
1003		neqne	$⊢ \neg b + (j - 1) T = B \to b + (j - 1) T \neq B$
1004	1003	3ad2ant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to b + (j - 1) T \neq B$
1005	993 994 1002 1004	leneltd	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B < b + (j - 1) T$
1006	990 991 992 1005	syl3anc	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land \neg b + (j - 1) T = B) \to B < b + (j - 1) T$
1007	390	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to E \in ℝ$
1008	1007	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to E \in ℝ$
1009	953	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℝ$
1010	1009	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℝ$
1011	269	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℝ$
1012	1010 1011	resubcld	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B \in ℝ$
1013	1012	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to b + (j - 1) T - B \in ℝ$
1014	1009 980	resubcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - (a + j T) \in ℝ$
1015	293	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to T \in ℝ$
1016	1014 1015	readdcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T) - (a + j T) + T \in ℝ$
1017	1016	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T) - (a + j T) + T \in ℝ$
1018	1017	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to (b + (j - 1) T) - (a + j T) + T \in ℝ$
1019	268	adantr	$⊢ (ψ \land B < b + (j - 1) T) \to φ$
1020	1019	3ad2antl1	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to φ$
1021	1020 7	syl	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to B \in A$
1022		simpl3r	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to b + (j - 1) T \in A$
1023		simpr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to B < b + (j - 1) T$
1024		simp2r	$⊢ (φ \land (B \in A \land b + (j - 1) T \in A) \land B < b + (j - 1) T) \to b + (j - 1) T \in A$
1025		eleq1	$⊢ d = b + (j - 1) T \to (d \in A \leftrightarrow b + (j - 1) T \in A)$
1026	1025	anbi2d	$⊢ d = b + (j - 1) T \to ((B \in A \land d \in A) \leftrightarrow (B \in A \land b + (j - 1) T \in A))$
1027		breq2	$⊢ d = b + (j - 1) T \to (B < d \leftrightarrow B < b + (j - 1) T)$
1028	1026 1027	3anbi23d	$⊢ d = b + (j - 1) T \to ((φ \land (B \in A \land d \in A) \land B < d) \leftrightarrow (φ \land (B \in A \land b + (j - 1) T \in A) \land B < b + (j - 1) T))$
1029		oveq1	$⊢ d = b + (j - 1) T \to d - B = b + (j - 1) T - B$
1030	1029	breq2d	$⊢ d = b + (j - 1) T \to (E \leq d - B \leftrightarrow E \leq b + (j - 1) T - B)$
1031	1028 1030	imbi12d	$⊢ d = b + (j - 1) T \to (((φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B) \leftrightarrow ((φ \land (B \in A \land b + (j - 1) T \in A) \land B < b + (j - 1) T) \to E \leq b + (j - 1) T - B))$
1032	1031 517	vtoclg	$⊢ b + (j - 1) T \in A \to ((φ \land (B \in A \land b + (j - 1) T \in A) \land B < b + (j - 1) T) \to E \leq b + (j - 1) T - B)$
1033	1024 1032	mpcom	$⊢ (φ \land (B \in A \land b + (j - 1) T \in A) \land B < b + (j - 1) T) \to E \leq b + (j - 1) T - B$
1034	1020 1021 1022 1023 1033	syl121anc	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to E \leq b + (j - 1) T - B$
1035	269	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℝ$
1036	980 1035	resubcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T - B \in ℝ$
1037	965 1015	eqeltrid	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C - B \in ℝ$
1038	271	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C \in ℝ$
1039	880	adantrr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \leq C$
1040	980 1038 1035 1039	lesub1dd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T - B \leq C - B$
1041	1036 1037 1014 1040	leadd2dd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T - (a + j T)) + (a + j T) - B \leq (b + (j - 1) T - (a + j T)) + C - B$
1042	975 981	npcand	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T - (a + j T)) + a + j T = b + (j - 1) T$
1043	1042	eqcomd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T = (b + (j - 1) T - (a + j T)) + a + j T$
1044	1043	oveq1d	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B = (b + (j - 1) T - (a + j T)) + (a + j T) - B$
1045	1014	recnd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - (a + j T) \in ℂ$
1046	891	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℂ$
1047	1045 981 1046	addsubassd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T - (a + j T)) + (a + j T) - B = (b + (j - 1) T - (a + j T)) + (a + j T) - B$
1048	1044 1047	eqtrd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B = (b + (j - 1) T - (a + j T)) + (a + j T) - B$
1049	4	oveq2i	$⊢ (b + (j - 1) T) - (a + j T) + T = (b + (j - 1) T - (a + j T)) + C - B$
1050	1049	a1i	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T) - (a + j T) + T = (b + (j - 1) T - (a + j T)) + C - B$
1051	1041 1048 1050	3brtr4d	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B \leq (b + (j - 1) T) - (a + j T) + T$
1052	1051	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B \leq (b + (j - 1) T) - (a + j T) + T$
1053	1052	adantr	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to b + (j - 1) T - B \leq (b + (j - 1) T) - (a + j T) + T$
1054	1008 1013 1018 1034 1053	letrd	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to E \leq (b + (j - 1) T) - (a + j T) + T$
1055	1006 1054	syldan	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land \neg b + (j - 1) T = B) \to E \leq (b + (j - 1) T) - (a + j T) + T$
1056	989 1055	pm2.61dan	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to E \leq (b + (j - 1) T) - (a + j T) + T$
1057	858 859 869 1056	syl3anc	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to E \leq (b + (j - 1) T) - (a + j T) + T$
1058	720	eqcomd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a = (b + k T) - (a + j T) + (j - k) T$
1059	1058	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k = j - 1) \to b - a = (b + k T) - (a + j T) + (j - k) T$
1060	862	oveq1d	$⊢ k = j - 1 \to b + k T - (a + j T) = b + (j - 1) T - (a + j T)$
1061	1060	adantl	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to b + k T - (a + j T) = b + (j - 1) T - (a + j T)$
1062		oveq2	$⊢ k = j - 1 \to j - k = j - (j - 1)$
1063	1062	oveq1d	$⊢ k = j - 1 \to (j - k) T = (j - (j - 1)) T$
1064	1063	adantl	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - k) T = (j - (j - 1)) T$
1065		1cnd	$⊢ j \in ℤ \to 1 \in ℂ$
1066	335 1065	nncand	$⊢ j \in ℤ \to j - (j - 1) = 1$
1067	1066	oveq1d	$⊢ j \in ℤ \to (j - (j - 1)) T = 1 T$
1068	1067	ad2antlr	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - (j - 1)) T = 1 T$
1069	319	ad2antrr	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to 1 T = T$
1070	1064 1068 1069	3eqtrd	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - k) T = T$
1071	1061 1070	oveq12d	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (b + k T) - (a + j T) + (j - k) T = (b + (j - 1) T) - (a + j T) + T$
1072	1071	adantlrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k = j - 1) \to (b + k T) - (a + j T) + (j - k) T = (b + (j - 1) T) - (a + j T) + T$
1073	1059 1072	eqtr2d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k = j - 1) \to (b + (j - 1) T) - (a + j T) + T = b - a$
1074	1073	3adantl3	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to (b + (j - 1) T) - (a + j T) + T = b - a$
1075	1057 1074	breqtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to E \leq b - a$
1076	839 857 1075	syl2anc	$⊢ ((((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land b + k T < a + j T) \land \neg k < j - 1) \to E \leq b - a$
1077	838 1076	pm2.61dan	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k < j) \land b + k T < a + j T) \to E \leq b - a$
1078	724 776 732 1077	syl21anc	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \land \neg a + j T \leq b + k T) \to E \leq b - a$
1079	723 1078	pm2.61dan	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to E \leq b - a$
1080	387 1079	mpdan	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq b - a$
1081	309 302 358	ltled	$⊢ ψ \to a \leq b$
1082	309 302 1081	abssuble0d	$⊢ ψ \to \|a - b\| = b - a$
1083	1082	eqcomd	$⊢ ψ \to b - a = \|a - b\|$
1084	1083	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b - a = \|a - b\|$
1085	1080 1084	breqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq \|a - b\|$
1086	1085	3exp	$⊢ ψ \to ((j \in ℤ \land k \in ℤ) \to ((a + j T \in A \land b + k T \in A) \to E \leq \|a - b\|))$
1087	1086	rexlimdvv	$⊢ ψ \to (\exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A) \to E \leq \|a - b\|)$
1088	265 1087	mpd	$⊢ ψ \to E \leq \|a - b\|$
1089	18 1088	sylbir	$⊢ ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)) \to E \leq \|a - b\|$
1090	264 1089	chvarvv	$⊢ ((φ \land (y \in ℝ \land b \in ℝ \land y < b)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land b + k T \in A)) \to E \leq \|y - b\|$
1091	251 1090	chvarvv	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y < z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \to E \leq \|y - z\|$
1092	231 237 238 1091	syl21anc	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land y < z) \to E \leq \|y - z\|$
1093		simpr	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to \neg y < z$
1094		simpl3	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to y \neq z$
1095		simpl1	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to y \in ℝ$
1096		simpl2	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to z \in ℝ$
1097	1095 1096	lttri2d	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (y \neq z \leftrightarrow (y < z \lor z < y))$
1098	1094 1097	mpbid	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (y < z \lor z < y)$
1099	1098	ord	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (\neg y < z \to z < y)$
1100	1093 1099	mpd	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to z < y$
1101	1100	adantll	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \neg y < z) \to z < y$
1102	1101	adantlr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land \neg y < z) \to z < y$
1103		simplll	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to φ$
1104		simplr	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to z \in ℝ$
1105		simpll	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to y \in ℝ$
1106		simpr	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to z < y$
1107	1104 1105 1106	3jca	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to (z \in ℝ \land y \in ℝ \land z < y)$
1108	1107	adantll	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land z < y) \to (z \in ℝ \land y \in ℝ \land z < y)$
1109	1108	adantlr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to (z \in ℝ \land y \in ℝ \land z < y)$
1110		oveq1	$⊢ j = i \to j T = i T$
1111	1110	oveq2d	$⊢ j = i \to y + j T = y + i T$
1112	1111	eleq1d	$⊢ j = i \to (y + j T \in A \leftrightarrow y + i T \in A)$
1113	1112	anbi1d	$⊢ j = i \to ((y + j T \in A \land z + k T \in A) \leftrightarrow (y + i T \in A \land z + k T \in A))$
1114		oveq1	$⊢ k = l \to k T = l T$
1115	1114	oveq2d	$⊢ k = l \to z + k T = z + l T$
1116	1115	eleq1d	$⊢ k = l \to (z + k T \in A \leftrightarrow z + l T \in A)$
1117	1116	anbi2d	$⊢ k = l \to ((y + i T \in A \land z + k T \in A) \leftrightarrow (y + i T \in A \land z + l T \in A))$
1118	1113 1117	cbvrex2vw	$⊢ \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A) \leftrightarrow \exists i \in ℤ \exists l \in ℤ (y + i T \in A \land z + l T \in A)$
1119		oveq1	$⊢ i = k \to i T = k T$
1120	1119	oveq2d	$⊢ i = k \to y + i T = y + k T$
1121	1120	eleq1d	$⊢ i = k \to (y + i T \in A \leftrightarrow y + k T \in A)$
1122	1121	anbi1d	$⊢ i = k \to ((y + i T \in A \land z + l T \in A) \leftrightarrow (y + k T \in A \land z + l T \in A))$
1123		oveq1	$⊢ l = j \to l T = j T$
1124	1123	oveq2d	$⊢ l = j \to z + l T = z + j T$
1125	1124	eleq1d	$⊢ l = j \to (z + l T \in A \leftrightarrow z + j T \in A)$
1126	1125	anbi2d	$⊢ l = j \to ((y + k T \in A \land z + l T \in A) \leftrightarrow (y + k T \in A \land z + j T \in A))$
1127	1122 1126	cbvrex2vw	$⊢ \exists i \in ℤ \exists l \in ℤ (y + i T \in A \land z + l T \in A) \leftrightarrow \exists k \in ℤ \exists j \in ℤ (y + k T \in A \land z + j T \in A)$
1128		rexcom	$⊢ \exists k \in ℤ \exists j \in ℤ (y + k T \in A \land z + j T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (y + k T \in A \land z + j T \in A)$
1129		ancom	$⊢ (y + k T \in A \land z + j T \in A) \leftrightarrow (z + j T \in A \land y + k T \in A)$
1130	1129	2rexbii	$⊢ \exists j \in ℤ \exists k \in ℤ (y + k T \in A \land z + j T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)$
1131	1127 1128 1130	3bitri	$⊢ \exists i \in ℤ \exists l \in ℤ (y + i T \in A \land z + l T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)$
1132	1118 1131	sylbb	$⊢ \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A) \to \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)$
1133	1132	ad2antlr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)$
1134		eleq1	$⊢ b = y \to (b \in ℝ \leftrightarrow y \in ℝ)$
1135		breq2	$⊢ b = y \to (z < b \leftrightarrow z < y)$
1136	1134 1135	3anbi23d	$⊢ b = y \to ((z \in ℝ \land b \in ℝ \land z < b) \leftrightarrow (z \in ℝ \land y \in ℝ \land z < y))$
1137	1136	anbi2d	$⊢ b = y \to ((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \leftrightarrow (φ \land (z \in ℝ \land y \in ℝ \land z < y)))$
1138		oveq1	$⊢ b = y \to b + k T = y + k T$
1139	1138	eleq1d	$⊢ b = y \to (b + k T \in A \leftrightarrow y + k T \in A)$
1140	1139	anbi2d	$⊢ b = y \to ((z + j T \in A \land b + k T \in A) \leftrightarrow (z + j T \in A \land y + k T \in A))$
1141	1140	2rexbidv	$⊢ b = y \to (\exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A))$
1142	1137 1141	anbi12d	$⊢ b = y \to (((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A)) \leftrightarrow ((φ \land (z \in ℝ \land y \in ℝ \land z < y)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)))$
1143		oveq2	$⊢ b = y \to z - b = z - y$
1144	1143	fveq2d	$⊢ b = y \to \|z - b\| = \|z - y\|$
1145	1144	breq2d	$⊢ b = y \to (E \leq \|z - b\| \leftrightarrow E \leq \|z - y\|)$
1146	1142 1145	imbi12d	$⊢ b = y \to ((((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A)) \to E \leq \|z - b\|) \leftrightarrow (((φ \land (z \in ℝ \land y \in ℝ \land z < y)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)) \to E \leq \|z - y\|))$
1147		eleq1	$⊢ a = z \to (a \in ℝ \leftrightarrow z \in ℝ)$
1148		breq1	$⊢ a = z \to (a < b \leftrightarrow z < b)$
1149	1147 1148	3anbi13d	$⊢ a = z \to ((a \in ℝ \land b \in ℝ \land a < b) \leftrightarrow (z \in ℝ \land b \in ℝ \land z < b))$
1150	1149	anbi2d	$⊢ a = z \to ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \leftrightarrow (φ \land (z \in ℝ \land b \in ℝ \land z < b)))$
1151		oveq1	$⊢ a = z \to a + j T = z + j T$
1152	1151	eleq1d	$⊢ a = z \to (a + j T \in A \leftrightarrow z + j T \in A)$
1153	1152	anbi1d	$⊢ a = z \to ((a + j T \in A \land b + k T \in A) \leftrightarrow (z + j T \in A \land b + k T \in A))$
1154	1153	2rexbidv	$⊢ a = z \to (\exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A) \leftrightarrow \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A))$
1155	1150 1154	anbi12d	$⊢ a = z \to (((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)) \leftrightarrow ((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A)))$
1156		oveq1	$⊢ a = z \to a - b = z - b$
1157	1156	fveq2d	$⊢ a = z \to \|a - b\| = \|z - b\|$
1158	1157	breq2d	$⊢ a = z \to (E \leq \|a - b\| \leftrightarrow E \leq \|z - b\|)$
1159	1155 1158	imbi12d	$⊢ a = z \to ((((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \land \exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A)) \to E \leq \|a - b\|) \leftrightarrow (((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A)) \to E \leq \|z - b\|))$
1160	1159 1089	chvarvv	$⊢ ((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land b + k T \in A)) \to E \leq \|z - b\|$
1161	1146 1160	chvarvv	$⊢ ((φ \land (z \in ℝ \land y \in ℝ \land z < y)) \land \exists j \in ℤ \exists k \in ℤ (z + j T \in A \land y + k T \in A)) \to E \leq \|z - y\|$
1162	1103 1109 1133 1161	syl21anc	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to E \leq \|z - y\|$
1163		recn	$⊢ z \in ℝ \to z \in ℂ$
1164	1163	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to z \in ℂ$
1165		recn	$⊢ y \in ℝ \to y \in ℂ$
1166	1165	adantr	$⊢ (y \in ℝ \land z \in ℝ) \to y \in ℂ$
1167	1164 1166	abssubd	$⊢ (y \in ℝ \land z \in ℝ) \to \|z - y\| = \|y - z\|$
1168	1167	adantl	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to \|z - y\| = \|y - z\|$
1169	1168	ad2antrr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to \|z - y\| = \|y - z\|$
1170	1162 1169	breqtrd	$⊢ (((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land z < y) \to E \leq \|y - z\|$
1171	1170	ex	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \to (z < y \to E \leq \|y - z\|)$
1172	1171	3adantlr3	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \to (z < y \to E \leq \|y - z\|)$
1173	1172	adantr	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land \neg y < z) \to (z < y \to E \leq \|y - z\|)$
1174	1102 1173	mpd	$⊢ (((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \land \neg y < z) \to E \leq \|y - z\|$
1175	1092 1174	pm2.61dan	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \exists j \in ℤ \exists k \in ℤ (y + j T \in A \land z + k T \in A)) \to E \leq \|y - z\|$
1176	198 206 230 1175	syl21anc	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to E \leq \|y - z\|$
1177	389	ad2antrr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to E \in ℝ$
1178	200 203	resubcld	$⊢ (φ \land (y \in H \land z \in H)) \to y - z \in ℝ$
1179	1178	recnd	$⊢ (φ \land (y \in H \land z \in H)) \to y - z \in ℂ$
1180	1179	abscld	$⊢ (φ \land (y \in H \land z \in H)) \to \|y - z\| \in ℝ$
1181	1180	adantr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to \|y - z\| \in ℝ$
1182	1177 1181	lenltd	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to (E \leq \|y - z\| \leftrightarrow \neg \|y - z\| < E)$
1183	1176 1182	mpbid	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to \neg \|y - z\| < E$
1184		nan	$⊢ ((φ \land (y \in H \land z \in H)) \to \neg (y \neq z \land \|y - z\| < E)) \leftrightarrow (((φ \land (y \in H \land z \in H)) \land y \neq z) \to \neg \|y - z\| < E)$
1185	1183 1184	mpbir	$⊢ (φ \land (y \in H \land z \in H)) \to \neg (y \neq z \land \|y - z\| < E)$
1186	1185	ralrimivva	$⊢ φ \to \forall y \in H \forall z \in H \neg (y \neq z \land \|y - z\| < E)$
1187		ralnex2	$⊢ \forall y \in H \forall z \in H \neg (y \neq z \land \|y - z\| < E) \leftrightarrow \neg \exists y \in H \exists z \in H (y \neq z \land \|y - z\| < E)$
1188	1186 1187	sylib	$⊢ φ \to \neg \exists y \in H \exists z \in H (y \neq z \land \|y - z\| < E)$
1189	1188	ad2antrr	$⊢ ((φ \land x \in ⋃ K) \land x \in limPt (J) (H)) \to \neg \exists y \in H \exists z \in H (y \neq z \land \|y - z\| < E)$
1190	197 1189	pm2.65da	$⊢ (φ \land x \in ⋃ K) \to \neg x \in limPt (J) (H)$
1191	1190	intnanrd	$⊢ (φ \land x \in ⋃ K) \to \neg (x \in limPt (J) (H) \land x \in [X, Y])$
1192		elin	$⊢ x \in (limPt (J) (H) \cap [X, Y]) \leftrightarrow (x \in limPt (J) (H) \land x \in [X, Y])$
1193	1191 1192	sylnibr	$⊢ (φ \land x \in ⋃ K) \to \neg x \in (limPt (J) (H) \cap [X, Y])$
1194	26	a1i	$⊢ (φ \land x \in ⋃ K) \to J \in Top$
1195	27	adantr	$⊢ (φ \land x \in ⋃ K) \to [X, Y] \subseteq ℝ$
1196	24	adantr	$⊢ (φ \land x \in ⋃ K) \to H \subseteq [X, Y]$
1197	30 16	restlp	$⊢ (J \in Top \land [X, Y] \subseteq ℝ \land H \subseteq [X, Y]) \to limPt (K) (H) = limPt (J) (H) \cap [X, Y]$
1198	1194 1195 1196 1197	syl3anc	$⊢ (φ \land x \in ⋃ K) \to limPt (K) (H) = limPt (J) (H) \cap [X, Y]$
1199	1193 1198	neleqtrrd	$⊢ (φ \land x \in ⋃ K) \to \neg x \in limPt (K) (H)$
1200	1199	nrexdv	$⊢ φ \to \neg \exists x \in ⋃ K x \in limPt (K) (H)$
1201	1200	adantr	$⊢ (φ \land \neg H \in Fin) \to \neg \exists x \in ⋃ K x \in limPt (K) (H)$
1202	41 1201	condan	$⊢ φ \to H \in Fin$

Metamath Proof Explorer

Theorem fourierdlem42

Proof