Step | Hyp | Ref
| Expression |
1 | | elnn0 12420 |
. 2
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | nnne0 12192 |
. . . . . . . 8
โข (๐ โ โ โ ๐ โ 0) |
3 | 2 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ 0) |
4 | | nncn 12166 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ
โ) |
5 | 4 | adantl 483 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
6 | 5 | negeq0d 11509 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ = 0 โ -๐ = 0)) |
7 | 6 | necon3abid 2977 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ โ 0 โ ยฌ -๐ = 0)) |
8 | 3, 7 | mpbid 231 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ
-๐ = 0) |
9 | 8 | iffalsed 4498 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ
if(-๐ = 0, 1, if(0 <
-๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐)))) = if(0 < -๐, (seq1( ยท , (โ
ร {๐ด}))โ-๐), (1 / (seq1( ยท ,
(โ ร {๐ด}))โ--๐)))) |
10 | | nnnn0 12425 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ0) |
11 | 10 | adantl 483 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
12 | | nn0nlt0 12444 |
. . . . . . . 8
โข (๐ โ โ0
โ ยฌ ๐ <
0) |
13 | 11, 12 | syl 17 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ
๐ < 0) |
14 | 11 | nn0red 12479 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
15 | 14 | lt0neg1d 11729 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ < 0 โ 0 < -๐)) |
16 | 13, 15 | mtbid 324 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ 0
< -๐) |
17 | 16 | iffalsed 4498 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ if(0
< -๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))) = (1 / (seq1( ยท ,
(โ ร {๐ด}))โ--๐))) |
18 | 5 | negnegd 11508 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ --๐ = ๐) |
19 | 18 | fveq2d 6847 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1(
ยท , (โ ร {๐ด}))โ--๐) = (seq1( ยท , (โ ร
{๐ด}))โ๐)) |
20 | 19 | oveq2d 7374 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ (1 /
(seq1( ยท , (โ ร {๐ด}))โ--๐)) = (1 / (seq1( ยท , (โ ร
{๐ด}))โ๐))) |
21 | 9, 17, 20 | 3eqtrd 2777 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ
if(-๐ = 0, 1, if(0 <
-๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐)))) = (1 / (seq1( ยท ,
(โ ร {๐ด}))โ๐))) |
22 | | nnnegz 12507 |
. . . . 5
โข (๐ โ โ โ -๐ โ
โค) |
23 | | expval 13975 |
. . . . 5
โข ((๐ด โ โ โง -๐ โ โค) โ (๐ดโ-๐) = if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))))) |
24 | 22, 23 | sylan2 594 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ-๐) = if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))))) |
25 | | expnnval 13976 |
. . . . 5
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = (seq1( ยท , (โ ร
{๐ด}))โ๐)) |
26 | 25 | oveq2d 7374 |
. . . 4
โข ((๐ด โ โ โง ๐ โ โ) โ (1 /
(๐ดโ๐)) = (1 / (seq1( ยท , (โ ร
{๐ด}))โ๐))) |
27 | 21, 24, 26 | 3eqtr4d 2783 |
. . 3
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
28 | | 1div1e1 11850 |
. . . . 5
โข (1 / 1) =
1 |
29 | 28 | eqcomi 2742 |
. . . 4
โข 1 = (1 /
1) |
30 | | negeq 11398 |
. . . . . . 7
โข (๐ = 0 โ -๐ = -0) |
31 | | neg0 11452 |
. . . . . . 7
โข -0 =
0 |
32 | 30, 31 | eqtrdi 2789 |
. . . . . 6
โข (๐ = 0 โ -๐ = 0) |
33 | 32 | oveq2d 7374 |
. . . . 5
โข (๐ = 0 โ (๐ดโ-๐) = (๐ดโ0)) |
34 | | exp0 13977 |
. . . . 5
โข (๐ด โ โ โ (๐ดโ0) = 1) |
35 | 33, 34 | sylan9eqr 2795 |
. . . 4
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ-๐) = 1) |
36 | | oveq2 7366 |
. . . . . 6
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
37 | 36, 34 | sylan9eqr 2795 |
. . . . 5
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ๐) = 1) |
38 | 37 | oveq2d 7374 |
. . . 4
โข ((๐ด โ โ โง ๐ = 0) โ (1 / (๐ดโ๐)) = (1 / 1)) |
39 | 29, 35, 38 | 3eqtr4a 2799 |
. . 3
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
40 | 27, 39 | jaodan 957 |
. 2
โข ((๐ด โ โ โง (๐ โ โ โจ ๐ = 0)) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
41 | 1, 40 | sylan2b 595 |
1
โข ((๐ด โ โ โง ๐ โ โ0)
โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |