Step |
Hyp |
Ref |
Expression |
1 |
|
elfz3nn0 |
โข ( ๐พ โ ( 0 ... ๐ ) โ ๐ โ โ0 ) |
2 |
|
elfzelz |
โข ( ๐พ โ ( 0 ... ๐ ) โ ๐พ โ โค ) |
3 |
|
bcval |
โข ( ( ๐ โ โ0 โง ๐พ โ โค ) โ ( ๐ C ๐พ ) = if ( ๐พ โ ( 0 ... ๐ ) , ( ( ! โ ๐ ) / ( ( ! โ ( ๐ โ ๐พ ) ) ยท ( ! โ ๐พ ) ) ) , 0 ) ) |
4 |
1 2 3
|
syl2anc |
โข ( ๐พ โ ( 0 ... ๐ ) โ ( ๐ C ๐พ ) = if ( ๐พ โ ( 0 ... ๐ ) , ( ( ! โ ๐ ) / ( ( ! โ ( ๐ โ ๐พ ) ) ยท ( ! โ ๐พ ) ) ) , 0 ) ) |
5 |
|
iftrue |
โข ( ๐พ โ ( 0 ... ๐ ) โ if ( ๐พ โ ( 0 ... ๐ ) , ( ( ! โ ๐ ) / ( ( ! โ ( ๐ โ ๐พ ) ) ยท ( ! โ ๐พ ) ) ) , 0 ) = ( ( ! โ ๐ ) / ( ( ! โ ( ๐ โ ๐พ ) ) ยท ( ! โ ๐พ ) ) ) ) |
6 |
4 5
|
eqtrd |
โข ( ๐พ โ ( 0 ... ๐ ) โ ( ๐ C ๐พ ) = ( ( ! โ ๐ ) / ( ( ! โ ( ๐ โ ๐พ ) ) ยท ( ! โ ๐พ ) ) ) ) |