Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ๐ด โ โ) |
2 | | recn 11149 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
3 | | recn 11149 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
4 | | recn 11149 |
. . . . . . . 8
โข (๐ถ โ โ โ ๐ถ โ
โ) |
5 | | adddi 11148 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |
6 | 2, 3, 4, 5 | syl3an 1161 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |
7 | 6 | 3expa 1119 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยท (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |
8 | | readdcl 11142 |
. . . . . . . 8
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต + ๐ถ) โ โ) |
9 | | rexmul 13199 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ต + ๐ถ) โ โ) โ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ))) |
10 | 8, 9 | sylan2 594 |
. . . . . . 7
โข ((๐ด โ โ โง (๐ต โ โ โง ๐ถ โ โ)) โ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ))) |
11 | 10 | anassrs 469 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต + ๐ถ)) = (๐ด ยท (๐ต + ๐ถ))) |
12 | | remulcl 11144 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
13 | 12 | adantr 482 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยท ๐ต) โ โ) |
14 | | remulcl 11144 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
15 | 14 | adantlr 714 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
16 | 13, 15 | rexaddd 13162 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) +๐ (๐ด ยท ๐ถ)) = ((๐ด ยท ๐ต) + (๐ด ยท ๐ถ))) |
17 | 7, 11, 16 | 3eqtr4d 2783 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต + ๐ถ)) = ((๐ด ยท ๐ต) +๐ (๐ด ยท ๐ถ))) |
18 | | rexadd 13160 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต +๐ ๐ถ) = (๐ต + ๐ถ)) |
19 | 18 | adantll 713 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ต +๐ ๐ถ) = (๐ต + ๐ถ)) |
20 | 19 | oveq2d 7377 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe (๐ต + ๐ถ))) |
21 | | rexmul 13199 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
22 | 21 | adantr 482 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |
23 | | rexmul 13199 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ)) |
24 | 23 | adantlr 714 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) = (๐ด ยท ๐ถ)) |
25 | 22, 24 | oveq12d 7379 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยท ๐ต) +๐ (๐ด ยท ๐ถ))) |
26 | 17, 20, 25 | 3eqtr4d 2783 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
27 | 1, 26 | sylanl1 679 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
28 | | rexr 11209 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ*) |
29 | 28 | 3ad2ant1 1134 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โ ๐ด โ
โ*) |
30 | | xmulpnf1 13202 |
. . . . . . . 8
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |
31 | 29, 30 | sylan 581 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ด ยทe +โ) =
+โ) |
32 | 31 | adantr 482 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ด ยทe +โ) =
+โ) |
33 | 21, 12 | eqeltrd 2834 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) โ
โ) |
34 | 1, 33 | sylan 581 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ด ยทe ๐ต) โ โ) |
35 | | rexr 11209 |
. . . . . . . 8
โข ((๐ด ยทe ๐ต) โ โ โ (๐ด ยทe ๐ต) โ
โ*) |
36 | | renemnf 11212 |
. . . . . . . 8
โข ((๐ด ยทe ๐ต) โ โ โ (๐ด ยทe ๐ต) โ
-โ) |
37 | | xaddpnf1 13154 |
. . . . . . . 8
โข (((๐ด ยทe ๐ต) โ โ*
โง (๐ด
ยทe ๐ต)
โ -โ) โ ((๐ด
ยทe ๐ต)
+๐ +โ) = +โ) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . 7
โข ((๐ด ยทe ๐ต) โ โ โ ((๐ด ยทe ๐ต) +๐
+โ) = +โ) |
39 | 34, 38 | syl 17 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ ((๐ด ยทe ๐ต) +๐ +โ) =
+โ) |
40 | 32, 39 | eqtr4d 2776 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ด ยทe +โ) = ((๐ด ยทe ๐ต) +๐
+โ)) |
41 | 40 | adantr 482 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ (๐ด ยทe +โ) = ((๐ด ยทe ๐ต) +๐
+โ)) |
42 | | oveq2 7369 |
. . . . . 6
โข (๐ถ = +โ โ (๐ต +๐ ๐ถ) = (๐ต +๐
+โ)) |
43 | | rexr 11209 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ*) |
44 | | renemnf 11212 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ -โ) |
45 | | xaddpnf1 13154 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ต โ -โ)
โ (๐ต
+๐ +โ) = +โ) |
46 | 43, 44, 45 | syl2anc 585 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต +๐ +โ)
= +โ) |
47 | 46 | adantl 483 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ต +๐ +โ) =
+โ) |
48 | 42, 47 | sylan9eqr 2795 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ (๐ต +๐ ๐ถ) = +โ) |
49 | 48 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
+โ)) |
50 | | oveq2 7369 |
. . . . . 6
โข (๐ถ = +โ โ (๐ด ยทe ๐ถ) = (๐ด ยทe
+โ)) |
51 | 50, 32 | sylan9eqr 2795 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ (๐ด ยทe ๐ถ) = +โ) |
52 | 51 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐
+โ)) |
53 | 41, 49, 52 | 3eqtr4d 2783 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
54 | | xmulmnf1 13204 |
. . . . . . . 8
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
-โ) = -โ) |
55 | 29, 54 | sylan 581 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ด ยทe -โ) =
-โ) |
56 | 55 | adantr 482 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ด ยทe -โ) =
-โ) |
57 | 56 | adantr 482 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe -โ) =
-โ) |
58 | 34 | adantr 482 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe ๐ต) โ โ) |
59 | | renepnf 11211 |
. . . . . . 7
โข ((๐ด ยทe ๐ต) โ โ โ (๐ด ยทe ๐ต) โ
+โ) |
60 | | xaddmnf1 13156 |
. . . . . . 7
โข (((๐ด ยทe ๐ต) โ โ*
โง (๐ด
ยทe ๐ต)
โ +โ) โ ((๐ด
ยทe ๐ต)
+๐ -โ) = -โ) |
61 | 35, 59, 60 | syl2anc 585 |
. . . . . 6
โข ((๐ด ยทe ๐ต) โ โ โ ((๐ด ยทe ๐ต) +๐
-โ) = -โ) |
62 | 58, 61 | syl 17 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ -โ) =
-โ) |
63 | 57, 62 | eqtr4d 2776 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe -โ) = ((๐ด ยทe ๐ต) +๐
-โ)) |
64 | | oveq2 7369 |
. . . . . 6
โข (๐ถ = -โ โ (๐ต +๐ ๐ถ) = (๐ต +๐
-โ)) |
65 | | renepnf 11211 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ +โ) |
66 | | xaddmnf1 13156 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ต โ +โ)
โ (๐ต
+๐ -โ) = -โ) |
67 | 43, 65, 66 | syl2anc 585 |
. . . . . . 7
โข (๐ต โ โ โ (๐ต +๐ -โ)
= -โ) |
68 | 67 | adantl 483 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ต +๐ -โ) =
-โ) |
69 | 64, 68 | sylan9eqr 2795 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ต +๐ ๐ถ) = -โ) |
70 | 69 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
-โ)) |
71 | | oveq2 7369 |
. . . . . 6
โข (๐ถ = -โ โ (๐ด ยทe ๐ถ) = (๐ด ยทe
-โ)) |
72 | 71, 56 | sylan9eqr 2795 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe ๐ถ) = -โ) |
73 | 72 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe ๐ต) +๐
-โ)) |
74 | 63, 70, 73 | 3eqtr4d 2783 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต โ โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
75 | | simpl3 1194 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ๐ถ โ
โ*) |
76 | | elxr 13045 |
. . . . 5
โข (๐ถ โ โ*
โ (๐ถ โ โ
โจ ๐ถ = +โ โจ
๐ถ =
-โ)) |
77 | 75, 76 | sylib 217 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
78 | 77 | adantr 482 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
79 | 27, 53, 74, 78 | mpjao3dan 1432 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
80 | 31 | ad2antrr 725 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe +โ) =
+โ) |
81 | 1 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ ๐ด โ โ) |
82 | 23, 14 | eqeltrd 2834 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) โ
โ) |
83 | 81, 82 | sylan 581 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) โ โ) |
84 | | rexr 11209 |
. . . . . . 7
โข ((๐ด ยทe ๐ถ) โ โ โ (๐ด ยทe ๐ถ) โ
โ*) |
85 | | renemnf 11212 |
. . . . . . 7
โข ((๐ด ยทe ๐ถ) โ โ โ (๐ด ยทe ๐ถ) โ
-โ) |
86 | | xaddpnf2 13155 |
. . . . . . 7
โข (((๐ด ยทe ๐ถ) โ โ*
โง (๐ด
ยทe ๐ถ)
โ -โ) โ (+โ +๐ (๐ด ยทe ๐ถ)) = +โ) |
87 | 84, 85, 86 | syl2anc 585 |
. . . . . 6
โข ((๐ด ยทe ๐ถ) โ โ โ
(+โ +๐ (๐ด ยทe ๐ถ)) = +โ) |
88 | 83, 87 | syl 17 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (+โ
+๐ (๐ด
ยทe ๐ถ)) =
+โ) |
89 | 80, 88 | eqtr4d 2776 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe +โ) = (+โ
+๐ (๐ด
ยทe ๐ถ))) |
90 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ ๐ต = +โ) |
91 | 90 | oveq1d 7376 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ (๐ต +๐ ๐ถ) = (+โ +๐ ๐ถ)) |
92 | | rexr 11209 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โ*) |
93 | | renemnf 11212 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ -โ) |
94 | | xaddpnf2 13155 |
. . . . . . 7
โข ((๐ถ โ โ*
โง ๐ถ โ -โ)
โ (+โ +๐ ๐ถ) = +โ) |
95 | 92, 93, 94 | syl2anc 585 |
. . . . . 6
โข (๐ถ โ โ โ (+โ
+๐ ๐ถ) =
+โ) |
96 | 91, 95 | sylan9eq 2793 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ต +๐ ๐ถ) = +โ) |
97 | 96 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
+โ)) |
98 | | oveq2 7369 |
. . . . . . 7
โข (๐ต = +โ โ (๐ด ยทe ๐ต) = (๐ด ยทe
+โ)) |
99 | 98, 31 | sylan9eqr 2795 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ (๐ด ยทe ๐ต) = +โ) |
100 | 99 | adantr 482 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ต) = +โ) |
101 | 100 | oveq1d 7376 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = (+โ +๐ (๐ด ยทe ๐ถ))) |
102 | 89, 97, 101 | 3eqtr4d 2783 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
103 | | pnfxr 11217 |
. . . . . . 7
โข +โ
โ โ* |
104 | | pnfnemnf 11218 |
. . . . . . 7
โข +โ
โ -โ |
105 | | xaddpnf1 13154 |
. . . . . . 7
โข
((+โ โ โ* โง +โ โ -โ)
โ (+โ +๐ +โ) = +โ) |
106 | 103, 104,
105 | mp2an 691 |
. . . . . 6
โข (+โ
+๐ +โ) = +โ |
107 | 31, 31 | oveq12d 7379 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe +โ)) = (+โ +๐
+โ)) |
108 | 106, 107,
31 | 3eqtr4a 2799 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe +โ)) = (๐ด ยทe
+โ)) |
109 | 108 | ad2antrr 725 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = +โ) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe +โ)) = (๐ด ยทe
+โ)) |
110 | 98, 50 | oveqan12d 7380 |
. . . . 5
โข ((๐ต = +โ โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โ)
+๐ (๐ด
ยทe +โ))) |
111 | 110 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โ)
+๐ (๐ด
ยทe +โ))) |
112 | | oveq12 7370 |
. . . . . . 7
โข ((๐ต = +โ โง ๐ถ = +โ) โ (๐ต +๐ ๐ถ) = (+โ
+๐ +โ)) |
113 | 112, 106 | eqtrdi 2789 |
. . . . . 6
โข ((๐ต = +โ โง ๐ถ = +โ) โ (๐ต +๐ ๐ถ) = +โ) |
114 | 113 | oveq2d 7377 |
. . . . 5
โข ((๐ต = +โ โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
+โ)) |
115 | 114 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
+โ)) |
116 | 109, 111,
115 | 3eqtr4rd 2784 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
117 | | pnfaddmnf 13158 |
. . . . . 6
โข (+โ
+๐ -โ) = 0 |
118 | 31, 55 | oveq12d 7379 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe -โ)) = (+โ +๐
-โ)) |
119 | | xmul01 13195 |
. . . . . . 7
โข (๐ด โ โ*
โ (๐ด
ยทe 0) = 0) |
120 | 1, 28, 119 | 3syl 18 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ด ยทe 0) =
0) |
121 | 117, 118,
120 | 3eqtr4a 2799 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe -โ)) = (๐ด ยทe 0)) |
122 | 121 | ad2antrr 725 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = -โ) โ ((๐ด ยทe +โ)
+๐ (๐ด
ยทe -โ)) = (๐ด ยทe 0)) |
123 | 98, 71 | oveqan12d 7380 |
. . . . 5
โข ((๐ต = +โ โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โ)
+๐ (๐ด
ยทe -โ))) |
124 | 123 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe +โ)
+๐ (๐ด
ยทe -โ))) |
125 | | oveq12 7370 |
. . . . . . 7
โข ((๐ต = +โ โง ๐ถ = -โ) โ (๐ต +๐ ๐ถ) = (+โ
+๐ -โ)) |
126 | 125, 117 | eqtrdi 2789 |
. . . . . 6
โข ((๐ต = +โ โง ๐ถ = -โ) โ (๐ต +๐ ๐ถ) = 0) |
127 | 126 | oveq2d 7377 |
. . . . 5
โข ((๐ต = +โ โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe 0)) |
128 | 127 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe 0)) |
129 | 122, 124,
128 | 3eqtr4rd 2784 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = +โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
130 | 77 | adantr 482 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
131 | 102, 116,
129, 130 | mpjao3dan 1432 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
132 | 55 | ad2antrr 725 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe -โ) =
-โ) |
133 | 1 | adantr 482 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ ๐ด โ โ) |
134 | 133, 82 | sylan 581 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ถ) โ โ) |
135 | | renepnf 11211 |
. . . . . . 7
โข ((๐ด ยทe ๐ถ) โ โ โ (๐ด ยทe ๐ถ) โ
+โ) |
136 | | xaddmnf2 13157 |
. . . . . . 7
โข (((๐ด ยทe ๐ถ) โ โ*
โง (๐ด
ยทe ๐ถ)
โ +โ) โ (-โ +๐ (๐ด ยทe ๐ถ)) = -โ) |
137 | 84, 135, 136 | syl2anc 585 |
. . . . . 6
โข ((๐ด ยทe ๐ถ) โ โ โ
(-โ +๐ (๐ด ยทe ๐ถ)) = -โ) |
138 | 134, 137 | syl 17 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (-โ
+๐ (๐ด
ยทe ๐ถ)) =
-โ) |
139 | 132, 138 | eqtr4d 2776 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe -โ) = (-โ
+๐ (๐ด
ยทe ๐ถ))) |
140 | | simpr 486 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ ๐ต = -โ) |
141 | 140 | oveq1d 7376 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ (๐ต +๐ ๐ถ) = (-โ +๐ ๐ถ)) |
142 | | renepnf 11211 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ +โ) |
143 | | xaddmnf2 13157 |
. . . . . . 7
โข ((๐ถ โ โ*
โง ๐ถ โ +โ)
โ (-โ +๐ ๐ถ) = -โ) |
144 | 92, 142, 143 | syl2anc 585 |
. . . . . 6
โข (๐ถ โ โ โ (-โ
+๐ ๐ถ) =
-โ) |
145 | 141, 144 | sylan9eq 2793 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ต +๐ ๐ถ) = -โ) |
146 | 145 | oveq2d 7377 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
-โ)) |
147 | | oveq2 7369 |
. . . . . . 7
โข (๐ต = -โ โ (๐ด ยทe ๐ต) = (๐ด ยทe
-โ)) |
148 | 147, 55 | sylan9eqr 2795 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ (๐ด ยทe ๐ต) = -โ) |
149 | 148 | adantr 482 |
. . . . 5
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe ๐ต) = -โ) |
150 | 149 | oveq1d 7376 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = (-โ +๐ (๐ด ยทe ๐ถ))) |
151 | 139, 146,
150 | 3eqtr4d 2783 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ โ โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
152 | 55, 31 | oveq12d 7379 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ)) = (-โ +๐
+โ)) |
153 | | mnfaddpnf 13159 |
. . . . . . 7
โข (-โ
+๐ +โ) = 0 |
154 | 152, 153 | eqtrdi 2789 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ)) = 0) |
155 | 120, 154 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ด ยทe 0) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ))) |
156 | 155 | ad2antrr 725 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = +โ) โ (๐ด ยทe 0) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ))) |
157 | | oveq12 7370 |
. . . . . . 7
โข ((๐ต = -โ โง ๐ถ = +โ) โ (๐ต +๐ ๐ถ) = (-โ
+๐ +โ)) |
158 | 157, 153 | eqtrdi 2789 |
. . . . . 6
โข ((๐ต = -โ โง ๐ถ = +โ) โ (๐ต +๐ ๐ถ) = 0) |
159 | 158 | oveq2d 7377 |
. . . . 5
โข ((๐ต = -โ โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe 0)) |
160 | 159 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe 0)) |
161 | 147, 50 | oveqan12d 7380 |
. . . . 5
โข ((๐ต = -โ โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ))) |
162 | 161 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = +โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe +โ))) |
163 | 156, 160,
162 | 3eqtr4d 2783 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = +โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
164 | | mnfxr 11220 |
. . . . . . 7
โข -โ
โ โ* |
165 | | mnfnepnf 11219 |
. . . . . . 7
โข -โ
โ +โ |
166 | | xaddmnf1 13156 |
. . . . . . 7
โข
((-โ โ โ* โง -โ โ +โ)
โ (-โ +๐ -โ) = -โ) |
167 | 164, 165,
166 | mp2an 691 |
. . . . . 6
โข (-โ
+๐ -โ) = -โ |
168 | 55, 55 | oveq12d 7379 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe -โ)
+๐ (๐ด
ยทe -โ)) = (-โ +๐
-โ)) |
169 | 167, 168,
55 | 3eqtr4a 2799 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ((๐ด ยทe -โ)
+๐ (๐ด
ยทe -โ)) = (๐ด ยทe
-โ)) |
170 | 169 | ad2antrr 725 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = -โ) โ ((๐ด ยทe -โ)
+๐ (๐ด
ยทe -โ)) = (๐ด ยทe
-โ)) |
171 | 147, 71 | oveqan12d 7380 |
. . . . 5
โข ((๐ต = -โ โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe -โ))) |
172 | 171 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = -โ) โ ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ)) = ((๐ด ยทe -โ)
+๐ (๐ด
ยทe -โ))) |
173 | | oveq12 7370 |
. . . . . . 7
โข ((๐ต = -โ โง ๐ถ = -โ) โ (๐ต +๐ ๐ถ) = (-โ
+๐ -โ)) |
174 | 173, 167 | eqtrdi 2789 |
. . . . . 6
โข ((๐ต = -โ โง ๐ถ = -โ) โ (๐ต +๐ ๐ถ) = -โ) |
175 | 174 | oveq2d 7377 |
. . . . 5
โข ((๐ต = -โ โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
-โ)) |
176 | 175 | adantll 713 |
. . . 4
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = (๐ด ยทe
-โ)) |
177 | 170, 172,
176 | 3eqtr4rd 2784 |
. . 3
โข
(((((๐ด โ
โ โง ๐ต โ
โ* โง ๐ถ
โ โ*) โง 0 < ๐ด) โง ๐ต = -โ) โง ๐ถ = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
178 | 77 | adantr 482 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ (๐ถ โ โ โจ ๐ถ = +โ โจ ๐ถ = -โ)) |
179 | 151, 163,
177, 178 | mpjao3dan 1432 |
. 2
โข ((((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โง ๐ต = -โ) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |
180 | | simpl2 1193 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ ๐ต โ
โ*) |
181 | | elxr 13045 |
. . 3
โข (๐ต โ โ*
โ (๐ต โ โ
โจ ๐ต = +โ โจ
๐ต =
-โ)) |
182 | 180, 181 | sylib 217 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ต โ โ โจ ๐ต = +โ โจ ๐ต = -โ)) |
183 | 79, 131, 179, 182 | mpjao3dan 1432 |
1
โข (((๐ด โ โ โง ๐ต โ โ*
โง ๐ถ โ
โ*) โง 0 < ๐ด) โ (๐ด ยทe (๐ต +๐ ๐ถ)) = ((๐ด ยทe ๐ต) +๐ (๐ด ยทe ๐ถ))) |