Metamath Proof Explorer

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 
|- ( ph -> E e. RR+ )
stoweidlem13.2 
|- ( ph -> X e. RR )
stoweidlem13.3 
|- ( ph -> Y e. RR )
stoweidlem13.4 
|- ( ph -> j e. RR )
stoweidlem13.5 
|- ( ph -> ( ( j - ( 4 / 3 ) ) x. E ) < X )
stoweidlem13.6 
|- ( ph -> X <_ ( ( j - ( 1 / 3 ) ) x. E ) )
stoweidlem13.7 
|- ( ph -> ( ( j - ( 4 / 3 ) ) x. E ) < Y )
stoweidlem13.8 
|- ( ph -> Y < ( ( j + ( 1 / 3 ) ) x. E ) )
Assertion stoweidlem13 
|- ( ph -> ( abs ` ( Y - X ) ) < ( 2 x. E ) )

Proof

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