Step | Hyp | Ref
| Expression |
1 | | 0re 7959 |
. . . . . 6
โข 0 โ
โ |
2 | | maxabs 11220 |
. . . . . 6
โข ((๐ด โ โ โง 0 โ
โ) โ sup({๐ด, 0},
โ, < ) = (((๐ด + 0)
+ (absโ(๐ด โ
0))) / 2)) |
3 | 1, 2 | mpan2 425 |
. . . . 5
โข (๐ด โ โ โ
sup({๐ด, 0}, โ, < )
= (((๐ด + 0) +
(absโ(๐ด โ 0)))
/ 2)) |
4 | | recn 7946 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
5 | 4 | addid1d 8108 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด + 0) = ๐ด) |
6 | 4 | subid1d 8259 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด โ 0) = ๐ด) |
7 | 6 | fveq2d 5521 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ(๐ด โ 0)) =
(absโ๐ด)) |
8 | 5, 7 | oveq12d 5895 |
. . . . . 6
โข (๐ด โ โ โ ((๐ด + 0) + (absโ(๐ด โ 0))) = (๐ด + (absโ๐ด))) |
9 | 8 | oveq1d 5892 |
. . . . 5
โข (๐ด โ โ โ (((๐ด + 0) + (absโ(๐ด โ 0))) / 2) = ((๐ด + (absโ๐ด)) / 2)) |
10 | 3, 9 | eqtrd 2210 |
. . . 4
โข (๐ด โ โ โ
sup({๐ด, 0}, โ, < )
= ((๐ด + (absโ๐ด)) / 2)) |
11 | | renegcl 8220 |
. . . . . 6
โข (๐ด โ โ โ -๐ด โ
โ) |
12 | | maxabs 11220 |
. . . . . 6
โข ((-๐ด โ โ โง 0 โ
โ) โ sup({-๐ด,
0}, โ, < ) = (((-๐ด
+ 0) + (absโ(-๐ด
โ 0))) / 2)) |
13 | 11, 1, 12 | sylancl 413 |
. . . . 5
โข (๐ด โ โ โ
sup({-๐ด, 0}, โ, <
) = (((-๐ด + 0) +
(absโ(-๐ด โ 0)))
/ 2)) |
14 | 11 | recnd 7988 |
. . . . . . . 8
โข (๐ด โ โ โ -๐ด โ
โ) |
15 | 14 | addid1d 8108 |
. . . . . . 7
โข (๐ด โ โ โ (-๐ด + 0) = -๐ด) |
16 | 14 | subid1d 8259 |
. . . . . . . . 9
โข (๐ด โ โ โ (-๐ด โ 0) = -๐ด) |
17 | 16 | fveq2d 5521 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ(-๐ด โ 0))
= (absโ-๐ด)) |
18 | 4 | absnegd 11200 |
. . . . . . . 8
โข (๐ด โ โ โ
(absโ-๐ด) =
(absโ๐ด)) |
19 | 17, 18 | eqtrd 2210 |
. . . . . . 7
โข (๐ด โ โ โ
(absโ(-๐ด โ 0))
= (absโ๐ด)) |
20 | 15, 19 | oveq12d 5895 |
. . . . . 6
โข (๐ด โ โ โ ((-๐ด + 0) + (absโ(-๐ด โ 0))) = (-๐ด + (absโ๐ด))) |
21 | 20 | oveq1d 5892 |
. . . . 5
โข (๐ด โ โ โ (((-๐ด + 0) + (absโ(-๐ด โ 0))) / 2) = ((-๐ด + (absโ๐ด)) / 2)) |
22 | 13, 21 | eqtrd 2210 |
. . . 4
โข (๐ด โ โ โ
sup({-๐ด, 0}, โ, <
) = ((-๐ด + (absโ๐ด)) / 2)) |
23 | 10, 22 | oveq12d 5895 |
. . 3
โข (๐ด โ โ โ
(sup({๐ด, 0}, โ, <
) + sup({-๐ด, 0}, โ,
< )) = (((๐ด +
(absโ๐ด)) / 2) +
((-๐ด + (absโ๐ด)) / 2))) |
24 | 4 | abscld 11192 |
. . . . . 6
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
25 | 24 | recnd 7988 |
. . . . 5
โข (๐ด โ โ โ
(absโ๐ด) โ
โ) |
26 | 4, 25 | addcld 7979 |
. . . 4
โข (๐ด โ โ โ (๐ด + (absโ๐ด)) โ โ) |
27 | 14, 25 | addcld 7979 |
. . . 4
โข (๐ด โ โ โ (-๐ด + (absโ๐ด)) โ โ) |
28 | | 2cnd 8994 |
. . . 4
โข (๐ด โ โ โ 2 โ
โ) |
29 | | 2ap0 9014 |
. . . . 5
โข 2 #
0 |
30 | 29 | a1i 9 |
. . . 4
โข (๐ด โ โ โ 2 #
0) |
31 | 26, 27, 28, 30 | divdirapd 8788 |
. . 3
โข (๐ด โ โ โ (((๐ด + (absโ๐ด)) + (-๐ด + (absโ๐ด))) / 2) = (((๐ด + (absโ๐ด)) / 2) + ((-๐ด + (absโ๐ด)) / 2))) |
32 | 4, 25, 14, 25 | add4d 8128 |
. . . . 5
โข (๐ด โ โ โ ((๐ด + (absโ๐ด)) + (-๐ด + (absโ๐ด))) = ((๐ด + -๐ด) + ((absโ๐ด) + (absโ๐ด)))) |
33 | 4 | negidd 8260 |
. . . . . 6
โข (๐ด โ โ โ (๐ด + -๐ด) = 0) |
34 | 33 | oveq1d 5892 |
. . . . 5
โข (๐ด โ โ โ ((๐ด + -๐ด) + ((absโ๐ด) + (absโ๐ด))) = (0 + ((absโ๐ด) + (absโ๐ด)))) |
35 | 25, 25 | addcld 7979 |
. . . . . 6
โข (๐ด โ โ โ
((absโ๐ด) +
(absโ๐ด)) โ
โ) |
36 | 35 | addid2d 8109 |
. . . . 5
โข (๐ด โ โ โ (0 +
((absโ๐ด) +
(absโ๐ด))) =
((absโ๐ด) +
(absโ๐ด))) |
37 | 32, 34, 36 | 3eqtrd 2214 |
. . . 4
โข (๐ด โ โ โ ((๐ด + (absโ๐ด)) + (-๐ด + (absโ๐ด))) = ((absโ๐ด) + (absโ๐ด))) |
38 | 37 | oveq1d 5892 |
. . 3
โข (๐ด โ โ โ (((๐ด + (absโ๐ด)) + (-๐ด + (absโ๐ด))) / 2) = (((absโ๐ด) + (absโ๐ด)) / 2)) |
39 | 23, 31, 38 | 3eqtr2d 2216 |
. 2
โข (๐ด โ โ โ
(sup({๐ด, 0}, โ, <
) + sup({-๐ด, 0}, โ,
< )) = (((absโ๐ด) +
(absโ๐ด)) /
2)) |
40 | 25 | 2timesd 9163 |
. . 3
โข (๐ด โ โ โ (2
ยท (absโ๐ด)) =
((absโ๐ด) +
(absโ๐ด))) |
41 | 40 | oveq1d 5892 |
. 2
โข (๐ด โ โ โ ((2
ยท (absโ๐ด)) /
2) = (((absโ๐ด) +
(absโ๐ด)) /
2)) |
42 | 25, 28, 30 | divcanap3d 8754 |
. 2
โข (๐ด โ โ โ ((2
ยท (absโ๐ด)) /
2) = (absโ๐ด)) |
43 | 39, 41, 42 | 3eqtr2d 2216 |
1
โข (๐ด โ โ โ
(sup({๐ด, 0}, โ, <
) + sup({-๐ด, 0}, โ,
< )) = (absโ๐ด)) |