P. 238 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 23701-23800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cxpne0 23701	Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) =/= 0 )
Theorem	cxpeq0 23702	Complex exponentiation is zero iff the mantissa is zero and the exponent is nonzero. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A ^c B ) = 0 <-> ( A = 0 /\ B =/= 0 ) ) )
Theorem	cxpadd 23703	Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + C ) ) = ( ( A ^c B ) x. ( A ^c C ) ) )
Theorem	cxpp1 23704	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. A ) )
Theorem	cxpneg 23705	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c -u B ) = ( 1 / ( A ^c B ) ) )
Theorem	cxpsub 23706	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ B e. CC /\ C e. CC ) -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )
Theorem	cxpge0 23707	Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> 0 <_ ( A ^c B ) )
Theorem	mulcxplem 23708	Lemma for mulcxp 23709. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( 0 ^c C ) = ( ( A ^c C ) x. ( 0 ^c C ) ) )
Theorem	mulcxp 23709	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. CC ) -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )
Theorem	cxprec 23710	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) )
Theorem	divcxp 23711	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )
Theorem	cxpmul 23712	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. RR /\ C e. CC ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )
Theorem	cxpmul2 23713	Product of exponents law for complex exponentiation. Variation on cxpmul 23712 with more general conditions on A and B when C is an integer. (Contributed by Mario Carneiro, 9-Aug-2014.)
|- ( ( A e. CC /\ B e. CC /\ C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	cxproot 23714	The complex power function allows us to write n-th roots via the idiom A ^c ( 1 / N ). (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ( A e. CC /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
Theorem	cxpmul2z 23715	Generalize cxpmul2 23713 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ C e. ZZ ) ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	abscxp 23716	Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( abs ` ( A ^c B ) ) = ( A ^c ( Re ` B ) ) )
Theorem	abscxp2 23717	Absolute value of a power, when the exponent is real. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. CC /\ B e. RR ) -> ( abs ` ( A ^c B ) ) = ( ( abs ` A ) ^c B ) )
Theorem	cxplt 23718	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( A ^c B ) < ( A ^c C ) ) )
Theorem	cxple 23719	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( ( A e. RR /\ 1 < A ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) )
Theorem	cxplea 23720	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 10-Sep-2014.)
|- ( ( ( A e. RR /\ 1 <_ A ) /\ ( B e. RR /\ C e. RR ) /\ B <_ C ) -> ( A ^c B ) <_ ( A ^c C ) )
Theorem	cxple2 23721	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
Theorem	cxplt2 23722	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) /\ C e. RR+ ) -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )
Theorem	cxple2a 23723	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( 0 <_ A /\ 0 <_ C ) /\ A <_ B ) -> ( A ^c C ) <_ ( B ^c C ) )
Theorem	cxplt3 23724	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B < C <-> ( A ^c C ) < ( A ^c B ) ) )
Theorem	cxple3 23725	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( ( ( A e. RR+ /\ A < 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B <_ C <-> ( A ^c C ) <_ ( A ^c B ) ) )
Theorem	cxpsqrtlem 23726	Lemma for cxpsqrt 23727. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( ( A e. CC /\ A =/= 0 ) /\ ( A ^c ( 1 / 2 ) ) = -u ( sqr ` A ) ) -> ( _i x. ( sqr ` A ) ) e. RR )
Theorem	cxpsqrt 23727	The complex exponential function with exponent 1 / 2 exactly matches the complex square root function (the branch cut is in the same place for both functions), and thus serves as a suitable generalization to other n-th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( A ^c ( 1 / 2 ) ) = ( sqr ` A ) )
Theorem	logsqrt 23728	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) )
Theorem	cxp0d 23729	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^c 0 ) = 1 )
Theorem	cxp1d 23730	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( A ^c 1 ) = A )
Theorem	1cxpd 23731	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   =>    |- ( ph -> ( 1 ^c A ) = 1 )
Theorem	cxpcld 23732	Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c B ) e. CC )
Theorem	cxpmul2d 23733	Product of exponents law for complex exponentiation. Variation on cxpmul 23712 with more general conditions on A and B when C is an integer. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. NN0 )   =>    |- ( ph -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	0cxpd 23734	Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   =>    |- ( ph -> ( 0 ^c A ) = 0 )
Theorem	cxpexpzd 23735	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. ZZ )   =>    |- ( ph -> ( A ^c B ) = ( A ^ B ) )
Theorem	cxpefd 23736	Value of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
Theorem	cxpne0d 23737	Complex exponentiation is nonzero if its mantissa is nonzero. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c B ) =/= 0 )
Theorem	cxpp1d 23738	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. A ) )
Theorem	cxpnegd 23739	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c -u B ) = ( 1 / ( A ^c B ) ) )
Theorem	cxpmul2zd 23740	Generalize cxpmul2 23713 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. ZZ )   =>    |- ( ph -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	cxpaddd 23741	Sum of exponents law for complex exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A ^c ( B + C ) ) = ( ( A ^c B ) x. ( A ^c C ) ) )
Theorem	cxpsubd 23742	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. CC )   &    |- ( ph -> A =/= 0 )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )
Theorem	cxpltd 23743	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 < A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B < C <-> ( A ^c B ) < ( A ^c C ) ) )
Theorem	cxpled 23744	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 < A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B <_ C <-> ( A ^c B ) <_ ( A ^c C ) ) )
Theorem	cxplead 23745	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> B <_ C )   =>    |- ( ph -> ( A ^c B ) <_ ( A ^c C ) )
Theorem	divcxpd 23746	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )
Theorem	recxpcld 23747	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A ^c B ) e. RR )
Theorem	cxpge0d 23748	Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> 0 <_ ( A ^c B ) )
Theorem	cxple2ad 23749	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. RR )   &    |- ( ph -> 0 <_ C )   &    |- ( ph -> A <_ B )   =>    |- ( ph -> ( A ^c C ) <_ ( B ^c C ) )
Theorem	cxplt2d 23750	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )
Theorem	cxple2d 23751	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> C e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
Theorem	mulcxpd 23752	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )
Theorem	cxprecd 23753	Complex exponentiation of a reciprocal. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( ( 1 / A ) ^c B ) = ( 1 / ( A ^c B ) ) )
Theorem	rpcxpcld 23754	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( A ^c B ) e. RR+ )
Theorem	logcxpd 23755	Logarithm of a complex power. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   =>    |- ( ph -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )
Theorem	cxplt3d 23756	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B < C <-> ( A ^c C ) < ( A ^c B ) ) )
Theorem	cxple3d 23757	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> A < 1 )   &    |- ( ph -> C e. RR )   =>    |- ( ph -> ( B <_ C <-> ( A ^c C ) <_ ( A ^c B ) ) )
Theorem	cxpmuld 23758	Product of exponents law for complex exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR )   &    |- ( ph -> C e. CC )   =>    |- ( ph -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^c C ) )
Theorem	dvcxp1 23759*	The derivative of a complex power with respect to the first argument. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( A e. CC -> ( RR _D ( x e. RR+ |-> ( x ^c A ) ) ) = ( x e. RR+ |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )
Theorem	dvcxp2 23760*	The derivative of a complex power with respect to the second argument. (Contributed by Mario Carneiro, 24-Feb-2015.)
|- ( A e. RR+ -> ( CC _D ( x e. CC |-> ( A ^c x ) ) ) = ( x e. CC |-> ( ( log ` A ) x. ( A ^c x ) ) ) )
Theorem	dvsqrt 23761	The derivative of the real square root function. (Contributed by Mario Carneiro, 1-May-2016.)
|- ( RR _D ( x e. RR+ |-> ( sqr ` x ) ) ) = ( x e. RR+ |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) )
Theorem	dvcncxp1 23762*	Derivative of complex power with respect to first argument on the complex plane. (Contributed by Brendan Leahy, 18-Dec-2018.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( A e. CC -> ( CC _D ( x e. D |-> ( x ^c A ) ) ) = ( x e. D |-> ( A x. ( x ^c ( A - 1 ) ) ) ) )
Theorem	dvcnsqrt 23763*	Derivative of square root function. (Contributed by Brendan Leahy, 18-Dec-2018.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( CC _D ( x e. D |-> ( sqr ` x ) ) ) = ( x e. D |-> ( 1 / ( 2 x. ( sqr ` x ) ) ) )
Theorem	cxpcn 23764*	Domain of continuity of the complex power function. (Contributed by Mario Carneiro, 1-May-2016.)
|- D = ( CC \ ( -oo (,] 0 ) )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t D )   =>    |- ( x e. D , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )
Theorem	cxpcn2 23765*	Continuity of the complex power function, when the base is real. (Contributed by Mario Carneiro, 1-May-2016.)
|- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t RR+ )   =>    |- ( x e. RR+ , y e. CC |-> ( x ^c y ) ) e. ( ( K tX J ) Cn J )
Theorem	cxpcn3lem 23766*	Lemma for cxpcn3 23767. (Contributed by Mario Carneiro, 2-May-2016.)
|- D = ( `' Re " RR+ )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t ( 0 [,) +oo ) )   &    |- L = ( J ↾t D )   &    |- U = ( if ( ( Re ` A ) <_ 1 , ( Re ` A ) , 1 ) / 2 )   &    |- T = if ( U <_ ( E ^c ( 1 / U ) ) , U , ( E ^c ( 1 / U ) ) )   =>    |- ( ( A e. D /\ E e. RR+ ) -> E. d e. RR+ A. a e. ( 0 [,) +oo ) A. b e. D ( ( ( abs ` a ) < d /\ ( abs ` ( A - b ) ) < d ) -> ( abs ` ( a ^c b ) ) < E ) )
Theorem	cxpcn3 23767*	Extend continuity of the complex power function to a base of zero, as long as the exponent has strictly positive real part. (Contributed by Mario Carneiro, 2-May-2016.)
|- D = ( `' Re " RR+ )   &    |- J = ( TopOpen ` ℂfld )   &    |- K = ( J ↾t ( 0 [,) +oo ) )   &    |- L = ( J ↾t D )   =>    |- ( x e. ( 0 [,) +oo ) , y e. D |-> ( x ^c y ) ) e. ( ( K tX L ) Cn J )
Theorem	resqrtcn 23768	Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( sqr |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR )
Theorem	sqrtcn 23769	Continuity of the square root function. (Contributed by Mario Carneiro, 2-May-2016.)
|- D = ( CC \ ( -oo (,] 0 ) )   =>    |- ( sqr |` D ) e. ( D -cn-> CC )
Theorem	cxpaddlelem 23770	Lemma for cxpaddle 23771. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> A <_ 1 )   &    |- ( ph -> B e. RR+ )   &    |- ( ph -> B <_ 1 )   =>    |- ( ph -> A <_ ( A ^c B ) )
Theorem	cxpaddle 23771	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- ( ph -> A e. RR )   &    |- ( ph -> 0 <_ A )   &    |- ( ph -> B e. RR )   &    |- ( ph -> 0 <_ B )   &    |- ( ph -> C e. RR+ )   &    |- ( ph -> C <_ 1 )   =>    |- ( ph -> ( ( A + B ) ^c C ) <_ ( ( A ^c C ) + ( B ^c C ) ) )
Theorem	abscxpbnd 23772	Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ph -> A e. CC )   &    |- ( ph -> B e. CC )   &    |- ( ph -> 0 <_ ( Re ` B ) )   &    |- ( ph -> M e. RR )   &    |- ( ph -> ( abs ` A ) <_ M )   =>    |- ( ph -> ( abs ` ( A ^c B ) ) <_ ( ( M ^c ( Re ` B ) ) x. ( exp ` ( ( abs ` B ) x. pi ) ) ) )
Theorem	root1id 23773	Property of an N-th root of unity. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( N e. NN -> ( ( -u 1 ^c ( 2 / N ) ) ^ N ) = 1 )
Theorem	root1eq1 23774	The only powers of an N-th root of unity that equal 1 are the multiples of N. In other words, -u 1 ^c ( 2 / N ) has order N in the multiplicative group of nonzero complex numbers. (In fact, these and their powers are the only elements of finite order in the complex numbers.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- ( ( N e. NN /\ K e. ZZ ) -> ( ( ( -u 1 ^c ( 2 / N ) ) ^ K ) = 1 <-> N || K ) )
Theorem	root1cj 23775	Within the N-th roots of unity, the conjugate of the K-th root is the N - K-th root. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( N e. NN /\ K e. ZZ ) -> ( * ` ( ( -u 1 ^c ( 2 / N ) ) ^ K ) ) = ( ( -u 1 ^c ( 2 / N ) ) ^ ( N - K ) ) )
Theorem	cxpeq 23776*	Solve an equation involving an N-th power. The expression -u 1 ^c ( 2 / N ) = exp ( 2 pi _i / N ) is a way to write the primitive N-th root of unity with the smallest positive argument. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( A e. CC /\ N e. NN /\ B e. CC ) -> ( ( A ^ N ) = B <-> E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( -u 1 ^c ( 2 / N ) ) ^ n ) ) ) )
Theorem	loglesqrt 23777	An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( A + 1 ) ) <_ ( sqr ` A ) )
Theorem	logreclem 23778	Symmetry of the natural logarithm range by negation. Lemma for logrec 23779. (Contributed by Saveliy Skresanov, 27-Dec-2016.)
|- ( ( A e. ran log /\ -. ( Im ` A ) = pi ) -> -u A e. ran log )
Theorem	logrec 23779	Logarithm of a reciprocal changes sign. (Contributed by Saveliy Skresanov, 28-Dec-2016.)
|- ( ( A e. CC /\ A =/= 0 /\ ( Im ` ( log ` A ) ) =/= pi ) -> ( log ` A ) = -u ( log ` ( 1 / A ) ) )
14.3.5  Logarithms to an arbitrary base Define "log using an arbitrary base" function and then prove some of its properties. Note that logb is generalized to an arbitrary base and arbitrary parameter in CC, but it doesn't accept infinities as arguments, unlike log. Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log". There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): ( B logb X ) where B is the base and X is the argument of the logarithm function. An alternative would be to support the notational form ( ( logb ` B ) ` X ); that looks a little more like traditional notation. Such a function ( logb ` B ) for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: (curry logb ` B ), see logbmpt 23804, logbf 23805 and logbfval 23806.
Syntax	clogb 23780	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 23781*	Define the logb operator. This is the logarithm generalized to an arbitrary base. It can be used as ( B logb X ) for "log base B of X". In the most common traditional notation, base B is a subscript of "log". The definition is according to Wikipedia "Complex logarithm": https://en.wikipedia.org/wiki/Complex_logarithm#Logarithms_to_other_bases (10-Jun-2020). (Contributed by David A. Wheeler, 21-Jan-2017.)
|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
Theorem	logbval 23782	Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
Theorem	logbcl 23783	General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ X e. ( CC \ { 0 } ) ) -> ( B logb X ) e. CC )
Theorem	logbid1 23784	General logarithm is 1 when base and arg match. Property 1(a) of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by David A. Wheeler, 22-Jul-2017.)
|- ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) -> ( A logb A ) = 1 )
Theorem	logb1 23785	The logarithm of 1 to an arbitrary base B is 0. Property 1(b) of [Cohen4] p. 361. See log1 23614. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. CC /\ B =/= 0 /\ B =/= 1 ) -> ( B logb 1 ) = 0 )
Theorem	elogb 23786	The general logarithm of a number to the base being Euler's constant is the natural logarithm of the number. Put another way, using _e as the base in logb is the same as log. Definition in [Cohen4] p. 352. (Contributed by David A. Wheeler, 17-Oct-2017.) (Revised by David A. Wheeler and AV, 16-Jun-2020.)
|- ( A e. ( CC \ { 0 } ) -> ( _e logb A ) = ( log ` A ) )
Theorem	logbchbase 23787	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
|- ( ( ( A e. CC /\ A =/= 0 /\ A =/= 1 ) /\ ( B e. CC /\ B =/= 0 /\ B =/= 1 ) /\ X e. ( CC \ { 0 } ) ) -> ( A logb X ) = ( ( B logb X ) / ( B logb A ) ) )
Theorem	relogbval 23788	Value of the general logarithm with integer base. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
Theorem	relogbcl 23789	Closure of the general logarithm with a positive real base on positive reals. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. RR+ /\ X e. RR+ /\ B =/= 1 ) -> ( B logb X ) e. RR )
Theorem	relogbzcl 23790	Closure of the general logarithm with integer base on positive reals. (Contributed by Thierry Arnoux, 27-Sep-2017.) (Proof shortened by AV, 9-Jun-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( B logb X ) e. RR )
Theorem	relogbreexp 23791	Power law for the general logarithm for real powers: The logarithm of a positive real number to the power of a real number is equal to the product of the exponent and the logarithm of the base of the power. Property 4 of [Cohen4] p. 361. (Contributed by AV, 9-Jun-2020.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )
Theorem	relogbzexp 23792	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. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) )
Theorem	relogbmul 23793	The logarithm of the product of two positive real numbers is the sum of logarithms. Property 2 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 29-May-2020.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. C ) ) = ( ( B logb A ) + ( B logb C ) ) )
Theorem	relogbmulexp 23794	The logarithm of the product of a positive real and a positive real number to the power of a real number is the sum of the logarithm of the first real number and the scaled logarithm of the second real number. (Contributed by AV, 29-May-2020.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ /\ E e. RR ) ) -> ( B logb ( A x. ( C ^c E ) ) ) = ( ( B logb A ) + ( E x. ( B logb C ) ) ) )
Theorem	relogbdiv 23795	The logarithm of the quotient of two positive real numbers is the difference of logarithms. Property 3 of [Cohen4] p. 361. (Contributed by AV, 29-May-2020.)
|- ( ( B e. ( CC \ { 0 , 1 } ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( ( B logb A ) - ( B logb C ) ) )
Theorem	relogbexp 23796	Identity law for general logarithm: the logarithm of a power to the base is the exponent. Property 6 of [Cohen4] p. 361. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by AV, 9-Jun-2020.)
|- ( ( B e. RR+ /\ B =/= 1 /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )
Theorem	nnlogbexp 23797	Identity law for general logarithm with integer base. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ M e. ZZ ) -> ( B logb ( B ^ M ) ) = M )
Theorem	logbrec 23798	Logarithm of a reciprocal changes sign. See logrec 23779. Particular case of Property 3 of [Cohen4] p. 361. (Contributed by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ A e. RR+ ) -> ( B logb ( 1 / A ) ) = -u ( B logb A ) )
Theorem	logbleb 23799	The general logarithm function is monotone/increasing. See logleb 23631. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by AV, 31-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X <_ Y <-> ( B logb X ) <_ ( B logb Y ) ) )
Theorem	logblt 23800	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 23628. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ /\ Y e. RR+ ) -> ( X < Y <-> ( B logb X ) < ( B logb Y ) ) )