Step | Hyp | Ref
| Expression |
1 | | elnn0 9177 |
. . 3
โข (๐ โ โ0
โ (๐ โ โ
โจ ๐ =
0)) |
2 | | nnne0 8946 |
. . . . . . . . . 10
โข (๐ โ โ โ ๐ โ 0) |
3 | 2 | adantl 277 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ 0) |
4 | | nncn 8926 |
. . . . . . . . . . . 12
โข (๐ โ โ โ ๐ โ
โ) |
5 | 4 | adantl 277 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
6 | 5 | negeq0d 8259 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ = 0 โ -๐ = 0)) |
7 | 6 | necon3abid 2386 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ โ 0 โ ยฌ -๐ = 0)) |
8 | 3, 7 | mpbid 147 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ
-๐ = 0) |
9 | 8 | iffalsed 3544 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ
if(-๐ = 0, 1, if(0 <
-๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐)))) = if(0 < -๐, (seq1( ยท , (โ
ร {๐ด}))โ-๐), (1 / (seq1( ยท ,
(โ ร {๐ด}))โ--๐)))) |
10 | | nnnn0 9182 |
. . . . . . . . . . 11
โข (๐ โ โ โ ๐ โ
โ0) |
11 | 10 | adantl 277 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ0) |
12 | | nn0nlt0 9201 |
. . . . . . . . . 10
โข (๐ โ โ0
โ ยฌ ๐ <
0) |
13 | 11, 12 | syl 14 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ
๐ < 0) |
14 | 11 | nn0red 9229 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ โ โ) โ ๐ โ
โ) |
15 | 14 | lt0neg1d 8471 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ < 0 โ 0 < -๐)) |
16 | 13, 15 | mtbid 672 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ ยฌ 0
< -๐) |
17 | 16 | iffalsed 3544 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ if(0
< -๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))) = (1 / (seq1( ยท ,
(โ ร {๐ด}))โ--๐))) |
18 | 5 | negnegd 8258 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ โ โ) โ --๐ = ๐) |
19 | 18 | fveq2d 5519 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ โ โ) โ (seq1(
ยท , (โ ร {๐ด}))โ--๐) = (seq1( ยท , (โ ร
{๐ด}))โ๐)) |
20 | 19 | oveq2d 5890 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (1 /
(seq1( ยท , (โ ร {๐ด}))โ--๐)) = (1 / (seq1( ยท , (โ ร
{๐ด}))โ๐))) |
21 | 9, 17, 20 | 3eqtrd 2214 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ
if(-๐ = 0, 1, if(0 <
-๐, (seq1( ยท ,
(โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐)))) = (1 / (seq1( ยท ,
(โ ร {๐ด}))โ๐))) |
22 | 21 | adantlr 477 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ) โ if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ
ร {๐ด}))โ-๐), (1 / (seq1( ยท ,
(โ ร {๐ด}))โ--๐)))) = (1 / (seq1( ยท , (โ
ร {๐ด}))โ๐))) |
23 | | simp1 997 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ ๐ด โ โ) |
24 | | simp3 999 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ ๐ โ โ) |
25 | 24 | nnzd 9373 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ ๐ โ โค) |
26 | 25 | znegcld 9376 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ -๐ โ โค) |
27 | | simp2 998 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ ๐ด # 0) |
28 | 27 | orcd 733 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ (๐ด # 0 โจ 0 โค -๐)) |
29 | | exp3val 10521 |
. . . . . . 7
โข ((๐ด โ โ โง -๐ โ โค โง (๐ด # 0 โจ 0 โค -๐)) โ (๐ดโ-๐) = if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))))) |
30 | 23, 26, 28, 29 | syl3anc 1238 |
. . . . . 6
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ) โ (๐ดโ-๐) = if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))))) |
31 | 30 | 3expa 1203 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ) โ (๐ดโ-๐) = if(-๐ = 0, 1, if(0 < -๐, (seq1( ยท , (โ ร {๐ด}))โ-๐), (1 / (seq1( ยท , (โ ร
{๐ด}))โ--๐))))) |
32 | | expnnval 10522 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ โ โ) โ (๐ดโ๐) = (seq1( ยท , (โ ร
{๐ด}))โ๐)) |
33 | 32 | oveq2d 5890 |
. . . . . 6
โข ((๐ด โ โ โง ๐ โ โ) โ (1 /
(๐ดโ๐)) = (1 / (seq1( ยท , (โ ร
{๐ด}))โ๐))) |
34 | 33 | adantlr 477 |
. . . . 5
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ) โ (1 / (๐ดโ๐)) = (1 / (seq1( ยท , (โ ร
{๐ด}))โ๐))) |
35 | 22, 31, 34 | 3eqtr4d 2220 |
. . . 4
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
36 | | 1div1e1 8660 |
. . . . . . 7
โข (1 / 1) =
1 |
37 | 36 | eqcomi 2181 |
. . . . . 6
โข 1 = (1 /
1) |
38 | | negeq 8149 |
. . . . . . . . 9
โข (๐ = 0 โ -๐ = -0) |
39 | | neg0 8202 |
. . . . . . . . 9
โข -0 =
0 |
40 | 38, 39 | eqtrdi 2226 |
. . . . . . . 8
โข (๐ = 0 โ -๐ = 0) |
41 | 40 | oveq2d 5890 |
. . . . . . 7
โข (๐ = 0 โ (๐ดโ-๐) = (๐ดโ0)) |
42 | | exp0 10523 |
. . . . . . 7
โข (๐ด โ โ โ (๐ดโ0) = 1) |
43 | 41, 42 | sylan9eqr 2232 |
. . . . . 6
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ-๐) = 1) |
44 | | oveq2 5882 |
. . . . . . . 8
โข (๐ = 0 โ (๐ดโ๐) = (๐ดโ0)) |
45 | 44, 42 | sylan9eqr 2232 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ๐) = 1) |
46 | 45 | oveq2d 5890 |
. . . . . 6
โข ((๐ด โ โ โง ๐ = 0) โ (1 / (๐ดโ๐)) = (1 / 1)) |
47 | 37, 43, 46 | 3eqtr4a 2236 |
. . . . 5
โข ((๐ด โ โ โง ๐ = 0) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
48 | 47 | adantlr 477 |
. . . 4
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ = 0) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
49 | 35, 48 | jaodan 797 |
. . 3
โข (((๐ด โ โ โง ๐ด # 0) โง (๐ โ โ โจ ๐ = 0)) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
50 | 1, 49 | sylan2b 287 |
. 2
โข (((๐ด โ โ โง ๐ด # 0) โง ๐ โ โ0) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |
51 | 50 | 3impa 1194 |
1
โข ((๐ด โ โ โง ๐ด # 0 โง ๐ โ โ0) โ (๐ดโ-๐) = (1 / (๐ดโ๐))) |