Step | Hyp | Ref
| Expression |
1 | | simpr 485 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด โ โ) โ ๐ด โ โ) |
2 | | simp2l 1199 |
. . . . 5
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ ๐ต โ
โ*) |
3 | 2 | ad2antrr 724 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด โ โ) โ ๐ต โ
โ*) |
4 | | simp3l 1201 |
. . . . 5
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ ๐ถ โ
โ*) |
5 | 4 | ad2antrr 724 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด โ โ) โ ๐ถ โ
โ*) |
6 | | xadddi 13270 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
7 | 1, 3, 5, 6 | syl3anc 1371 |
. . 3
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
8 | | pnfxr 11264 |
. . . . . 6
โข +โ
โ โ* |
9 | 4 | adantr 481 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ๐ถ โ
โ*) |
10 | | xmulcl 13248 |
. . . . . 6
โข
((+โ โ โ* โง ๐ถ โ โ*) โ
(+โ ยทe ๐ถ) โ
โ*) |
11 | 8, 9, 10 | sylancr 587 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (+โ
ยทe ๐ถ)
โ โ*) |
12 | | simpl3r 1229 |
. . . . . . . 8
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ 0 โค ๐ถ) |
13 | | 0lepnf 13108 |
. . . . . . . . 9
โข 0 โค
+โ |
14 | | xmulge0 13259 |
. . . . . . . . 9
โข
(((+โ โ โ* โง 0 โค +โ) โง
(๐ถ โ
โ* โง 0 โค ๐ถ)) โ 0 โค (+โ
ยทe ๐ถ)) |
15 | 8, 13, 14 | mpanl12 700 |
. . . . . . . 8
โข ((๐ถ โ โ*
โง 0 โค ๐ถ) โ 0
โค (+โ ยทe ๐ถ)) |
16 | 4, 12, 15 | syl2an2r 683 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ 0 โค (+โ
ยทe ๐ถ)) |
17 | | ge0nemnf 13148 |
. . . . . . 7
โข
(((+โ ยทe ๐ถ) โ โ* โง 0 โค
(+โ ยทe ๐ถ)) โ (+โ ยทe
๐ถ) โ
-โ) |
18 | 11, 16, 17 | syl2anc 584 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (+โ
ยทe ๐ถ)
โ -โ) |
19 | 18 | adantr 481 |
. . . . 5
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = +โ) โ (+โ
ยทe ๐ถ)
โ -โ) |
20 | | xaddpnf2 13202 |
. . . . 5
โข
(((+โ ยทe ๐ถ) โ โ* โง (+โ
ยทe ๐ถ)
โ -โ) โ (+โ +๐ (+โ
ยทe ๐ถ)) =
+โ) |
21 | 11, 19, 20 | syl2an2r 683 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = +โ) โ (+โ
+๐ (+โ ยทe ๐ถ)) = +โ) |
22 | | oveq1 7412 |
. . . . . 6
โข (๐ด = +โ โ (๐ด ยทe ๐ต) = (+โ
ยทe ๐ต)) |
23 | | oveq1 7412 |
. . . . . 6
โข (๐ด = +โ โ (๐ด ยทe ๐ถ) = (+โ
ยทe ๐ถ)) |
24 | 22, 23 | oveq12d 7423 |
. . . . 5
โข (๐ด = +โ โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((+โ
ยทe ๐ต)
+๐ (+โ ยทe ๐ถ))) |
25 | | xmulpnf2 13250 |
. . . . . . 7
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(+โ ยทe ๐ต) = +โ) |
26 | 2, 25 | sylan 580 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (+โ
ยทe ๐ต) =
+โ) |
27 | 26 | oveq1d 7420 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ((+โ
ยทe ๐ต)
+๐ (+โ ยทe ๐ถ)) = (+โ +๐
(+โ ยทe ๐ถ))) |
28 | 24, 27 | sylan9eqr 2794 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = (+โ +๐
(+โ ยทe ๐ถ))) |
29 | | oveq1 7412 |
. . . . 5
โข (๐ด = +โ โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (+โ
ยทe (๐ต
+๐ ๐ถ))) |
30 | | xaddcl 13214 |
. . . . . . 7
โข ((๐ต โ โ*
โง ๐ถ โ
โ*) โ (๐ต +๐ ๐ถ) โ
โ*) |
31 | 2, 4, 30 | syl2anc 584 |
. . . . . 6
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ต +๐ ๐ถ) โ
โ*) |
32 | | 0xr 11257 |
. . . . . . . 8
โข 0 โ
โ* |
33 | 32 | a1i 11 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ 0 โ
โ*) |
34 | 2 | adantr 481 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ๐ต โ
โ*) |
35 | 31 | adantr 481 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (๐ต +๐ ๐ถ) โ
โ*) |
36 | | simpr 485 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ 0 < ๐ต) |
37 | 34 | xaddridd 13218 |
. . . . . . . 8
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (๐ต +๐ 0) = ๐ต) |
38 | | xleadd2a 13229 |
. . . . . . . . 9
โข (((0
โ โ* โง ๐ถ โ โ* โง ๐ต โ โ*)
โง 0 โค ๐ถ) โ
(๐ต +๐ 0)
โค (๐ต
+๐ ๐ถ)) |
39 | 33, 9, 34, 12, 38 | syl31anc 1373 |
. . . . . . . 8
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (๐ต +๐ 0) โค (๐ต +๐ ๐ถ)) |
40 | 37, 39 | eqbrtrrd 5171 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ๐ต โค (๐ต +๐ ๐ถ)) |
41 | 33, 34, 35, 36, 40 | xrltletrd 13136 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ 0 < (๐ต +๐ ๐ถ)) |
42 | | xmulpnf2 13250 |
. . . . . 6
โข (((๐ต +๐ ๐ถ) โ โ*
โง 0 < (๐ต
+๐ ๐ถ))
โ (+โ ยทe (๐ต +๐ ๐ถ)) = +โ) |
43 | 31, 41, 42 | syl2an2r 683 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (+โ
ยทe (๐ต
+๐ ๐ถ)) =
+โ) |
44 | 29, 43 | sylan9eqr 2794 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = +โ) |
45 | 21, 28, 44 | 3eqtr4rd 2783 |
. . 3
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
46 | | mnfxr 11267 |
. . . . . . 7
โข -โ
โ โ* |
47 | | xmulcl 13248 |
. . . . . . 7
โข
((-โ โ โ* โง ๐ถ โ โ*) โ
(-โ ยทe ๐ถ) โ
โ*) |
48 | 46, 9, 47 | sylancr 587 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (-โ
ยทe ๐ถ)
โ โ*) |
49 | | xmulneg1 13244 |
. . . . . . . . . . . 12
โข
((-โ โ โ* โง ๐ถ โ โ*) โ
(-๐-โ ยทe ๐ถ) = -๐(-โ
ยทe ๐ถ)) |
50 | 46, 9, 49 | sylancr 587 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ
(-๐-โ ยทe ๐ถ) = -๐(-โ
ยทe ๐ถ)) |
51 | | xnegmnf 13185 |
. . . . . . . . . . . 12
โข
-๐-โ = +โ |
52 | 51 | oveq1i 7415 |
. . . . . . . . . . 11
โข
(-๐-โ ยทe ๐ถ) = (+โ ยทe ๐ถ) |
53 | 50, 52 | eqtr3di 2787 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ
-๐(-โ ยทe ๐ถ) = (+โ ยทe ๐ถ)) |
54 | | xnegpnf 13184 |
. . . . . . . . . . 11
โข
-๐+โ = -โ |
55 | 54 | a1i 11 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ
-๐+โ = -โ) |
56 | 53, 55 | eqeq12d 2748 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ
(-๐(-โ ยทe ๐ถ) = -๐+โ โ
(+โ ยทe ๐ถ) = -โ)) |
57 | | xneg11 13190 |
. . . . . . . . . 10
โข
(((-โ ยทe ๐ถ) โ โ* โง +โ
โ โ*) โ (-๐(-โ
ยทe ๐ถ) =
-๐+โ โ (-โ ยทe ๐ถ) = +โ)) |
58 | 48, 8, 57 | sylancl 586 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ
(-๐(-โ ยทe ๐ถ) = -๐+โ โ
(-โ ยทe ๐ถ) = +โ)) |
59 | 56, 58 | bitr3d 280 |
. . . . . . . 8
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ((+โ
ยทe ๐ถ) =
-โ โ (-โ ยทe ๐ถ) = +โ)) |
60 | 59 | necon3bid 2985 |
. . . . . . 7
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ((+โ
ยทe ๐ถ)
โ -โ โ (-โ ยทe ๐ถ) โ +โ)) |
61 | 18, 60 | mpbid 231 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (-โ
ยทe ๐ถ)
โ +โ) |
62 | | xaddmnf2 13204 |
. . . . . 6
โข
(((-โ ยทe ๐ถ) โ โ* โง (-โ
ยทe ๐ถ)
โ +โ) โ (-โ +๐ (-โ
ยทe ๐ถ)) =
-โ) |
63 | 48, 61, 62 | syl2anc 584 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (-โ
+๐ (-โ ยทe ๐ถ)) = -โ) |
64 | 63 | adantr 481 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = -โ) โ (-โ
+๐ (-โ ยทe ๐ถ)) = -โ) |
65 | | oveq1 7412 |
. . . . . 6
โข (๐ด = -โ โ (๐ด ยทe ๐ต) = (-โ
ยทe ๐ต)) |
66 | | oveq1 7412 |
. . . . . 6
โข (๐ด = -โ โ (๐ด ยทe ๐ถ) = (-โ
ยทe ๐ถ)) |
67 | 65, 66 | oveq12d 7423 |
. . . . 5
โข (๐ด = -โ โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((-โ
ยทe ๐ต)
+๐ (-โ ยทe ๐ถ))) |
68 | | xmulmnf2 13252 |
. . . . . . 7
โข ((๐ต โ โ*
โง 0 < ๐ต) โ
(-โ ยทe ๐ต) = -โ) |
69 | 2, 68 | sylan 580 |
. . . . . 6
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (-โ
ยทe ๐ต) =
-โ) |
70 | 69 | oveq1d 7420 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ((-โ
ยทe ๐ต)
+๐ (-โ ยทe ๐ถ)) = (-โ +๐
(-โ ยทe ๐ถ))) |
71 | 67, 70 | sylan9eqr 2794 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = (-โ +๐
(-โ ยทe ๐ถ))) |
72 | | oveq1 7412 |
. . . . 5
โข (๐ด = -โ โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (-โ
ยทe (๐ต
+๐ ๐ถ))) |
73 | | xmulmnf2 13252 |
. . . . . 6
โข (((๐ต +๐ ๐ถ) โ โ*
โง 0 < (๐ต
+๐ ๐ถ))
โ (-โ ยทe (๐ต +๐ ๐ถ)) = -โ) |
74 | 31, 41, 73 | syl2an2r 683 |
. . . . 5
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (-โ
ยทe (๐ต
+๐ ๐ถ)) =
-โ) |
75 | 72, 74 | sylan9eqr 2794 |
. . . 4
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = -โ) |
76 | 64, 71, 75 | 3eqtr4rd 2783 |
. . 3
โข ((((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โง ๐ด = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
77 | | simpl1 1191 |
. . . 4
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ ๐ด โ
โ*) |
78 | | elxr 13092 |
. . . 4
โข (๐ด โ โ*
โ (๐ด โ โ
โจ ๐ด = +โ โจ
๐ด =
-โ)) |
79 | 77, 78 | sylib 217 |
. . 3
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (๐ด โ โ โจ ๐ด = +โ โจ ๐ด = -โ)) |
80 | 7, 45, 76, 79 | mpjao3dan 1431 |
. 2
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 < ๐ต) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
81 | | simp1 1136 |
. . . . . 6
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ ๐ด โ
โ*) |
82 | | xmulcl 13248 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ถ โ
โ*) โ (๐ด ยทe ๐ถ) โ
โ*) |
83 | 81, 4, 82 | syl2anc 584 |
. . . . 5
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ด ยทe ๐ถ) โ
โ*) |
84 | 83 | adantr 481 |
. . . 4
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (๐ด ยทe ๐ถ) โ
โ*) |
85 | | xaddlid 13217 |
. . . 4
โข ((๐ด ยทe ๐ถ) โ โ*
โ (0 +๐ (๐ด ยทe ๐ถ)) = (๐ด ยทe ๐ถ)) |
86 | 84, 85 | syl 17 |
. . 3
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (0
+๐ (๐ด
ยทe ๐ถ)) =
(๐ด ยทe
๐ถ)) |
87 | | oveq2 7413 |
. . . . . 6
โข (0 =
๐ต โ (๐ด ยทe 0) = (๐ด ยทe ๐ต)) |
88 | 87 | eqcomd 2738 |
. . . . 5
โข (0 =
๐ต โ (๐ด ยทe ๐ต) = (๐ด ยทe 0)) |
89 | | xmul01 13242 |
. . . . . 6
โข (๐ด โ โ*
โ (๐ด
ยทe 0) = 0) |
90 | 89 | 3ad2ant1 1133 |
. . . . 5
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ด ยทe 0) =
0) |
91 | 88, 90 | sylan9eqr 2794 |
. . . 4
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (๐ด ยทe ๐ต) = 0) |
92 | 91 | oveq1d 7420 |
. . 3
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = (0 +๐ (๐ด ยทe ๐ถ))) |
93 | | oveq1 7412 |
. . . . . 6
โข (0 =
๐ต โ (0
+๐ ๐ถ) =
(๐ต +๐
๐ถ)) |
94 | 93 | eqcomd 2738 |
. . . . 5
โข (0 =
๐ต โ (๐ต +๐ ๐ถ) = (0 +๐ ๐ถ)) |
95 | | xaddlid 13217 |
. . . . . 6
โข (๐ถ โ โ*
โ (0 +๐ ๐ถ) = ๐ถ) |
96 | 4, 95 | syl 17 |
. . . . 5
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (0
+๐ ๐ถ) =
๐ถ) |
97 | 94, 96 | sylan9eqr 2794 |
. . . 4
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (๐ต +๐ ๐ถ) = ๐ถ) |
98 | 97 | oveq2d 7421 |
. . 3
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe ๐ถ)) |
99 | 86, 92, 98 | 3eqtr4rd 2783 |
. 2
โข (((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โง 0 = ๐ต) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
100 | | simp2r 1200 |
. . 3
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ 0 โค ๐ต) |
101 | | xrleloe 13119 |
. . . 4
โข ((0
โ โ* โง ๐ต โ โ*) โ (0 โค
๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
102 | 32, 2, 101 | sylancr 587 |
. . 3
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (0 โค ๐ต โ (0 < ๐ต โจ 0 = ๐ต))) |
103 | 100, 102 | mpbid 231 |
. 2
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (0 < ๐ต โจ 0 = ๐ต)) |
104 | 80, 99, 103 | mpjaodan 957 |
1
โข ((๐ด โ โ*
โง (๐ต โ
โ* โง 0 โค ๐ต) โง (๐ถ โ โ* โง 0 โค
๐ถ)) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |