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 ⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
stoweidlem13.2 ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
stoweidlem13.3 ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
stoweidlem13.4 ⊢ ( 𝜑 → 𝑗 ∈ ℝ )
stoweidlem13.5 ⊢ ( 𝜑 → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < 𝑋 )
stoweidlem13.6 ⊢ ( 𝜑 → 𝑋 ≤ ( ( 𝑗 − ( 1 / 3 ) ) · 𝐸 ) )
stoweidlem13.7 ⊢ ( 𝜑 → ( ( 𝑗 − ( 4 / 3 ) ) · 𝐸 ) < 𝑌 )
stoweidlem13.8 ⊢ ( 𝜑 → 𝑌 < ( ( 𝑗 + ( 1 / 3 ) ) · 𝐸 ) )
Assertion stoweidlem13 ( 𝜑 → ( abs ‘ ( 𝑌 − 𝑋 ) ) < ( 2 · 𝐸 ) )

Proof

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