Description: Power law for the general logarithm for integer powers: The logarithm of a positive real number to the power of an integer is equal to the product of the exponent and the logarithm of the base of the power, a deduction version (Contributed by metakunt, 22-May-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | relogbzexpd.1 | |- ( ph -> B e. RR+ ) |
|
| relogbzexpd.2 | |- ( ph -> B =/= 1 ) |
||
| relogbzexpd.3 | |- ( ph -> C e. RR+ ) |
||
| relogbzexpd.4 | |- ( ph -> N e. ZZ ) |
||
| Assertion | relogbzexpd | |- ( ph -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relogbzexpd.1 | |- ( ph -> B e. RR+ ) |
|
| 2 | relogbzexpd.2 | |- ( ph -> B =/= 1 ) |
|
| 3 | relogbzexpd.3 | |- ( ph -> C e. RR+ ) |
|
| 4 | relogbzexpd.4 | |- ( ph -> N e. ZZ ) |
|
| 5 | 1 | rpcnd | |- ( ph -> B e. CC ) |
| 6 | 1 | rpne0d | |- ( ph -> B =/= 0 ) |
| 7 | 6 2 | nelprd | |- ( ph -> -. B e. { 0 , 1 } ) |
| 8 | 5 7 | eldifd | |- ( ph -> B e. ( CC \ { 0 , 1 } ) ) |
| 9 | 8 3 4 | 3jca | |- ( ph -> ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) ) |
| 10 | relogbzexp | |- ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) ) |
|
| 11 | 9 10 | syl | |- ( ph -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) ) |