Step | Hyp | Ref
| Expression |
1 | | pnfxr 11216 |
. . . 4
โข +โ
โ โ* |
2 | | xmulval 13151 |
. . . 4
โข ((๐ด โ โ*
โง +โ โ โ*) โ (๐ด ยทe +โ) = if((๐ด = 0 โจ +โ = 0), 0,
if((((0 < +โ โง ๐ด = +โ) โจ (+โ < 0 โง
๐ด = -โ)) โจ ((0
< ๐ด โง +โ =
+โ) โจ (๐ด < 0
โง +โ = -โ))), +โ, if((((0 < +โ โง ๐ด = -โ) โจ (+โ <
0 โง ๐ด = +โ)) โจ
((0 < ๐ด โง +โ =
-โ) โจ (๐ด < 0
โง +โ = +โ))), -โ, (๐ด ยท +โ))))) |
3 | 1, 2 | mpan2 690 |
. . 3
โข (๐ด โ โ*
โ (๐ด
ยทe +โ) = if((๐ด = 0 โจ +โ = 0), 0, if((((0 <
+โ โง ๐ด =
+โ) โจ (+โ < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง +โ = +โ) โจ
(๐ด < 0 โง +โ =
-โ))), +โ, if((((0 < +โ โง ๐ด = -โ) โจ (+โ < 0 โง
๐ด = +โ)) โจ ((0
< ๐ด โง +โ =
-โ) โจ (๐ด < 0
โง +โ = +โ))), -โ, (๐ด ยท +โ))))) |
4 | 3 | adantr 482 |
. 2
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = if((๐ด = 0 โจ
+โ = 0), 0, if((((0 < +โ โง ๐ด = +โ) โจ (+โ < 0 โง
๐ด = -โ)) โจ ((0
< ๐ด โง +โ =
+โ) โจ (๐ด < 0
โง +โ = -โ))), +โ, if((((0 < +โ โง ๐ด = -โ) โจ (+โ <
0 โง ๐ด = +โ)) โจ
((0 < ๐ด โง +โ =
-โ) โจ (๐ด < 0
โง +โ = +โ))), -โ, (๐ด ยท +โ))))) |
5 | | 0xr 11209 |
. . . . 5
โข 0 โ
โ* |
6 | | xrltne 13089 |
. . . . 5
โข ((0
โ โ* โง ๐ด โ โ* โง 0 <
๐ด) โ ๐ด โ 0) |
7 | 5, 6 | mp3an1 1449 |
. . . 4
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
๐ด โ 0) |
8 | | 0re 11164 |
. . . . . 6
โข 0 โ
โ |
9 | | renepnf 11210 |
. . . . . 6
โข (0 โ
โ โ 0 โ +โ) |
10 | 8, 9 | ax-mp 5 |
. . . . 5
โข 0 โ
+โ |
11 | 10 | necomi 2999 |
. . . 4
โข +โ
โ 0 |
12 | | neanior 3038 |
. . . 4
โข ((๐ด โ 0 โง +โ โ 0)
โ ยฌ (๐ด = 0 โจ
+โ = 0)) |
13 | 7, 11, 12 | sylanblc 590 |
. . 3
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
ยฌ (๐ด = 0 โจ +โ
= 0)) |
14 | 13 | iffalsed 4502 |
. 2
โข ((๐ด โ โ*
โง 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
โง +โ = +โ))), -โ, (๐ด ยท +โ)))) |
15 | | simpr 486 |
. . . . . 6
โข ((๐ด โ โ*
โง 0 < ๐ด) โ 0
< ๐ด) |
16 | | eqid 2737 |
. . . . . 6
โข +โ
= +โ |
17 | 15, 16 | jctir 522 |
. . . . 5
โข ((๐ด โ โ*
โง 0 < ๐ด) โ (0
< ๐ด โง +โ =
+โ)) |
18 | 17 | orcd 872 |
. . . 4
โข ((๐ด โ โ*
โง 0 < ๐ด) โ ((0
< ๐ด โง +โ =
+โ) โจ (๐ด < 0
โง +โ = -โ))) |
19 | 18 | olcd 873 |
. . 3
โข ((๐ด โ โ*
โง 0 < ๐ด) โ (((0
< +โ โง ๐ด =
+โ) โจ (+โ < 0 โง ๐ด = -โ)) โจ ((0 < ๐ด โง +โ = +โ) โจ
(๐ด < 0 โง +โ =
-โ)))) |
20 | 19 | iftrued 4499 |
. 2
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
if((((0 < +โ โง ๐ด = +โ) โจ (+โ < 0 โง
๐ด = -โ)) โจ ((0
< ๐ด โง +โ =
+โ) โจ (๐ด < 0
โง +โ = -โ))), +โ, if((((0 < +โ โง ๐ด = -โ) โจ (+โ <
0 โง ๐ด = +โ)) โจ
((0 < ๐ด โง +โ =
-โ) โจ (๐ด < 0
โง +โ = +โ))), -โ, (๐ด ยท +โ))) =
+โ) |
21 | 4, 14, 20 | 3eqtrd 2781 |
1
โข ((๐ด โ โ*
โง 0 < ๐ด) โ
(๐ด ยทe
+โ) = +โ) |