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 ABeA+B=eAeB

Proof

Step Hyp Ref Expression
1 eqid n0Ann!=n0Ann!
2 eqid n0Bnn!=n0Bnn!
3 eqid n0A+Bnn!=n0A+Bnn!
4 simpl ABA
5 simpr ABB
6 1 2 3 4 5 efaddlem ABeA+B=eAeB