Metamath Proof Explorer


Theorem efadd

Description: Sum of exponents law for exponential function. (Contributed by NM, 10-Jan-2006) (Proof shortened by Mario Carneiro, 29-Apr-2014)

Ref Expression
Assertion efadd ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โ†’ ( exp โ€˜ ( ๐ด + ๐ต ) ) = ( ( exp โ€˜ ๐ด ) ยท ( exp โ€˜ ๐ต ) ) )

Proof

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 โ€˜ ๐ต ) ) )