Step | Hyp | Ref
| Expression |
1 | | xneg0 13140 |
. . . . . . . . 9
โข
-๐0 = 0 |
2 | 1 | eqeq2i 2746 |
. . . . . . . 8
โข
(-๐๐ด = -๐0 โ
-๐๐ด =
0) |
3 | | 0xr 11210 |
. . . . . . . . 9
โข 0 โ
โ* |
4 | | xneg11 13143 |
. . . . . . . . 9
โข ((๐ด โ โ*
โง 0 โ โ*) โ (-๐๐ด = -๐0 โ
๐ด = 0)) |
5 | 3, 4 | mpan2 690 |
. . . . . . . 8
โข (๐ด โ โ*
โ (-๐๐ด = -๐0 โ ๐ด = 0)) |
6 | 2, 5 | bitr3id 285 |
. . . . . . 7
โข (๐ด โ โ*
โ (-๐๐ด = 0 โ ๐ด = 0)) |
7 | 6 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (-๐๐ด = 0 โ ๐ด = 0)) |
8 | 7 | orbi1d 916 |
. . . . 5
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((-๐๐ด = 0 โจ ๐ต = 0) โ (๐ด = 0 โจ ๐ต = 0))) |
9 | 8 | ifbid 4513 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ if((-๐๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)))) = if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))))) |
10 | | xnegpnf 13137 |
. . . . . . . . . . . . . 14
โข
-๐+โ = -โ |
11 | 10 | eqeq2i 2746 |
. . . . . . . . . . . . 13
โข
(-๐๐ด = -๐+โ โ
-๐๐ด =
-โ) |
12 | | simpll 766 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ๐ด โ
โ*) |
13 | | pnfxr 11217 |
. . . . . . . . . . . . . 14
โข +โ
โ โ* |
14 | | xneg11 13143 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ*
โง +โ โ โ*) โ (-๐๐ด = -๐+โ
โ ๐ด =
+โ)) |
15 | 12, 13, 14 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (-๐๐ด = -๐+โ
โ ๐ด =
+โ)) |
16 | 11, 15 | bitr3id 285 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (-๐๐ด = -โ โ ๐ด = +โ)) |
17 | 16 | anbi2d 630 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((0 < ๐ต โง -๐๐ด = -โ) โ (0 <
๐ต โง ๐ด = +โ))) |
18 | | xnegmnf 13138 |
. . . . . . . . . . . . . 14
โข
-๐-โ = +โ |
19 | 18 | eqeq2i 2746 |
. . . . . . . . . . . . 13
โข
(-๐๐ด = -๐-โ โ
-๐๐ด =
+โ) |
20 | | mnfxr 11220 |
. . . . . . . . . . . . . 14
โข -โ
โ โ* |
21 | | xneg11 13143 |
. . . . . . . . . . . . . 14
โข ((๐ด โ โ*
โง -โ โ โ*) โ (-๐๐ด = -๐-โ
โ ๐ด =
-โ)) |
22 | 12, 20, 21 | sylancl 587 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (-๐๐ด = -๐-โ
โ ๐ด =
-โ)) |
23 | 19, 22 | bitr3id 285 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (-๐๐ด = +โ โ ๐ด = -โ)) |
24 | 23 | anbi2d 630 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((๐ต < 0 โง -๐๐ด = +โ) โ (๐ต < 0 โง ๐ด = -โ))) |
25 | 17, 24 | orbi12d 918 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โ ((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)))) |
26 | | xlt0neg1 13147 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ*
โ (๐ด < 0 โ 0
< -๐๐ด)) |
27 | 26 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (๐ด < 0 โ 0 <
-๐๐ด)) |
28 | 27 | bicomd 222 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (0 <
-๐๐ด
โ ๐ด <
0)) |
29 | 28 | anbi1d 631 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((0 <
-๐๐ด
โง ๐ต = -โ) โ
(๐ด < 0 โง ๐ต = -โ))) |
30 | | xlt0neg2 13148 |
. . . . . . . . . . . . . . 15
โข (๐ด โ โ*
โ (0 < ๐ด โ
-๐๐ด <
0)) |
31 | 30 | ad2antrr 725 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (0 < ๐ด โ -๐๐ด < 0)) |
32 | 31 | bicomd 222 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (-๐๐ด < 0 โ 0 < ๐ด)) |
33 | 32 | anbi1d 631 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((-๐๐ด < 0 โง ๐ต = +โ) โ (0 < ๐ด โง ๐ต = +โ))) |
34 | 29, 33 | orbi12d 918 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต = +โ))
โ ((๐ด < 0 โง
๐ต = -โ) โจ (0 <
๐ด โง ๐ต = +โ)))) |
35 | | orcom 869 |
. . . . . . . . . . 11
โข (((๐ด < 0 โง ๐ต = -โ) โจ (0 < ๐ด โง ๐ต = +โ)) โ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) |
36 | 34, 35 | bitrdi 287 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต = +โ))
โ ((0 < ๐ด โง
๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) |
37 | 25, 36 | orbi12d 918 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))) โ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))))) |
38 | 37 | biimpar 479 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ (((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ)))) |
39 | 38 | iftrued 4498 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)) = -โ) |
40 | | xmullem2 13193 |
. . . . . . . . . . 11
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ ((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))))) |
41 | 40 | adantr 482 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))))) |
42 | 23 | anbi2d 630 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((0 < ๐ต โง -๐๐ด = +โ) โ (0 <
๐ต โง ๐ด = -โ))) |
43 | 16 | anbi2d 630 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((๐ต < 0 โง -๐๐ด = -โ) โ (๐ต < 0 โง ๐ด = +โ))) |
44 | 42, 43 | orbi12d 918 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โ ((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)))) |
45 | 28 | anbi1d 631 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((0 <
-๐๐ด
โง ๐ต = +โ) โ
(๐ด < 0 โง ๐ต = +โ))) |
46 | 32 | anbi1d 631 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((-๐๐ด < 0 โง ๐ต = -โ) โ (0 < ๐ด โง ๐ต = -โ))) |
47 | 45, 46 | orbi12d 918 |
. . . . . . . . . . . . 13
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต = -โ))
โ ((๐ด < 0 โง
๐ต = +โ) โจ (0 <
๐ด โง ๐ต = -โ)))) |
48 | | orcom 869 |
. . . . . . . . . . . . 13
โข (((๐ด < 0 โง ๐ต = +โ) โจ (0 < ๐ด โง ๐ต = -โ)) โ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) |
49 | 47, 48 | bitrdi 287 |
. . . . . . . . . . . 12
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต = -โ))
โ ((0 < ๐ด โง
๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) |
50 | 44, 49 | orbi12d 918 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))) โ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))))) |
51 | 50 | notbid 318 |
. . . . . . . . . 10
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (ยฌ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))) โ ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))))) |
52 | 41, 51 | sylibrd 259 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))))) |
53 | 52 | imp 408 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ)))) |
54 | 53 | iffalsed 4501 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) |
55 | | iftrue 4496 |
. . . . . . . . . 10
โข ((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = +โ) |
56 | 55 | adantl 483 |
. . . . . . . . 9
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = +โ) |
57 | | xnegeq 13135 |
. . . . . . . . 9
โข (if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = +โ โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) =
-๐+โ) |
58 | 56, 57 | syl 17 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) =
-๐+โ) |
59 | 58, 10 | eqtrdi 2789 |
. . . . . . 7
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = -โ) |
60 | 39, 54, 59 | 3eqtr4d 2783 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
61 | 50 | biimpar 479 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ)))) |
62 | 61 | iftrued 4498 |
. . . . . . . . 9
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = +โ) |
63 | 41 | con2d 134 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))))) |
64 | 63 | imp 408 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) |
65 | 64 | iffalsed 4501 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) |
66 | | iftrue 4496 |
. . . . . . . . . . . . 13
โข ((((0
< ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)) = -โ) |
67 | 66 | adantl 483 |
. . . . . . . . . . . 12
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)) = -โ) |
68 | 65, 67 | eqtrd 2773 |
. . . . . . . . . . 11
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = -โ) |
69 | | xnegeq 13135 |
. . . . . . . . . . 11
โข (if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = -โ โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) =
-๐-โ) |
70 | 68, 69 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) =
-๐-โ) |
71 | 70, 18 | eqtrdi 2789 |
. . . . . . . . 9
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = +โ) |
72 | 62, 71 | eqtr4d 2776 |
. . . . . . . 8
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
73 | 72 | adantlr 714 |
. . . . . . 7
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
74 | 37 | notbid 318 |
. . . . . . . . . . 11
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ (ยฌ (((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))) โ ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))))) |
75 | 74 | biimpar 479 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ)))) |
76 | 75 | adantr 482 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ)))) |
77 | 76 | iffalsed 4501 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
-โ) โจ (๐ต < 0
โง -๐๐ด = +โ)) โจ ((0 <
-๐๐ด
โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)) = (-๐๐ด ยท ๐ต)) |
78 | 51 | biimpar 479 |
. . . . . . . . . 10
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ)))) |
79 | 78 | adantlr 714 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ยฌ (((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ)))) |
80 | 79 | iffalsed 4501 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) |
81 | | iffalse 4499 |
. . . . . . . . . . . 12
โข (ยฌ
(((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) |
82 | 81 | ad2antlr 726 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) |
83 | | iffalse 4499 |
. . . . . . . . . . . 12
โข (ยฌ
(((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)) = (๐ด ยท ๐ต)) |
84 | 83 | adantl 483 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)) = (๐ด ยท ๐ต)) |
85 | 82, 84 | eqtrd 2773 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = (๐ด ยท ๐ต)) |
86 | | xnegeq 13135 |
. . . . . . . . . 10
โข (if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = (๐ด ยท ๐ต) โ -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = -๐(๐ด ยท ๐ต)) |
87 | 85, 86 | syl 17 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = -๐(๐ด ยท ๐ต)) |
88 | | xmullem 13192 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ๐ด โ โ) |
89 | 88 | recnd 11191 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ๐ด โ โ) |
90 | | ancom 462 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ต โ โ* โง ๐ด โ
โ*)) |
91 | | orcom 869 |
. . . . . . . . . . . . . . . 16
โข ((๐ด = 0 โจ ๐ต = 0) โ (๐ต = 0 โจ ๐ด = 0)) |
92 | 91 | notbii 320 |
. . . . . . . . . . . . . . 15
โข (ยฌ
(๐ด = 0 โจ ๐ต = 0) โ ยฌ (๐ต = 0 โจ ๐ด = 0)) |
93 | 90, 92 | anbi12i 628 |
. . . . . . . . . . . . . 14
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ ((๐ต โ โ* โง ๐ด โ โ*)
โง ยฌ (๐ต = 0 โจ
๐ด = 0))) |
94 | | orcom 869 |
. . . . . . . . . . . . . . 15
โข ((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ (((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)) โจ ((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)))) |
95 | 94 | notbii 320 |
. . . . . . . . . . . . . 14
โข (ยฌ
(((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ ยฌ (((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)) โจ ((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)))) |
96 | 93, 95 | anbi12i 628 |
. . . . . . . . . . . . 13
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ (((๐ต โ โ* โง ๐ด โ โ*)
โง ยฌ (๐ต = 0 โจ
๐ด = 0)) โง ยฌ (((0
< ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)) โจ ((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ))))) |
97 | | orcom 869 |
. . . . . . . . . . . . . 14
โข ((((0
< ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ (((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)) โจ ((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)))) |
98 | 97 | notbii 320 |
. . . . . . . . . . . . 13
โข (ยฌ
(((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ ยฌ (((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)) โจ ((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)))) |
99 | | xmullem 13192 |
. . . . . . . . . . . . 13
โข
(((((๐ต โ
โ* โง ๐ด
โ โ*) โง ยฌ (๐ต = 0 โจ ๐ด = 0)) โง ยฌ (((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)) โจ ((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)))) โง ยฌ (((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)) โจ ((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)))) โ ๐ต โ โ) |
100 | 96, 98, 99 | syl2anb 599 |
. . . . . . . . . . . 12
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ๐ต โ โ) |
101 | 100 | recnd 11191 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ ๐ต โ โ) |
102 | 89, 101 | mulneg1d 11616 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ (-๐ด ยท ๐ต) = -(๐ด ยท ๐ต)) |
103 | | rexneg 13139 |
. . . . . . . . . . . 12
โข (๐ด โ โ โ
-๐๐ด =
-๐ด) |
104 | 88, 103 | syl 17 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐๐ด =
-๐ด) |
105 | 104 | oveq1d 7376 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
(-๐๐ด
ยท ๐ต) = (-๐ด ยท ๐ต)) |
106 | 88, 100 | remulcld 11193 |
. . . . . . . . . . 11
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ (๐ด ยท ๐ต) โ โ) |
107 | | rexneg 13139 |
. . . . . . . . . . 11
โข ((๐ด ยท ๐ต) โ โ โ
-๐(๐ด
ยท ๐ต) = -(๐ด ยท ๐ต)) |
108 | 106, 107 | syl 17 |
. . . . . . . . . 10
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐(๐ด
ยท ๐ต) = -(๐ด ยท ๐ต)) |
109 | 102, 105,
108 | 3eqtr4d 2783 |
. . . . . . . . 9
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
(-๐๐ด
ยท ๐ต) =
-๐(๐ด
ยท ๐ต)) |
110 | 87, 109 | eqtr4d 2776 |
. . . . . . . 8
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ
-๐if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = (-๐๐ด ยท ๐ต)) |
111 | 77, 80, 110 | 3eqtr4d 2783 |
. . . . . . 7
โข
(((((๐ด โ
โ* โง ๐ต
โ โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โง ยฌ (((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
112 | 73, 111 | pm2.61dan 812 |
. . . . . 6
โข ((((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โง ยฌ (((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) โ if((((0 < ๐ต โง
-๐๐ด =
+โ) โจ (๐ต < 0
โง -๐๐ด = -โ)) โจ ((0 <
-๐๐ด
โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
113 | 60, 112 | pm2.61dan 812 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ
โ*) โง ยฌ (๐ด = 0 โจ ๐ต = 0)) โ if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
114 | 113 | ifeq2da 4522 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)))) = if((๐ด = 0 โจ ๐ต = 0), 0, -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
115 | 9, 114 | eqtrd 2773 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ if((-๐๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)))) = if((๐ด = 0 โจ ๐ต = 0), 0, -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
116 | | xnegeq 13135 |
. . . . 5
โข
(if((๐ด = 0 โจ
๐ต = 0), 0, if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = 0 โ
-๐if((๐ด
= 0 โจ ๐ต = 0), 0, if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) =
-๐0) |
117 | 116, 1 | eqtrdi 2789 |
. . . 4
โข
(if((๐ด = 0 โจ
๐ต = 0), 0, if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = 0 โ
-๐if((๐ด
= 0 โจ ๐ต = 0), 0, if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = 0) |
118 | | xnegeq 13135 |
. . . 4
โข
(if((๐ด = 0 โจ
๐ต = 0), 0, if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) โ -๐if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
119 | 117, 118 | ifsb 4503 |
. . 3
โข
-๐if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = if((๐ด = 0 โจ ๐ต = 0), 0, -๐if((((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) |
120 | 115, 119 | eqtr4di 2791 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ if((-๐๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต)))) = -๐if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
121 | | xnegcl 13141 |
. . 3
โข (๐ด โ โ*
โ -๐๐ด โ
โ*) |
122 | | xmulval 13153 |
. . 3
โข
((-๐๐ด โ โ* โง ๐ต โ โ*)
โ (-๐๐ด ยทe ๐ต) = if((-๐๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))))) |
123 | 121, 122 | sylan 581 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (-๐๐ด ยทe ๐ต) = if((-๐๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง -๐๐ด = +โ) โจ (๐ต < 0 โง
-๐๐ด =
-โ)) โจ ((0 < -๐๐ด โง ๐ต = +โ) โจ
(-๐๐ด
< 0 โง ๐ต =
-โ))), +โ, if((((0 < ๐ต โง -๐๐ด = -โ) โจ (๐ต < 0 โง
-๐๐ด =
+โ)) โจ ((0 < -๐๐ด โง ๐ต = -โ) โจ
(-๐๐ด
< 0 โง ๐ต =
+โ))), -โ, (-๐๐ด ยท ๐ต))))) |
124 | | xmulval 13153 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) = if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
125 | | xnegeq 13135 |
. . 3
โข ((๐ด ยทe ๐ต) = if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) โ -๐(๐ด ยทe ๐ต) =
-๐if((๐ด
= 0 โจ ๐ต = 0), 0, if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
126 | 124, 125 | syl 17 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ -๐(๐ด ยทe ๐ต) = -๐if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
127 | 120, 123,
126 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (-๐๐ด ยทe ๐ต) = -๐(๐ด ยทe ๐ต)) |