Theorem stoweidlem13

Description: Lemma for stoweid . This lemma is used to prove the statement abs( f(t) - g(t) ) < 2 epsilon, in the last step of the proof in BrosowskiDeutsh p. 92. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem13.1	$$⊢\phi \to E\in {ℝ}^{+}$$
	stoweidlem13.2	$$⊢\phi \to X\in ℝ$$
	stoweidlem13.3	$$⊢\phi \to Y\in ℝ$$
	stoweidlem13.4	$$⊢\phi \to j\in ℝ$$
	stoweidlem13.5	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E<X$$
	stoweidlem13.6	$$⊢\phi \to X\le \left(j-\left(\frac{1}{3}\right)\right)E$$
	stoweidlem13.7	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E<Y$$
	stoweidlem13.8	$$⊢\phi \to Y<\left(j+\left(\frac{1}{3}\right)\right)E$$
Assertion	stoweidlem13	$$⊢\phi \to \left|Y-X\right|<2E$$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem13.1	$$⊢\phi \to E\in {ℝ}^{+}$$
2		stoweidlem13.2	$$⊢\phi \to X\in ℝ$$
3		stoweidlem13.3	$$⊢\phi \to Y\in ℝ$$
4		stoweidlem13.4	$$⊢\phi \to j\in ℝ$$
5		stoweidlem13.5	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E<X$$
6		stoweidlem13.6	$$⊢\phi \to X\le \left(j-\left(\frac{1}{3}\right)\right)E$$
7		stoweidlem13.7	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E<Y$$
8		stoweidlem13.8	$$⊢\phi \to Y<\left(j+\left(\frac{1}{3}\right)\right)E$$
9	3 2	resubcld	$$⊢\phi \to Y-X\in ℝ$$
10		2re	$$⊢2\in ℝ$$
11	1	rpred	$$⊢\phi \to E\in ℝ$$
12		remulcl	$$⊢\left(2\in ℝ\wedge E\in ℝ\right)\to 2E\in ℝ$$
13	10 11 12	sylancr	$$⊢\phi \to 2E\in ℝ$$
14	3	recnd	$$⊢\phi \to Y\in ℂ$$
15	2	recnd	$$⊢\phi \to X\in ℂ$$
16	14 15	negsubdi2d	$$⊢\phi \to -\left(Y-X\right)=X-Y$$
17	2 3	resubcld	$$⊢\phi \to X-Y\in ℝ$$
18		1red	$$⊢\phi \to 1\in ℝ$$
19	18 11	remulcld	$$⊢\phi \to 1E\in ℝ$$
20		3re	$$⊢3\in ℝ$$
21		3ne0	$$⊢3\ne 0$$
22	20 21	rereccli	$$⊢\frac{1}{3}\in ℝ$$
23	22	a1i	$$⊢\phi \to \frac{1}{3}\in ℝ$$
24	4 23	resubcld	$$⊢\phi \to j-\left(\frac{1}{3}\right)\in ℝ$$
25	24 11	remulcld	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)\right)E\in ℝ$$
26	25 3	resubcld	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)\right)E-Y\in ℝ$$
27		4re	$$⊢4\in ℝ$$
28	27 20 21	3pm3.2i	$$⊢\left(4\in ℝ\wedge 3\in ℝ\wedge 3\ne 0\right)$$
29		redivcl	$$⊢\left(4\in ℝ\wedge 3\in ℝ\wedge 3\ne 0\right)\to \frac{4}{3}\in ℝ$$
30	28 29	mp1i	$$⊢\phi \to \frac{4}{3}\in ℝ$$
31	4 30	resubcld	$$⊢\phi \to j-\left(\frac{4}{3}\right)\in ℝ$$
32	31 11	remulcld	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E\in ℝ$$
33	25 32	resubcld	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)\right)E-\left(j-\left(\frac{4}{3}\right)\right)E\in ℝ$$
34	2 25 3 6	lesub1dd	$$⊢\phi \to X-Y\le \left(j-\left(\frac{1}{3}\right)\right)E-Y$$
35	32 3 25 7	ltsub2dd	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)\right)E-Y<\left(j-\left(\frac{1}{3}\right)\right)E-\left(j-\left(\frac{4}{3}\right)\right)E$$
36	17 26 33 34 35	lelttrd	$$⊢\phi \to X-Y<\left(j-\left(\frac{1}{3}\right)\right)E-\left(j-\left(\frac{4}{3}\right)\right)E$$
37	4	recnd	$$⊢\phi \to j\in ℂ$$
38	23	recnd	$$⊢\phi \to \frac{1}{3}\in ℂ$$
39	37 38	subcld	$$⊢\phi \to j-\left(\frac{1}{3}\right)\in ℂ$$
40	30	recnd	$$⊢\phi \to \frac{4}{3}\in ℂ$$
41	37 40	subcld	$$⊢\phi \to j-\left(\frac{4}{3}\right)\in ℂ$$
42	11	recnd	$$⊢\phi \to E\in ℂ$$
43	39 41 42	subdird	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)-\left(j-\left(\frac{4}{3}\right)\right)\right)E=\left(j-\left(\frac{1}{3}\right)\right)E-\left(j-\left(\frac{4}{3}\right)\right)E$$
44	37 38 37 40	sub4d	$$⊢\phi \to j-\left(\frac{1}{3}\right)-\left(j-\left(\frac{4}{3}\right)\right)=j-j-\left(\left(\frac{1}{3}\right)-\left(\frac{4}{3}\right)\right)$$
45	37 37	subcld	$$⊢\phi \to j-j\in ℂ$$
46	45 38 40	subsub2d	$$⊢\phi \to j-j-\left(\left(\frac{1}{3}\right)-\left(\frac{4}{3}\right)\right)=\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)$$
47	44 46	eqtrd	$$⊢\phi \to j-\left(\frac{1}{3}\right)-\left(j-\left(\frac{4}{3}\right)\right)=\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)$$
48	47	oveq1d	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)-\left(j-\left(\frac{4}{3}\right)\right)\right)E=\left(\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)\right)E$$
49	43 48	eqtr3d	$$⊢\phi \to \left(j-\left(\frac{1}{3}\right)\right)E-\left(j-\left(\frac{4}{3}\right)\right)E=\left(\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)\right)E$$
50	36 49	breqtrd	$$⊢\phi \to X-Y<\left(\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)\right)E$$
51	37	subidd	$$⊢\phi \to j-j=0$$
52	51	oveq1d	$$⊢\phi \to \left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)=0+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)$$
53		4cn	$$⊢4\in ℂ$$
54		3cn	$$⊢3\in ℂ$$
55	53 54 21	divcli	$$⊢\frac{4}{3}\in ℂ$$
56		ax-1cn	$$⊢1\in ℂ$$
57	56 54 21	divcli	$$⊢\frac{1}{3}\in ℂ$$
58		1div1e1	$$⊢\frac{1}{1}=1$$
59	58	oveq2i	$$⊢\left(\frac{1}{3}\right)+\left(\frac{1}{1}\right)=\left(\frac{1}{3}\right)+1$$
60		ax-1ne0	$$⊢1\ne 0$$
61	56 54 56 56 21 60	divadddivi	$$⊢\left(\frac{1}{3}\right)+\left(\frac{1}{1}\right)=\frac{1\cdot 1+1\cdot 3}{3\cdot 1}$$
62	59 61	eqtr3i	$$⊢\left(\frac{1}{3}\right)+1=\frac{1\cdot 1+1\cdot 3}{3\cdot 1}$$
63	54 56	addcomi	$$⊢3+1=1+3$$
64		df-4	$$⊢4=3+1$$
65		1t1e1	$$⊢1\cdot 1=1$$
66	54	mulid2i	$$⊢1\cdot 3=3$$
67	65 66	oveq12i	$$⊢1\cdot 1+1\cdot 3=1+3$$
68	63 64 67	3eqtr4ri	$$⊢1\cdot 1+1\cdot 3=4$$
69	68	oveq1i	$$⊢\frac{1\cdot 1+1\cdot 3}{3\cdot 1}=\frac{4}{3\cdot 1}$$
70		3t1e3	$$⊢3\cdot 1=3$$
71	70	oveq2i	$$⊢\frac{4}{3\cdot 1}=\frac{4}{3}$$
72	62 69 71	3eqtri	$$⊢\left(\frac{1}{3}\right)+1=\frac{4}{3}$$
73	55 57 56 72	subaddrii	$$⊢\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)=1$$
74	73	oveq2i	$$⊢0+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)=0+1$$
75		1e0p1	$$⊢1=0+1$$
76	74 75	eqtr4i	$$⊢0+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)=1$$
77	52 76	eqtrdi	$$⊢\phi \to \left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)=1$$
78	77	oveq1d	$$⊢\phi \to \left(\left(j-j\right)+\left(\frac{4}{3}\right)-\left(\frac{1}{3}\right)\right)E=1E$$
79	50 78	breqtrd	$$⊢\phi \to X-Y<1E$$
80		1lt2	$$⊢1<2$$
81	10	a1i	$$⊢\phi \to 2\in ℝ$$
82	18 81 1	ltmul1d	$$⊢\phi \to \left(1<2\leftrightarrow 1E<2E\right)$$
83	80 82	mpbii	$$⊢\phi \to 1E<2E$$
84	17 19 13 79 83	lttrd	$$⊢\phi \to X-Y<2E$$
85	16 84	eqbrtrd	$$⊢\phi \to -\left(Y-X\right)<2E$$
86	9 13 85	ltnegcon1d	$$⊢\phi \to -2E<Y-X$$
87		5re	$$⊢5\in ℝ$$
88	87	a1i	$$⊢\phi \to 5\in ℝ$$
89	20	a1i	$$⊢\phi \to 3\in ℝ$$
90	21	a1i	$$⊢\phi \to 3\ne 0$$
91	88 89 90	redivcld	$$⊢\phi \to \frac{5}{3}\in ℝ$$
92	91 11	remulcld	$$⊢\phi \to \left(\frac{5}{3}\right)E\in ℝ$$
93	2	renegcld	$$⊢\phi \to -X\in ℝ$$
94	4 23	readdcld	$$⊢\phi \to j+\left(\frac{1}{3}\right)\in ℝ$$
95	94 11	remulcld	$$⊢\phi \to \left(j+\left(\frac{1}{3}\right)\right)E\in ℝ$$
96	32	renegcld	$$⊢\phi \to -\left(j-\left(\frac{4}{3}\right)\right)E\in ℝ$$
97	32 2	ltnegd	$$⊢\phi \to \left(\left(j-\left(\frac{4}{3}\right)\right)E<X\leftrightarrow -X<-\left(j-\left(\frac{4}{3}\right)\right)E\right)$$
98	5 97	mpbid	$$⊢\phi \to -X<-\left(j-\left(\frac{4}{3}\right)\right)E$$
99	3 93 95 96 8 98	lt2addd	$$⊢\phi \to Y+\left(-X\right)<\left(j+\left(\frac{1}{3}\right)\right)E+\left(-\left(j-\left(\frac{4}{3}\right)\right)E\right)$$
100	14 15	negsubd	$$⊢\phi \to Y+\left(-X\right)=Y-X$$
101	37 38 42	adddird	$$⊢\phi \to \left(j+\left(\frac{1}{3}\right)\right)E=jE+\left(\frac{1}{3}\right)E$$
102	37 40	negsubd	$$⊢\phi \to j+\left(-\frac{4}{3}\right)=j-\left(\frac{4}{3}\right)$$
103	102	eqcomd	$$⊢\phi \to j-\left(\frac{4}{3}\right)=j+\left(-\frac{4}{3}\right)$$
104	103	oveq1d	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E=\left(j+\left(-\frac{4}{3}\right)\right)E$$
105	40	negcld	$$⊢\phi \to -\frac{4}{3}\in ℂ$$
106	37 105 42	adddird	$$⊢\phi \to \left(j+\left(-\frac{4}{3}\right)\right)E=jE+\left(-\frac{4}{3}\right)E$$
107	40 42	mulneg1d	$$⊢\phi \to \left(-\frac{4}{3}\right)E=-\left(\frac{4}{3}\right)E$$
108	107	oveq2d	$$⊢\phi \to jE+\left(-\frac{4}{3}\right)E=jE+\left(-\left(\frac{4}{3}\right)E\right)$$
109	104 106 108	3eqtrd	$$⊢\phi \to \left(j-\left(\frac{4}{3}\right)\right)E=jE+\left(-\left(\frac{4}{3}\right)E\right)$$
110	109	negeqd	$$⊢\phi \to -\left(j-\left(\frac{4}{3}\right)\right)E=-\left(jE+\left(-\left(\frac{4}{3}\right)E\right)\right)$$
111	37 42	mulcld	$$⊢\phi \to jE\in ℂ$$
112	40 42	mulcld	$$⊢\phi \to \left(\frac{4}{3}\right)E\in ℂ$$
113	112	negcld	$$⊢\phi \to -\left(\frac{4}{3}\right)E\in ℂ$$
114	111 113	negdid	$$⊢\phi \to -\left(jE+\left(-\left(\frac{4}{3}\right)E\right)\right)=-jE+\left(-\left(-\left(\frac{4}{3}\right)E\right)\right)$$
115	112	negnegd	$$⊢\phi \to -\left(-\left(\frac{4}{3}\right)E\right)=\left(\frac{4}{3}\right)E$$
116	115	oveq2d	$$⊢\phi \to -jE+\left(-\left(-\left(\frac{4}{3}\right)E\right)\right)=-jE+\left(\frac{4}{3}\right)E$$
117	110 114 116	3eqtrd	$$⊢\phi \to -\left(j-\left(\frac{4}{3}\right)\right)E=-jE+\left(\frac{4}{3}\right)E$$
118	101 117	oveq12d	$$⊢\phi \to \left(j+\left(\frac{1}{3}\right)\right)E+\left(-\left(j-\left(\frac{4}{3}\right)\right)E\right)=jE+\left(\frac{1}{3}\right)E+\left(-jE\right)+\left(\frac{4}{3}\right)E$$
119	38 42	mulcld	$$⊢\phi \to \left(\frac{1}{3}\right)E\in ℂ$$
120	111	negcld	$$⊢\phi \to -jE\in ℂ$$
121	111 119 120 112	add4d	$$⊢\phi \to jE+\left(\frac{1}{3}\right)E+\left(-jE\right)+\left(\frac{4}{3}\right)E=jE+\left(-jE\right)+\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E$$
122	111	negidd	$$⊢\phi \to jE+\left(-jE\right)=0$$
123	122	oveq1d	$$⊢\phi \to jE+\left(-jE\right)+\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E=0+\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E$$
124	119 112	addcld	$$⊢\phi \to \left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E\in ℂ$$
125	124	addid2d	$$⊢\phi \to 0+\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E=\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E$$
126	121 123 125	3eqtrd	$$⊢\phi \to jE+\left(\frac{1}{3}\right)E+\left(-jE\right)+\left(\frac{4}{3}\right)E=\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E$$
127	38 40 42	adddird	$$⊢\phi \to \left(\left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)\right)E=\left(\frac{1}{3}\right)E+\left(\frac{4}{3}\right)E$$
128	89	recnd	$$⊢\phi \to 3\in ℂ$$
129	38 40	addcld	$$⊢\phi \to \left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)\in ℂ$$
130	128 38 40	adddid	$$⊢\phi \to 3\left(\left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)\right)=3\left(\frac{1}{3}\right)+3\left(\frac{4}{3}\right)$$
131	56 53	addcomi	$$⊢1+4=4+1$$
132	56 54 21	divcan2i	$$⊢3\left(\frac{1}{3}\right)=1$$
133	53 54 21	divcan2i	$$⊢3\left(\frac{4}{3}\right)=4$$
134	132 133	oveq12i	$$⊢3\left(\frac{1}{3}\right)+3\left(\frac{4}{3}\right)=1+4$$
135		df-5	$$⊢5=4+1$$
136	131 134 135	3eqtr4i	$$⊢3\left(\frac{1}{3}\right)+3\left(\frac{4}{3}\right)=5$$
137	130 136	eqtrdi	$$⊢\phi \to 3\left(\left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)\right)=5$$
138	128 129 90 137	mvllmuld	$$⊢\phi \to \left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)=\frac{5}{3}$$
139	138	oveq1d	$$⊢\phi \to \left(\left(\frac{1}{3}\right)+\left(\frac{4}{3}\right)\right)E=\left(\frac{5}{3}\right)E$$
140	126 127 139	3eqtr2d	$$⊢\phi \to jE+\left(\frac{1}{3}\right)E+\left(-jE\right)+\left(\frac{4}{3}\right)E=\left(\frac{5}{3}\right)E$$
141	118 140	eqtrd	$$⊢\phi \to \left(j+\left(\frac{1}{3}\right)\right)E+\left(-\left(j-\left(\frac{4}{3}\right)\right)E\right)=\left(\frac{5}{3}\right)E$$
142	99 100 141	3brtr3d	$$⊢\phi \to Y-X<\left(\frac{5}{3}\right)E$$
143		5lt6	$$⊢5<6$$
144		3t2e6	$$⊢3\cdot 2=6$$
145	143 144	breqtrri	$$⊢5<3\cdot 2$$
146		3pos	$$⊢0<3$$
147	20 146	pm3.2i	$$⊢\left(3\in ℝ\wedge 0<3\right)$$
148		ltdivmul	$$⊢\left(5\in ℝ\wedge 2\in ℝ\wedge \left(3\in ℝ\wedge 0<3\right)\right)\to \left(\frac{5}{3}<2\leftrightarrow 5<3\cdot 2\right)$$
149	87 10 147 148	mp3an	$$⊢\frac{5}{3}<2\leftrightarrow 5<3\cdot 2$$
150	145 149	mpbir	$$⊢\frac{5}{3}<2$$
151	150	a1i	$$⊢\phi \to \frac{5}{3}<2$$
152	91 81 1 151	ltmul1dd	$$⊢\phi \to \left(\frac{5}{3}\right)E<2E$$
153	9 92 13 142 152	lttrd	$$⊢\phi \to Y-X<2E$$
154	9 13	absltd	$$⊢\phi \to \left(\left|Y-X\right|<2E\leftrightarrow \left(-2E<Y-X\wedge Y-X<2E\right)\right)$$
155	86 153 154	mpbir2and	$$⊢\phi \to \left|Y-X\right|<2E$$