Step | Hyp | Ref
| Expression |
1 | | zre 12510 |
. . . . . 6
โข (๐ด โ โค โ ๐ด โ
โ) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
๐ด โ
โ) |
3 | | absresq 15194 |
. . . . 5
โข (๐ด โ โ โ
((absโ๐ด)โ2) =
(๐ดโ2)) |
4 | 2, 3 | syl 17 |
. . . 4
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
((absโ๐ด)โ2) =
(๐ดโ2)) |
5 | 2 | recnd 11190 |
. . . . . . 7
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
๐ด โ
โ) |
6 | 5 | abscld 15328 |
. . . . . 6
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(absโ๐ด) โ
โ) |
7 | 6 | recnd 11190 |
. . . . 5
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(absโ๐ด) โ
โ) |
8 | 7 | sqvald 14055 |
. . . 4
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
((absโ๐ด)โ2) =
((absโ๐ด) ยท
(absโ๐ด))) |
9 | 4, 8 | eqtr3d 2779 |
. . 3
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(๐ดโ2) =
((absโ๐ด) ยท
(absโ๐ด))) |
10 | | simpr 486 |
. . 3
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(๐ดโ2) โ
โ) |
11 | 9, 10 | eqeltrrd 2839 |
. 2
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
((absโ๐ด) ยท
(absโ๐ด)) โ
โ) |
12 | | nn0abscl 15204 |
. . . . . 6
โข (๐ด โ โค โ
(absโ๐ด) โ
โ0) |
13 | 12 | adantr 482 |
. . . . 5
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(absโ๐ด) โ
โ0) |
14 | 13 | nn0zd 12532 |
. . . 4
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(absโ๐ด) โ
โค) |
15 | | sq1 14106 |
. . . . . 6
โข
(1โ2) = 1 |
16 | | prmuz2 16579 |
. . . . . . . . 9
โข ((๐ดโ2) โ โ โ
(๐ดโ2) โ
(โคโฅโ2)) |
17 | 16 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(๐ดโ2) โ
(โคโฅโ2)) |
18 | | eluz2gt1 12852 |
. . . . . . . 8
โข ((๐ดโ2) โ
(โคโฅโ2) โ 1 < (๐ดโ2)) |
19 | 17, 18 | syl 17 |
. . . . . . 7
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
1 < (๐ดโ2)) |
20 | 19, 4 | breqtrrd 5138 |
. . . . . 6
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
1 < ((absโ๐ด)โ2)) |
21 | 15, 20 | eqbrtrid 5145 |
. . . . 5
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(1โ2) < ((absโ๐ด)โ2)) |
22 | 5 | absge0d 15336 |
. . . . . 6
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
0 โค (absโ๐ด)) |
23 | | 1re 11162 |
. . . . . . 7
โข 1 โ
โ |
24 | | 0le1 11685 |
. . . . . . 7
โข 0 โค
1 |
25 | | lt2sq 14045 |
. . . . . . 7
โข (((1
โ โ โง 0 โค 1) โง ((absโ๐ด) โ โ โง 0 โค
(absโ๐ด))) โ (1
< (absโ๐ด) โ
(1โ2) < ((absโ๐ด)โ2))) |
26 | 23, 24, 25 | mpanl12 701 |
. . . . . 6
โข
(((absโ๐ด)
โ โ โง 0 โค (absโ๐ด)) โ (1 < (absโ๐ด) โ (1โ2) <
((absโ๐ด)โ2))) |
27 | 6, 22, 26 | syl2anc 585 |
. . . . 5
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(1 < (absโ๐ด)
โ (1โ2) < ((absโ๐ด)โ2))) |
28 | 21, 27 | mpbird 257 |
. . . 4
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
1 < (absโ๐ด)) |
29 | | eluz2b1 12851 |
. . . 4
โข
((absโ๐ด)
โ (โคโฅโ2) โ ((absโ๐ด) โ โค โง 1 <
(absโ๐ด))) |
30 | 14, 28, 29 | sylanbrc 584 |
. . 3
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
(absโ๐ด) โ
(โคโฅโ2)) |
31 | | nprm 16571 |
. . 3
โข
(((absโ๐ด)
โ (โคโฅโ2) โง (absโ๐ด) โ (โคโฅโ2))
โ ยฌ ((absโ๐ด)
ยท (absโ๐ด))
โ โ) |
32 | 30, 30, 31 | syl2anc 585 |
. 2
โข ((๐ด โ โค โง (๐ดโ2) โ โ) โ
ยฌ ((absโ๐ด)
ยท (absโ๐ด))
โ โ) |
33 | 11, 32 | pm2.65da 816 |
1
โข (๐ด โ โค โ ยฌ
(๐ดโ2) โ
โ) |