Description: Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | relogbcxp | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifsn | |
|
2 | rpcn | |
|
3 | 2 | adantr | |
4 | rpne0 | |
|
5 | 4 | adantr | |
6 | simpr | |
|
7 | eldifpr | |
|
8 | 3 5 6 7 | syl3anbrc | |
9 | 1 8 | sylbi | |
10 | eldifi | |
|
11 | 10 2 | syl | |
12 | recn | |
|
13 | cxpcl | |
|
14 | 11 12 13 | syl2an | |
15 | 11 | adantr | |
16 | 1 5 | sylbi | |
17 | 16 | adantr | |
18 | 12 | adantl | |
19 | 15 17 18 | cxpne0d | |
20 | eldifsn | |
|
21 | 14 19 20 | sylanbrc | |
22 | logbval | |
|
23 | 9 21 22 | syl2an2r | |
24 | logcxp | |
|
25 | 10 24 | sylan | |
26 | 25 | oveq1d | |
27 | eldif | |
|
28 | rpcnne0 | |
|
29 | 28 | adantr | |
30 | 27 29 | sylbi | |
31 | logcl | |
|
32 | 30 31 | syl | |
33 | 32 | adantr | |
34 | logne0 | |
|
35 | 1 34 | sylbi | |
36 | 35 | adantr | |
37 | 18 33 36 | divcan4d | |
38 | 23 26 37 | 3eqtrd | |