Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ ๐ต โ โ+ ) |
2 |
1
|
rpreccld |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ ( 1 / ๐ต ) โ โ+ ) |
3 |
2
|
rprege0d |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ ( ( 1 / ๐ต ) โ โ โง 0 โค ( 1 / ๐ต ) ) ) |
4 |
|
flge0nn0 |
โข ( ( ( 1 / ๐ต ) โ โ โง 0 โค ( 1 / ๐ต ) ) โ ( โ โ ( 1 / ๐ต ) ) โ โ0 ) |
5 |
|
nn0p1nn |
โข ( ( โ โ ( 1 / ๐ต ) ) โ โ0 โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) |
6 |
3 4 5
|
3syl |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) |
7 |
|
irrapxlem4 |
โข ( ( ๐ด โ โ+ โง ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) โ โ ๐ โ โ โ ๐ โ โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) |
8 |
6 7
|
syldan |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ โ ๐ โ โ โ ๐ โ โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) |
9 |
|
simplrr |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
10 |
|
nnq |
โข ( ๐ โ โ โ ๐ โ โ ) |
11 |
9 10
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
12 |
|
simplrl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
13 |
|
nnq |
โข ( ๐ โ โ โ ๐ โ โ ) |
14 |
12 13
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
15 |
12
|
nnne0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ 0 ) |
16 |
|
qdivcl |
โข ( ( ๐ โ โ โง ๐ โ โ โง ๐ โ 0 ) โ ( ๐ / ๐ ) โ โ ) |
17 |
11 14 15 16
|
syl3anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ๐ ) โ โ ) |
18 |
9
|
nnrpd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ+ ) |
19 |
12
|
nnrpd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ+ ) |
20 |
18 19
|
rpdivcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ๐ ) โ โ+ ) |
21 |
20
|
rpgt0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 < ( ๐ / ๐ ) ) |
22 |
12
|
nnred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
23 |
12
|
nnnn0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ0 ) |
24 |
23
|
nn0ge0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 โค ๐ ) |
25 |
22 24
|
absidd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ๐ ) = ๐ ) |
26 |
25
|
eqcomd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ = ( abs โ ๐ ) ) |
27 |
26
|
oveq1d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) = ( ( abs โ ๐ ) ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) ) |
28 |
12
|
nncnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
29 |
|
qre |
โข ( ( ๐ / ๐ ) โ โ โ ( ๐ / ๐ ) โ โ ) |
30 |
17 29
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ๐ ) โ โ ) |
31 |
|
rpre |
โข ( ๐ด โ โ+ โ ๐ด โ โ ) |
32 |
31
|
ad3antrrr |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ด โ โ ) |
33 |
30 32
|
resubcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ / ๐ ) โ ๐ด ) โ โ ) |
34 |
33
|
recnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ / ๐ ) โ ๐ด ) โ โ ) |
35 |
28 34
|
absmuld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ๐ ยท ( ( ๐ / ๐ ) โ ๐ด ) ) ) = ( ( abs โ ๐ ) ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) ) |
36 |
27 35
|
eqtr4d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) = ( abs โ ( ๐ ยท ( ( ๐ / ๐ ) โ ๐ด ) ) ) ) |
37 |
|
qcn |
โข ( ( ๐ / ๐ ) โ โ โ ( ๐ / ๐ ) โ โ ) |
38 |
17 37
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ๐ ) โ โ ) |
39 |
|
rpcn |
โข ( ๐ด โ โ+ โ ๐ด โ โ ) |
40 |
39
|
ad3antrrr |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ด โ โ ) |
41 |
28 38 40
|
subdid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( ( ๐ / ๐ ) โ ๐ด ) ) = ( ( ๐ ยท ( ๐ / ๐ ) ) โ ( ๐ ยท ๐ด ) ) ) |
42 |
9
|
nncnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
43 |
42 28 15
|
divcan2d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( ๐ / ๐ ) ) = ๐ ) |
44 |
28 40
|
mulcomd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ๐ด ) = ( ๐ด ยท ๐ ) ) |
45 |
43 44
|
oveq12d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ ยท ( ๐ / ๐ ) ) โ ( ๐ ยท ๐ด ) ) = ( ๐ โ ( ๐ด ยท ๐ ) ) ) |
46 |
41 45
|
eqtrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( ( ๐ / ๐ ) โ ๐ด ) ) = ( ๐ โ ( ๐ด ยท ๐ ) ) ) |
47 |
46
|
fveq2d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ๐ ยท ( ( ๐ / ๐ ) โ ๐ด ) ) ) = ( abs โ ( ๐ โ ( ๐ด ยท ๐ ) ) ) ) |
48 |
32 22
|
remulcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ด ยท ๐ ) โ โ ) |
49 |
48
|
recnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ด ยท ๐ ) โ โ ) |
50 |
42 49
|
abssubd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ๐ โ ( ๐ด ยท ๐ ) ) ) = ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) ) |
51 |
36 47 50
|
3eqtrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) = ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) ) |
52 |
9
|
nnred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โ ) |
53 |
48 52
|
resubcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ด ยท ๐ ) โ ๐ ) โ โ ) |
54 |
53
|
recnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ด ยท ๐ ) โ ๐ ) โ โ ) |
55 |
54
|
abscld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) โ โ ) |
56 |
|
simpllr |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ต โ โ+ ) |
57 |
56
|
rprecred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ๐ต ) โ โ ) |
58 |
56
|
rpreccld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ๐ต ) โ โ+ ) |
59 |
58
|
rpge0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 โค ( 1 / ๐ต ) ) |
60 |
57 59 4
|
syl2anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( โ โ ( 1 / ๐ต ) ) โ โ0 ) |
61 |
60 5
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) |
62 |
61
|
nnrpd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ+ ) |
63 |
62 19
|
ifcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) โ โ+ ) |
64 |
63
|
rprecred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โ โ ) |
65 |
56
|
rpred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ต โ โ ) |
66 |
22 65
|
remulcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ๐ต ) โ โ ) |
67 |
|
simpr |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) |
68 |
58
|
rprecred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( 1 / ๐ต ) ) โ โ ) |
69 |
61
|
nnred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) |
70 |
69 22
|
ifcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) โ โ ) |
71 |
|
fllep1 |
โข ( ( 1 / ๐ต ) โ โ โ ( 1 / ๐ต ) โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) ) |
72 |
57 71
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ๐ต ) โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) ) |
73 |
|
max2 |
โข ( ( ๐ โ โ โง ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) |
74 |
22 69 73
|
syl2anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) |
75 |
57 69 70 72 74
|
letrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ๐ต ) โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) |
76 |
58 63
|
lerecd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( 1 / ๐ต ) โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โค ( 1 / ( 1 / ๐ต ) ) ) ) |
77 |
75 76
|
mpbid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โค ( 1 / ( 1 / ๐ต ) ) ) |
78 |
65
|
recnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ต โ โ ) |
79 |
56
|
rpne0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ต โ 0 ) |
80 |
78 79
|
recrecd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( 1 / ๐ต ) ) = ๐ต ) |
81 |
78
|
mulid2d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 ยท ๐ต ) = ๐ต ) |
82 |
80 81
|
eqtr4d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( 1 / ๐ต ) ) = ( 1 ยท ๐ต ) ) |
83 |
12
|
nnge1d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 1 โค ๐ ) |
84 |
|
1red |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 1 โ โ ) |
85 |
84 22 56
|
lemul1d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 โค ๐ โ ( 1 ยท ๐ต ) โค ( ๐ ยท ๐ต ) ) ) |
86 |
83 85
|
mpbid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 ยท ๐ต ) โค ( ๐ ยท ๐ต ) ) |
87 |
82 86
|
eqbrtrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( 1 / ๐ต ) ) โค ( ๐ ยท ๐ต ) ) |
88 |
64 68 66 77 87
|
letrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โค ( ๐ ยท ๐ต ) ) |
89 |
55 64 66 67 88
|
ltletrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( ๐ ยท ๐ต ) ) |
90 |
51 89
|
eqbrtrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ๐ต ) ) |
91 |
34
|
abscld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) โ โ ) |
92 |
12
|
nngt0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 < ๐ ) |
93 |
|
ltmul2 |
โข ( ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) โ โ โง ๐ต โ โ โง ( ๐ โ โ โง 0 < ๐ ) ) โ ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ๐ต ) ) ) |
94 |
91 65 22 92 93
|
syl112anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ๐ต ) ) ) |
95 |
90 94
|
mpbird |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต ) |
96 |
22 22
|
remulcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ๐ ) โ โ ) |
97 |
22 15
|
msqgt0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 < ( ๐ ยท ๐ ) ) |
98 |
97
|
gt0ne0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ๐ ) โ 0 ) |
99 |
96 98
|
rereccld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( ๐ ยท ๐ ) ) โ โ ) |
100 |
|
qdencl |
โข ( ( ๐ / ๐ ) โ โ โ ( denom โ ( ๐ / ๐ ) ) โ โ ) |
101 |
17 100
|
syl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โ โ ) |
102 |
101
|
nnred |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โ โ ) |
103 |
102 102
|
remulcld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โ โ ) |
104 |
101
|
nnne0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โ 0 ) |
105 |
102 104
|
msqgt0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 < ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) |
106 |
105
|
gt0ne0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โ 0 ) |
107 |
103 106
|
rereccld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) โ โ ) |
108 |
22 15
|
rereccld |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ๐ ) โ โ ) |
109 |
|
max1 |
โข ( ( ๐ โ โ โง ( ( โ โ ( 1 / ๐ต ) ) + 1 ) โ โ ) โ ๐ โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) |
110 |
22 69 109
|
syl2anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) |
111 |
19 63
|
lerecd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ โค if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โค ( 1 / ๐ ) ) ) |
112 |
110 111
|
mpbid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โค ( 1 / ๐ ) ) |
113 |
55 64 108 67 112
|
ltletrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / ๐ ) ) |
114 |
28 28 28 15 15
|
divdiv1d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ / ๐ ) / ๐ ) = ( ๐ / ( ๐ ยท ๐ ) ) ) |
115 |
28 15
|
dividd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ๐ ) = 1 ) |
116 |
115
|
oveq1d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ๐ / ๐ ) / ๐ ) = ( 1 / ๐ ) ) |
117 |
96
|
recnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ๐ ) โ โ ) |
118 |
28 117 98
|
divrecd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ / ( ๐ ยท ๐ ) ) = ( ๐ ยท ( 1 / ( ๐ ยท ๐ ) ) ) ) |
119 |
114 116 118
|
3eqtr3rd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( 1 / ( ๐ ยท ๐ ) ) ) = ( 1 / ๐ ) ) |
120 |
113 51 119
|
3brtr4d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ( 1 / ( ๐ ยท ๐ ) ) ) ) |
121 |
|
ltmul2 |
โข ( ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) โ โ โง ( 1 / ( ๐ ยท ๐ ) ) โ โ โง ( ๐ โ โ โง 0 < ๐ ) ) โ ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( 1 / ( ๐ ยท ๐ ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ( 1 / ( ๐ ยท ๐ ) ) ) ) ) |
122 |
91 99 22 92 121
|
syl112anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( 1 / ( ๐ ยท ๐ ) ) โ ( ๐ ยท ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) < ( ๐ ยท ( 1 / ( ๐ ยท ๐ ) ) ) ) ) |
123 |
120 122
|
mpbird |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( 1 / ( ๐ ยท ๐ ) ) ) |
124 |
9
|
nnzd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ๐ โ โค ) |
125 |
|
divdenle |
โข ( ( ๐ โ โค โง ๐ โ โ ) โ ( denom โ ( ๐ / ๐ ) ) โค ๐ ) |
126 |
124 12 125
|
syl2anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โค ๐ ) |
127 |
101
|
nnnn0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โ โ0 ) |
128 |
127
|
nn0ge0d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ 0 โค ( denom โ ( ๐ / ๐ ) ) ) |
129 |
|
le2msq |
โข ( ( ( ( denom โ ( ๐ / ๐ ) ) โ โ โง 0 โค ( denom โ ( ๐ / ๐ ) ) ) โง ( ๐ โ โ โง 0 โค ๐ ) ) โ ( ( denom โ ( ๐ / ๐ ) ) โค ๐ โ ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โค ( ๐ ยท ๐ ) ) ) |
130 |
102 128 22 24 129
|
syl22anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) โค ๐ โ ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โค ( ๐ ยท ๐ ) ) ) |
131 |
126 130
|
mpbid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โค ( ๐ ยท ๐ ) ) |
132 |
|
lerec |
โข ( ( ( ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โ โ โง 0 < ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) โง ( ( ๐ ยท ๐ ) โ โ โง 0 < ( ๐ ยท ๐ ) ) ) โ ( ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โค ( ๐ ยท ๐ ) โ ( 1 / ( ๐ ยท ๐ ) ) โค ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) ) |
133 |
103 105 96 97 132
|
syl22anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) โค ( ๐ ยท ๐ ) โ ( 1 / ( ๐ ยท ๐ ) ) โค ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) ) |
134 |
131 133
|
mpbid |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( ๐ ยท ๐ ) ) โค ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) |
135 |
91 99 107 123 134
|
ltletrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) |
136 |
101
|
nncnd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( denom โ ( ๐ / ๐ ) ) โ โ ) |
137 |
|
2nn0 |
โข 2 โ โ0 |
138 |
|
expneg |
โข ( ( ( denom โ ( ๐ / ๐ ) ) โ โ โง 2 โ โ0 ) โ ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) = ( 1 / ( ( denom โ ( ๐ / ๐ ) ) โ 2 ) ) ) |
139 |
136 137 138
|
sylancl |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) = ( 1 / ( ( denom โ ( ๐ / ๐ ) ) โ 2 ) ) ) |
140 |
136
|
sqvald |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) โ 2 ) = ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) |
141 |
140
|
oveq2d |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( 1 / ( ( denom โ ( ๐ / ๐ ) ) โ 2 ) ) = ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) |
142 |
139 141
|
eqtrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) = ( 1 / ( ( denom โ ( ๐ / ๐ ) ) ยท ( denom โ ( ๐ / ๐ ) ) ) ) ) |
143 |
135 142
|
breqtrrd |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) ) |
144 |
|
breq2 |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( 0 < ๐ฅ โ 0 < ( ๐ / ๐ ) ) ) |
145 |
|
fvoveq1 |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( abs โ ( ๐ฅ โ ๐ด ) ) = ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) ) |
146 |
145
|
breq1d |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต ) ) |
147 |
|
fveq2 |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( denom โ ๐ฅ ) = ( denom โ ( ๐ / ๐ ) ) ) |
148 |
147
|
oveq1d |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( ( denom โ ๐ฅ ) โ - 2 ) = ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) ) |
149 |
145 148
|
breq12d |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) โ ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) ) ) |
150 |
144 146 149
|
3anbi123d |
โข ( ๐ฅ = ( ๐ / ๐ ) โ ( ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) โ ( 0 < ( ๐ / ๐ ) โง ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต โง ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) ) ) ) |
151 |
150
|
rspcev |
โข ( ( ( ๐ / ๐ ) โ โ โง ( 0 < ( ๐ / ๐ ) โง ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ๐ต โง ( abs โ ( ( ๐ / ๐ ) โ ๐ด ) ) < ( ( denom โ ( ๐ / ๐ ) ) โ - 2 ) ) ) โ โ ๐ฅ โ โ ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) ) |
152 |
17 21 95 143 151
|
syl13anc |
โข ( ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โง ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) ) โ โ ๐ฅ โ โ ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) ) |
153 |
152
|
ex |
โข ( ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โ โ ๐ฅ โ โ ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) ) ) |
154 |
153
|
rexlimdvva |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ ( โ ๐ โ โ โ ๐ โ โ ( abs โ ( ( ๐ด ยท ๐ ) โ ๐ ) ) < ( 1 / if ( ๐ โค ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ( ( โ โ ( 1 / ๐ต ) ) + 1 ) , ๐ ) ) โ โ ๐ฅ โ โ ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) ) ) |
155 |
8 154
|
mpd |
โข ( ( ๐ด โ โ+ โง ๐ต โ โ+ ) โ โ ๐ฅ โ โ ( 0 < ๐ฅ โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ๐ต โง ( abs โ ( ๐ฅ โ ๐ด ) ) < ( ( denom โ ๐ฅ ) โ - 2 ) ) ) |