Description: The natural logarithm is one-to-one on positive reals. (Contributed by SN, 25-Apr-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rplog11d.a | |- ( ph -> A e. RR+ ) |
|
rplog11d.b | |- ( ph -> B e. RR+ ) |
||
Assertion | rplog11d | |- ( ph -> ( ( log ` A ) = ( log ` B ) <-> A = B ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rplog11d.a | |- ( ph -> A e. RR+ ) |
|
2 | rplog11d.b | |- ( ph -> B e. RR+ ) |
|
3 | 1 | rpcnd | |- ( ph -> A e. CC ) |
4 | 2 | rpcnd | |- ( ph -> B e. CC ) |
5 | 1 | rpne0d | |- ( ph -> A =/= 0 ) |
6 | 2 | rpne0d | |- ( ph -> B =/= 0 ) |
7 | 3 4 5 6 | log11d | |- ( ph -> ( ( log ` A ) = ( log ` B ) <-> A = B ) ) |