P. 245 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 24401-24500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	advlogexp 24401*	The antiderivative of a power of the logarithm. (Set A = 1 and multiply by ( -u 1 ) ^ N x. N ! to get the antiderivative of log ( x ) ^ N itself.) (Contributed by Mario Carneiro, 22-May-2016.)
|- ( ( A e. RR+ /\ N e. NN0 ) -> ( RR _D ( x e. RR+ |-> ( x x. sum_ k e. ( 0 ... N ) ( ( ( log ` ( A / x ) ) ^ k ) / ( ! ` k ) ) ) ) ) = ( x e. RR+ |-> ( ( ( log ` ( A / x ) ) ^ N ) / ( ! ` N ) ) ) )
Theorem	efopnlem1 24402	Lemma for efopn 24404. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
|- ( ( ( R e. RR+ /\ R < pi ) /\ A e. ( 0 ( ball ` ( abs o. - ) ) R ) ) -> ( abs ` ( Im ` A ) ) < pi )
Theorem	efopnlem2 24403	Lemma for efopn 24404. (Contributed by Mario Carneiro, 2-May-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( ( R e. RR+ /\ R < pi ) -> ( exp " ( 0 ( ball ` ( abs o. - ) ) R ) ) e. J )
Theorem	efopn 24404	The exponential map is an open map. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- J = ( TopOpen ` ℂfld )   =>    |- ( S e. J -> ( exp " S ) e. J )
Theorem	logtayllem 24405*	Lemma for logtayl 24406. (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 0 ( + , ( n e. NN0 |-> ( if ( n = 0 , 0 , ( 1 / n ) ) x. ( A ^ n ) ) ) ) e. dom ~~> )
Theorem	logtayl 24406*	The Taylor series for -u log ( 1 - A ). (Contributed by Mario Carneiro, 1-Apr-2015.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> seq 1 ( + , ( k e. NN |-> ( ( A ^ k ) / k ) ) ) ~~> -u ( log ` ( 1 - A ) ) )
Theorem	logtaylsum 24407*	The Taylor series for -u log ( 1 - A ), as an infinite sum. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- ( ( A e. CC /\ ( abs ` A ) < 1 ) -> sum_ k e. NN ( ( A ^ k ) / k ) = -u ( log ` ( 1 - A ) ) )
Theorem	logtayl2 24408*	Power series expression for the logarithm. (Contributed by Mario Carneiro, 31-Mar-2015.)
|- S = ( 1 ( ball ` ( abs o. - ) ) 1 )   =>    |- ( A e. S -> seq 1 ( + , ( k e. NN |-> ( ( ( -u 1 ^ ( k - 1 ) ) / k ) x. ( ( A - 1 ) ^ k ) ) ) ) ~~> ( log ` A ) )
Theorem	logccv 24409	The natural logarithm function on the reals is a strictly concave function. (Contributed by Mario Carneiro, 20-Jun-2015.)
|- ( ( ( A e. RR+ /\ B e. RR+ /\ A < B ) /\ T e. ( 0 (,) 1 ) ) -> ( ( T x. ( log ` A ) ) + ( ( 1 - T ) x. ( log ` B ) ) ) < ( log ` ( ( T x. A ) + ( ( 1 - T ) x. B ) ) ) )
Theorem	cxpval 24410	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) = if ( A = 0 , if ( B = 0 , 1 , 0 ) , ( exp ` ( B x. ( log ` A ) ) ) ) )
Theorem	cxpef 24411	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
Theorem	0cxp 24412	Value of the complex power function when the first argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 ) -> ( 0 ^c A ) = 0 )
Theorem	cxpexpz 24413	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ A =/= 0 /\ B e. ZZ ) -> ( A ^c B ) = ( A ^ B ) )
Theorem	cxpexp 24414	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ B e. NN0 ) -> ( A ^c B ) = ( A ^ B ) )
Theorem	logcxp 24415	Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )
Theorem	cxp0 24416	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( A ^c 0 ) = 1 )
Theorem	cxp1 24417	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( A ^c 1 ) = A )
Theorem	1cxp 24418	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( 1 ^c A ) = 1 )
Theorem	ecxp 24419	Write the exponential function as an exponent to the power _e. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( _e ^c A ) = ( exp ` A ) )
Theorem	cxpcl 24420	Closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. CC /\ B e. CC ) -> ( A ^c B ) e. CC )
Theorem	recxpcl 24421	Real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR /\ 0 <_ A /\ B e. RR ) -> ( A ^c B ) e. RR )
Theorem	rpcxpcl 24422	Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) e. RR+ )
Theorem	cxpne0 24423	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 24424	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 24425	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 24426	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 24427	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 24428	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 24429	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 24430	Lemma for mulcxp 24431. (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 24431	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 24432	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 24433	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 24434	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 24435	Product of exponents law for complex exponentiation. Variation on cxpmul 24434 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 24436	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 24437	Generalize cxpmul2 24435 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 24438	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 24439	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 24440	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 24441	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 24442	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 24443	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 24444	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 24445	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 24446	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 24447	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 24448	Lemma for cxpsqrt 24449. (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 24449	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 24450	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) )
Theorem	cxp0d 24451	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 24452	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 24453	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 24454	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 24455	Product of exponents law for complex exponentiation. Variation on cxpmul 24434 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 24456	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 24457	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 24458	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 24459	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 24460	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 24461	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 24462	Generalize cxpmul2 24435 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 24463	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 24464	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 24465	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 24466	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 24467	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 24468	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 24469	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 24470	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 24471	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 24472	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 24473	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 24474	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 24475	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 24476	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 24477	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 24478	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 24479	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 24480	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 24481*	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 24482*	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 24483	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 24484*	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 24485*	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 24486*	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 24487*	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 24488*	Lemma for cxpcn3 24489. (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 24489*	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 24490	Continuity of the real square root function. (Contributed by Mario Carneiro, 2-May-2016.)
|- ( sqr |` ( 0 [,) +oo ) ) e. ( ( 0 [,) +oo ) -cn-> RR )
Theorem	sqrtcn 24491	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 24492	Lemma for cxpaddle 24493. (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 24493	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 24494	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 24495	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 24496	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 24497	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 24498*	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 24499	An upper bound on the logarithm. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by AV, 2-Aug-2021.)
|- ( ( A e. RR /\ 0 <_ A ) -> ( log ` ( A + 1 ) ) <_ ( sqr ` A ) )
Theorem	logreclem 24500	Symmetry of the natural logarithm range by negation. Lemma for logrec 24501. (Contributed by Saveliy Skresanov, 27-Dec-2016.)
|- ( ( A e. ran log /\ -. ( Im ` A ) = pi ) -> -u A e. ran log )