Metamath Proof Explorer


Theorem log11d

Description: The natural logarithm is one-to-one. (Contributed by SN, 25-Apr-2025)

Ref Expression
Hypotheses log11d.a
|- ( ph -> A e. CC )
log11d.b
|- ( ph -> B e. CC )
log11d.1
|- ( ph -> A =/= 0 )
log11d.2
|- ( ph -> B =/= 0 )
Assertion log11d
|- ( ph -> ( ( log ` A ) = ( log ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 log11d.a
 |-  ( ph -> A e. CC )
2 log11d.b
 |-  ( ph -> B e. CC )
3 log11d.1
 |-  ( ph -> A =/= 0 )
4 log11d.2
 |-  ( ph -> B =/= 0 )
5 fveq2
 |-  ( ( log ` A ) = ( log ` B ) -> ( exp ` ( log ` A ) ) = ( exp ` ( log ` B ) ) )
6 eflog
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
7 1 3 6 syl2anc
 |-  ( ph -> ( exp ` ( log ` A ) ) = A )
8 eflog
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( exp ` ( log ` B ) ) = B )
9 2 4 8 syl2anc
 |-  ( ph -> ( exp ` ( log ` B ) ) = B )
10 7 9 eqeq12d
 |-  ( ph -> ( ( exp ` ( log ` A ) ) = ( exp ` ( log ` B ) ) <-> A = B ) )
11 5 10 imbitrid
 |-  ( ph -> ( ( log ` A ) = ( log ` B ) -> A = B ) )
12 fveq2
 |-  ( A = B -> ( log ` A ) = ( log ` B ) )
13 11 12 impbid1
 |-  ( ph -> ( ( log ` A ) = ( log ` B ) <-> A = B ) )