Metamath Proof Explorer


Theorem relogbcxp

Description: Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020)

Ref Expression
Assertion relogbcxp B+1XlogBBX=X

Proof

Step Hyp Ref Expression
1 eldifsn B+1B+B1
2 rpcn B+B
3 2 adantr B+B1B
4 rpne0 B+B0
5 4 adantr B+B1B0
6 simpr B+B1B1
7 eldifpr B01BB0B1
8 3 5 6 7 syl3anbrc B+B1B01
9 1 8 sylbi B+1B01
10 eldifi B+1B+
11 10 2 syl B+1B
12 recn XX
13 cxpcl BXBX
14 11 12 13 syl2an B+1XBX
15 11 adantr B+1XB
16 1 5 sylbi B+1B0
17 16 adantr B+1XB0
18 12 adantl B+1XX
19 15 17 18 cxpne0d B+1XBX0
20 eldifsn BX0BXBX0
21 14 19 20 sylanbrc B+1XBX0
22 logbval B01BX0logBBX=logBXlogB
23 9 21 22 syl2an2r B+1XlogBBX=logBXlogB
24 logcxp B+XlogBX=XlogB
25 10 24 sylan B+1XlogBX=XlogB
26 25 oveq1d B+1XlogBXlogB=XlogBlogB
27 eldif B+1B+¬B1
28 rpcnne0 B+BB0
29 28 adantr B+¬B1BB0
30 27 29 sylbi B+1BB0
31 logcl BB0logB
32 30 31 syl B+1logB
33 32 adantr B+1XlogB
34 logne0 B+B1logB0
35 1 34 sylbi B+1logB0
36 35 adantr B+1XlogB0
37 18 33 36 divcan4d B+1XXlogBlogB=X
38 23 26 37 3eqtrd B+1XlogBBX=X