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 = inf (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 = inf (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	ffvelcdmd	$⊢ (φ \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 inf (R ℝ <) \in R$
193	133 143 179 191 192	syl13anc	$⊢ φ \to inf (R ℝ <) \in R$
194	131 193	sseldd	$⊢ φ \to inf (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	mullidd	$⊢ ψ \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	sselid	$⊢ φ \to inf (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	bilani	$⊢ (φ \land y \in R) \to y \in ran ({D ↾}_{I})$
422	67	adantr	$⊢ (φ \land y \in R) \to ({D ↾}_{I}) Fn I$
423		fvelrnb	$⊢ ({D ↾}_{I}) Fn I \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
424	422 423	syl	$⊢ (φ \land y \in R) \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
425	421 424	mpbid	$⊢ (φ \land y \in R) \to \exists x \in I ({D ↾}_{I}) (x) = y$
426	127	rpge0d	$⊢ (φ \land x \in I) \to 0 \leq ({D ↾}_{I}) (x)$
427	426	3adant3	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to 0 \leq ({D ↾}_{I}) (x)$
428		simp3	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to ({D ↾}_{I}) (x) = y$
429	427 428	breqtrd	$⊢ (φ \land x \in I \land ({D ↾}_{I}) (x) = y) \to 0 \leq y$
430	429	3exp	$⊢ φ \to (x \in I \to (({D ↾}_{I}) (x) = y \to 0 \leq y))$
431	430	adantr	$⊢ (φ \land y \in R) \to (x \in I \to (({D ↾}_{I}) (x) = y \to 0 \leq y))$
432	431	rexlimdv	$⊢ (φ \land y \in R) \to (\exists x \in I ({D ↾}_{I}) (x) = y \to 0 \leq y)$
433	425 432	mpd	$⊢ (φ \land y \in R) \to 0 \leq y$
434	433	ralrimiva	$⊢ φ \to \forall y \in R 0 \leq y$
435		breq1	$⊢ x = 0 \to (x \leq y \leftrightarrow 0 \leq y)$
436	435	ralbidv	$⊢ x = 0 \to (\forall y \in R x \leq y \leftrightarrow \forall y \in R 0 \leq y)$
437	436	rspcev	$⊢ (0 \in ℝ \land \forall y \in R 0 \leq y) \to \exists x \in ℝ \forall y \in R x \leq y$
438	419 434 437	sylancr	$⊢ φ \to \exists x \in ℝ \forall y \in R x \leq y$
439	438	3ad2ant1	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \exists x \in ℝ \forall y \in R x \leq y$
440		pm3.22	$⊢ (c \in A \land d \in A) \to (d \in A \land c \in A)$
441		opelxp	$⊢ ⟨d, c⟩ \in (A \times A) \leftrightarrow (d \in A \land c \in A)$
442	440 441	sylibr	$⊢ (c \in A \land d \in A) \to ⟨d, c⟩ \in (A \times A)$
443	442	3ad2ant2	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in (A \times A)$
444	5 58	sstrd	$⊢ φ \to A \subseteq ℝ$
445	444	sselda	$⊢ (φ \land c \in A) \to c \in ℝ$
446	445	adantrr	$⊢ (φ \land (c \in A \land d \in A)) \to c \in ℝ$
447	446	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \in ℝ$
448		simp3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c < d$
449	447 448	gtned	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d \neq c$
450	449	neneqd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \neg d = c$
451		df-br	$⊢ d I c \leftrightarrow ⟨d, c⟩ \in I$
452		vex	$⊢ c \in V$
453	452	ideq	$⊢ d I c \leftrightarrow d = c$
454	451 453	bitr3i	$⊢ ⟨d, c⟩ \in I \leftrightarrow d = c$
455	450 454	sylnibr	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \neg ⟨d, c⟩ \in I$
456	443 455	eldifd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in ((A \times A) ∖ I)$
457	456 10	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ⟨d, c⟩ \in I$
458	447 448	ltned	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \neq d$
459	146	3ad2ant1	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to {D ↾}_{I} = {(abs \circ -) ↾}_{I}$
460	459	fveq1d	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({D ↾}_{I}) (⟨d, c⟩) = ({(abs \circ -) ↾}_{I}) (⟨d, c⟩)$
461	442	3ad2ant2	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in (A \times A)$
462		necom	$⊢ c \neq d \leftrightarrow d \neq c$
463	462	biimpi	$⊢ c \neq d \to d \neq c$
464	463	neneqd	$⊢ c \neq d \to \neg d = c$
465	464	3ad2ant3	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to \neg d = c$
466	465 454	sylnibr	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to \neg ⟨d, c⟩ \in I$
467	461 466	eldifd	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in ((A \times A) ∖ I)$
468	467 10	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in I$
469		fvres	$⊢ ⟨d, c⟩ \in I \to ({(abs \circ -) ↾}_{I}) (⟨d, c⟩) = (abs \circ -) (⟨d, c⟩)$
470	468 469	syl	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({(abs \circ -) ↾}_{I}) (⟨d, c⟩) = (abs \circ -) (⟨d, c⟩)$
471		simp1	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to φ$
472	471 468	jca	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (φ \land ⟨d, c⟩ \in I)$
473		eleq1	$⊢ x = ⟨d, c⟩ \to (x \in I \leftrightarrow ⟨d, c⟩ \in I)$
474	473	anbi2d	$⊢ x = ⟨d, c⟩ \to ((φ \land x \in I) \leftrightarrow (φ \land ⟨d, c⟩ \in I))$
475		eleq1	$⊢ x = ⟨d, c⟩ \to (x \in dom - \leftrightarrow ⟨d, c⟩ \in dom -)$
476	474 475	imbi12d	$⊢ x = ⟨d, c⟩ \to (((φ \land x \in I) \to x \in dom -) \leftrightarrow ((φ \land ⟨d, c⟩ \in I) \to ⟨d, c⟩ \in dom -))$
477	476 76	vtoclg	$⊢ ⟨d, c⟩ \in I \to ((φ \land ⟨d, c⟩ \in I) \to ⟨d, c⟩ \in dom -)$
478	468 472 477	sylc	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ⟨d, c⟩ \in dom -$
479		fvco	$⊢ (Fun - \land ⟨d, c⟩ \in dom -) \to (abs \circ -) (⟨d, c⟩) = \|- (⟨d, c⟩)\|$
480	73 478 479	sylancr	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (abs \circ -) (⟨d, c⟩) = \|- (⟨d, c⟩)\|$
481		df-ov	$⊢ d - c = - (⟨d, c⟩)$
482	481	eqcomi	$⊢ - (⟨d, c⟩) = d - c$
483	482	fveq2i	$⊢ \|- (⟨d, c⟩)\| = \|d - c\|$
484	480 483	eqtrdi	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to (abs \circ -) (⟨d, c⟩) = \|d - c\|$
485	460 470 484	3eqtrd	$⊢ (φ \land (c \in A \land d \in A) \land c \neq d) \to ({D ↾}_{I}) (⟨d, c⟩) = \|d - c\|$
486	458 485	syld3an3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ({D ↾}_{I}) (⟨d, c⟩) = \|d - c\|$
487	444	sselda	$⊢ (φ \land d \in A) \to d \in ℝ$
488	487	adantrl	$⊢ (φ \land (c \in A \land d \in A)) \to d \in ℝ$
489	488	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d \in ℝ$
490	447 489 448	ltled	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to c \leq d$
491	447 489 490	abssubge0d	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \|d - c\| = d - c$
492	486 491	eqtrd	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to ({D ↾}_{I}) (⟨d, c⟩) = d - c$
493		fveq2	$⊢ x = ⟨d, c⟩ \to ({D ↾}_{I}) (x) = ({D ↾}_{I}) (⟨d, c⟩)$
494	493	eqeq1d	$⊢ x = ⟨d, c⟩ \to (({D ↾}_{I}) (x) = d - c \leftrightarrow ({D ↾}_{I}) (⟨d, c⟩) = d - c)$
495	494	rspcev	$⊢ (⟨d, c⟩ \in I \land ({D ↾}_{I}) (⟨d, c⟩) = d - c) \to \exists x \in I ({D ↾}_{I}) (x) = d - c$
496	457 492 495	syl2anc	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to \exists x \in I ({D ↾}_{I}) (x) = d - c$
497	488 446	resubcld	$⊢ (φ \land (c \in A \land d \in A)) \to d - c \in ℝ$
498		elex	$⊢ d - c \in ℝ \to d - c \in V$
499	497 498	syl	$⊢ (φ \land (c \in A \land d \in A)) \to d - c \in V$
500	499	3adant3	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in V$
501		simp1	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to φ$
502		eleq1	$⊢ y = d - c \to (y \in ran ({D ↾}_{I}) \leftrightarrow d - c \in ran ({D ↾}_{I}))$
503		eqeq2	$⊢ y = d - c \to (({D ↾}_{I}) (x) = y \leftrightarrow ({D ↾}_{I}) (x) = d - c)$
504	503	rexbidv	$⊢ y = d - c \to (\exists x \in I ({D ↾}_{I}) (x) = y \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c)$
505	502 504	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))$
506	505	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)))$
507	67 423	syl	$⊢ φ \to (y \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = y)$
508	506 507	vtoclg	$⊢ d - c \in V \to (φ \to (d - c \in ran ({D ↾}_{I}) \leftrightarrow \exists x \in I ({D ↾}_{I}) (x) = d - c))$
509	500 501 508	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)$
510	496 509	mpbird	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in ran ({D ↾}_{I})$
511	510 11	eleqtrrdi	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to d - c \in R$
512		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall y \in R x \leq y \land d - c \in R) \to inf (R ℝ <) \leq d - c$
513	418 439 511 512	syl3anc	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to inf (R ℝ <) \leq d - c$
514	12 513	eqbrtrid	$⊢ (φ \land (c \in A \land d \in A) \land c < d) \to E \leq d - c$
515	417 514	vtoclg	$⊢ B \in A \to ((φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B)$
516	410 515	mpcom	$⊢ (φ \land (B \in A \land d \in A) \land B < d) \to E \leq d - B$
517	409 516	vtoclg	$⊢ C \in A \to ((φ \land (B \in A \land C \in A) \land B < C) \to E \leq C - B)$
518	8 402 517	sylc	$⊢ φ \to E \leq C - B$
519	518 4	breqtrrdi	$⊢ φ \to E \leq T$
520	268 519	syl	$⊢ ψ \to E \leq T$
521	520	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq T$
522	521	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$
523	364	adantr	$⊢ (ψ \land k \in ℤ) \to b \in ℂ$
524	523 366	pncan2d	$⊢ (ψ \land k \in ℤ) \to b + k T - b = k T$
525	524	oveq1d	$⊢ (ψ \land k \in ℤ) \to \frac{b + k T - b}{T} = \frac{k T}{T}$
526	340	adantl	$⊢ (ψ \land k \in ℤ) \to k \in ℂ$
527	318	adantr	$⊢ (ψ \land k \in ℤ) \to T \in ℂ$
528	419	a1i	$⊢ φ \to 0 \in ℝ$
529	528 350	gtned	$⊢ φ \to T \neq 0$
530	268 529	syl	$⊢ ψ \to T \neq 0$
531	530	adantr	$⊢ (ψ \land k \in ℤ) \to T \neq 0$
532	526 527 531	divcan4d	$⊢ (ψ \land k \in ℤ) \to \frac{k T}{T} = k$
533	525 532	eqtr2d	$⊢ (ψ \land k \in ℤ) \to k = \frac{b + k T - b}{T}$
534	533	adantrl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k = \frac{b + k T - b}{T}$
535	534	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k = \frac{b + k T - b}{T}$
536		oveq1	$⊢ a + j T = b + k T \to a + j T - b = b + k T - b$
537	536	oveq1d	$⊢ a + j T = b + k T \to \frac{a + j T - b}{T} = \frac{b + k T - b}{T}$
538	537	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}$
539	368	adantr	$⊢ (ψ \land j \in ℤ) \to a \in ℂ$
540	364	adantr	$⊢ (ψ \land j \in ℤ) \to b \in ℂ$
541	539 370 540	addsubd	$⊢ (ψ \land j \in ℤ) \to a + j T - b = a - b + j T$
542	539 540	subcld	$⊢ (ψ \land j \in ℤ) \to a - b \in ℂ$
543	542 370	addcomd	$⊢ (ψ \land j \in ℤ) \to a - b + j T = j T + a - b$
544	541 543	eqtrd	$⊢ (ψ \land j \in ℤ) \to a + j T - b = j T + a - b$
545	544	oveq1d	$⊢ (ψ \land j \in ℤ) \to \frac{a + j T - b}{T} = \frac{j T + a - b}{T}$
546	318	adantr	$⊢ (ψ \land j \in ℤ) \to T \in ℂ$
547	530	adantr	$⊢ (ψ \land j \in ℤ) \to T \neq 0$
548	370 542 546 547	divdird	$⊢ (ψ \land j \in ℤ) \to \frac{j T + a - b}{T} = (\frac{j T}{T}) + (\frac{a - b}{T})$
549	335	adantl	$⊢ (ψ \land j \in ℤ) \to j \in ℂ$
550	549 546 547	divcan4d	$⊢ (ψ \land j \in ℤ) \to \frac{j T}{T} = j$
551	550	oveq1d	$⊢ (ψ \land j \in ℤ) \to (\frac{j T}{T}) + (\frac{a - b}{T}) = j + (\frac{a - b}{T})$
552	545 548 551	3eqtrd	$⊢ (ψ \land j \in ℤ) \to \frac{a + j T - b}{T} = j + (\frac{a - b}{T})$
553	552	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to \frac{a + j T - b}{T} = j + (\frac{a - b}{T})$
554	553	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})$
555	535 538 554	3eqtr2d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k = j + (\frac{a - b}{T})$
556	309 302	resubcld	$⊢ ψ \to a - b \in ℝ$
557	309 302	sublt0d	$⊢ ψ \to (a - b < 0 \leftrightarrow a < b)$
558	358 557	mpbird	$⊢ ψ \to a - b < 0$
559	556 352 558	divlt0gt0d	$⊢ ψ \to \frac{a - b}{T} < 0$
560	559	adantr	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} < 0$
561	335	subidd	$⊢ j \in ℤ \to j - j = 0$
562	561	eqcomd	$⊢ j \in ℤ \to 0 = j - j$
563	562	adantl	$⊢ (ψ \land j \in ℤ) \to 0 = j - j$
564	560 563	breqtrd	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} < j - j$
565	556 293 530	redivcld	$⊢ ψ \to \frac{a - b}{T} \in ℝ$
566	565	adantr	$⊢ (ψ \land j \in ℤ) \to \frac{a - b}{T} \in ℝ$
567	311 566 311	ltaddsub2d	$⊢ (ψ \land j \in ℤ) \to (j + (\frac{a - b}{T}) < j \leftrightarrow \frac{a - b}{T} < j - j)$
568	564 567	mpbird	$⊢ (ψ \land j \in ℤ) \to j + (\frac{a - b}{T}) < j$
569	568	adantrr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j + (\frac{a - b}{T}) < j$
570	569	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to j + (\frac{a - b}{T}) < j$
571	555 570	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to k < j$
572	320	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T = 1 T$
573		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k < j$
574		simplr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \in ℤ$
575		simpll	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to j \in ℤ$
576		zltp1le	$⊢ (k \in ℤ \land j \in ℤ) \to (k < j \leftrightarrow k + 1 \leq j)$
577	574 575 576	syl2anc	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to (k < j \leftrightarrow k + 1 \leq j)$
578	573 577	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k + 1 \leq j$
579	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \in ℝ$
580	330	a1i	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to 1 \in ℝ$
581	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to j \in ℝ$
582	579 580 581	leaddsub2d	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to (k + 1 \leq j \leftrightarrow 1 \leq j - k)$
583	578 582	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to 1 \leq j - k$
584	583	adantll	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 \leq j - k$
585	330	a1i	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 \in ℝ$
586	395	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to j - k \in ℝ$
587	352	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T \in ℝ^{+}$
588	585 586 587	lemul1d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to (1 \leq j - k \leftrightarrow 1 T \leq (j - k) T)$
589	584 588	mpbid	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to 1 T \leq (j - k) T$
590	572 589	eqbrtrd	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k < j) \to T \leq (j - k) T$
591	571 590	syldan	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land a + j T = b + k T) \to T \leq (j - k) T$
592	591	adantlr	$⊢ (((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \land a + j T = b + k T) \to T \leq (j - k) T$
593	592	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$
594	392 394 399 522 593	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$
595		oveq2	$⊢ a + j T = b + k T \to b + k T - (a + j T) = b + k T - (b + k T)$
596	595	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$
597	596	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$
598	268 444	syl	$⊢ ψ \to A \subseteq ℝ$
599	598	sselda	$⊢ (ψ \land b + k T \in A) \to b + k T \in ℝ$
600	599	adantrl	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℝ$
601	600	recnd	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℂ$
602	601	subidd	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (b + k T) = 0$
603	602	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$
604	603	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$
605	597 604	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$
606	605	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$
607	606	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$
608	374 373	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to j - k \in ℂ$
609	608 375	mulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k) T \in ℂ$
610	609	addlidd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to 0 + (j - k) T = (j - k) T$
611	610	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$
612	611	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$
613	607 612	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$
614	594 613	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$
615	614	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$
616	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 ℝ$
617	598	sselda	$⊢ (ψ \land a + j T \in A) \to a + j T \in ℝ$
618	617	adantrr	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T \in ℝ$
619	600 618	resubcld	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to b + k T - (a + j T) \in ℝ$
620	619	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 ℝ$
621	620	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 ℝ$
622	620 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 ℝ$
623	622	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 ℝ$
624	268	adantr	$⊢ (ψ \land k \leq j) \to φ$
625	624	3ad2antl1	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to φ$
626	625	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 φ$
627		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)$
628	627	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)$
629		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$
630	618	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 ℝ$
631	600	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 ℝ$
632	630 631	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)$
633	629 632	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$
634		eqcom	$⊢ a + j T = b + k T \leftrightarrow b + k T = a + j T$
635	634	notbii	$⊢ \neg a + j T = b + k T \leftrightarrow \neg b + k T = a + j T$
636	635	bilani	$⊢ (((ψ \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$
637		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)$
638	633 636 637	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)$
639	631 630	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))$
640	638 639	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$
641	640	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$
642	641	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$
643	618	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to a + j T \in ℝ$
644	643	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 ℝ$
645	644	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 ℝ$
646	600	adantr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land k \leq j) \to b + k T \in ℝ$
647	646	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 ℝ$
648	647	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 ℝ$
649	645 648	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)$
650	642 649	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$
651		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$
652		eleq1	$⊢ c = a + j T \to (c \in A \leftrightarrow a + j T \in A)$
653	652	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))$
654		breq1	$⊢ c = a + j T \to (c < b + k T \leftrightarrow a + j T < b + k T)$
655	653 654	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))$
656		oveq2	$⊢ c = a + j T \to b + k T - c = b + k T - (a + j T)$
657	656	breq2d	$⊢ c = a + j T \to (E \leq b + k T - c \leftrightarrow E \leq b + k T - (a + j T))$
658	655 657	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)))$
659		simp2r	$⊢ (φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to b + k T \in A$
660		eleq1	$⊢ d = b + k T \to (d \in A \leftrightarrow b + k T \in A)$
661	660	anbi2d	$⊢ d = b + k T \to ((c \in A \land d \in A) \leftrightarrow (c \in A \land b + k T \in A))$
662		breq2	$⊢ d = b + k T \to (c < d \leftrightarrow c < b + k T)$
663	661 662	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))$
664		oveq1	$⊢ d = b + k T \to d - c = b + k T - c$
665	664	breq2d	$⊢ d = b + k T \to (E \leq d - c \leftrightarrow E \leq b + k T - c)$
666	663 665	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))$
667	666 514	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)$
668	659 667	mpcom	$⊢ (φ \land (c \in A \land b + k T \in A) \land c < b + k T) \to E \leq b + k T - c$
669	658 668	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))$
670	651 669	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)$
671	626 628 650 670	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)$
672	395	ad2antlr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to j - k \in ℝ$
673	293	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to T \in ℝ$
674		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to k \leq j$
675	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to j \in ℝ$
676	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to k \in ℝ$
677	675 676	subge0d	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to (0 \leq j - k \leftrightarrow k \leq j)$
678	674 677	mpbird	$⊢ ((j \in ℤ \land k \in ℤ) \land k \leq j) \to 0 \leq j - k$
679	678	adantll	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq j - k$
680	352	rpge0d	$⊢ ψ \to 0 \leq T$
681	680	ad2antrr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq T$
682	672 673 679 681	mulge0d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k \leq j) \to 0 \leq (j - k) T$
683	682	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$
684	620	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 ℝ$
685	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 ℝ$
686	684 685	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)$
687	683 686	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$
688	687	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$
689	616 621 623 671 688	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$
690	615 689	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$
691	372 378	eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b + k T - (a + j T) = b - a + (k - j) T$
692	691	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$
693	365 369	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a \in ℂ$
694	373 374	subcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to k - j \in ℂ$
695	694 375	mulcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T \in ℂ$
696	693 695 609	addassd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = (b - a) + (k - j) T + (j - k) T$
697	341 336 336 341	subadd4b	$⊢ (j \in ℤ \land k \in ℤ) \to (k - j) + j - k = (k - k) + j - j$
698	697	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) + j - k = (k - k) + j - j$
699	698	oveq1d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - j) + j - k) T = ((k - k) + j - j) T$
700	694 608 375	adddird	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - j) + j - k) T = (k - j) T + (j - k) T$
701	340	subidd	$⊢ k \in ℤ \to k - k = 0$
702	701	adantl	$⊢ (j \in ℤ \land k \in ℤ) \to k - k = 0$
703	561	adantr	$⊢ (j \in ℤ \land k \in ℤ) \to j - j = 0$
704	702 703	oveq12d	$⊢ (j \in ℤ \land k \in ℤ) \to (k - k) + j - j = 0 + 0$
705		00id	$⊢ 0 + 0 = 0$
706	704 705	eqtrdi	$⊢ (j \in ℤ \land k \in ℤ) \to (k - k) + j - j = 0$
707	706	oveq1d	$⊢ (j \in ℤ \land k \in ℤ) \to ((k - k) + j - j) T = 0 \cdot T$
708	707	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to ((k - k) + j - j) T = 0 \cdot T$
709	699 700 708	3eqtr3d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (k - j) T + (j - k) T = 0 \cdot T$
710	709	oveq2d	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = b - a + 0 \cdot T$
711	318	mul02d	$⊢ ψ \to 0 \cdot T = 0$
712	711	oveq2d	$⊢ ψ \to b - a + 0 \cdot T = b - a + 0$
713	364 368	subcld	$⊢ ψ \to b - a \in ℂ$
714	713	addridd	$⊢ ψ \to b - a + 0 = b - a$
715	712 714	eqtrd	$⊢ ψ \to b - a + 0 \cdot T = b - a$
716	715	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a + 0 \cdot T = b - a$
717	710 716	eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b - a) + (k - j) T + (j - k) T = b - a$
718	692 696 717	3eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (b + k T) - (a + j T) + (j - k) T = b - a$
719	718	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$
720	719	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$
721	690 720	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$
722		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))$
723		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$
724	600	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b + k T \in ℝ$
725	724	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 ℝ$
726	618	3adant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j 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 a + j T \in ℝ$
728	725 727	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)$
729	723 728	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$
730	729	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$
731	534	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}$
732	731	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}$
733	599	3adant2	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b + k T \in ℝ$
734	302	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b \in ℝ$
735	733 734	resubcld	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to b + k T - b \in ℝ$
736	293	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to T \in ℝ$
737	530	3ad2ant1	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to T \neq 0$
738	735 736 737	redivcld	$⊢ (ψ \land k \in ℤ \land b + k T \in A) \to \frac{b + k T - b}{T} \in ℝ$
739	738	3adant3l	$⊢ (ψ \land k \in ℤ \land (a + j T \in A \land b + k T \in A)) \to \frac{b + k T - b}{T} \in ℝ$
740	739	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 ℝ$
741	740	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 ℝ$
742	617	3adant2	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T \in ℝ$
743	302	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to b \in ℝ$
744	742 743	resubcld	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T - b \in ℝ$
745	293	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to T \in ℝ$
746	530	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to T \neq 0$
747	744 745 746	redivcld	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to \frac{a + j T - b}{T} \in ℝ$
748	747	3adant3r	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + k T \in A)) \to \frac{a + j T - b}{T} \in ℝ$
749	748	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 ℝ$
750	749	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 ℝ$
751	284	3ad2ant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j \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 j \in ℝ$
753	724	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 ℝ$
754	302	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b \in ℝ$
755	754	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 ℝ$
756	753 755	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 ℝ$
757	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 a + j T \in ℝ$
758	757 755	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 ℝ$
759	352	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to T \in ℝ^{+}$
760	759	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 ℝ^{+}$
761	600	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 ℝ$
762	618	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 ℝ$
763	302	ad2antrr	$⊢ ((ψ \land (a + j T \in A \land b + k T \in A)) \land b + k T < a + j T) \to b \in ℝ$
764		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$
765	761 762 763 764	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$
766	765	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$
767	756 758 760 766	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}$
768	553 569	eqbrtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to \frac{a + j T - b}{T} < j$
769	768	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$
770	769	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$
771	741 750 752 767 770	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$
772	732 771	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$
773	772	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$
774	730 773	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$
775	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 ℝ$
776	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 ℝ$
777	622	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 ℝ$
778	521	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$
779		peano2rem	$⊢ j \in ℝ \to j - 1 \in ℝ$
780	751 779	syl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j - 1 \in ℝ$
781	287	3ad2ant2	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to k \in ℝ$
782	780 781	resubcld	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to j - 1 - k \in ℝ$
783	782 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 ℝ$
784	783	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 ℝ$
785	751	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 ℝ$
786	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 ℝ$
787	785 786	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 ℝ$
788	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \in ℝ$
789	788	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 ℝ$
790	787 789	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 ℝ$
791	680	adantr	$⊢ (ψ \land k < j - 1) \to 0 \leq T$
792	791	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$
793	283	ad2antrr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j \in ℝ$
794	330	a1i	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \in ℝ$
795	793 794	resubcld	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j - 1 \in ℝ$
796		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k < j - 1$
797		simplr	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \in ℤ$
798		simpll	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j \in ℤ$
799		1zzd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \in ℤ$
800	798 799	zsubcld	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to j - 1 \in ℤ$
801		zltlem1	$⊢ (k \in ℤ \land j - 1 \in ℤ) \to (k < j - 1 \leftrightarrow k \leq j - 1 - 1)$
802	797 800 801	syl2anc	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to (k < j - 1 \leftrightarrow k \leq j - 1 - 1)$
803	796 802	mpbid	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to k \leq j - 1 - 1$
804	788 795 794 803	lesubd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j - 1) \to 1 \leq j - 1 - k$
805	804	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$
806	776 790 792 805	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$
807	336 337 341	sub32d	$⊢ (j \in ℤ \land k \in ℤ) \to j - 1 - k = j - k - 1$
808	807	oveq1d	$⊢ (j \in ℤ \land k \in ℤ) \to (j - 1 - k) T = (j - k - 1) T$
809	808	adantl	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - 1 - k) T = (j - k - 1) T$
810		1cnd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to 1 \in ℂ$
811	608 810 375	subdird	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k - 1) T = (j - k) T - 1 T$
812	319	oveq2d	$⊢ ψ \to (j - k) T - 1 T = (j - k) T - T$
813	812	adantr	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - k) T - 1 T = (j - k) T - T$
814	809 811 813	3eqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to (j - 1 - k) T = (j - k) T - T$
815	814	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$
816	726 724	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 ℝ$
817	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$
818	817 4	breqtrrdi	$⊢ (ψ \land (a + j T \in A \land b + k T \in A)) \to a + j T - (b + k T) \leq T$
819	818	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$
820	816 393 398 819	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))$
821	815 820	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))$
822	609	3adant3	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to (j - k) T \in ℂ$
823	726	recnd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to a + j T \in ℂ$
824	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 ℂ$
825	822 823 824	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)$
826	620	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 ℂ$
827	822 826	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$
828	825 827	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$
829	821 828	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$
830	829	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$
831	776 784 777 806 830	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$
832	775 776 777 778 831	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$
833	719	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$
834	832 833	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$
835	834	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$
836	835	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$
837		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))$
838		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 ℤ)$
839		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$
840		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$
841	580 581 579 583	lesubd	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j) \to k \leq j - 1$
842	841	3adant3	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k \leq j - 1$
843		simpr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to \neg k < j - 1$
844	284 779	syl	$⊢ (j \in ℤ \land k \in ℤ) \to j - 1 \in ℝ$
845	844	adantr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to j - 1 \in ℝ$
846	286	ad2antlr	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to k \in ℝ$
847	845 846	lenltd	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to (j - 1 \leq k \leftrightarrow \neg k < j - 1)$
848	843 847	mpbird	$⊢ ((j \in ℤ \land k \in ℤ) \land \neg k < j - 1) \to j - 1 \leq k$
849	848	3adant2	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to j - 1 \leq k$
850	579	3adant3	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k \in ℝ$
851	844	3ad2ant1	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to j - 1 \in ℝ$
852	850 851	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))$
853	842 849 852	mpbir2and	$⊢ ((j \in ℤ \land k \in ℤ) \land k < j \land \neg k < j - 1) \to k = j - 1$
854	838 839 840 853	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$
855	854	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$
856		simpl1	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \land k = j - 1) \to ψ$
857		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 ℤ$
858		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$
859		oveq1	$⊢ k = j - 1 \to k T = (j - 1) T$
860	859	oveq2d	$⊢ k = j - 1 \to b + k T = b + (j - 1) T$
861	860	eqcomd	$⊢ k = j - 1 \to b + (j - 1) T = b + k T$
862	861	adantl	$⊢ (b + k T \in A \land k = j - 1) \to b + (j - 1) T = b + k T$
863		simpl	$⊢ (b + k T \in A \land k = j - 1) \to b + k T \in A$
864	862 863	eqeltrd	$⊢ (b + k T \in A \land k = j - 1) \to b + (j - 1) T \in A$
865	864	adantll	$⊢ ((a + j T \in A \land b + k T \in A) \land k = j - 1) \to b + (j - 1) T \in A$
866	865	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$
867	858 866	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)$
868		id	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to (ψ \land j \in ℤ \land a + j T \in A)$
869	868	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)$
870	742	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T \in ℝ$
871	271	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to C \in ℝ$
872	871	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to C \in ℝ$
873	269	adantr	$⊢ (ψ \land a + j T \in A) \to B \in ℝ$
874	271	adantr	$⊢ (ψ \land a + j T \in A) \to C \in ℝ$
875		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))$
876	873 874 875	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))$
877	276 876	mpbid	$⊢ (ψ \land a + j T \in A) \to (a + j T \in ℝ \land B \leq a + j T \land a + j T \leq C)$
878	877	simp3d	$⊢ (ψ \land a + j T \in A) \to a + j T \leq C$
879	878	3adant2	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to a + j T \leq C$
880	879	adantr	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T \leq C$
881		nne	$⊢ \neg C \neq a + j T \leftrightarrow C = a + j T$
882	539 370	pncand	$⊢ (ψ \land j \in ℤ) \to a + j T - j T = a$
883	882	eqcomd	$⊢ (ψ \land j \in ℤ) \to a = a + j T - j T$
884	883	adantr	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a = a + j T - j T$
885		oveq1	$⊢ C = a + j T \to C - j T = a + j T - j T$
886	885	eqcomd	$⊢ C = a + j T \to a + j T - j T = C - j T$
887	886	adantl	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a + j T - j T = C - j T$
888	4	oveq2i	$⊢ B + T = B + C - B$
889	268 161	syl	$⊢ ψ \to B \in ℂ$
890	268 162	syl	$⊢ ψ \to C \in ℂ$
891	889 890	pncan3d	$⊢ ψ \to B + C - B = C$
892	888 891	eqtr2id	$⊢ ψ \to C = B + T$
893	892	oveq1d	$⊢ ψ \to C - j T = B + T - j T$
894	893	adantr	$⊢ (ψ \land j \in ℤ) \to C - j T = B + T - j T$
895	889	adantr	$⊢ (ψ \land j \in ℤ) \to B \in ℂ$
896	895 370 546	subsub3d	$⊢ (ψ \land j \in ℤ) \to B - (j T - T) = B + T - j T$
897	549 546	mulsubfacd	$⊢ (ψ \land j \in ℤ) \to j T - T = (j - 1) T$
898	897	oveq2d	$⊢ (ψ \land j \in ℤ) \to B - (j T - T) = B - (j - 1) T$
899	894 896 898	3eqtr2d	$⊢ (ψ \land j \in ℤ) \to C - j T = B - (j - 1) T$
900	899	adantr	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to C - j T = B - (j - 1) T$
901	884 887 900	3eqtrd	$⊢ ((ψ \land j \in ℤ) \land C = a + j T) \to a = B - (j - 1) T$
902	901	3adantl3	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land C = a + j T) \to a = B - (j - 1) T$
903	902	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$
904		oveq1	$⊢ b + (j - 1) T = B \to b + (j - 1) T - (j - 1) T = B - (j - 1) T$
905	904	eqcomd	$⊢ b + (j - 1) T = B \to B - (j - 1) T = b + (j - 1) T - (j - 1) T$
906	905	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$
907	364	ad2antrr	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to b \in ℂ$
908		1cnd	$⊢ (ψ \land j \in ℤ) \to 1 \in ℂ$
909	549 908	subcld	$⊢ (ψ \land j \in ℤ) \to j - 1 \in ℂ$
910	909 546	mulcld	$⊢ (ψ \land j \in ℤ) \to (j - 1) T \in ℂ$
911	910	adantr	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to (j - 1) T \in ℂ$
912	907 911	pncand	$⊢ ((ψ \land j \in ℤ) \land b + (j - 1) T = B) \to b + (j - 1) T - (j - 1) T = b$
913	912	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$
914	913	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$
915	903 906 914	3eqtrd	$⊢ (((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \land C = a + j T) \to a = b$
916	881 915	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$
917	309 358	ltned	$⊢ ψ \to a \neq b$
918	917	neneqd	$⊢ ψ \to \neg a = b$
919	918	3ad2ant1	$⊢ (ψ \land j \in ℤ \land a + j T \in A) \to \neg a = b$
920	919	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$
921	916 920	condan	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to C \neq a + j T$
922	870 872 880 921	leneltd	$⊢ ((ψ \land j \in ℤ \land a + j T \in A) \land b + (j - 1) T = B) \to a + j T < C$
923	869 922	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$
924	268	ad2antrr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to φ$
925		simplr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to a + j T \in A$
926	924 8	syl	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to C \in A$
927		simpr	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to a + j T < C$
928		simp2l	$⊢ (φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to a + j T \in A$
929	652	anbi1d	$⊢ c = a + j T \to ((c \in A \land C \in A) \leftrightarrow (a + j T \in A \land C \in A))$
930		breq1	$⊢ c = a + j T \to (c < C \leftrightarrow a + j T < C)$
931	929 930	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))$
932		oveq2	$⊢ c = a + j T \to C - c = C - (a + j T)$
933	932	breq2d	$⊢ c = a + j T \to (E \leq C - c \leftrightarrow E \leq C - (a + j T))$
934	931 933	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)))$
935		simp2r	$⊢ (φ \land (c \in A \land C \in A) \land c < C) \to C \in A$
936	403	anbi2d	$⊢ d = C \to ((c \in A \land d \in A) \leftrightarrow (c \in A \land C \in A))$
937		breq2	$⊢ d = C \to (c < d \leftrightarrow c < C)$
938	936 937	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))$
939		oveq1	$⊢ d = C \to d - c = C - c$
940	939	breq2d	$⊢ d = C \to (E \leq d - c \leftrightarrow E \leq C - c)$
941	938 940	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))$
942	941 514	vtoclg	$⊢ C \in A \to ((φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c)$
943	935 942	mpcom	$⊢ (φ \land (c \in A \land C \in A) \land c < C) \to E \leq C - c$
944	934 943	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))$
945	928 944	mpcom	$⊢ (φ \land (a + j T \in A \land C \in A) \land a + j T < C) \to E \leq C - (a + j T)$
946	924 925 926 927 945	syl121anc	$⊢ ((ψ \land a + j T \in A) \land a + j T < C) \to E \leq C - (a + j T)$
947	946	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)$
948	947	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)$
949	948	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)$
950	890	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to C \in ℂ$
951	598	sselda	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in ℝ$
952	951	recnd	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in ℂ$
953	950 952	npcand	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - (b + (j - 1) T)) + b + (j - 1) T = C$
954	953	eqcomd	$⊢ (ψ \land b + (j - 1) T \in A) \to C = (C - (b + (j - 1) T)) + b + (j - 1) T$
955	954	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)$
956	955	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)$
957	956	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)$
958	957	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)$
959		oveq2	$⊢ b + (j - 1) T = B \to C - (b + (j - 1) T) = C - B$
960	959	oveq1d	$⊢ b + (j - 1) T = B \to (C - (b + (j - 1) T)) + b + (j - 1) T = (C - B) + b + (j - 1) T$
961	960	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)$
962	961	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)$
963	4	eqcomi	$⊢ C - B = T$
964	963	oveq1i	$⊢ (C - B) + b + (j - 1) T = T + b + (j - 1) T$
965	964	a1i	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - B) + b + (j - 1) T = T + b + (j - 1) T$
966	318	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to T \in ℂ$
967	966 952	addcomd	$⊢ (ψ \land b + (j - 1) T \in A) \to T + b + (j - 1) T = b + (j - 1) T + T$
968	965 967	eqtrd	$⊢ (ψ \land b + (j - 1) T \in A) \to (C - B) + b + (j - 1) T = b + (j - 1) T + T$
969	968	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)$
970	969	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)$
971	970	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)$
972	971	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)$
973	952	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℂ$
974	973	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℂ$
975	974	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 ℂ$
976	318	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to 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 T \in ℂ$
978	617	adantrr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℝ$
979	978	recnd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℂ$
980	979	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \in ℂ$
981	980	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 ℂ$
982	975 977 981	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$
983	972 982	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$
984	958 962 983	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$
985	984	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$
986	949 985	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$
987	923 986	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$
988		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 ψ$
989		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$
990		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$
991	269	3ad2ant1	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B \in ℝ$
992	951	3adant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to b + (j - 1) T \in ℝ$
993	273	sselda	$⊢ (ψ \land b + (j - 1) T \in A) \to b + (j - 1) T \in [B, C]$
994	269	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to B \in ℝ$
995	271	adantr	$⊢ (ψ \land b + (j - 1) T \in A) \to C \in ℝ$
996		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))$
997	994 995 996	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))$
998	993 997	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)$
999	998	simp2d	$⊢ (ψ \land b + (j - 1) T \in A) \to B \leq b + (j - 1) T$
1000	999	3adant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B \leq b + (j - 1) T$
1001		neqne	$⊢ \neg b + (j - 1) T = B \to b + (j - 1) T \neq B$
1002	1001	3ad2ant3	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to b + (j - 1) T \neq B$
1003	991 992 1000 1002	leneltd	$⊢ (ψ \land b + (j - 1) T \in A \land \neg b + (j - 1) T = B) \to B < b + (j - 1) T$
1004	988 989 990 1003	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$
1005	390	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to E \in ℝ$
1006	1005	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 ℝ$
1007	951	adantrl	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℝ$
1008	1007	3adant2	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T \in ℝ$
1009	269	3ad2ant1	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℝ$
1010	1008 1009	resubcld	$⊢ (ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - B \in ℝ$
1011	1010	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 ℝ$
1012	1007 978	resubcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - (a + j T) \in ℝ$
1013	293	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to T \in ℝ$
1014	1012 1013	readdcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to (b + (j - 1) T) - (a + j T) + T \in ℝ$
1015	1014	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 ℝ$
1016	1015	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 ℝ$
1017	268	adantr	$⊢ (ψ \land B < b + (j - 1) T) \to φ$
1018	1017	3ad2antl1	$⊢ ((ψ \land j \in ℤ \land (a + j T \in A \land b + (j - 1) T \in A)) \land B < b + (j - 1) T) \to φ$
1019	1018 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$
1020		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$
1021		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$
1022		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$
1023		eleq1	$⊢ d = b + (j - 1) T \to (d \in A \leftrightarrow b + (j - 1) T \in A)$
1024	1023	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))$
1025		breq2	$⊢ d = b + (j - 1) T \to (B < d \leftrightarrow B < b + (j - 1) T)$
1026	1024 1025	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))$
1027		oveq1	$⊢ d = b + (j - 1) T \to d - B = b + (j - 1) T - B$
1028	1027	breq2d	$⊢ d = b + (j - 1) T \to (E \leq d - B \leftrightarrow E \leq b + (j - 1) T - B)$
1029	1026 1028	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))$
1030	1029 516	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)$
1031	1022 1030	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$
1032	1018 1019 1020 1021 1031	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$
1033	269	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℝ$
1034	978 1033	resubcld	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T - B \in ℝ$
1035	963 1013	eqeltrid	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C - B \in ℝ$
1036	271	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to C \in ℝ$
1037	878	adantrr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T \leq C$
1038	978 1036 1033 1037	lesub1dd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to a + j T - B \leq C - B$
1039	1034 1035 1012 1038	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$
1040	973 979	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$
1041	1040	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$
1042	1041	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$
1043	1012	recnd	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to b + (j - 1) T - (a + j T) \in ℂ$
1044	889	adantr	$⊢ (ψ \land (a + j T \in A \land b + (j - 1) T \in A)) \to B \in ℂ$
1045	1043 979 1044	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$
1046	1042 1045	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$
1047	4	oveq2i	$⊢ (b + (j - 1) T) - (a + j T) + T = (b + (j - 1) T - (a + j T)) + C - B$
1048	1047	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$
1049	1039 1046 1048	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$
1050	1049	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$
1051	1050	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$
1052	1006 1011 1016 1032 1051	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$
1053	1004 1052	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$
1054	987 1053	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$
1055	856 857 867 1054	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$
1056	718	eqcomd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ)) \to b - a = (b + k T) - (a + j T) + (j - k) T$
1057	1056	adantr	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k = j - 1) \to b - a = (b + k T) - (a + j T) + (j - k) T$
1058	860	oveq1d	$⊢ k = j - 1 \to b + k T - (a + j T) = b + (j - 1) T - (a + j T)$
1059	1058	adantl	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to b + k T - (a + j T) = b + (j - 1) T - (a + j T)$
1060		oveq2	$⊢ k = j - 1 \to j - k = j - (j - 1)$
1061	1060	oveq1d	$⊢ k = j - 1 \to (j - k) T = (j - (j - 1)) T$
1062	1061	adantl	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - k) T = (j - (j - 1)) T$
1063		1cnd	$⊢ j \in ℤ \to 1 \in ℂ$
1064	335 1063	nncand	$⊢ j \in ℤ \to j - (j - 1) = 1$
1065	1064	oveq1d	$⊢ j \in ℤ \to (j - (j - 1)) T = 1 T$
1066	1065	ad2antlr	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - (j - 1)) T = 1 T$
1067	319	ad2antrr	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to 1 T = T$
1068	1062 1066 1067	3eqtrd	$⊢ ((ψ \land j \in ℤ) \land k = j - 1) \to (j - k) T = T$
1069	1059 1068	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$
1070	1069	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$
1071	1057 1070	eqtr2d	$⊢ ((ψ \land (j \in ℤ \land k \in ℤ)) \land k = j - 1) \to (b + (j - 1) T) - (a + j T) + T = b - a$
1072	1071	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$
1073	1055 1072	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$
1074	837 855 1073	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$
1075	836 1074	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$
1076	722 774 730 1075	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$
1077	721 1076	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$
1078	387 1077	mpdan	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq b - a$
1079	309 302 358	ltled	$⊢ ψ \to a \leq b$
1080	309 302 1079	abssuble0d	$⊢ ψ \to \|a - b\| = b - a$
1081	1080	eqcomd	$⊢ ψ \to b - a = \|a - b\|$
1082	1081	3ad2ant1	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to b - a = \|a - b\|$
1083	1078 1082	breqtrd	$⊢ (ψ \land (j \in ℤ \land k \in ℤ) \land (a + j T \in A \land b + k T \in A)) \to E \leq \|a - b\|$
1084	1083	3exp	$⊢ ψ \to ((j \in ℤ \land k \in ℤ) \to ((a + j T \in A \land b + k T \in A) \to E \leq \|a - b\|))$
1085	1084	rexlimdvv	$⊢ ψ \to (\exists j \in ℤ \exists k \in ℤ (a + j T \in A \land b + k T \in A) \to E \leq \|a - b\|)$
1086	265 1085	mpd	$⊢ ψ \to E \leq \|a - b\|$
1087	18 1086	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\|$
1088	264 1087	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\|$
1089	251 1088	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\|$
1090	231 237 238 1089	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\|$
1091		simpr	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to \neg y < z$
1092		simpl3	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to y \neq z$
1093		simpl1	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to y \in ℝ$
1094		simpl2	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to z \in ℝ$
1095	1093 1094	lttri2d	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (y \neq z \leftrightarrow (y < z \lor z < y))$
1096	1092 1095	mpbid	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (y < z \lor z < y)$
1097	1096	ord	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to (\neg y < z \to z < y)$
1098	1091 1097	mpd	$⊢ ((y \in ℝ \land z \in ℝ \land y \neq z) \land \neg y < z) \to z < y$
1099	1098	adantll	$⊢ ((φ \land (y \in ℝ \land z \in ℝ \land y \neq z)) \land \neg y < z) \to z < y$
1100	1099	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$
1101		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 φ$
1102		simplr	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to z \in ℝ$
1103		simpll	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to y \in ℝ$
1104		simpr	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to z < y$
1105	1102 1103 1104	3jca	$⊢ ((y \in ℝ \land z \in ℝ) \land z < y) \to (z \in ℝ \land y \in ℝ \land z < y)$
1106	1105	adantll	$⊢ ((φ \land (y \in ℝ \land z \in ℝ)) \land z < y) \to (z \in ℝ \land y \in ℝ \land z < y)$
1107	1106	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)$
1108		oveq1	$⊢ j = i \to j T = i T$
1109	1108	oveq2d	$⊢ j = i \to y + j T = y + i T$
1110	1109	eleq1d	$⊢ j = i \to (y + j T \in A \leftrightarrow y + i T \in A)$
1111	1110	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))$
1112		oveq1	$⊢ k = l \to k T = l T$
1113	1112	oveq2d	$⊢ k = l \to z + k T = z + l T$
1114	1113	eleq1d	$⊢ k = l \to (z + k T \in A \leftrightarrow z + l T \in A)$
1115	1114	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))$
1116	1111 1115	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)$
1117		oveq1	$⊢ i = k \to i T = k T$
1118	1117	oveq2d	$⊢ i = k \to y + i T = y + k T$
1119	1118	eleq1d	$⊢ i = k \to (y + i T \in A \leftrightarrow y + k T \in A)$
1120	1119	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))$
1121		oveq1	$⊢ l = j \to l T = j T$
1122	1121	oveq2d	$⊢ l = j \to z + l T = z + j T$
1123	1122	eleq1d	$⊢ l = j \to (z + l T \in A \leftrightarrow z + j T \in A)$
1124	1123	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))$
1125	1120 1124	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)$
1126		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)$
1127		ancom	$⊢ (y + k T \in A \land z + j T \in A) \leftrightarrow (z + j T \in A \land y + k T \in A)$
1128	1127	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)$
1129	1125 1126 1128	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)$
1130	1116 1129	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)$
1131	1130	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)$
1132		eleq1	$⊢ b = y \to (b \in ℝ \leftrightarrow y \in ℝ)$
1133		breq2	$⊢ b = y \to (z < b \leftrightarrow z < y)$
1134	1132 1133	3anbi23d	$⊢ b = y \to ((z \in ℝ \land b \in ℝ \land z < b) \leftrightarrow (z \in ℝ \land y \in ℝ \land z < y))$
1135	1134	anbi2d	$⊢ b = y \to ((φ \land (z \in ℝ \land b \in ℝ \land z < b)) \leftrightarrow (φ \land (z \in ℝ \land y \in ℝ \land z < y)))$
1136		oveq1	$⊢ b = y \to b + k T = y + k T$
1137	1136	eleq1d	$⊢ b = y \to (b + k T \in A \leftrightarrow y + k T \in A)$
1138	1137	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))$
1139	1138	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))$
1140	1135 1139	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)))$
1141		oveq2	$⊢ b = y \to z - b = z - y$
1142	1141	fveq2d	$⊢ b = y \to \|z - b\| = \|z - y\|$
1143	1142	breq2d	$⊢ b = y \to (E \leq \|z - b\| \leftrightarrow E \leq \|z - y\|)$
1144	1140 1143	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\|))$
1145		eleq1	$⊢ a = z \to (a \in ℝ \leftrightarrow z \in ℝ)$
1146		breq1	$⊢ a = z \to (a < b \leftrightarrow z < b)$
1147	1145 1146	3anbi13d	$⊢ a = z \to ((a \in ℝ \land b \in ℝ \land a < b) \leftrightarrow (z \in ℝ \land b \in ℝ \land z < b))$
1148	1147	anbi2d	$⊢ a = z \to ((φ \land (a \in ℝ \land b \in ℝ \land a < b)) \leftrightarrow (φ \land (z \in ℝ \land b \in ℝ \land z < b)))$
1149		oveq1	$⊢ a = z \to a + j T = z + j T$
1150	1149	eleq1d	$⊢ a = z \to (a + j T \in A \leftrightarrow z + j T \in A)$
1151	1150	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))$
1152	1151	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))$
1153	1148 1152	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)))$
1154		oveq1	$⊢ a = z \to a - b = z - b$
1155	1154	fveq2d	$⊢ a = z \to \|a - b\| = \|z - b\|$
1156	1155	breq2d	$⊢ a = z \to (E \leq \|a - b\| \leftrightarrow E \leq \|z - b\|)$
1157	1153 1156	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\|))$
1158	1157 1087	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\|$
1159	1144 1158	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\|$
1160	1101 1107 1131 1159	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\|$
1161		recn	$⊢ z \in ℝ \to z \in ℂ$
1162	1161	adantl	$⊢ (y \in ℝ \land z \in ℝ) \to z \in ℂ$
1163		recn	$⊢ y \in ℝ \to y \in ℂ$
1164	1163	adantr	$⊢ (y \in ℝ \land z \in ℝ) \to y \in ℂ$
1165	1162 1164	abssubd	$⊢ (y \in ℝ \land z \in ℝ) \to \|z - y\| = \|y - z\|$
1166	1165	adantl	$⊢ (φ \land (y \in ℝ \land z \in ℝ)) \to \|z - y\| = \|y - z\|$
1167	1166	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\|$
1168	1160 1167	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\|$
1169	1168	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\|)$
1170	1169	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\|)$
1171	1170	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\|)$
1172	1100 1171	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\|$
1173	1090 1172	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\|$
1174	198 206 230 1173	syl21anc	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to E \leq \|y - z\|$
1175	389	ad2antrr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to E \in ℝ$
1176	200 203	resubcld	$⊢ (φ \land (y \in H \land z \in H)) \to y - z \in ℝ$
1177	1176	recnd	$⊢ (φ \land (y \in H \land z \in H)) \to y - z \in ℂ$
1178	1177	abscld	$⊢ (φ \land (y \in H \land z \in H)) \to \|y - z\| \in ℝ$
1179	1178	adantr	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to \|y - z\| \in ℝ$
1180	1175 1179	lenltd	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to (E \leq \|y - z\| \leftrightarrow \neg \|y - z\| < E)$
1181	1174 1180	mpbid	$⊢ ((φ \land (y \in H \land z \in H)) \land y \neq z) \to \neg \|y - z\| < E$
1182		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)$
1183	1181 1182	mpbir	$⊢ (φ \land (y \in H \land z \in H)) \to \neg (y \neq z \land \|y - z\| < E)$
1184	1183	ralrimivva	$⊢ φ \to \forall y \in H \forall z \in H \neg (y \neq z \land \|y - z\| < E)$
1185		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)$
1186	1184 1185	sylib	$⊢ φ \to \neg \exists y \in H \exists z \in H (y \neq z \land \|y - z\| < E)$
1187	1186	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)$
1188	197 1187	pm2.65da	$⊢ (φ \land x \in ⋃ K) \to \neg x \in limPt (J) (H)$
1189	1188	intnanrd	$⊢ (φ \land x \in ⋃ K) \to \neg (x \in limPt (J) (H) \land x \in [X, Y])$
1190		elin	$⊢ x \in (limPt (J) (H) \cap [X, Y]) \leftrightarrow (x \in limPt (J) (H) \land x \in [X, Y])$
1191	1189 1190	sylnibr	$⊢ (φ \land x \in ⋃ K) \to \neg x \in (limPt (J) (H) \cap [X, Y])$
1192	26	a1i	$⊢ (φ \land x \in ⋃ K) \to J \in Top$
1193	27	adantr	$⊢ (φ \land x \in ⋃ K) \to [X, Y] \subseteq ℝ$
1194	24	adantr	$⊢ (φ \land x \in ⋃ K) \to H \subseteq [X, Y]$
1195	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]$
1196	1192 1193 1194 1195	syl3anc	$⊢ (φ \land x \in ⋃ K) \to limPt (K) (H) = limPt (J) (H) \cap [X, Y]$
1197	1191 1196	neleqtrrd	$⊢ (φ \land x \in ⋃ K) \to \neg x \in limPt (K) (H)$
1198	1197	nrexdv	$⊢ φ \to \neg \exists x \in ⋃ K x \in limPt (K) (H)$
1199	1198	adantr	$⊢ (φ \land \neg H \in Fin) \to \neg \exists x \in ⋃ K x \in limPt (K) (H)$
1200	41 1199	condan	$⊢ φ \to H \in Fin$

Metamath Proof Explorer

Theorem fourierdlem42

Proof