Metamath Proof Explorer

Theorem reef11

Description: The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008) (Revised by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion reef11 
|- ( ( A e. RR /\ B e. RR ) -> ( ( exp ` A ) = ( exp ` B ) <-> A = B ) )

Proof

Step Hyp Ref Expression
1 efle 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( exp ` A ) <_ ( exp ` B ) ) )
2 efle 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B <_ A <-> ( exp ` B ) <_ ( exp ` A ) ) )
3 2 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( B <_ A <-> ( exp ` B ) <_ ( exp ` A ) ) )
4 1 3 anbi12d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ B /\ B <_ A ) <-> ( ( exp ` A ) <_ ( exp ` B ) /\ ( exp ` B ) <_ ( exp ` A ) ) ) )
5 letri3 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ B <_ A ) ) )
6 reefcl 
 |-  ( A e. RR -> ( exp ` A ) e. RR )
7 reefcl 
 |-  ( B e. RR -> ( exp ` B ) e. RR )
8 letri3 
 |-  ( ( ( exp ` A ) e. RR /\ ( exp ` B ) e. RR ) -> ( ( exp ` A ) = ( exp ` B ) <-> ( ( exp ` A ) <_ ( exp ` B ) /\ ( exp ` B ) <_ ( exp ` A ) ) ) )
9 6 7 8 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( exp ` A ) = ( exp ` B ) <-> ( ( exp ` A ) <_ ( exp ` B ) /\ ( exp ` B ) <_ ( exp ` A ) ) ) )
10 4 5 9 3bitr4rd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( exp ` A ) = ( exp ` B ) <-> A = B ) )