Step | Hyp | Ref
| Expression |
1 | | maxabslemlub.clt |
. . 3
โข (๐ โ ๐ถ < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
2 | | maxabslemlub.c |
. . . 4
โข (๐ โ ๐ถ โ โ) |
3 | | maxabslemlub.a |
. . . . . . 7
โข (๐ โ ๐ด โ โ) |
4 | | maxabslemlub.b |
. . . . . . 7
โข (๐ โ ๐ต โ โ) |
5 | 3, 4 | readdcld 7987 |
. . . . . 6
โข (๐ โ (๐ด + ๐ต) โ โ) |
6 | 3 | recnd 7986 |
. . . . . . . 8
โข (๐ โ ๐ด โ โ) |
7 | 4 | recnd 7986 |
. . . . . . . 8
โข (๐ โ ๐ต โ โ) |
8 | 6, 7 | subcld 8268 |
. . . . . . 7
โข (๐ โ (๐ด โ ๐ต) โ โ) |
9 | 8 | abscld 11190 |
. . . . . 6
โข (๐ โ (absโ(๐ด โ ๐ต)) โ โ) |
10 | 5, 9 | readdcld 7987 |
. . . . 5
โข (๐ โ ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) โ โ) |
11 | 10 | rehalfcld 9165 |
. . . 4
โข (๐ โ (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) โ โ) |
12 | | axltwlin 8025 |
. . . 4
โข ((๐ถ โ โ โง (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) โ โ โง ๐ด โ โ) โ (๐ถ < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) โ (๐ถ < ๐ด โจ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)))) |
13 | 2, 11, 3, 12 | syl3anc 1238 |
. . 3
โข (๐ โ (๐ถ < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) โ (๐ถ < ๐ด โจ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)))) |
14 | 1, 13 | mpd 13 |
. 2
โข (๐ โ (๐ถ < ๐ด โจ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2))) |
15 | 1 | adantr 276 |
. . . . 5
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ถ < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
16 | 3 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ด โ โ) |
17 | 4 | adantr 276 |
. . . . . 6
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ต โ โ) |
18 | 16, 17 | resubcld 8338 |
. . . . . . . 8
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (๐ด โ ๐ต) โ โ) |
19 | | 2re 8989 |
. . . . . . . . . . . . . 14
โข 2 โ
โ |
20 | 19 | a1i 9 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ 2 โ
โ) |
21 | 20, 16 | remulcld 7988 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (2 ยท ๐ด) โ
โ) |
22 | 21 | recnd 7986 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (2 ยท ๐ด) โ
โ) |
23 | 6 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ด โ โ) |
24 | 7 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ต โ โ) |
25 | 22, 23, 24 | subsub4d 8299 |
. . . . . . . . . 10
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (((2 ยท ๐ด) โ ๐ด) โ ๐ต) = ((2 ยท ๐ด) โ (๐ด + ๐ต))) |
26 | | 2cnd 8992 |
. . . . . . . . . . . . . 14
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ 2 โ
โ) |
27 | 26, 23 | mulsubfacd 8375 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) โ ๐ด) = ((2 โ 1) ยท ๐ด)) |
28 | | 2m1e1 9037 |
. . . . . . . . . . . . . 14
โข (2
โ 1) = 1 |
29 | 28 | oveq1i 5885 |
. . . . . . . . . . . . 13
โข ((2
โ 1) ยท ๐ด) = (1
ยท ๐ด) |
30 | 27, 29 | eqtrdi 2226 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) โ ๐ด) = (1 ยท ๐ด)) |
31 | 23 | mulid2d 7976 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (1 ยท ๐ด) = ๐ด) |
32 | 30, 31 | eqtrd 2210 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) โ ๐ด) = ๐ด) |
33 | 32 | oveq1d 5890 |
. . . . . . . . . 10
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (((2 ยท ๐ด) โ ๐ด) โ ๐ต) = (๐ด โ ๐ต)) |
34 | 25, 33 | eqtr3d 2212 |
. . . . . . . . 9
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) โ (๐ด + ๐ต)) = (๐ด โ ๐ต)) |
35 | | simpr 110 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
36 | 10 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) โ โ) |
37 | | 2rp 9658 |
. . . . . . . . . . . . 13
โข 2 โ
โ+ |
38 | 37 | a1i 9 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ 2 โ
โ+) |
39 | 16, 36, 38 | ltmuldiv2d 9745 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) < ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) โ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2))) |
40 | 35, 39 | mpbird 167 |
. . . . . . . . . 10
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (2 ยท ๐ด) < ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต)))) |
41 | 5 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (๐ด + ๐ต) โ โ) |
42 | 9 | adantr 276 |
. . . . . . . . . . 11
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (absโ(๐ด โ ๐ต)) โ โ) |
43 | 21, 41, 42 | ltsubadd2d 8500 |
. . . . . . . . . 10
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (((2 ยท ๐ด) โ (๐ด + ๐ต)) < (absโ(๐ด โ ๐ต)) โ (2 ยท ๐ด) < ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))))) |
44 | 40, 43 | mpbird 167 |
. . . . . . . . 9
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((2 ยท ๐ด) โ (๐ด + ๐ต)) < (absโ(๐ด โ ๐ต))) |
45 | 34, 44 | eqbrtrrd 4028 |
. . . . . . . 8
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (๐ด โ ๐ต) < (absโ(๐ด โ ๐ต))) |
46 | | ltabs 11096 |
. . . . . . . 8
โข (((๐ด โ ๐ต) โ โ โง (๐ด โ ๐ต) < (absโ(๐ด โ ๐ต))) โ (๐ด โ ๐ต) < 0) |
47 | 18, 45, 46 | syl2anc 411 |
. . . . . . 7
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (๐ด โ ๐ต) < 0) |
48 | 16, 17 | sublt0d 8527 |
. . . . . . 7
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ((๐ด โ ๐ต) < 0 โ ๐ด < ๐ต)) |
49 | 47, 48 | mpbid 147 |
. . . . . 6
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ด < ๐ต) |
50 | 16, 17, 49 | maxabslemab 11215 |
. . . . 5
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) = ๐ต) |
51 | 15, 50 | breqtrd 4030 |
. . . 4
โข ((๐ โง ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ ๐ถ < ๐ต) |
52 | 51 | ex 115 |
. . 3
โข (๐ โ (๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) โ ๐ถ < ๐ต)) |
53 | 52 | orim2d 788 |
. 2
โข (๐ โ ((๐ถ < ๐ด โจ ๐ด < (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) โ (๐ถ < ๐ด โจ ๐ถ < ๐ต))) |
54 | 14, 53 | mpd 13 |
1
โข (๐ โ (๐ถ < ๐ด โจ ๐ถ < ๐ต)) |