Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
โข ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) / ( ! โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ด โ ๐ ) / ( ! โ ๐ ) ) ) |
2 |
|
eqid |
โข ( ๐ โ โ0 โฆ ( ( ๐ต โ ๐ ) / ( ! โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ๐ต โ ๐ ) / ( ! โ ๐ ) ) ) |
3 |
|
eqid |
โข ( ๐ โ โ0 โฆ ( ( ( ๐ด + ๐ต ) โ ๐ ) / ( ! โ ๐ ) ) ) = ( ๐ โ โ0 โฆ ( ( ( ๐ด + ๐ต ) โ ๐ ) / ( ! โ ๐ ) ) ) |
4 |
|
simpl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ๐ด โ โ ) |
5 |
|
simpr |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ๐ต โ โ ) |
6 |
1 2 3 4 5
|
efaddlem |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( exp โ ( ๐ด + ๐ต ) ) = ( ( exp โ ๐ด ) ยท ( exp โ ๐ต ) ) ) |