Step | Hyp | Ref
| Expression |
1 | | nn0opth.1 |
. . . . 5
โข ๐ด โ
โ0 |
2 | | nn0opth.2 |
. . . . 5
โข ๐ต โ
โ0 |
3 | 1, 2 | nn0addcli 12384 |
. . . 4
โข (๐ด + ๐ต) โ
โ0 |
4 | | nn0opth.3 |
. . . 4
โข ๐ถ โ
โ0 |
5 | 3, 4 | nn0opthlem1 14096 |
. . 3
โข ((๐ด + ๐ต) < ๐ถ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) < (๐ถ ยท ๐ถ)) |
6 | 2 | nn0rei 12358 |
. . . . . 6
โข ๐ต โ โ |
7 | 6, 1 | nn0addge2i 12396 |
. . . . 5
โข ๐ต โค (๐ด + ๐ต) |
8 | 3, 2 | nn0lele2xi 12402 |
. . . . . 6
โข (๐ต โค (๐ด + ๐ต) โ ๐ต โค (2 ยท (๐ด + ๐ต))) |
9 | | 2re 12161 |
. . . . . . . 8
โข 2 โ
โ |
10 | 3 | nn0rei 12358 |
. . . . . . . 8
โข (๐ด + ๐ต) โ โ |
11 | 9, 10 | remulcli 11105 |
. . . . . . 7
โข (2
ยท (๐ด + ๐ต)) โ
โ |
12 | 10, 10 | remulcli 11105 |
. . . . . . 7
โข ((๐ด + ๐ต) ยท (๐ด + ๐ต)) โ โ |
13 | 6, 11, 12 | leadd2i 11645 |
. . . . . 6
โข (๐ต โค (2 ยท (๐ด + ๐ต)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต)))) |
14 | 8, 13 | sylib 217 |
. . . . 5
โข (๐ต โค (๐ด + ๐ต) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต)))) |
15 | 7, 14 | ax-mp 5 |
. . . 4
โข (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) |
16 | 12, 6 | readdcli 11104 |
. . . . 5
โข (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โ |
17 | 12, 11 | readdcli 11104 |
. . . . 5
โข (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) โ โ |
18 | 4 | nn0rei 12358 |
. . . . . 6
โข ๐ถ โ โ |
19 | 18, 18 | remulcli 11105 |
. . . . 5
โข (๐ถ ยท ๐ถ) โ โ |
20 | 16, 17, 19 | lelttri 11216 |
. . . 4
โข
(((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) โง (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) < (๐ถ ยท ๐ถ)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ)) |
21 | 15, 20 | mpan 689 |
. . 3
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) < (๐ถ ยท ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ)) |
22 | 5, 21 | sylbi 216 |
. 2
โข ((๐ด + ๐ต) < ๐ถ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ)) |
23 | | nn0opth.4 |
. . . 4
โข ๐ท โ
โ0 |
24 | 19, 23 | nn0addge1i 12395 |
. . 3
โข (๐ถ ยท ๐ถ) โค ((๐ถ ยท ๐ถ) + ๐ท) |
25 | 23 | nn0rei 12358 |
. . . . 5
โข ๐ท โ โ |
26 | 19, 25 | readdcli 11104 |
. . . 4
โข ((๐ถ ยท ๐ถ) + ๐ท) โ โ |
27 | 16, 19, 26 | ltletri 11217 |
. . 3
โข
(((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ) โง (๐ถ ยท ๐ถ) โค ((๐ถ ยท ๐ถ) + ๐ท)) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < ((๐ถ ยท ๐ถ) + ๐ท)) |
28 | 24, 27 | mpan2 690 |
. 2
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < ((๐ถ ยท ๐ถ) + ๐ท)) |
29 | 16, 26 | ltnei 11213 |
. 2
โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < ((๐ถ ยท ๐ถ) + ๐ท) โ ((๐ถ ยท ๐ถ) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) |
30 | 22, 28, 29 | 3syl 18 |
1
โข ((๐ด + ๐ต) < ๐ถ โ ((๐ถ ยท ๐ถ) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) |