Step | Hyp | Ref
| Expression |
1 | | elfznn 13495 |
. . . 4
โข (๐ โ (1...if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต)) โ ๐ โ โ) |
2 | 1 | ad3antlr 729 |
. . 3
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โ โ) |
3 | | nn0z 12548 |
. . . . 5
โข (๐ โ โ0
โ ๐ โ
โค) |
4 | 3 | ad2antlr 725 |
. . . 4
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โ โค) |
5 | | simpl 483 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ๐ด โ
โ+) |
6 | 5 | ad3antrrr 728 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ด โ
โ+) |
7 | 6 | rpred 12981 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ด โ โ) |
8 | 2 | nnred 12192 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โ โ) |
9 | 7, 8 | remulcld 11209 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (๐ด ยท ๐) โ โ) |
10 | | nn0re 12446 |
. . . . . . . . . . . 12
โข (๐ โ โ0
โ ๐ โ
โ) |
11 | 10 | ad2antlr 725 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โ โ) |
12 | 9, 11 | resubcld 11607 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((๐ด ยท ๐) โ ๐) โ โ) |
13 | 12 | recnd 11207 |
. . . . . . . . 9
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((๐ด ยท ๐) โ ๐) โ โ) |
14 | 13 | abscld 15348 |
. . . . . . . 8
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (absโ((๐ด ยท ๐) โ ๐)) โ โ) |
15 | 5 | rpreccld 12991 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ (1 / ๐ด) โ
โ+) |
16 | 15 | rprege0d 12988 |
. . . . . . . . . . . 12
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ((1 / ๐ด) โ
โ โง 0 โค (1 / ๐ด))) |
17 | | flge0nn0 13750 |
. . . . . . . . . . . 12
โข (((1 /
๐ด) โ โ โง 0
โค (1 / ๐ด)) โ
(โโ(1 / ๐ด))
โ โ0) |
18 | | nn0p1nn 12476 |
. . . . . . . . . . . 12
โข
((โโ(1 / ๐ด)) โ โ0 โ
((โโ(1 / ๐ด)) +
1) โ โ) |
19 | 16, 17, 18 | 3syl 18 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ((โโ(1 / ๐ด)) + 1) โ โ) |
20 | 19 | ad3antrrr 728 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((โโ(1 / ๐ด)) + 1) โ
โ) |
21 | | simpr 485 |
. . . . . . . . . . 11
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ ๐ต โ
โ) |
22 | 21 | ad3antrrr 728 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ต โ โ) |
23 | 20, 22 | ifcld 4552 |
. . . . . . . . 9
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ) |
24 | 23 | nnrecred 12228 |
. . . . . . . 8
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โ โ) |
25 | | 0red 11182 |
. . . . . . . . 9
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 โ
โ) |
26 | 9, 25 | resubcld 11607 |
. . . . . . . 8
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((๐ด ยท ๐) โ 0) โ โ) |
27 | | simpr 485 |
. . . . . . . 8
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (absโ((๐ด ยท ๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต))) |
28 | 20 | nnrecred 12228 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / ((โโ(1 / ๐ด)) + 1)) โ
โ) |
29 | 22 | nnred 12192 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ต โ โ) |
30 | 6 | rprecred 12992 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / ๐ด) โ โ) |
31 | 30 | flcld 13728 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (โโ(1 / ๐ด)) โ
โค) |
32 | 31 | zred 12631 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (โโ(1 / ๐ด)) โ
โ) |
33 | | peano2re 11352 |
. . . . . . . . . . . . 13
โข
((โโ(1 / ๐ด)) โ โ โ ((โโ(1
/ ๐ด)) + 1) โ
โ) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((โโ(1 / ๐ด)) + 1) โ
โ) |
35 | | max2 13131 |
. . . . . . . . . . . 12
โข ((๐ต โ โ โง
((โโ(1 / ๐ด)) +
1) โ โ) โ ((โโ(1 / ๐ด)) + 1) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
36 | 29, 34, 35 | syl2anc 584 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((โโ(1 / ๐ด)) + 1) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต)) |
37 | 20 | nngt0d 12226 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < ((โโ(1 / ๐ด)) + 1)) |
38 | 23 | nnred 12192 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ) |
39 | 23 | nngt0d 12226 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
40 | | lerec 12062 |
. . . . . . . . . . . 12
โข
(((((โโ(1 / ๐ด)) + 1) โ โ โง 0 <
((โโ(1 / ๐ด)) +
1)) โง (if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ โง 0 < if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (((โโ(1 / ๐ด)) + 1) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / ((โโ(1 / ๐ด)) + 1)))) |
41 | 34, 37, 38, 39, 40 | syl22anc 837 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (((โโ(1 / ๐ด)) + 1) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / ((โโ(1 / ๐ด)) + 1)))) |
42 | 36, 41 | mpbid 231 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / ((โโ(1 / ๐ด)) + 1))) |
43 | | fllep1 13731 |
. . . . . . . . . . . . 13
โข ((1 /
๐ด) โ โ โ (1
/ ๐ด) โค
((โโ(1 / ๐ด)) +
1)) |
44 | 30, 43 | syl 17 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / ๐ด) โค ((โโ(1 / ๐ด)) + 1)) |
45 | 20 | nncnd 12193 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((โโ(1 / ๐ด)) + 1) โ
โ) |
46 | 20 | nnne0d 12227 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((โโ(1 / ๐ด)) + 1) โ 0) |
47 | 45, 46 | recrecd 11952 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / (1 / ((โโ(1 /
๐ด)) + 1))) =
((โโ(1 / ๐ด)) +
1)) |
48 | 44, 47 | breqtrrd 5153 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / ๐ด) โค (1 / (1 / ((โโ(1 / ๐ด)) + 1)))) |
49 | 34, 37 | recgt0d 12113 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < (1 / ((โโ(1 /
๐ด)) + 1))) |
50 | 6 | rpgt0d 12984 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < ๐ด) |
51 | | lerec 12062 |
. . . . . . . . . . . 12
โข ((((1 /
((โโ(1 / ๐ด)) +
1)) โ โ โง 0 < (1 / ((โโ(1 / ๐ด)) + 1))) โง (๐ด โ โ โง 0 < ๐ด)) โ ((1 /
((โโ(1 / ๐ด)) +
1)) โค ๐ด โ (1 /
๐ด) โค (1 / (1 /
((โโ(1 / ๐ด)) +
1))))) |
52 | 28, 49, 7, 50, 51 | syl22anc 837 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((1 / ((โโ(1 / ๐ด)) + 1)) โค ๐ด โ (1 / ๐ด) โค (1 / (1 / ((โโ(1 / ๐ด)) + 1))))) |
53 | 48, 52 | mpbird 256 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / ((โโ(1 / ๐ด)) + 1)) โค ๐ด) |
54 | 24, 28, 7, 42, 53 | letrd 11336 |
. . . . . . . . 9
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค ๐ด) |
55 | 7 | recnd 11207 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ด โ โ) |
56 | 55 | mulridd 11196 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (๐ด ยท 1) = ๐ด) |
57 | 2 | nnge1d 12225 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 1 โค ๐) |
58 | | 1red 11180 |
. . . . . . . . . . . . 13
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 1 โ
โ) |
59 | 58, 8, 6 | lemul2d 13025 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 โค ๐ โ (๐ด ยท 1) โค (๐ด ยท ๐))) |
60 | 57, 59 | mpbid 231 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (๐ด ยท 1) โค (๐ด ยท ๐)) |
61 | 56, 60 | eqbrtrrd 5149 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ด โค (๐ด ยท ๐)) |
62 | 9 | recnd 11207 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (๐ด ยท ๐) โ โ) |
63 | 62 | subid1d 11525 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((๐ด ยท ๐) โ 0) = (๐ด ยท ๐)) |
64 | 61, 63 | breqtrrd 5153 |
. . . . . . . . 9
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ด โค ((๐ด ยท ๐) โ 0)) |
65 | 24, 7, 26, 54, 64 | letrd 11336 |
. . . . . . . 8
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค ((๐ด ยท ๐) โ 0)) |
66 | 14, 24, 26, 27, 65 | ltletrd 11339 |
. . . . . . 7
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (absโ((๐ด ยท ๐) โ ๐)) < ((๐ด ยท ๐) โ 0)) |
67 | 12, 26 | absltd 15341 |
. . . . . . 7
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((absโ((๐ด ยท ๐) โ ๐)) < ((๐ด ยท ๐) โ 0) โ (-((๐ด ยท ๐) โ 0) < ((๐ด ยท ๐) โ ๐) โง ((๐ด ยท ๐) โ ๐) < ((๐ด ยท ๐) โ 0)))) |
68 | 66, 67 | mpbid 231 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (-((๐ด ยท ๐) โ 0) < ((๐ด ยท ๐) โ ๐) โง ((๐ด ยท ๐) โ ๐) < ((๐ด ยท ๐) โ 0))) |
69 | 68 | simprd 496 |
. . . . 5
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ((๐ด ยท ๐) โ ๐) < ((๐ด ยท ๐) โ 0)) |
70 | 25, 11, 9 | ltsub2d 11789 |
. . . . 5
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (0 < ๐ โ ((๐ด ยท ๐) โ ๐) < ((๐ด ยท ๐) โ 0))) |
71 | 69, 70 | mpbird 256 |
. . . 4
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < ๐) |
72 | | elnnz 12533 |
. . . 4
โข (๐ โ โ โ (๐ โ โค โง 0 <
๐)) |
73 | 4, 71, 72 | sylanbrc 583 |
. . 3
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โ โ) |
74 | 22, 2 | ifcld 4552 |
. . . . 5
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ if(๐ โค ๐ต, ๐ต, ๐) โ โ) |
75 | 74 | nnrecred 12228 |
. . . 4
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ โค ๐ต, ๐ต, ๐)) โ โ) |
76 | | elfzle2 13470 |
. . . . . . 7
โข (๐ โ (1...if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต)) โ ๐ โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
77 | 76 | ad3antlr 729 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
78 | | max1 13129 |
. . . . . . 7
โข ((๐ต โ โ โง
((โโ(1 / ๐ด)) +
1) โ โ) โ ๐ต
โค if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
79 | 29, 34, 78 | syl2anc 584 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ต โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
80 | | maxle 13135 |
. . . . . . 7
โข ((๐ โ โ โง ๐ต โ โ โง if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต) โ โ) โ (if(๐ โค ๐ต, ๐ต, ๐) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ (๐ โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โง ๐ต โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)))) |
81 | 8, 29, 38, 80 | syl3anc 1371 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (if(๐ โค ๐ต, ๐ต, ๐) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ (๐ โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โง ๐ต โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)))) |
82 | 77, 79, 81 | mpbir2and 711 |
. . . . 5
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ if(๐ โค ๐ต, ๐ต, ๐) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) |
83 | 29, 8 | ifcld 4552 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ if(๐ โค ๐ต, ๐ต, ๐) โ โ) |
84 | 22 | nngt0d 12226 |
. . . . . . 7
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < ๐ต) |
85 | | max2 13131 |
. . . . . . . 8
โข ((๐ โ โ โง ๐ต โ โ) โ ๐ต โค if(๐ โค ๐ต, ๐ต, ๐)) |
86 | 8, 29, 85 | syl2anc 584 |
. . . . . . 7
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ ๐ต โค if(๐ โค ๐ต, ๐ต, ๐)) |
87 | 25, 29, 83, 84, 86 | ltletrd 11339 |
. . . . . 6
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ 0 < if(๐ โค ๐ต, ๐ต, ๐)) |
88 | | lerec 12062 |
. . . . . 6
โข
(((if(๐ โค ๐ต, ๐ต, ๐) โ โ โง 0 < if(๐ โค ๐ต, ๐ต, ๐)) โง (if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ โง 0 < if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (if(๐ โค ๐ต, ๐ต, ๐) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / if(๐ โค ๐ต, ๐ต, ๐)))) |
89 | 83, 87, 38, 39, 88 | syl22anc 837 |
. . . . 5
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (if(๐ โค ๐ต, ๐ต, ๐) โค if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / if(๐ โค ๐ต, ๐ต, ๐)))) |
90 | 82, 89 | mpbid 231 |
. . . 4
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 / ๐ด)) + 1), ๐ต)) โค (1 / if(๐ โค ๐ต, ๐ต, ๐))) |
91 | 14, 24, 75, 27, 90 | ltletrd 11339 |
. . 3
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ (absโ((๐ด ยท ๐) โ ๐)) < (1 / if(๐ โค ๐ต, ๐ต, ๐))) |
92 | | oveq2 7385 |
. . . . . 6
โข (๐ฅ = ๐ โ (๐ด ยท ๐ฅ) = (๐ด ยท ๐)) |
93 | 92 | fvoveq1d 7399 |
. . . . 5
โข (๐ฅ = ๐ โ (absโ((๐ด ยท ๐ฅ) โ ๐ฆ)) = (absโ((๐ด ยท ๐) โ ๐ฆ))) |
94 | | breq1 5128 |
. . . . . . 7
โข (๐ฅ = ๐ โ (๐ฅ โค ๐ต โ ๐ โค ๐ต)) |
95 | | id 22 |
. . . . . . 7
โข (๐ฅ = ๐ โ ๐ฅ = ๐) |
96 | 94, 95 | ifbieq2d 4532 |
. . . . . 6
โข (๐ฅ = ๐ โ if(๐ฅ โค ๐ต, ๐ต, ๐ฅ) = if(๐ โค ๐ต, ๐ต, ๐)) |
97 | 96 | oveq2d 7393 |
. . . . 5
โข (๐ฅ = ๐ โ (1 / if(๐ฅ โค ๐ต, ๐ต, ๐ฅ)) = (1 / if(๐ โค ๐ต, ๐ต, ๐))) |
98 | 93, 97 | breq12d 5138 |
. . . 4
โข (๐ฅ = ๐ โ ((absโ((๐ด ยท ๐ฅ) โ ๐ฆ)) < (1 / if(๐ฅ โค ๐ต, ๐ต, ๐ฅ)) โ (absโ((๐ด ยท ๐) โ ๐ฆ)) < (1 / if(๐ โค ๐ต, ๐ต, ๐)))) |
99 | | oveq2 7385 |
. . . . . 6
โข (๐ฆ = ๐ โ ((๐ด ยท ๐) โ ๐ฆ) = ((๐ด ยท ๐) โ ๐)) |
100 | 99 | fveq2d 6866 |
. . . . 5
โข (๐ฆ = ๐ โ (absโ((๐ด ยท ๐) โ ๐ฆ)) = (absโ((๐ด ยท ๐) โ ๐))) |
101 | 100 | breq1d 5135 |
. . . 4
โข (๐ฆ = ๐ โ ((absโ((๐ด ยท ๐) โ ๐ฆ)) < (1 / if(๐ โค ๐ต, ๐ต, ๐)) โ (absโ((๐ด ยท ๐) โ ๐)) < (1 / if(๐ โค ๐ต, ๐ต, ๐)))) |
102 | 98, 101 | rspc2ev 3606 |
. . 3
โข ((๐ โ โ โง ๐ โ โ โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ โค ๐ต, ๐ต, ๐))) โ โ๐ฅ โ โ โ๐ฆ โ โ (absโ((๐ด ยท ๐ฅ) โ ๐ฆ)) < (1 / if(๐ฅ โค ๐ต, ๐ต, ๐ฅ))) |
103 | 2, 73, 91, 102 | syl3anc 1371 |
. 2
โข
(((((๐ด โ
โ+ โง ๐ต
โ โ) โง ๐
โ (1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))) โง ๐ โ โ0) โง
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) โ โ๐ฅ โ โ โ๐ฆ โ โ (absโ((๐ด ยท ๐ฅ) โ ๐ฆ)) < (1 / if(๐ฅ โค ๐ต, ๐ต, ๐ฅ))) |
104 | 19, 21 | ifcld 4552 |
. . 3
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ) |
105 | | irrapxlem3 41238 |
. . 3
โข ((๐ด โ โ+
โง if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต) โ โ) โ โ๐ โ (1...if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))โ๐ โ โ0
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) |
106 | 5, 104, 105 | syl2anc 584 |
. 2
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ โ๐ โ
(1...if(๐ต โค
((โโ(1 / ๐ด)) +
1), ((โโ(1 / ๐ด)) + 1), ๐ต))โ๐ โ โ0
(absโ((๐ด ยท
๐) โ ๐)) < (1 / if(๐ต โค ((โโ(1 / ๐ด)) + 1), ((โโ(1 /
๐ด)) + 1), ๐ต))) |
107 | 103, 106 | r19.29vva 3212 |
1
โข ((๐ด โ โ+
โง ๐ต โ โ)
โ โ๐ฅ โ
โ โ๐ฆ โ
โ (absโ((๐ด
ยท ๐ฅ) โ ๐ฆ)) < (1 / if(๐ฅ โค ๐ต, ๐ต, ๐ฅ))) |