Metamath Proof Explorer


Theorem relogeftb

Description: Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007)

Ref Expression
Assertion relogeftb A+BlogA=BeB=A

Proof

Step Hyp Ref Expression
1 rpcnne0 A+AA0
2 relogrn BBranlog
3 logeftb AA0BranloglogA=BeB=A
4 3 3expa AA0BranloglogA=BeB=A
5 1 2 4 syl2an A+BlogA=BeB=A