Metamath Proof Explorer


Theorem relogbcxpb

Description: The logarithm is the inverse of the exponentiation. Observation in Cohen4 p. 348. (Contributed by AV, 11-Jun-2020)

Ref Expression
Assertion relogbcxpb B + B 1 X + Y log B X = Y B Y = X

Proof

Step Hyp Ref Expression
1 oveq2 Y = log B X B Y = B log B X
2 1 eqcoms log B X = Y B Y = B log B X
3 rpcn B + B
4 3 adantr B + B 1 B
5 rpne0 B + B 0
6 5 adantr B + B 1 B 0
7 simpr B + B 1 B 1
8 eldifpr B 0 1 B B 0 B 1
9 4 6 7 8 syl3anbrc B + B 1 B 0 1
10 rpcndif0 X + X 0
11 9 10 anim12i B + B 1 X + B 0 1 X 0
12 11 3adant3 B + B 1 X + Y B 0 1 X 0
13 cxplogb B 0 1 X 0 B log B X = X
14 12 13 syl B + B 1 X + Y B log B X = X
15 2 14 sylan9eqr B + B 1 X + Y log B X = Y B Y = X
16 oveq2 X = B Y log B X = log B B Y
17 16 eqcoms B Y = X log B X = log B B Y
18 eldifsn B + 1 B + B 1
19 18 biimpri B + B 1 B + 1
20 19 anim1i B + B 1 Y B + 1 Y
21 20 3adant2 B + B 1 X + Y B + 1 Y
22 relogbcxp B + 1 Y log B B Y = Y
23 21 22 syl B + B 1 X + Y log B B Y = Y
24 17 23 sylan9eqr B + B 1 X + Y B Y = X log B X = Y
25 15 24 impbida B + B 1 X + Y log B X = Y B Y = X