Step |
Hyp |
Ref |
Expression |
1 |
|
0z |
โข 0 โ โค |
2 |
|
expval |
โข ( ( ๐ด โ โ โง 0 โ โค ) โ ( ๐ด โ 0 ) = if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ 0 ) , ( 1 / ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ - 0 ) ) ) ) ) |
3 |
1 2
|
mpan2 |
โข ( ๐ด โ โ โ ( ๐ด โ 0 ) = if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ 0 ) , ( 1 / ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ - 0 ) ) ) ) ) |
4 |
|
eqid |
โข 0 = 0 |
5 |
4
|
iftruei |
โข if ( 0 = 0 , 1 , if ( 0 < 0 , ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ 0 ) , ( 1 / ( seq 1 ( ยท , ( โ ร { ๐ด } ) ) โ - 0 ) ) ) ) = 1 |
6 |
3 5
|
eqtrdi |
โข ( ๐ด โ โ โ ( ๐ด โ 0 ) = 1 ) |