This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )