(related to Proposition: Calculation Rules for General Powers)
Let \(x,y\) be real numbers and let \(a,b\) be positive real numbers.
It follows from the definition of the general power function and the functional equation of exponential function of general base.
The rule can be concluded as follows from the definition of exponential function of general base, and the definition of natural logarithm: Because \[a^x=\exp_a(x)=\exp(x\ln(a))\Longleftrightarrow \ln(a^x)=x\ln a,\] we get \[a^{xy}=\exp_a(xy)=\exp(yx\ln a)=\exp(y\ln(a^x))=(a^x)^y.\]
This rule follows from the definition of the general power function, the definition of exponential function of general base, the functional equation of exponential function, the distributivity law for real numbers and the functional equation of natural logarithms:
\[\begin{array}{rcll} a^x\cdot b^x&=&\exp_a(x)\cdot\exp_b(x)&\text{definition of general power function}\\ &=&\exp(x\cdot \ln a)\cdot\exp(x\cdot \ln b)&\text{definition of exponential function of general base}\\ &=&\exp(x\cdot \ln a+ x\cdot \ln b)&\text{functional equation of exponential function}\\ &=&\exp(x\cdot (\ln a+ \ln b))&\text{distributivity law for real numbers}\\ &=&\exp(x\cdot (\ln (a\cdot b))&\text{functional equation of natural logarithm}\\ &=&\exp_{ab}(x)&\text{definition of exponential function of general base}\\ &=&(ab)^x&\text{definition of general power function}\\ \end{array}\]
This calculation rule follows from the definition of the general power function and the reciprocity of exponential function of general base.
