Step | Hyp | Ref
| Expression |
1 | | recn 11149 |
. . . . . . . . . 10
โข (๐ด โ โ โ ๐ด โ
โ) |
2 | | recn 11149 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ
โ) |
3 | | recn 11149 |
. . . . . . . . . 10
โข (๐ถ โ โ โ ๐ถ โ
โ) |
4 | | mulass 11147 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) |
5 | 1, 2, 3, 4 | syl3an 1161 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) |
6 | 5 | 3expa 1119 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = (๐ด ยท (๐ต ยท ๐ถ))) |
7 | | remulcl 11144 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
8 | | rexmul 13199 |
. . . . . . . . 9
โข (((๐ด ยท ๐ต) โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยทe ๐ถ) = ((๐ด ยท ๐ต) ยท ๐ถ)) |
9 | 7, 8 | sylan 581 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยทe ๐ถ) = ((๐ด ยท ๐ต) ยท ๐ถ)) |
10 | | remulcl 11144 |
. . . . . . . . . 10
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
11 | | rexmul 13199 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ต ยท ๐ถ) โ โ) โ (๐ด ยทe (๐ต ยท ๐ถ)) = (๐ด ยท (๐ต ยท ๐ถ))) |
12 | 10, 11 | sylan2 594 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ถ โ โ)) โ (๐ด ยทe (๐ต ยท ๐ถ)) = (๐ด ยท (๐ต ยท ๐ถ))) |
13 | 12 | anassrs 469 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต ยท ๐ถ)) = (๐ด ยท (๐ต ยท ๐ถ))) |
14 | 6, 9, 13 | 3eqtr4d 2783 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยท ๐ถ))) |
15 | | rexmul 13199 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
16 | 15 | adantr 482 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
17 | 16 | oveq1d 7376 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = ((๐ด ยท ๐ต) ยทe ๐ถ)) |
18 | | rexmul 13199 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยทe ๐ถ) = (๐ต ยท ๐ถ)) |
19 | 18 | adantll 713 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ต ยทe ๐ถ) = (๐ต ยท ๐ถ)) |
20 | 19 | oveq2d 7377 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต ยทe ๐ถ)) = (๐ด ยทe (๐ต ยท ๐ถ))) |
21 | 14, 17, 20 | 3eqtr4d 2783 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
22 | 21 | adantll 713 |
. . . . 5
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
23 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ถ = +โ โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = ((๐ด ยทe ๐ต) ยทe
+โ)) |
24 | | simp1l 1198 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ ๐ด โ
โ*) |
25 | | simp2l 1200 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ ๐ต โ
โ*) |
26 | | xmulcl 13201 |
. . . . . . . . . . 11
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) โ
โ*) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ด ยทe ๐ต) โ
โ*) |
28 | | xmulgt0 13211 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต)) โ 0 < (๐ด ยทe ๐ต)) |
29 | 28 | 3adant3 1133 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ 0 < (๐ด ยทe ๐ต)) |
30 | | xmulpnf1 13202 |
. . . . . . . . . 10
โข (((๐ด ยทe ๐ต) โ โ*
โง 0 < (๐ด
ยทe ๐ต))
โ ((๐ด
ยทe ๐ต)
ยทe +โ) = +โ) |
31 | 27, 29, 30 | syl2anc 585 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ ((๐ด ยทe ๐ต) ยทe +โ)
= +โ) |
32 | 23, 31 | sylan9eqr 2795 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = +โ) |
33 | | simpl1 1192 |
. . . . . . . . 9
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ (๐ด โ โ* โง 0 <
๐ด)) |
34 | | xmulpnf1 13202 |
. . . . . . . . 9
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
35 | 33, 34 | syl 17 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ (๐ด ยทe +โ) =
+โ) |
36 | 32, 35 | eqtr4d 2776 |
. . . . . . 7
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe
+โ)) |
37 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ถ = +โ โ (๐ต ยทe ๐ถ) = (๐ต ยทe
+โ)) |
38 | | xmulpnf1 13202 |
. . . . . . . . . 10
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(๐ต ยทe
+โ) = +โ) |
39 | 38 | 3ad2ant2 1135 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ต ยทe +โ)
= +โ) |
40 | 37, 39 | sylan9eqr 2795 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ (๐ต ยทe ๐ถ) = +โ) |
41 | 40 | oveq2d 7377 |
. . . . . . 7
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต ยทe ๐ถ)) = (๐ด ยทe
+โ)) |
42 | 36, 41 | eqtr4d 2776 |
. . . . . 6
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
43 | 42 | adantlr 714 |
. . . . 5
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
44 | | simpl3r 1230 |
. . . . . 6
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โ 0 <
๐ถ) |
45 | | xmulasslem2 13210 |
. . . . . 6
โข ((0 <
๐ถ โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
46 | 44, 45 | sylan 581 |
. . . . 5
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
47 | | simp3l 1202 |
. . . . . . 7
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ ๐ถ โ
โ*) |
48 | | elxr 13045 |
. . . . . . 7
โข (๐ถ โ โ*
โ (๐ถ โ โ
โจ ๐ถ = +โ โจ
๐ถ =
-โ)) |
49 | 47, 48 | sylib 217 |
. . . . . 6
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
50 | 49 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
51 | 22, 43, 46, 50 | mpjao3dan 1432 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง (๐ด โ โ โง ๐ต โ โ)) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
52 | 51 | anassrs 469 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โง ๐ต โ โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
53 | | xmulpnf2 13203 |
. . . . . . . 8
โข ((๐ถ โ โ*
โง 0 < ๐ถ) โ
(+โ ยทe ๐ถ) = +โ) |
54 | 53 | 3ad2ant3 1136 |
. . . . . . 7
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (+โ
ยทe ๐ถ) =
+โ) |
55 | 34 | 3ad2ant1 1134 |
. . . . . . 7
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ด ยทe +โ)
= +โ) |
56 | 54, 55 | eqtr4d 2776 |
. . . . . 6
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (+โ
ยทe ๐ถ) =
(๐ด ยทe
+โ)) |
57 | 56 | adantr 482 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ (+โ
ยทe ๐ถ) =
(๐ด ยทe
+โ)) |
58 | | oveq2 7369 |
. . . . . . 7
โข (๐ต = +โ โ (๐ด ยทe ๐ต) = (๐ด ยทe
+โ)) |
59 | 58, 55 | sylan9eqr 2795 |
. . . . . 6
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ (๐ด ยทe ๐ต) = +โ) |
60 | 59 | oveq1d 7376 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (+โ ยทe ๐ถ)) |
61 | | oveq1 7368 |
. . . . . . 7
โข (๐ต = +โ โ (๐ต ยทe ๐ถ) = (+โ
ยทe ๐ถ)) |
62 | 61, 54 | sylan9eqr 2795 |
. . . . . 6
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ (๐ต ยทe ๐ถ) = +โ) |
63 | 62 | oveq2d 7377 |
. . . . 5
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ (๐ด ยทe (๐ต ยทe ๐ถ)) = (๐ด ยทe
+โ)) |
64 | 57, 60, 63 | 3eqtr4d 2783 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ต = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
65 | 64 | adantlr 714 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โง ๐ต = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
66 | | simpl2r 1228 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โ 0 < ๐ต) |
67 | | xmulasslem2 13210 |
. . . 4
โข ((0 <
๐ต โง ๐ต = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
68 | 66, 67 | sylan 581 |
. . 3
โข
(((((๐ด โ
โ* โง 0 < ๐ด) โง (๐ต โ โ* โง 0 <
๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โง ๐ต = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
69 | | elxr 13045 |
. . . . 5
โข (๐ต โ โ*
โ (๐ต โ โ
โจ ๐ต = +โ โจ
๐ต =
-โ)) |
70 | 25, 69 | sylib 217 |
. . . 4
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
71 | 70 | adantr 482 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
72 | 52, 65, 68, 71 | mpjao3dan 1432 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด โ โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
73 | | simpl3 1194 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ (๐ถ โ โ* โง 0 <
๐ถ)) |
74 | 73, 53 | syl 17 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ (+โ
ยทe ๐ถ) =
+โ) |
75 | | oveq1 7368 |
. . . . 5
โข (๐ด = +โ โ (๐ด ยทe ๐ต) = (+โ
ยทe ๐ต)) |
76 | | xmulpnf2 13203 |
. . . . . 6
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(+โ ยทe ๐ต) = +โ) |
77 | 76 | 3ad2ant2 1135 |
. . . . 5
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (+โ
ยทe ๐ต) =
+โ) |
78 | 75, 77 | sylan9eqr 2795 |
. . . 4
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ (๐ด ยทe ๐ต) = +โ) |
79 | 78 | oveq1d 7376 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (+โ ยทe ๐ถ)) |
80 | | oveq1 7368 |
. . . 4
โข (๐ด = +โ โ (๐ด ยทe (๐ต ยทe ๐ถ)) = (+โ
ยทe (๐ต
ยทe ๐ถ))) |
81 | | xmulcl 13201 |
. . . . . 6
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ต ยทe ๐ถ) โ
โ*) |
82 | 25, 47, 81 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ต ยทe ๐ถ) โ
โ*) |
83 | | xmulgt0 13211 |
. . . . . 6
โข (((๐ต โ โ*
โง 0 < ๐ต) โง
(๐ถ โ
โ* โง 0 < ๐ถ)) โ 0 < (๐ต ยทe ๐ถ)) |
84 | 83 | 3adant1 1131 |
. . . . 5
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ 0 < (๐ต ยทe ๐ถ)) |
85 | | xmulpnf2 13203 |
. . . . 5
โข (((๐ต ยทe ๐ถ) โ โ*
โง 0 < (๐ต
ยทe ๐ถ))
โ (+โ ยทe (๐ต ยทe ๐ถ)) = +โ) |
86 | 82, 84, 85 | syl2anc 585 |
. . . 4
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (+โ
ยทe (๐ต
ยทe ๐ถ)) =
+โ) |
87 | 80, 86 | sylan9eqr 2795 |
. . 3
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ (๐ด ยทe (๐ต ยทe ๐ถ)) = +โ) |
88 | 74, 79, 87 | 3eqtr4d 2783 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = +โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
89 | | simp1r 1199 |
. . 3
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ 0 < ๐ด) |
90 | | xmulasslem2 13210 |
. . 3
โข ((0 <
๐ด โง ๐ด = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
91 | 89, 90 | sylan 581 |
. 2
โข ((((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โง ๐ด = -โ) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |
92 | | elxr 13045 |
. . 3
โข (๐ด โ โ*
โ (๐ด โ โ
โจ ๐ด = +โ โจ
๐ด =
-โ)) |
93 | 24, 92 | sylib 217 |
. 2
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) |
94 | 72, 88, 91, 93 | mpjao3dan 1432 |
1
โข (((๐ด โ โ*
โง 0 < ๐ด) โง
(๐ต โ
โ* โง 0 < ๐ต) โง (๐ถ โ โ* โง 0 <
๐ถ)) โ ((๐ด ยทe ๐ต) ยทe ๐ถ) = (๐ด ยทe (๐ต ยทe ๐ถ))) |