Step | Hyp | Ref
| Expression |
1 | | rprene0 12940 |
. . . . 5
โข (๐ด โ โ+
โ (๐ด โ โ
โง ๐ด โ
0)) |
2 | | pnfxr 11217 |
. . . . 5
โข +โ
โ โ* |
3 | 1, 2 | jctil 521 |
. . . 4
โข (๐ด โ โ+
โ (+โ โ โ* โง (๐ด โ โ โง ๐ด โ 0))) |
4 | | 3anass 1096 |
. . . 4
โข
((+โ โ โ* โง ๐ด โ โ โง ๐ด โ 0) โ (+โ โ
โ* โง (๐ด โ โ โง ๐ด โ 0))) |
5 | 3, 4 | sylibr 233 |
. . 3
โข (๐ด โ โ+
โ (+โ โ โ* โง ๐ด โ โ โง ๐ด โ 0)) |
6 | | xdivval 31831 |
. . 3
โข
((+โ โ โ* โง ๐ด โ โ โง ๐ด โ 0) โ (+โ
/๐ ๐ด) =
(โฉ๐ฅ โ
โ* (๐ด
ยทe ๐ฅ) =
+โ)) |
7 | 5, 6 | syl 17 |
. 2
โข (๐ด โ โ+
โ (+โ /๐ ๐ด) = (โฉ๐ฅ โ โ* (๐ด ยทe ๐ฅ) = +โ)) |
8 | 2 | a1i 11 |
. . 3
โข (๐ด โ โ+
โ +โ โ โ*) |
9 | | xlemul2 13219 |
. . . . . . 7
โข
((+โ โ โ* โง ๐ฅ โ โ* โง ๐ด โ โ+)
โ (+โ โค ๐ฅ
โ (๐ด
ยทe +โ) โค (๐ด ยทe ๐ฅ))) |
10 | 2, 9 | mp3an1 1449 |
. . . . . 6
โข ((๐ฅ โ โ*
โง ๐ด โ
โ+) โ (+โ โค ๐ฅ โ (๐ด ยทe +โ) โค (๐ด ยทe ๐ฅ))) |
11 | 10 | ancoms 460 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (+โ โค ๐ฅ โ (๐ด ยทe +โ) โค (๐ด ยทe ๐ฅ))) |
12 | | rpxr 12932 |
. . . . . . . 8
โข (๐ด โ โ+
โ ๐ด โ
โ*) |
13 | | rpgt0 12935 |
. . . . . . . 8
โข (๐ด โ โ+
โ 0 < ๐ด) |
14 | | xmulpnf1 13202 |
. . . . . . . 8
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
15 | 12, 13, 14 | syl2anc 585 |
. . . . . . 7
โข (๐ด โ โ+
โ (๐ด
ยทe +โ) = +โ) |
16 | 15 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (๐ด ยทe +โ) =
+โ) |
17 | 16 | breq1d 5119 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ ((๐ด ยทe +โ) โค (๐ด ยทe ๐ฅ) โ +โ โค (๐ด ยทe ๐ฅ))) |
18 | 11, 17 | bitr2d 280 |
. . . 4
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (+โ โค (๐ด ยทe ๐ฅ) โ +โ โค ๐ฅ)) |
19 | | xmulcl 13201 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ฅ โ
โ*) โ (๐ด ยทe ๐ฅ) โ
โ*) |
20 | 12, 19 | sylan 581 |
. . . . 5
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (๐ด ยทe ๐ฅ) โ
โ*) |
21 | | xgepnf 13093 |
. . . . 5
โข ((๐ด ยทe ๐ฅ) โ โ*
โ (+โ โค (๐ด
ยทe ๐ฅ)
โ (๐ด
ยทe ๐ฅ) =
+โ)) |
22 | 20, 21 | syl 17 |
. . . 4
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (+โ โค (๐ด ยทe ๐ฅ) โ (๐ด ยทe ๐ฅ) = +โ)) |
23 | | xgepnf 13093 |
. . . . 5
โข (๐ฅ โ โ*
โ (+โ โค ๐ฅ
โ ๐ฅ =
+โ)) |
24 | 23 | adantl 483 |
. . . 4
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ (+โ โค ๐ฅ โ ๐ฅ = +โ)) |
25 | 18, 22, 24 | 3bitr3d 309 |
. . 3
โข ((๐ด โ โ+
โง ๐ฅ โ
โ*) โ ((๐ด ยทe ๐ฅ) = +โ โ ๐ฅ = +โ)) |
26 | 8, 25 | riota5 7347 |
. 2
โข (๐ด โ โ+
โ (โฉ๐ฅ
โ โ* (๐ด ยทe ๐ฅ) = +โ) = +โ) |
27 | 7, 26 | eqtrd 2773 |
1
โข (๐ด โ โ+
โ (+โ /๐ ๐ด) = +โ) |