Step | Hyp | Ref
| Expression |
1 | | nnrp 12984 |
. . . . . 6
โข (๐ท โ โ โ ๐ท โ
โ+) |
2 | 1 | ad2antrr 724 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ
โ+) |
3 | | 1rp 12977 |
. . . . . 6
โข 1 โ
โ+ |
4 | 3 | a1i 11 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ+) |
5 | 2, 4 | rpaddcld 13030 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) โ
โ+) |
6 | 5 | rpsqrtcld 15357 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โ โ+) |
7 | 6 | rpred 13015 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โ โ) |
8 | 2 | rpsqrtcld 15357 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ+) |
9 | 8 | rpred 13015 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ) |
10 | | nn0re 12480 |
. . . 4
โข (๐ด โ โ0
โ ๐ด โ
โ) |
11 | 10 | adantr 481 |
. . 3
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ด โ โ) |
12 | 11 | ad2antlr 725 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ด โ โ) |
13 | | nn0re 12480 |
. . . . 5
โข (๐ต โ โ0
โ ๐ต โ
โ) |
14 | 13 | adantl 482 |
. . . 4
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ ๐ต โ โ) |
15 | 14 | ad2antlr 725 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ โ) |
16 | 9, 15 | remulcld 11243 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ๐ท) ยท
๐ต) โ
โ) |
17 | 2 | rpred 13015 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ โ) |
18 | | 1re 11213 |
. . . . . . . 8
โข 1 โ
โ |
19 | 18 | a1i 11 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ) |
20 | 15 | resqcld 14089 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ตโ2) โ โ) |
21 | 19, 20 | resubcld 11641 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โ (๐ตโ2)) โ
โ) |
22 | 17, 21 | remulcld 11243 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (1 โ (๐ตโ2))) โ โ) |
23 | | 0red 11216 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โ
โ) |
24 | 17, 23 | remulcld 11243 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 0) โ
โ) |
25 | 12 | resqcld 14089 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) โ โ) |
26 | | sq1 14158 |
. . . . . . . . 9
โข
(1โ2) = 1 |
27 | 26 | a1i 11 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1โ2) =
1) |
28 | | nnge1 12239 |
. . . . . . . . . . 11
โข (๐ต โ โ โ 1 โค
๐ต) |
29 | 28 | adantl 482 |
. . . . . . . . . 10
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต โ โ) โ 1 โค ๐ต) |
30 | | simplrl 775 |
. . . . . . . . . . . 12
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 < (๐ด + ((โโ๐ท) ยท ๐ต))) |
31 | | oveq1 7415 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ต = 0 โ (๐ตโ2) = (0โ2)) |
32 | 31 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ตโ2) = (0โ2)) |
33 | | sq0 14155 |
. . . . . . . . . . . . . . . . . . . . 21
โข
(0โ2) = 0 |
34 | 32, 33 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ตโ2) = 0) |
35 | 34 | oveq2d 7424 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท (๐ตโ2)) = (๐ท ยท 0)) |
36 | 2 | rpcnd 13017 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ท โ โ) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ๐ท โ โ) |
38 | 37 | mul01d 11412 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท 0) = 0) |
39 | 35, 38 | eqtrd 2772 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ท ยท (๐ตโ2)) = 0) |
40 | 39 | oveq2d 7424 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = ((๐ดโ2) โ 0)) |
41 | | simplrr 776 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1) |
42 | 12 | recnd 11241 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ด โ โ) |
43 | 42 | sqcld 14108 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) โ โ) |
44 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ดโ2) โ โ) |
45 | 44 | subid1d 11559 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((๐ดโ2) โ 0) = (๐ดโ2)) |
46 | 40, 41, 45 | 3eqtr3d 2780 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 = (๐ดโ2)) |
47 | 26, 46 | eqtr2id 2785 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ดโ2) = (1โ2)) |
48 | | nn0ge0 12496 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ด โ โ0
โ 0 โค ๐ด) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ 0 โค ๐ด) |
50 | 49 | ad2antlr 725 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค ๐ด) |
51 | | 0le1 11736 |
. . . . . . . . . . . . . . . . . 18
โข 0 โค
1 |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค
1) |
53 | | sq11 14095 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง 0 โค
๐ด) โง (1 โ โ
โง 0 โค 1)) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
54 | 12, 50, 19, 52, 53 | syl22anc 837 |
. . . . . . . . . . . . . . . 16
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) = (1โ2) โ ๐ด = 1)) |
55 | 54 | adantr 481 |
. . . . . . . . . . . . . . 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 485 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ๐ต = 0) |
58 | 57 | oveq2d 7424 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท ๐ต) = ((โโ๐ท) ยท 0)) |
59 | 8 | rpcnd 13017 |
. . . . . . . . . . . . . . . . 17
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โ
โ) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . . 16
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (โโ๐ท) โ
โ) |
61 | 60 | mul01d 11412 |
. . . . . . . . . . . . . . 15
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท 0) =
0) |
62 | 58, 61 | eqtrd 2772 |
. . . . . . . . . . . . . 14
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ ((โโ๐ท) ยท ๐ต) = 0) |
63 | 56, 62 | oveq12d 7426 |
. . . . . . . . . . . . 13
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = (1 + 0)) |
64 | | 1p0e1 12335 |
. . . . . . . . . . . . 13
โข (1 + 0) =
1 |
65 | 63, 64 | eqtrdi 2788 |
. . . . . . . . . . . 12
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ (๐ด + ((โโ๐ท) ยท ๐ต)) = 1) |
66 | 30, 65 | breqtrd 5174 |
. . . . . . . . . . 11
โข ((((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โง ๐ต = 0) โ 1 < 1) |
67 | 18 | ltnri 11322 |
. . . . . . . . . . 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 776 |
. . . . . . . . . . 11
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ
โ0) |
71 | | elnn0 12473 |
. . . . . . . . . . 11
โข (๐ต โ โ0
โ (๐ต โ โ
โจ ๐ต =
0)) |
72 | 70, 71 | sylib 217 |
. . . . . . . . . 10
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ต โ โ โจ ๐ต = 0)) |
73 | 29, 69, 72 | mpjaodan 957 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โค ๐ต) |
74 | | nn0ge0 12496 |
. . . . . . . . . . . 12
โข (๐ต โ โ0
โ 0 โค ๐ต) |
75 | 74 | adantl 482 |
. . . . . . . . . . 11
โข ((๐ด โ โ0
โง ๐ต โ
โ0) โ 0 โค ๐ต) |
76 | 75 | ad2antlr 725 |
. . . . . . . . . 10
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค ๐ต) |
77 | 19, 15, 52, 76 | le2sqd 14219 |
. . . . . . . . 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 5172 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โค (๐ตโ2)) |
80 | 19, 20 | suble0d 11804 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((1 โ (๐ตโ2)) โค 0 โ 1 โค
(๐ตโ2))) |
81 | 79, 80 | mpbird 256 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (1 โ (๐ตโ2)) โค
0) |
82 | 21, 23, 2 | lemul2d 13059 |
. . . . . 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 11828 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2)))) โค ((๐ดโ2) + (๐ท ยท 0))) |
85 | 5 | rpcnd 13017 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) โ โ) |
86 | 85 | sqsqrtd 15385 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) = (๐ท +
1)) |
87 | | simprr 771 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1) |
88 | 87 | eqcomd 2738 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 = ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) |
89 | 88 | oveq2d 7424 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + 1) = (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2))))) |
90 | 15 | recnd 11241 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ๐ต โ โ) |
91 | 90 | sqcld 14108 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ตโ2) โ โ) |
92 | 36, 91 | mulcld 11233 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (๐ตโ2)) โ โ) |
93 | 36, 43, 92 | addsub12d 11593 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท โ (๐ท ยท (๐ตโ2))))) |
94 | 19 | recnd 11241 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 1 โ
โ) |
95 | 36, 94, 91 | subdid 11669 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท (1 โ (๐ตโ2))) = ((๐ท ยท 1) โ (๐ท ยท (๐ตโ2)))) |
96 | 36 | mulridd 11230 |
. . . . . . . . 9
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 1) = ๐ท) |
97 | 96 | oveq1d 7423 |
. . . . . . . 8
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ท ยท 1) โ (๐ท ยท (๐ตโ2))) = (๐ท โ (๐ท ยท (๐ตโ2)))) |
98 | 95, 97 | eqtr2d 2773 |
. . . . . . 7
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท โ (๐ท ยท (๐ตโ2))) = (๐ท ยท (1 โ (๐ตโ2)))) |
99 | 98 | oveq2d 7424 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2))))) |
100 | 93, 99 | eqtrd 2772 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท + ((๐ดโ2) โ (๐ท ยท (๐ตโ2)))) = ((๐ดโ2) + (๐ท ยท (1 โ (๐ตโ2))))) |
101 | 86, 89, 100 | 3eqtrd 2776 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) = ((๐ดโ2) +
(๐ท ยท (1 โ
(๐ตโ2))))) |
102 | 36 | mul01d 11412 |
. . . . . 6
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ท ยท 0) = 0) |
103 | 102 | oveq2d 7424 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + (๐ท ยท 0)) = ((๐ดโ2) + 0)) |
104 | 43 | addridd 11413 |
. . . . 5
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ ((๐ดโ2) + 0) = (๐ดโ2)) |
105 | 103, 104 | eqtr2d 2773 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (๐ดโ2) = ((๐ดโ2) + (๐ท ยท 0))) |
106 | 84, 101, 105 | 3brtr4d 5180 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท +
1))โ2) โค (๐ดโ2)) |
107 | 6 | rpge0d 13019 |
. . . 4
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ 0 โค
(โโ(๐ท +
1))) |
108 | 7, 12, 107, 50 | le2sqd 14219 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท + 1))
โค ๐ด โ
((โโ(๐ท +
1))โ2) โค (๐ดโ2))) |
109 | 106, 108 | mpbird 256 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
(โโ(๐ท + 1))
โค ๐ด) |
110 | 59 | mulridd 11230 |
. . 3
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ๐ท) ยท
1) = (โโ๐ท)) |
111 | 19, 15, 8 | lemul2d 13059 |
. . . 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 5172 |
. 2
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ (โโ๐ท) โค ((โโ๐ท) ยท ๐ต)) |
114 | 7, 9, 12, 16, 109, 113 | le2addd 11832 |
1
โข (((๐ท โ โ โง (๐ด โ โ0
โง ๐ต โ
โ0)) โง (1 < (๐ด + ((โโ๐ท) ยท ๐ต)) โง ((๐ดโ2) โ (๐ท ยท (๐ตโ2))) = 1)) โ
((โโ(๐ท + 1)) +
(โโ๐ท)) โค
(๐ด + ((โโ๐ท) ยท ๐ต))) |