Proof of Theorem stoweidlem13
Step | Hyp | Ref
| Expression |
1 | | stoweidlem13.3 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
2 | | stoweidlem13.2 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ ℝ) |
3 | 1, 2 | resubcld 11401 |
. . 3
⊢ (𝜑 → (𝑌 − 𝑋) ∈ ℝ) |
4 | | 2re 12045 |
. . . 4
⊢ 2 ∈
ℝ |
5 | | stoweidlem13.1 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
6 | 5 | rpred 12769 |
. . . 4
⊢ (𝜑 → 𝐸 ∈ ℝ) |
7 | | remulcl 10955 |
. . . 4
⊢ ((2
∈ ℝ ∧ 𝐸
∈ ℝ) → (2 · 𝐸) ∈ ℝ) |
8 | 4, 6, 7 | sylancr 587 |
. . 3
⊢ (𝜑 → (2 · 𝐸) ∈
ℝ) |
9 | 1 | recnd 11002 |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ ℂ) |
10 | 2 | recnd 11002 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ ℂ) |
11 | 9, 10 | negsubdi2d 11346 |
. . . 4
⊢ (𝜑 → -(𝑌 − 𝑋) = (𝑋 − 𝑌)) |
12 | 2, 1 | resubcld 11401 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝑌) ∈ ℝ) |
13 | | 1red 10975 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
14 | 13, 6 | remulcld 11004 |
. . . . 5
⊢ (𝜑 → (1 · 𝐸) ∈
ℝ) |
15 | | stoweidlem13.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑗 ∈ ℝ) |
16 | | 3re 12051 |
. . . . . . . . . . . . 13
⊢ 3 ∈
ℝ |
17 | | 3ne0 12077 |
. . . . . . . . . . . . 13
⊢ 3 ≠
0 |
18 | 16, 17 | rereccli 11738 |
. . . . . . . . . . . 12
⊢ (1 / 3)
∈ ℝ |
19 | 18 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 3) ∈
ℝ) |
20 | 15, 19 | resubcld 11401 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 − (1 / 3)) ∈
ℝ) |
21 | 20, 6 | remulcld 11004 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − (1 / 3)) · 𝐸) ∈ ℝ) |
22 | 21, 1 | resubcld 11401 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − (1 / 3)) · 𝐸) − 𝑌) ∈ ℝ) |
23 | | 4re 12055 |
. . . . . . . . . . . . 13
⊢ 4 ∈
ℝ |
24 | 23, 16, 17 | 3pm3.2i 1338 |
. . . . . . . . . . . 12
⊢ (4 ∈
ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) |
25 | | redivcl 11692 |
. . . . . . . . . . . 12
⊢ ((4
∈ ℝ ∧ 3 ∈ ℝ ∧ 3 ≠ 0) → (4 / 3) ∈
ℝ) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → (4 / 3) ∈
ℝ) |
27 | 15, 26 | resubcld 11401 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 − (4 / 3)) ∈
ℝ) |
28 | 27, 6 | remulcld 11004 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ) |
29 | 21, 28 | resubcld 11401 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − (1 / 3)) · 𝐸) − ((𝑗 − (4 / 3)) · 𝐸)) ∈ ℝ) |
30 | | stoweidlem13.6 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ≤ ((𝑗 − (1 / 3)) · 𝐸)) |
31 | 2, 21, 1, 30 | lesub1dd 11589 |
. . . . . . . 8
⊢ (𝜑 → (𝑋 − 𝑌) ≤ (((𝑗 − (1 / 3)) · 𝐸) − 𝑌)) |
32 | | stoweidlem13.7 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) < 𝑌) |
33 | 28, 1, 21, 32 | ltsub2dd 11586 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − (1 / 3)) · 𝐸) − 𝑌) < (((𝑗 − (1 / 3)) · 𝐸) − ((𝑗 − (4 / 3)) · 𝐸))) |
34 | 12, 22, 29, 31, 33 | lelttrd 11131 |
. . . . . . 7
⊢ (𝜑 → (𝑋 − 𝑌) < (((𝑗 − (1 / 3)) · 𝐸) − ((𝑗 − (4 / 3)) · 𝐸))) |
35 | 15 | recnd 11002 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑗 ∈ ℂ) |
36 | 19 | recnd 11002 |
. . . . . . . . . 10
⊢ (𝜑 → (1 / 3) ∈
ℂ) |
37 | 35, 36 | subcld 11330 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 − (1 / 3)) ∈
ℂ) |
38 | 26 | recnd 11002 |
. . . . . . . . . 10
⊢ (𝜑 → (4 / 3) ∈
ℂ) |
39 | 35, 38 | subcld 11330 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 − (4 / 3)) ∈
ℂ) |
40 | 6 | recnd 11002 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℂ) |
41 | 37, 39, 40 | subdird 11430 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − (1 / 3)) − (𝑗 − (4 / 3))) · 𝐸) = (((𝑗 − (1 / 3)) · 𝐸) − ((𝑗 − (4 / 3)) · 𝐸))) |
42 | 35, 36, 35, 38 | sub4d 11379 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 − (1 / 3)) − (𝑗 − (4 / 3))) = ((𝑗 − 𝑗) − ((1 / 3) − (4 /
3)))) |
43 | 35, 35 | subcld 11330 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 − 𝑗) ∈ ℂ) |
44 | 43, 36, 38 | subsub2d 11359 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑗 − 𝑗) − ((1 / 3) − (4 / 3))) =
((𝑗 − 𝑗) + ((4 / 3) − (1 /
3)))) |
45 | 42, 44 | eqtrd 2780 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − (1 / 3)) − (𝑗 − (4 / 3))) = ((𝑗 − 𝑗) + ((4 / 3) − (1 /
3)))) |
46 | 45 | oveq1d 7284 |
. . . . . . . 8
⊢ (𝜑 → (((𝑗 − (1 / 3)) − (𝑗 − (4 / 3))) · 𝐸) = (((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) · 𝐸)) |
47 | 41, 46 | eqtr3d 2782 |
. . . . . . 7
⊢ (𝜑 → (((𝑗 − (1 / 3)) · 𝐸) − ((𝑗 − (4 / 3)) · 𝐸)) = (((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) · 𝐸)) |
48 | 34, 47 | breqtrd 5105 |
. . . . . 6
⊢ (𝜑 → (𝑋 − 𝑌) < (((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) · 𝐸)) |
49 | 35 | subidd 11318 |
. . . . . . . . 9
⊢ (𝜑 → (𝑗 − 𝑗) = 0) |
50 | 49 | oveq1d 7284 |
. . . . . . . 8
⊢ (𝜑 → ((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) = (0 + ((4 /
3) − (1 / 3)))) |
51 | | 4cn 12056 |
. . . . . . . . . . . 12
⊢ 4 ∈
ℂ |
52 | | 3cn 12052 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℂ |
53 | 51, 52, 17 | divcli 11715 |
. . . . . . . . . . 11
⊢ (4 / 3)
∈ ℂ |
54 | | ax-1cn 10928 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
55 | 54, 52, 17 | divcli 11715 |
. . . . . . . . . . 11
⊢ (1 / 3)
∈ ℂ |
56 | | 1div1e1 11663 |
. . . . . . . . . . . . . 14
⊢ (1 / 1) =
1 |
57 | 56 | oveq2i 7280 |
. . . . . . . . . . . . 13
⊢ ((1 / 3)
+ (1 / 1)) = ((1 / 3) + 1) |
58 | | ax-1ne0 10939 |
. . . . . . . . . . . . . 14
⊢ 1 ≠
0 |
59 | 54, 52, 54, 54, 17, 58 | divadddivi 11735 |
. . . . . . . . . . . . 13
⊢ ((1 / 3)
+ (1 / 1)) = (((1 · 1) + (1 · 3)) / (3 ·
1)) |
60 | 57, 59 | eqtr3i 2770 |
. . . . . . . . . . . 12
⊢ ((1 / 3)
+ 1) = (((1 · 1) + (1 · 3)) / (3 · 1)) |
61 | 52, 54 | addcomi 11164 |
. . . . . . . . . . . . . 14
⊢ (3 + 1) =
(1 + 3) |
62 | | df-4 12036 |
. . . . . . . . . . . . . 14
⊢ 4 = (3 +
1) |
63 | | 1t1e1 12133 |
. . . . . . . . . . . . . . 15
⊢ (1
· 1) = 1 |
64 | 52 | mulid2i 10979 |
. . . . . . . . . . . . . . 15
⊢ (1
· 3) = 3 |
65 | 63, 64 | oveq12i 7281 |
. . . . . . . . . . . . . 14
⊢ ((1
· 1) + (1 · 3)) = (1 + 3) |
66 | 61, 62, 65 | 3eqtr4ri 2779 |
. . . . . . . . . . . . 13
⊢ ((1
· 1) + (1 · 3)) = 4 |
67 | 66 | oveq1i 7279 |
. . . . . . . . . . . 12
⊢ (((1
· 1) + (1 · 3)) / (3 · 1)) = (4 / (3 ·
1)) |
68 | | 3t1e3 12136 |
. . . . . . . . . . . . 13
⊢ (3
· 1) = 3 |
69 | 68 | oveq2i 7280 |
. . . . . . . . . . . 12
⊢ (4 / (3
· 1)) = (4 / 3) |
70 | 60, 67, 69 | 3eqtri 2772 |
. . . . . . . . . . 11
⊢ ((1 / 3)
+ 1) = (4 / 3) |
71 | 53, 55, 54, 70 | subaddrii 11308 |
. . . . . . . . . 10
⊢ ((4 / 3)
− (1 / 3)) = 1 |
72 | 71 | oveq2i 7280 |
. . . . . . . . 9
⊢ (0 + ((4
/ 3) − (1 / 3))) = (0 + 1) |
73 | | 1e0p1 12476 |
. . . . . . . . 9
⊢ 1 = (0 +
1) |
74 | 72, 73 | eqtr4i 2771 |
. . . . . . . 8
⊢ (0 + ((4
/ 3) − (1 / 3))) = 1 |
75 | 50, 74 | eqtrdi 2796 |
. . . . . . 7
⊢ (𝜑 → ((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) =
1) |
76 | 75 | oveq1d 7284 |
. . . . . 6
⊢ (𝜑 → (((𝑗 − 𝑗) + ((4 / 3) − (1 / 3))) · 𝐸) = (1 · 𝐸)) |
77 | 48, 76 | breqtrd 5105 |
. . . . 5
⊢ (𝜑 → (𝑋 − 𝑌) < (1 · 𝐸)) |
78 | | 1lt2 12142 |
. . . . . 6
⊢ 1 <
2 |
79 | 4 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 2 ∈
ℝ) |
80 | 13, 79, 5 | ltmul1d 12810 |
. . . . . 6
⊢ (𝜑 → (1 < 2 ↔ (1
· 𝐸) < (2
· 𝐸))) |
81 | 78, 80 | mpbii 232 |
. . . . 5
⊢ (𝜑 → (1 · 𝐸) < (2 · 𝐸)) |
82 | 12, 14, 8, 77, 81 | lttrd 11134 |
. . . 4
⊢ (𝜑 → (𝑋 − 𝑌) < (2 · 𝐸)) |
83 | 11, 82 | eqbrtrd 5101 |
. . 3
⊢ (𝜑 → -(𝑌 − 𝑋) < (2 · 𝐸)) |
84 | 3, 8, 83 | ltnegcon1d 11553 |
. 2
⊢ (𝜑 → -(2 · 𝐸) < (𝑌 − 𝑋)) |
85 | | 5re 12058 |
. . . . . 6
⊢ 5 ∈
ℝ |
86 | 85 | a1i 11 |
. . . . 5
⊢ (𝜑 → 5 ∈
ℝ) |
87 | 16 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ∈
ℝ) |
88 | 17 | a1i 11 |
. . . . 5
⊢ (𝜑 → 3 ≠ 0) |
89 | 86, 87, 88 | redivcld 11801 |
. . . 4
⊢ (𝜑 → (5 / 3) ∈
ℝ) |
90 | 89, 6 | remulcld 11004 |
. . 3
⊢ (𝜑 → ((5 / 3) · 𝐸) ∈
ℝ) |
91 | 2 | renegcld 11400 |
. . . . 5
⊢ (𝜑 → -𝑋 ∈ ℝ) |
92 | 15, 19 | readdcld 11003 |
. . . . . 6
⊢ (𝜑 → (𝑗 + (1 / 3)) ∈ ℝ) |
93 | 92, 6 | remulcld 11004 |
. . . . 5
⊢ (𝜑 → ((𝑗 + (1 / 3)) · 𝐸) ∈ ℝ) |
94 | 28 | renegcld 11400 |
. . . . 5
⊢ (𝜑 → -((𝑗 − (4 / 3)) · 𝐸) ∈ ℝ) |
95 | | stoweidlem13.8 |
. . . . 5
⊢ (𝜑 → 𝑌 < ((𝑗 + (1 / 3)) · 𝐸)) |
96 | | stoweidlem13.5 |
. . . . . 6
⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) < 𝑋) |
97 | 28, 2 | ltnegd 11551 |
. . . . . 6
⊢ (𝜑 → (((𝑗 − (4 / 3)) · 𝐸) < 𝑋 ↔ -𝑋 < -((𝑗 − (4 / 3)) · 𝐸))) |
98 | 96, 97 | mpbid 231 |
. . . . 5
⊢ (𝜑 → -𝑋 < -((𝑗 − (4 / 3)) · 𝐸)) |
99 | 1, 91, 93, 94, 95, 98 | lt2addd 11596 |
. . . 4
⊢ (𝜑 → (𝑌 + -𝑋) < (((𝑗 + (1 / 3)) · 𝐸) + -((𝑗 − (4 / 3)) · 𝐸))) |
100 | 9, 10 | negsubd 11336 |
. . . 4
⊢ (𝜑 → (𝑌 + -𝑋) = (𝑌 − 𝑋)) |
101 | 35, 36, 40 | adddird 10999 |
. . . . . 6
⊢ (𝜑 → ((𝑗 + (1 / 3)) · 𝐸) = ((𝑗 · 𝐸) + ((1 / 3) · 𝐸))) |
102 | 35, 38 | negsubd 11336 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑗 + -(4 / 3)) = (𝑗 − (4 / 3))) |
103 | 102 | eqcomd 2746 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑗 − (4 / 3)) = (𝑗 + -(4 / 3))) |
104 | 103 | oveq1d 7284 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) = ((𝑗 + -(4 / 3)) · 𝐸)) |
105 | 38 | negcld 11317 |
. . . . . . . . . 10
⊢ (𝜑 → -(4 / 3) ∈
ℂ) |
106 | 35, 105, 40 | adddird 10999 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 + -(4 / 3)) · 𝐸) = ((𝑗 · 𝐸) + (-(4 / 3) · 𝐸))) |
107 | 38, 40 | mulneg1d 11426 |
. . . . . . . . . 10
⊢ (𝜑 → (-(4 / 3) · 𝐸) = -((4 / 3) · 𝐸)) |
108 | 107 | oveq2d 7285 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑗 · 𝐸) + (-(4 / 3) · 𝐸)) = ((𝑗 · 𝐸) + -((4 / 3) · 𝐸))) |
109 | 104, 106,
108 | 3eqtrd 2784 |
. . . . . . . 8
⊢ (𝜑 → ((𝑗 − (4 / 3)) · 𝐸) = ((𝑗 · 𝐸) + -((4 / 3) · 𝐸))) |
110 | 109 | negeqd 11213 |
. . . . . . 7
⊢ (𝜑 → -((𝑗 − (4 / 3)) · 𝐸) = -((𝑗 · 𝐸) + -((4 / 3) · 𝐸))) |
111 | 35, 40 | mulcld 10994 |
. . . . . . . 8
⊢ (𝜑 → (𝑗 · 𝐸) ∈ ℂ) |
112 | 38, 40 | mulcld 10994 |
. . . . . . . . 9
⊢ (𝜑 → ((4 / 3) · 𝐸) ∈
ℂ) |
113 | 112 | negcld 11317 |
. . . . . . . 8
⊢ (𝜑 → -((4 / 3) · 𝐸) ∈
ℂ) |
114 | 111, 113 | negdid 11343 |
. . . . . . 7
⊢ (𝜑 → -((𝑗 · 𝐸) + -((4 / 3) · 𝐸)) = (-(𝑗 · 𝐸) + --((4 / 3) · 𝐸))) |
115 | 112 | negnegd 11321 |
. . . . . . . 8
⊢ (𝜑 → --((4 / 3) · 𝐸) = ((4 / 3) · 𝐸)) |
116 | 115 | oveq2d 7285 |
. . . . . . 7
⊢ (𝜑 → (-(𝑗 · 𝐸) + --((4 / 3) · 𝐸)) = (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸))) |
117 | 110, 114,
116 | 3eqtrd 2784 |
. . . . . 6
⊢ (𝜑 → -((𝑗 − (4 / 3)) · 𝐸) = (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸))) |
118 | 101, 117 | oveq12d 7287 |
. . . . 5
⊢ (𝜑 → (((𝑗 + (1 / 3)) · 𝐸) + -((𝑗 − (4 / 3)) · 𝐸)) = (((𝑗 · 𝐸) + ((1 / 3) · 𝐸)) + (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸)))) |
119 | 36, 40 | mulcld 10994 |
. . . . . . . 8
⊢ (𝜑 → ((1 / 3) · 𝐸) ∈
ℂ) |
120 | 111 | negcld 11317 |
. . . . . . . 8
⊢ (𝜑 → -(𝑗 · 𝐸) ∈ ℂ) |
121 | 111, 119,
120, 112 | add4d 11201 |
. . . . . . 7
⊢ (𝜑 → (((𝑗 · 𝐸) + ((1 / 3) · 𝐸)) + (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸))) = (((𝑗 · 𝐸) + -(𝑗 · 𝐸)) + (((1 / 3) · 𝐸) + ((4 / 3) · 𝐸)))) |
122 | 111 | negidd 11320 |
. . . . . . . 8
⊢ (𝜑 → ((𝑗 · 𝐸) + -(𝑗 · 𝐸)) = 0) |
123 | 122 | oveq1d 7284 |
. . . . . . 7
⊢ (𝜑 → (((𝑗 · 𝐸) + -(𝑗 · 𝐸)) + (((1 / 3) · 𝐸) + ((4 / 3) · 𝐸))) = (0 + (((1 / 3) · 𝐸) + ((4 / 3) · 𝐸)))) |
124 | 119, 112 | addcld 10993 |
. . . . . . . 8
⊢ (𝜑 → (((1 / 3) · 𝐸) + ((4 / 3) · 𝐸)) ∈
ℂ) |
125 | 124 | addid2d 11174 |
. . . . . . 7
⊢ (𝜑 → (0 + (((1 / 3) ·
𝐸) + ((4 / 3) ·
𝐸))) = (((1 / 3) ·
𝐸) + ((4 / 3) ·
𝐸))) |
126 | 121, 123,
125 | 3eqtrd 2784 |
. . . . . 6
⊢ (𝜑 → (((𝑗 · 𝐸) + ((1 / 3) · 𝐸)) + (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸))) = (((1 / 3) · 𝐸) + ((4 / 3) · 𝐸))) |
127 | 36, 38, 40 | adddird 10999 |
. . . . . 6
⊢ (𝜑 → (((1 / 3) + (4 / 3))
· 𝐸) = (((1 / 3)
· 𝐸) + ((4 / 3)
· 𝐸))) |
128 | 87 | recnd 11002 |
. . . . . . . 8
⊢ (𝜑 → 3 ∈
ℂ) |
129 | 36, 38 | addcld 10993 |
. . . . . . . 8
⊢ (𝜑 → ((1 / 3) + (4 / 3)) ∈
ℂ) |
130 | 128, 36, 38 | adddid 10998 |
. . . . . . . . 9
⊢ (𝜑 → (3 · ((1 / 3) + (4
/ 3))) = ((3 · (1 / 3)) + (3 · (4 / 3)))) |
131 | 54, 51 | addcomi 11164 |
. . . . . . . . . 10
⊢ (1 + 4) =
(4 + 1) |
132 | 54, 52, 17 | divcan2i 11716 |
. . . . . . . . . . 11
⊢ (3
· (1 / 3)) = 1 |
133 | 51, 52, 17 | divcan2i 11716 |
. . . . . . . . . . 11
⊢ (3
· (4 / 3)) = 4 |
134 | 132, 133 | oveq12i 7281 |
. . . . . . . . . 10
⊢ ((3
· (1 / 3)) + (3 · (4 / 3))) = (1 + 4) |
135 | | df-5 12037 |
. . . . . . . . . 10
⊢ 5 = (4 +
1) |
136 | 131, 134,
135 | 3eqtr4i 2778 |
. . . . . . . . 9
⊢ ((3
· (1 / 3)) + (3 · (4 / 3))) = 5 |
137 | 130, 136 | eqtrdi 2796 |
. . . . . . . 8
⊢ (𝜑 → (3 · ((1 / 3) + (4
/ 3))) = 5) |
138 | 128, 129,
88, 137 | mvllmuld 11805 |
. . . . . . 7
⊢ (𝜑 → ((1 / 3) + (4 / 3)) = (5 /
3)) |
139 | 138 | oveq1d 7284 |
. . . . . 6
⊢ (𝜑 → (((1 / 3) + (4 / 3))
· 𝐸) = ((5 / 3)
· 𝐸)) |
140 | 126, 127,
139 | 3eqtr2d 2786 |
. . . . 5
⊢ (𝜑 → (((𝑗 · 𝐸) + ((1 / 3) · 𝐸)) + (-(𝑗 · 𝐸) + ((4 / 3) · 𝐸))) = ((5 / 3) · 𝐸)) |
141 | 118, 140 | eqtrd 2780 |
. . . 4
⊢ (𝜑 → (((𝑗 + (1 / 3)) · 𝐸) + -((𝑗 − (4 / 3)) · 𝐸)) = ((5 / 3) · 𝐸)) |
142 | 99, 100, 141 | 3brtr3d 5110 |
. . 3
⊢ (𝜑 → (𝑌 − 𝑋) < ((5 / 3) · 𝐸)) |
143 | | 5lt6 12152 |
. . . . . . 7
⊢ 5 <
6 |
144 | | 3t2e6 12137 |
. . . . . . 7
⊢ (3
· 2) = 6 |
145 | 143, 144 | breqtrri 5106 |
. . . . . 6
⊢ 5 < (3
· 2) |
146 | | 3pos 12076 |
. . . . . . . 8
⊢ 0 <
3 |
147 | 16, 146 | pm3.2i 471 |
. . . . . . 7
⊢ (3 ∈
ℝ ∧ 0 < 3) |
148 | | ltdivmul 11848 |
. . . . . . 7
⊢ ((5
∈ ℝ ∧ 2 ∈ ℝ ∧ (3 ∈ ℝ ∧ 0 < 3))
→ ((5 / 3) < 2 ↔ 5 < (3 · 2))) |
149 | 85, 4, 147, 148 | mp3an 1460 |
. . . . . 6
⊢ ((5 / 3)
< 2 ↔ 5 < (3 · 2)) |
150 | 145, 149 | mpbir 230 |
. . . . 5
⊢ (5 / 3)
< 2 |
151 | 150 | a1i 11 |
. . . 4
⊢ (𝜑 → (5 / 3) <
2) |
152 | 89, 79, 5, 151 | ltmul1dd 12824 |
. . 3
⊢ (𝜑 → ((5 / 3) · 𝐸) < (2 · 𝐸)) |
153 | 3, 90, 8, 142, 152 | lttrd 11134 |
. 2
⊢ (𝜑 → (𝑌 − 𝑋) < (2 · 𝐸)) |
154 | 3, 8 | absltd 15137 |
. 2
⊢ (𝜑 → ((abs‘(𝑌 − 𝑋)) < (2 · 𝐸) ↔ (-(2 · 𝐸) < (𝑌 − 𝑋) ∧ (𝑌 − 𝑋) < (2 · 𝐸)))) |
155 | 84, 153, 154 | mpbir2and 710 |
1
⊢ (𝜑 → (abs‘(𝑌 − 𝑋)) < (2 · 𝐸)) |