Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Steven Nguyen
Exponents and divisibility
log11d
Next ⟩
rplog11d
Metamath Proof Explorer
Ascii
Unicode
Theorem
log11d
Description:
The natural logarithm is one-to-one.
(Contributed by
SN
, 25-Apr-2025)
Ref
Expression
Hypotheses
log11d.a
⊢
φ
→
A
∈
ℂ
log11d.b
⊢
φ
→
B
∈
ℂ
log11d.1
⊢
φ
→
A
≠
0
log11d.2
⊢
φ
→
B
≠
0
Assertion
log11d
⊢
φ
→
log
⁡
A
=
log
⁡
B
↔
A
=
B
Proof
Step
Hyp
Ref
Expression
1
log11d.a
⊢
φ
→
A
∈
ℂ
2
log11d.b
⊢
φ
→
B
∈
ℂ
3
log11d.1
⊢
φ
→
A
≠
0
4
log11d.2
⊢
φ
→
B
≠
0
5
fveq2
⊢
log
⁡
A
=
log
⁡
B
→
e
log
⁡
A
=
e
log
⁡
B
6
eflog
⊢
A
∈
ℂ
∧
A
≠
0
→
e
log
⁡
A
=
A
7
1
3
6
syl2anc
⊢
φ
→
e
log
⁡
A
=
A
8
eflog
⊢
B
∈
ℂ
∧
B
≠
0
→
e
log
⁡
B
=
B
9
2
4
8
syl2anc
⊢
φ
→
e
log
⁡
B
=
B
10
7
9
eqeq12d
⊢
φ
→
e
log
⁡
A
=
e
log
⁡
B
↔
A
=
B
11
5
10
imbitrid
⊢
φ
→
log
⁡
A
=
log
⁡
B
→
A
=
B
12
fveq2
⊢
A
=
B
→
log
⁡
A
=
log
⁡
B
13
11
12
impbid1
⊢
φ
→
log
⁡
A
=
log
⁡
B
↔
A
=
B