Step | Hyp | Ref
| Expression |
1 | | renepnf 11211 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ +โ) |
2 | 1 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ +โ) |
3 | 2 | necon2bi 2971 |
. . . . . . . . 9
โข (๐ด = +โ โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
4 | 3 | adantl 483 |
. . . . . . . 8
โข ((0 <
๐ต โง ๐ด = +โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
5 | | renemnf 11212 |
. . . . . . . . . . 11
โข (๐ด โ โ โ ๐ด โ -โ) |
6 | 5 | adantr 482 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ด โ -โ) |
7 | 6 | necon2bi 2971 |
. . . . . . . . 9
โข (๐ด = -โ โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
8 | 7 | adantl 483 |
. . . . . . . 8
โข ((๐ต < 0 โง ๐ด = -โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
9 | 4, 8 | jaoi 856 |
. . . . . . 7
โข (((0 <
๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
10 | | renepnf 11211 |
. . . . . . . . . . 11
โข (๐ต โ โ โ ๐ต โ +โ) |
11 | 10 | adantl 483 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ +โ) |
12 | 11 | necon2bi 2971 |
. . . . . . . . 9
โข (๐ต = +โ โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
13 | 12 | adantl 483 |
. . . . . . . 8
โข ((0 <
๐ด โง ๐ต = +โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
14 | | renemnf 11212 |
. . . . . . . . . . 11
โข (๐ต โ โ โ ๐ต โ -โ) |
15 | 14 | adantl 483 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ) โ ๐ต โ -โ) |
16 | 15 | necon2bi 2971 |
. . . . . . . . 9
โข (๐ต = -โ โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
17 | 16 | adantl 483 |
. . . . . . . 8
โข ((๐ด < 0 โง ๐ต = -โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
18 | 13, 17 | jaoi 856 |
. . . . . . 7
โข (((0 <
๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
19 | 9, 18 | jaoi 856 |
. . . . . 6
โข ((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
20 | 19 | con2i 139 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ยฌ
(((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ)))) |
21 | 20 | iffalsed 4501 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) |
22 | 7 | adantl 483 |
. . . . . . . 8
โข ((0 <
๐ต โง ๐ด = -โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
23 | 3 | adantl 483 |
. . . . . . . 8
โข ((๐ต < 0 โง ๐ด = +โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
24 | 22, 23 | jaoi 856 |
. . . . . . 7
โข (((0 <
๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
25 | 16 | adantl 483 |
. . . . . . . 8
โข ((0 <
๐ด โง ๐ต = -โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
26 | 12 | adantl 483 |
. . . . . . . 8
โข ((๐ด < 0 โง ๐ต = +โ) โ ยฌ (๐ด โ โ โง ๐ต โ โ)) |
27 | 25, 26 | jaoi 856 |
. . . . . . 7
โข (((0 <
๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
28 | 24, 27 | jaoi 856 |
. . . . . 6
โข ((((0
< ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))) โ ยฌ (๐ด โ โ โง ๐ต โ
โ)) |
29 | 28 | con2i 139 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ยฌ
(((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ)))) |
30 | 29 | iffalsed 4501 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ if((((0
< ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)) = (๐ด ยท ๐ต)) |
31 | 21, 30 | eqtrd 2773 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ if((((0
< ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))) = (๐ด ยท ๐ต)) |
32 | 31 | ifeq2d 4510 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ
if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต)))) = if((๐ด = 0 โจ ๐ต = 0), 0, (๐ด ยท ๐ต))) |
33 | | rexr 11209 |
. . 3
โข (๐ด โ โ โ ๐ด โ
โ*) |
34 | | rexr 11209 |
. . 3
โข (๐ต โ โ โ ๐ต โ
โ*) |
35 | | xmulval 13153 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ
โ*) โ (๐ด ยทe ๐ต) = if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
36 | 33, 34, 35 | syl2an 597 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = if((๐ด = 0 โจ ๐ต = 0), 0, if((((0 < ๐ต โง ๐ด = +โ) โจ (๐ต < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง ๐ต = +โ) โจ (๐ด < 0 โง ๐ต = -โ))), +โ, if((((0 < ๐ต โง ๐ด = -โ) โจ (๐ต < 0 โง ๐ด = +โ)) โจ ((0 < ๐ด โง ๐ต = -โ) โจ (๐ด < 0 โง ๐ต = +โ))), -โ, (๐ด ยท ๐ต))))) |
37 | | ifid 4530 |
. . 3
โข if((๐ด = 0 โจ ๐ต = 0), (๐ด ยท ๐ต), (๐ด ยท ๐ต)) = (๐ด ยท ๐ต) |
38 | | oveq1 7368 |
. . . . . 6
โข (๐ด = 0 โ (๐ด ยท ๐ต) = (0 ยท ๐ต)) |
39 | | mul02lem2 11340 |
. . . . . . 7
โข (๐ต โ โ โ (0
ยท ๐ต) =
0) |
40 | 39 | adantl 483 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (0
ยท ๐ต) =
0) |
41 | 38, 40 | sylan9eqr 2795 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ด = 0) โ (๐ด ยท ๐ต) = 0) |
42 | | oveq2 7369 |
. . . . . 6
โข (๐ต = 0 โ (๐ด ยท ๐ต) = (๐ด ยท 0)) |
43 | | recn 11149 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
44 | 43 | mul01d 11362 |
. . . . . . 7
โข (๐ด โ โ โ (๐ด ยท 0) =
0) |
45 | 44 | adantr 482 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท 0) =
0) |
46 | 42, 45 | sylan9eqr 2795 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ต = 0) โ (๐ด ยท ๐ต) = 0) |
47 | 41, 46 | jaodan 957 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ด = 0 โจ ๐ต = 0)) โ (๐ด ยท ๐ต) = 0) |
48 | 47 | ifeq1da 4521 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ
if((๐ด = 0 โจ ๐ต = 0), (๐ด ยท ๐ต), (๐ด ยท ๐ต)) = if((๐ด = 0 โจ ๐ต = 0), 0, (๐ด ยท ๐ต))) |
49 | 37, 48 | eqtr3id 2787 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) = if((๐ด = 0 โจ ๐ต = 0), 0, (๐ด ยท ๐ต))) |
50 | 32, 36, 49 | 3eqtr4d 2783 |
1
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยทe ๐ต) = (๐ด ยท ๐ต)) |