Step | Hyp | Ref
| Expression |
1 | | nn0opthd.1 |
. . . . . . . 8
โข (๐ โ ๐ด โ
โ0) |
2 | | nn0opthd.2 |
. . . . . . . 8
โข (๐ โ ๐ต โ
โ0) |
3 | 1, 2 | nn0addcld 9233 |
. . . . . . 7
โข (๐ โ (๐ด + ๐ต) โ
โ0) |
4 | 3 | nn0red 9230 |
. . . . . 6
โข (๐ โ (๐ด + ๐ต) โ โ) |
5 | 4, 4 | remulcld 7988 |
. . . . 5
โข (๐ โ ((๐ด + ๐ต) ยท (๐ด + ๐ต)) โ โ) |
6 | 2 | nn0red 9230 |
. . . . 5
โข (๐ โ ๐ต โ โ) |
7 | 5, 6 | readdcld 7987 |
. . . 4
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โ) |
8 | 7 | adantr 276 |
. . 3
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โ โ) |
9 | | nn0opthd.3 |
. . . . . . 7
โข (๐ โ ๐ถ โ
โ0) |
10 | 9 | nn0red 9230 |
. . . . . 6
โข (๐ โ ๐ถ โ โ) |
11 | 10, 10 | remulcld 7988 |
. . . . 5
โข (๐ โ (๐ถ ยท ๐ถ) โ โ) |
12 | 11 | adantr 276 |
. . . 4
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (๐ถ ยท ๐ถ) โ โ) |
13 | | nn0opthd.4 |
. . . . . . 7
โข (๐ โ ๐ท โ
โ0) |
14 | 13 | nn0red 9230 |
. . . . . 6
โข (๐ โ ๐ท โ โ) |
15 | 11, 14 | readdcld 7987 |
. . . . 5
โข (๐ โ ((๐ถ ยท ๐ถ) + ๐ท) โ โ) |
16 | 15 | adantr 276 |
. . . 4
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ ((๐ถ ยท ๐ถ) + ๐ท) โ โ) |
17 | | 2re 8989 |
. . . . . . . . 9
โข 2 โ
โ |
18 | 17 | a1i 9 |
. . . . . . . 8
โข (๐ โ 2 โ
โ) |
19 | 18, 4 | remulcld 7988 |
. . . . . . 7
โข (๐ โ (2 ยท (๐ด + ๐ต)) โ โ) |
20 | 5, 19 | readdcld 7987 |
. . . . . 6
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) โ โ) |
21 | 20 | adantr 276 |
. . . . 5
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) โ โ) |
22 | | nn0addge2 9223 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ด โ โ0)
โ ๐ต โค (๐ด + ๐ต)) |
23 | 6, 1, 22 | syl2anc 411 |
. . . . . . . 8
โข (๐ โ ๐ต โค (๐ด + ๐ต)) |
24 | | nn0addge1 9222 |
. . . . . . . . . 10
โข (((๐ด + ๐ต) โ โ โง (๐ด + ๐ต) โ โ0) โ (๐ด + ๐ต) โค ((๐ด + ๐ต) + (๐ด + ๐ต))) |
25 | 4, 3, 24 | syl2anc 411 |
. . . . . . . . 9
โข (๐ โ (๐ด + ๐ต) โค ((๐ด + ๐ต) + (๐ด + ๐ต))) |
26 | 4 | recnd 7986 |
. . . . . . . . . 10
โข (๐ โ (๐ด + ๐ต) โ โ) |
27 | 26 | 2timesd 9161 |
. . . . . . . . 9
โข (๐ โ (2 ยท (๐ด + ๐ต)) = ((๐ด + ๐ต) + (๐ด + ๐ต))) |
28 | 25, 27 | breqtrrd 4032 |
. . . . . . . 8
โข (๐ โ (๐ด + ๐ต) โค (2 ยท (๐ด + ๐ต))) |
29 | 6, 4, 19, 23, 28 | letrd 8081 |
. . . . . . 7
โข (๐ โ ๐ต โค (2 ยท (๐ด + ๐ต))) |
30 | 6, 19, 5, 29 | leadd2dd 8517 |
. . . . . 6
โข (๐ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต)))) |
31 | 30 | adantr 276 |
. . . . 5
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) โค (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต)))) |
32 | 3, 9 | nn0opthlem1d 10700 |
. . . . . 6
โข (๐ โ ((๐ด + ๐ต) < ๐ถ โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) < (๐ถ ยท ๐ถ))) |
33 | 32 | biimpa 296 |
. . . . 5
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + (2 ยท (๐ด + ๐ต))) < (๐ถ ยท ๐ถ)) |
34 | 8, 21, 12, 31, 33 | lelttrd 8082 |
. . . 4
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < (๐ถ ยท ๐ถ)) |
35 | | nn0addge1 9222 |
. . . . . 6
โข (((๐ถ ยท ๐ถ) โ โ โง ๐ท โ โ0) โ (๐ถ ยท ๐ถ) โค ((๐ถ ยท ๐ถ) + ๐ท)) |
36 | 11, 13, 35 | syl2anc 411 |
. . . . 5
โข (๐ โ (๐ถ ยท ๐ถ) โค ((๐ถ ยท ๐ถ) + ๐ท)) |
37 | 36 | adantr 276 |
. . . 4
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (๐ถ ยท ๐ถ) โค ((๐ถ ยท ๐ถ) + ๐ท)) |
38 | 8, 12, 16, 34, 37 | ltletrd 8380 |
. . 3
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) < ((๐ถ ยท ๐ถ) + ๐ท)) |
39 | 8, 38 | gtned 8070 |
. 2
โข ((๐ โง (๐ด + ๐ต) < ๐ถ) โ ((๐ถ ยท ๐ถ) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) |
40 | 39 | ex 115 |
1
โข (๐ โ ((๐ด + ๐ต) < ๐ถ โ ((๐ถ ยท ๐ถ) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต))) |