Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . 6
โข ((๐ด โ โ*
โง 0 < ๐ด) โ 0
< ๐ด) |
2 | | simpr 486 |
. . . . . 6
โข ((๐ต โ โ*
โง 0 < ๐ต) โ 0
< ๐ต) |
3 | 1, 2 | anim12i 614 |
. . . . 5
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ (0 < ๐ด โง 0 < ๐ต)) |
4 | | mulgt0 11237 |
. . . . . . . 8
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) |
5 | 4 | an4s 659 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (0 <
๐ด โง 0 < ๐ต)) โ 0 < (๐ด ยท ๐ต)) |
6 | 5 | ancoms 460 |
. . . . . 6
โข (((0 <
๐ด โง 0 < ๐ต) โง (๐ด โ โ โง ๐ต โ โ)) โ 0 < (๐ด ยท ๐ต)) |
7 | | rexmul 13196 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
8 | 7 | adantl 483 |
. . . . . 6
โข (((0 <
๐ด โง 0 < ๐ต) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
9 | 6, 8 | breqtrrd 5134 |
. . . . 5
โข (((0 <
๐ด โง 0 < ๐ต) โง (๐ด โ โ โง ๐ต โ โ)) โ 0 < (๐ด ยทe ๐ต)) |
10 | 3, 9 | sylan 581 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง (๐ด โ โ โง ๐ต โ โ)) โ 0 < (๐ด ยทe ๐ต)) |
11 | 10 | anassrs 469 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต)) โง ๐ด โ โ) โง ๐ต โ โ) โ 0 < (๐ด ยทe ๐ต)) |
12 | | 0ltpnf 13048 |
. . . . 5
โข 0 <
+โ |
13 | | oveq2 7366 |
. . . . . 6
โข (๐ต = +โ โ (๐ด ยทe ๐ต) = (๐ด ยทe
+โ)) |
14 | | xmulpnf1 13199 |
. . . . . . 7
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
15 | 14 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ (๐ด ยทe +โ) =
+โ) |
16 | 13, 15 | sylan9eqr 2795 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ต = +โ) โ (๐ด ยทe ๐ต) = +โ) |
17 | 12, 16 | breqtrrid 5144 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ต = +โ) โ 0 < (๐ด ยทe ๐ต)) |
18 | 17 | adantlr 714 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต)) โง ๐ด โ โ) โง ๐ต = +โ) โ 0 < (๐ด ยทe ๐ต)) |
19 | | simplrr 777 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด โ โ) โ 0 < ๐ต) |
20 | | xmulasslem2 13207 |
. . . 4
โข ((0 <
๐ต โง ๐ต = -โ) โ 0 < (๐ด ยทe ๐ต)) |
21 | 19, 20 | sylan 581 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต)) โง ๐ด โ โ) โง ๐ต = -โ) โ 0 < (๐ด ยทe ๐ต)) |
22 | | simprl 770 |
. . . . 5
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ ๐ต โ
โ*) |
23 | | elxr 13042 |
. . . . 5
โข (๐ต โ โ*
โ (๐ต โ โ
โจ ๐ต = +โ โจ
๐ต =
-โ)) |
24 | 22, 23 | sylib 217 |
. . . 4
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
25 | 24 | adantr 482 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด โ โ) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
26 | 11, 18, 21, 25 | mpjao3dan 1432 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด โ โ) โ 0 < (๐ด ยทe ๐ต)) |
27 | | oveq1 7365 |
. . . 4
โข (๐ด = +โ โ (๐ด ยทe ๐ต) = (+โ
ยทe ๐ต)) |
28 | | xmulpnf2 13200 |
. . . . 5
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(+โ ยทe ๐ต) = +โ) |
29 | 28 | adantl 483 |
. . . 4
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ (+โ ยทe
๐ต) =
+โ) |
30 | 27, 29 | sylan9eqr 2795 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด = +โ) โ (๐ด ยทe ๐ต) = +โ) |
31 | 12, 30 | breqtrrid 5144 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด = +โ) โ 0 < (๐ด ยทe ๐ต)) |
32 | | xmulasslem2 13207 |
. . 3
โข ((0 <
๐ด โง ๐ด = -โ) โ 0 < (๐ด ยทe ๐ต)) |
33 | 32 | ad4ant24 753 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โง ๐ด = -โ) โ 0 < (๐ด ยทe ๐ต)) |
34 | | simpll 766 |
. . 3
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ ๐ด โ
โ*) |
35 | | elxr 13042 |
. . 3
โข (๐ด โ โ*
โ (๐ด โ โ
โจ ๐ด = +โ โจ
๐ด =
-โ)) |
36 | 34, 35 | sylib 217 |
. 2
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) |
37 | 26, 31, 33, 36 | mpjao3dan 1432 |
1
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |