Step | Hyp | Ref
| Expression |
1 | | nnrp 12934 |
. . . . . 6
โข (๐ท โ โ โ ๐ท โ
โ+) |
2 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ
โ+) |
3 | | 1rp 12927 |
. . . . . 6
โข 1 โ
โ+ |
4 | 3 | a1i 11 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ+) |
5 | 2, 4 | rpaddcld 12980 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) โ
โ+) |
6 | 5 | rpsqrtcld 15305 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โ โ+) |
7 | 6 | rpred 12965 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โ โ) |
8 | 2 | rpsqrtcld 15305 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ+) |
9 | 8 | rpred 12965 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ) |
10 | | nn0re 12430 |
. . . 4
โข (๐ด โ โ0
โ ๐ด โ
โ) |
11 | 10 | adantr 482 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ด โ โ) |
12 | 11 | ad2antlr 726 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ด โ โ) |
13 | | nn0re 12430 |
. . . . 5
โข (๐ต โ โ0
โ ๐ต โ
โ) |
14 | 13 | adantl 483 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ต โ โ) |
15 | 14 | ad2antlr 726 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ โ) |
16 | 9, 15 | remulcld 11193 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ๐ท) ยท
๐ต) โ
โ) |
17 | 2 | rpred 12965 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ โ) |
18 | | 1re 11163 |
. . . . . . . 8
โข 1 โ
โ |
19 | 18 | a1i 11 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ) |
20 | 15 | resqcld 14039 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ตโ2) โ โ) |
21 | 19, 20 | resubcld 11591 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โ (๐ตโ2)) โ
โ) |
22 | 17, 21 | remulcld 11193 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (1 โ (๐ตโ2))) โ โ) |
23 | | 0red 11166 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โ
โ) |
24 | 17, 23 | remulcld 11193 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 0) โ
โ) |
25 | 12 | resqcld 14039 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) โ โ) |
26 | | sq1 14108 |
. . . . . . . . 9
โข
(1โ2) = 1 |
27 | 26 | a1i 11 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1โ2) =
1) |
28 | | nnge1 12189 |
. . . . . . . . . . 11
โข (๐ต โ โ โ 1 โค
๐ต) |
29 | 28 | adantl 483 |
. . . . . . . . . 10
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต โ โ) โ 1 โค ๐ต) |
30 | | simplrl 776 |
. . . . . . . . . . . 12
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 < (๐ด + ((โโ๐ท) ยท ๐ต))) |
31 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ต = 0 โ (๐ตโ2) = (0โ2)) |
32 | 31 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ตโ2) = (0โ2)) |
33 | | sq0 14105 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(0โ2) = 0 |
34 | 32, 33 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ตโ2) = 0) |
35 | 34 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท (๐ตโ2)) = (๐ท ยท 0)) |
36 | 2 | rpcnd 12967 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ โ) |
37 | 36 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ๐ท โ โ) |
38 | 37 | mul01d 11362 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท 0) = 0) |
39 | 35, 38 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท (๐ตโ2)) = 0) |
40 | 39 | oveq2d 7377 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = ((๐ดโ2) โ 0)) |
41 | | simplrr 777 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1) |
42 | 12 | recnd 11191 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ด โ โ) |
43 | 42 | sqcld 14058 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) โ โ) |
44 | 43 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ดโ2) โ โ) |
45 | 44 | subid1d 11509 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ 0) = (๐ดโ2)) |
46 | 40, 41, 45 | 3eqtr3d 2781 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 = (๐ดโ2)) |
47 | 26, 46 | eqtr2id 2786 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ดโ2) = (1โ2)) |
48 | | nn0ge0 12446 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ0
โ 0 โค ๐ด) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ 0 โค ๐ด) |
50 | 49 | ad2antlr 726 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค ๐ด) |
51 | | 0le1 11686 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
1 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค
1) |
53 | | sq11 14045 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง 0 โค
๐ด) โง (1 โ โ
โง 0 โค 1)) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
54 | 12, 50, 19, 52, 53 | syl22anc 838 |
. . . . . . . . . . . . . . . 16
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
55 | 54 | adantr 482 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
56 | 47, 55 | mpbid 231 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ๐ด = 1) |
57 | | simpr 486 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ๐ต = 0) |
58 | 57 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท ๐ต) = ((โโ๐ท) ยท 0)) |
59 | 8 | rpcnd 12967 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ) |
60 | 59 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (โโ๐ท) โ
โ) |
61 | 60 | mul01d 11362 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท 0) =
0) |
62 | 58, 61 | eqtrd 2773 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท ๐ต) = 0) |
63 | 56, 62 | oveq12d 7379 |
. . . . . . . . . . . . 13
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = (1 + 0)) |
64 | | 1p0e1 12285 |
. . . . . . . . . . . . 13
โข (1 + 0) =
1 |
65 | 63, 64 | eqtrdi 2789 |
. . . . . . . . . . . 12
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = 1) |
66 | 30, 65 | breqtrd 5135 |
. . . . . . . . . . 11
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 < 1) |
67 | 18 | ltnri 11272 |
. . . . . . . . . . 11
โข ยฌ 1
< 1 |
68 | | pm2.24 124 |
. . . . . . . . . . 11
โข (1 < 1
โ (ยฌ 1 < 1 โ 1 โค ๐ต)) |
69 | 66, 67, 68 | mpisyl 21 |
. . . . . . . . . 10
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 โค ๐ต) |
70 | | simplrr 777 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ
โ0) |
71 | | elnn0 12423 |
. . . . . . . . . . 11
โข (๐ต โ โ0
โ (๐ต โ โ
โจ ๐ต =
0)) |
72 | 70, 71 | sylib 217 |
. . . . . . . . . 10
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ต โ โ โจ ๐ต = 0)) |
73 | 29, 69, 72 | mpjaodan 958 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โค ๐ต) |
74 | | nn0ge0 12446 |
. . . . . . . . . . . 12
โข (๐ต โ โ0
โ 0 โค ๐ต) |
75 | 74 | adantl 483 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ 0 โค ๐ต) |
76 | 75 | ad2antlr 726 |
. . . . . . . . . 10
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค ๐ต) |
77 | 19, 15, 52, 76 | le2sqd 14169 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โค ๐ต โ (1โ2) โค (๐ตโ2))) |
78 | 73, 77 | mpbid 231 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1โ2) โค
(๐ตโ2)) |
79 | 27, 78 | eqbrtrrd 5133 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โค (๐ตโ2)) |
80 | 19, 20 | suble0d 11754 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((1 โ (๐ตโ2)) โค 0 โ 1 โค
(๐ตโ2))) |
81 | 79, 80 | mpbird 257 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โ (๐ตโ2)) โค
0) |
82 | 21, 23, 2 | lemul2d 13009 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((1 โ (๐ตโ2)) โค 0 โ (๐ท ยท (1 โ (๐ตโ2))) โค (๐ท ยท 0))) |
83 | 81, 82 | mpbid 231 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (1 โ (๐ตโ2))) โค (๐ท ยท 0)) |
84 | 22, 24, 25, 83 | leadd2dd 11778 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2)))) โค ((๐ดโ2) + (๐ท ยท 0))) |
85 | 5 | rpcnd 12967 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) โ โ) |
86 | 85 | sqsqrtd 15333 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) = (๐ท +
1)) |
87 | | simprr 772 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1) |
88 | 87 | eqcomd 2739 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 = ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) |
89 | 88 | oveq2d 7377 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) = (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2))))) |
90 | 15 | recnd 11191 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ โ) |
91 | 90 | sqcld 14058 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ตโ2) โ โ) |
92 | 36, 91 | mulcld 11183 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (๐ตโ2)) โ โ) |
93 | 36, 43, 92 | addsub12d 11543 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท โ (๐ท ยท (๐ตโ2))))) |
94 | 19 | recnd 11191 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ) |
95 | 36, 94, 91 | subdid 11619 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (1 โ (๐ตโ2))) = ((๐ท ยท 1) โ (๐ท ยท (๐ตโ2)))) |
96 | 36 | mulid1d 11180 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 1) = ๐ท) |
97 | 96 | oveq1d 7376 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ท ยท 1) โ (๐ท ยท (๐ตโ2))) = (๐ท โ (๐ท ยท (๐ตโ2)))) |
98 | 95, 97 | eqtr2d 2774 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท โ (๐ท ยท (๐ตโ2))) = (๐ท ยท (1 โ (๐ตโ2)))) |
99 | 98 | oveq2d 7377 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2))))) |
100 | 93, 99 | eqtrd 2773 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2))))) |
101 | 86, 89, 100 | 3eqtrd 2777 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) = ((๐ดโ2) +
(๐ท ยท (1 โ
(๐ตโ2))))) |
102 | 36 | mul01d 11362 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 0) = 0) |
103 | 102 | oveq2d 7377 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท ยท 0)) = ((๐ดโ2) + 0)) |
104 | 43 | addid1d 11363 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + 0) = (๐ดโ2)) |
105 | 103, 104 | eqtr2d 2774 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) = ((๐ดโ2) + (๐ท ยท 0))) |
106 | 84, 101, 105 | 3brtr4d 5141 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) โค (๐ดโ2)) |
107 | 6 | rpge0d 12969 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค
(โโ(๐ท +
1))) |
108 | 7, 12, 107, 50 | le2sqd 14169 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท + 1))
โค ๐ด โ
((โโ(๐ท +
1))โ2) โค (๐ดโ2))) |
109 | 106, 108 | mpbird 257 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โค ๐ด) |
110 | 59 | mulid1d 11180 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ๐ท) ยท
1) = (โโ๐ท)) |
111 | 19, 15, 8 | lemul2d 13009 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โค ๐ต โ ((โโ๐ท) ยท 1) โค
((โโ๐ท) ยท
๐ต))) |
112 | 73, 111 | mpbid 231 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ๐ท) ยท
1) โค ((โโ๐ท)
ยท ๐ต)) |
113 | 110, 112 | eqbrtrrd 5133 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โค ((โโ๐ท) ยท ๐ต)) |
114 | 7, 9, 12, 16, 109, 113 | le2addd 11782 |
1
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
(๐ด + ((โโ๐ท) ยท ๐ต))) |