Step | Hyp | Ref
| Expression |
1 | | readdcl 11158 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
2 | 1 | 3adant3 1132 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด + ๐ต) โ โ) |
3 | | readdcl 11158 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ถ) โ โ) |
4 | 3 | anidms 567 |
. . . . . 6
โข (๐ถ โ โ โ (๐ถ + ๐ถ) โ โ) |
5 | 4 | 3ad2ant3 1135 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ถ) โ โ) |
6 | | 2re 12251 |
. . . . . . 7
โข 2 โ
โ |
7 | | remulcl 11160 |
. . . . . . 7
โข ((2
โ โ โง ๐ถ
โ โ) โ (2 ยท ๐ถ) โ โ) |
8 | 6, 7 | mpan 688 |
. . . . . 6
โข (๐ถ โ โ โ (2
ยท ๐ถ) โ
โ) |
9 | 8 | 3ad2ant3 1135 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (2
ยท ๐ถ) โ
โ) |
10 | 2, 5, 9 | 3jca 1128 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) โ โ โง (๐ถ + ๐ถ) โ โ โง (2 ยท ๐ถ) โ
โ)) |
11 | 10 | adantr 481 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) โ โ โง (๐ถ + ๐ถ) โ โ โง (2 ยท ๐ถ) โ
โ)) |
12 | | id 22 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ โ โง ๐ต โ
โ)) |
13 | 12 | 3adant3 1132 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ โ โง ๐ต โ
โ)) |
14 | | id 22 |
. . . . . . . . 9
โข (๐ถ โ โ โ ๐ถ โ
โ) |
15 | 14, 14 | jca 512 |
. . . . . . . 8
โข (๐ถ โ โ โ (๐ถ โ โ โง ๐ถ โ
โ)) |
16 | 15 | 3ad2ant3 1135 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ โ โง ๐ถ โ
โ)) |
17 | 13, 16 | jca 512 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ถ โ
โ))) |
18 | 17 | adantr 481 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ถ โ โ))) |
19 | | simpr 485 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด < ๐ถ โง ๐ต < ๐ถ)) |
20 | | lt2add 11664 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ถ โ โ)) โ ((๐ด < ๐ถ โง ๐ต < ๐ถ) โ (๐ด + ๐ต) < (๐ถ + ๐ถ))) |
21 | 18, 19, 20 | sylc 65 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด + ๐ต) < (๐ถ + ๐ถ)) |
22 | | recn 11165 |
. . . . . . . 8
โข (๐ถ โ โ โ ๐ถ โ
โ) |
23 | 22 | 2timesd 12420 |
. . . . . . 7
โข (๐ถ โ โ โ (2
ยท ๐ถ) = (๐ถ + ๐ถ)) |
24 | 8 | leidd 11745 |
. . . . . . 7
โข (๐ถ โ โ โ (2
ยท ๐ถ) โค (2
ยท ๐ถ)) |
25 | 23, 24 | eqbrtrrd 5149 |
. . . . . 6
โข (๐ถ โ โ โ (๐ถ + ๐ถ) โค (2 ยท ๐ถ)) |
26 | 25 | 3ad2ant3 1135 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ + ๐ถ) โค (2 ยท ๐ถ)) |
27 | 26 | adantr 481 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ถ + ๐ถ) โค (2 ยท ๐ถ)) |
28 | 21, 27 | jca 512 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ ((๐ด + ๐ต) < (๐ถ + ๐ถ) โง (๐ถ + ๐ถ) โค (2 ยท ๐ถ))) |
29 | | ltletr 11271 |
. . 3
โข (((๐ด + ๐ต) โ โ โง (๐ถ + ๐ถ) โ โ โง (2 ยท ๐ถ) โ โ) โ
(((๐ด + ๐ต) < (๐ถ + ๐ถ) โง (๐ถ + ๐ถ) โค (2 ยท ๐ถ)) โ (๐ด + ๐ต) < (2 ยท ๐ถ))) |
30 | 11, 28, 29 | sylc 65 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ด < ๐ถ โง ๐ต < ๐ถ)) โ (๐ด + ๐ต) < (2 ยท ๐ถ)) |
31 | 30 | ex 413 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด < ๐ถ โง ๐ต < ๐ถ) โ (๐ด + ๐ต) < (2 ยท ๐ถ))) |