Step | Hyp | Ref
| Expression |
1 | | simpl1 1000 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ด โ โ) |
2 | | simpl2 1001 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ต โ โ) |
3 | | maxcl 11218 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
sup({๐ด, ๐ต}, โ, < ) โ
โ) |
4 | 1, 2, 3 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ sup({๐ด, ๐ต}, โ, < ) โ
โ) |
5 | | simpl3 1002 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ถ โ โ) |
6 | | maxle1 11219 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โค sup({๐ด, ๐ต}, โ, < )) |
7 | 6 | 3adant3 1017 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ด โค sup({๐ด, ๐ต}, โ, < )) |
8 | 7 | adantr 276 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ด โค sup({๐ด, ๐ต}, โ, < )) |
9 | | simpr 110 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ sup({๐ด, ๐ต}, โ, < ) < ๐ถ) |
10 | 1, 4, 5, 8, 9 | lelttrd 8081 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ด < ๐ถ) |
11 | | maxle2 11220 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โค sup({๐ด, ๐ต}, โ, < )) |
12 | 1, 2, 11 | syl2anc 411 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ต โค sup({๐ด, ๐ต}, โ, < )) |
13 | 2, 4, 5, 12, 9 | lelttrd 8081 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ ๐ต < ๐ถ) |
14 | 10, 13 | jca 306 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง
sup({๐ด, ๐ต}, โ, < ) < ๐ถ) โ (๐ด < ๐ถ โง ๐ต < ๐ถ)) |
15 | | maxabs 11217 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ
sup({๐ด, ๐ต}, โ, < ) = (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
16 | 15 | 3adant3 1017 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
sup({๐ด, ๐ต}, โ, < ) = (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
17 | 16 | adantr 276 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ sup({๐ด, ๐ต}, โ, < ) = (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2)) |
18 | | 2re 8988 |
. . . . . . . . . . . 12
โข 2 โ
โ |
19 | 18 | a1i 9 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ 2 โ โ) |
20 | | simpl3 1002 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ถ โ โ) |
21 | 19, 20 | remulcld 7987 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ถ) โ โ) |
22 | 21 | recnd 7985 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ถ) โ โ) |
23 | | simpl1 1000 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ด โ โ) |
24 | 23 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ด โ โ) |
25 | | simpl2 1001 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ต โ โ) |
26 | 25 | recnd 7985 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ต โ โ) |
27 | 24, 26 | addcld 7976 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด + ๐ต) โ โ) |
28 | 22, 27 | negsubdi2d 8283 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ -((2 ยท ๐ถ) โ (๐ด + ๐ต)) = ((๐ด + ๐ต) โ (2 ยท ๐ถ))) |
29 | 23, 25 | readdcld 7986 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด + ๐ต) โ โ) |
30 | 23, 25 | resubcld 8337 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด โ ๐ต) โ โ) |
31 | 26 | 2timesd 9160 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ต) = (๐ต + ๐ต)) |
32 | 24, 26, 26 | pnncand 8306 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) = (๐ต + ๐ต)) |
33 | 31, 32 | eqtr4d 2213 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ต) = ((๐ด + ๐ต) โ (๐ด โ ๐ต))) |
34 | | 2rp 9657 |
. . . . . . . . . . . 12
โข 2 โ
โ+ |
35 | 34 | a1i 9 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ 2 โ
โ+) |
36 | | simprr 531 |
. . . . . . . . . . 11
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ต < ๐ถ) |
37 | 25, 20, 35, 36 | ltmul2dd 9752 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ต) < (2 ยท ๐ถ)) |
38 | 33, 37 | eqbrtrrd 4027 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) โ (๐ด โ ๐ต)) < (2 ยท ๐ถ)) |
39 | 29, 30, 21, 38 | ltsub23d 8506 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) โ (2 ยท ๐ถ)) < (๐ด โ ๐ต)) |
40 | 28, 39 | eqbrtrd 4025 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ -((2 ยท ๐ถ) โ (๐ด + ๐ต)) < (๐ด โ ๐ต)) |
41 | 24, 26, 24 | nppcan3d 8294 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด โ ๐ต) + (๐ด + ๐ต)) = (๐ด + ๐ด)) |
42 | 24 | 2timesd 9160 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ด) = (๐ด + ๐ด)) |
43 | 41, 42 | eqtr4d 2213 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด โ ๐ต) + (๐ด + ๐ต)) = (2 ยท ๐ด)) |
44 | | simprl 529 |
. . . . . . . . . 10
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ๐ด < ๐ถ) |
45 | 23, 20, 35, 44 | ltmul2dd 9752 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (2 ยท ๐ด) < (2 ยท ๐ถ)) |
46 | 43, 45 | eqbrtrd 4025 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด โ ๐ต) + (๐ด + ๐ต)) < (2 ยท ๐ถ)) |
47 | 30, 29, 21 | ltaddsubd 8501 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (((๐ด โ ๐ต) + (๐ด + ๐ต)) < (2 ยท ๐ถ) โ (๐ด โ ๐ต) < ((2 ยท ๐ถ) โ (๐ด + ๐ต)))) |
48 | 46, 47 | mpbid 147 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด โ ๐ต) < ((2 ยท ๐ถ) โ (๐ด + ๐ต))) |
49 | 40, 48 | jca 306 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (-((2 ยท ๐ถ) โ (๐ด + ๐ต)) < (๐ด โ ๐ต) โง (๐ด โ ๐ต) < ((2 ยท ๐ถ) โ (๐ด + ๐ต)))) |
50 | 21, 29 | resubcld 8337 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((2 ยท ๐ถ) โ (๐ด + ๐ต)) โ โ) |
51 | 30, 50 | absltd 11182 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((absโ(๐ด โ ๐ต)) < ((2 ยท ๐ถ) โ (๐ด + ๐ต)) โ (-((2 ยท ๐ถ) โ (๐ด + ๐ต)) < (๐ด โ ๐ต) โง (๐ด โ ๐ต) < ((2 ยท ๐ถ) โ (๐ด + ๐ต))))) |
52 | 49, 51 | mpbird 167 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (absโ(๐ด โ ๐ต)) < ((2 ยท ๐ถ) โ (๐ด + ๐ต))) |
53 | 30 | recnd 7985 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด โ ๐ต) โ โ) |
54 | 53 | abscld 11189 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (absโ(๐ด โ ๐ต)) โ โ) |
55 | 29, 54, 21 | ltaddsub2d 8502 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) < (2 ยท ๐ถ) โ (absโ(๐ด โ ๐ต)) < ((2 ยท ๐ถ) โ (๐ด + ๐ต)))) |
56 | 52, 55 | mpbird 167 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) < (2 ยท ๐ถ)) |
57 | 29, 54 | readdcld 7986 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) โ โ) |
58 | 57, 20, 35 | ltdivmuld 9747 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) < ๐ถ โ ((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) < (2 ยท ๐ถ))) |
59 | 56, 58 | mpbird 167 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (((๐ด + ๐ต) + (absโ(๐ด โ ๐ต))) / 2) < ๐ถ) |
60 | 17, 59 | eqbrtrd 4025 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ sup({๐ด, ๐ต}, โ, < ) < ๐ถ) |
61 | 14, 60 | impbida 596 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(sup({๐ด, ๐ต}, โ, < ) < ๐ถ โ (๐ด < ๐ถ โง ๐ต < ๐ถ))) |