P. 162 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 16101-16200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfrelog 16101	The natural logarithm function on the positive reals in terms of the real exponential function. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) = `' ( exp |` RR )
Theorem	relogf1o 16102	The natural logarithm function maps the positive reals one-to-one onto the real numbers. (Contributed by Paul Chapman, 21-Apr-2008.)
|- ( log |` RR+ ) : RR+ -1-1-onto-> RR
Theorem	relogcl 16103	Closure of the natural logarithm function on positive reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( log ` A ) e. RR )
Theorem	reeflog 16104	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR+ -> ( exp ` ( log ` A ) ) = A )
Theorem	relogef 16105	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( A e. RR -> ( log ` ( exp ` A ) ) = A )
Theorem	relogeftb 16106	Relationship between the natural logarithm function and the exponential function. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( ( log ` A ) = B <-> ( exp ` B ) = A ) )
Theorem	log1 16107	The natural logarithm of 1. One case of Property 1a of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log ` 1 ) = 0
Theorem	loge 16108	The natural logarithm of _e. One case of Property 1b of [Cohen] p. 301. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log ` _e ) = 1
Theorem	reaplog 16109	Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A # B <-> ( log ` A ) # ( log ` B ) ) )
Theorem	relogoprlem 16110	Lemma for relogmul 16111 and relogdiv 16112. Remark of [Cohen] p. 301 ("The proof of Property 3 is quite similar to the proof given for Property 2"). (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( ( log ` A ) e. CC /\ ( log ` B ) e. CC ) -> ( exp ` ( ( log ` A ) F ( log ` B ) ) ) = ( ( exp ` ( log ` A ) ) G ( exp ` ( log ` B ) ) ) )   &    |- ( ( ( log ` A ) e. RR /\ ( log ` B ) e. RR ) -> ( ( log ` A ) F ( log ` B ) ) e. RR )   =>    |- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A G B ) ) = ( ( log ` A ) F ( log ` B ) ) )
Theorem	relogmul 16111	The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdiv 16112	The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	reexplog 16113	Exponentiation of a positive real number to an integer power. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )
Theorem	relogexp 16114	The natural logarithm of positive A raised to an integer power. Property 4 of [Cohen] p. 301-302, restricted to natural logarithms and integer powers N. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ N e. ZZ ) -> ( log ` ( A ^ N ) ) = ( N x. ( log ` A ) ) )
Theorem	relogiso 16115	The natural logarithm function on positive reals determines an isomorphism from the positive reals onto the reals. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( log |` RR+ ) Isom < , < ( RR+ , RR )
Theorem	logltb 16116	The natural logarithm function on positive reals is strictly monotonic. (Contributed by Steve Rodriguez, 25-Nov-2007.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( log ` A ) < ( log ` B ) ) )
Theorem	logleb 16117	Natural logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
Theorem	logrpap0b 16118	The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.)
|- ( A e. RR+ -> ( A # 1 <-> ( log ` A ) # 0 ) )
Theorem	logrpap0 16119	The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.)
|- ( ( A e. RR+ /\ A # 1 ) -> ( log ` A ) # 0 )
Theorem	logrpap0d 16120	Deduction form of logrpap0 16119. (Contributed by Jim Kingdon, 3-Jul-2024.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> A # 1 )   =>    |- ( ph -> ( log ` A ) # 0 )
Theorem	rplogcl 16121	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 21-Sep-2014.)
|- ( ( A e. RR /\ 1 < A ) -> ( log ` A ) e. RR+ )
Theorem	logge0 16122	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ( A e. RR /\ 1 <_ A ) -> 0 <_ ( log ` A ) )
Theorem	logdivlti 16123	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ( ( A e. RR /\ B e. RR /\ _e <_ A ) /\ A < B ) -> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) )
Theorem	relogcld 16124	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( log ` A ) e. RR )
Theorem	reeflogd 16125	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( exp ` ( log ` A ) ) = A )
Theorem	relogmuld 16126	The natural logarithm of the product of two positive real numbers is the sum of natural logarithms. Property 2 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A x. B ) ) = ( ( log ` A ) + ( log ` B ) ) )
Theorem	relogdivd 16127	The natural logarithm of the quotient of two positive real numbers is the difference of natural logarithms. Exercise 72(a) and Property 3 of [Cohen] p. 301, restricted to natural logarithms. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( log ` ( A / B ) ) = ( ( log ` A ) - ( log ` B ) ) )
Theorem	logled 16128	Natural logarithm preserves <_. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> ( A <_ B <-> ( log ` A ) <_ ( log ` B ) ) )
Theorem	relogefd 16129	Relationship between the natural logarithm function and the exponential function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   =>    |- ( ph -> ( log ` ( exp ` A ) ) = A )
Theorem	rplogcld 16130	Closure of the logarithm function in the positive reals. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 < A )   =>    |- ( ph -> ( log ` A ) e. RR+ )
Theorem	logge0d 16131	The logarithm of a number greater than 1 is nonnegative. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> 1 <_ A )   =>    |- ( ph -> 0 <_ ( log ` A ) )
Theorem	logge0b 16132	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( 0 <_ ( log ` A ) <-> 1 <_ A ) )
Theorem	loggt0b 16133	The logarithm of a number is positive iff the number is greater than 1. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( 0 < ( log ` A ) <-> 1 < A ) )
Theorem	logle1b 16134	The logarithm of a number is less than or equal to 1 iff the number is less than or equal to Euler's constant. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( ( log ` A ) <_ 1 <-> A <_ _e ) )
Theorem	loglt1b 16135	The logarithm of a number is less than 1 iff the number is less than Euler's constant. (Contributed by AV, 30-May-2020.)
|- ( A e. RR+ -> ( ( log ` A ) < 1 <-> A < _e ) )
Theorem	logdivlt 16136	The log x / x function is strictly decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 14-Mar-2014.)
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A < B <-> ( ( log ` B ) / B ) < ( ( log ` A ) / A ) ) )
Theorem	logdivle 16137	The log x / x function is decreasing on the reals greater than _e. (Contributed by Mario Carneiro, 3-May-2016.)
|- ( ( ( A e. RR /\ _e <_ A ) /\ ( B e. RR /\ _e <_ B ) ) -> ( A <_ B <-> ( ( log ` B ) / B ) <_ ( ( log ` A ) / A ) ) )
Theorem	logfac 16138*	The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015.)
|- ( N e. NN0 -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )
Theorem	rpcxpef 16139	Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
Theorem	cxpexprp 16140	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
|- ( ( A e. RR+ /\ B e. ZZ ) -> ( A ^c B ) = ( A ^ B ) )
Theorem	cxpexpnn 16141	Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
|- ( ( A e. NN /\ B e. ZZ ) -> ( A ^c B ) = ( A ^ B ) )
Theorem	logcxp 16142	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	rpcxp0 16143	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
|- ( A e. RR+ -> ( A ^c 0 ) = 1 )
Theorem	rpcxp1 16144	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. RR+ -> ( A ^c 1 ) = A )
Theorem	1cxp 16145	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( 1 ^c A ) = 1 )
Theorem	ecxp 16146	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	rpcncxpcl 16147	Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) e. CC )
Theorem	rpcxpcl 16148	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	cxpap0 16149	Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c B ) # 0 )
Theorem	rpcxpadd 16150	Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> ( A ^c ( B + C ) ) = ( ( A ^c B ) x. ( A ^c C ) ) )
Theorem	rpcxpp1 16151	Value of a nonzero complex number raised to a complex power plus one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c ( B + 1 ) ) = ( ( A ^c B ) x. A ) )
Theorem	rpcxpneg 16152	Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. CC ) -> ( A ^c -u B ) = ( 1 / ( A ^c B ) ) )
Theorem	rpcxpsub 16153	Exponent subtraction law for complex exponentiation. (Contributed by Mario Carneiro, 22-Sep-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. CC ) -> ( A ^c ( B - C ) ) = ( ( A ^c B ) / ( A ^c C ) ) )
Theorem	rpmulcxp 16154	Complex exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( ( A e. RR+ /\ B e. RR+ /\ C e. CC ) -> ( ( A x. B ) ^c C ) = ( ( A ^c C ) x. ( B ^c C ) ) )
Theorem	cxprec 16155	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	rpdivcxp 16156	Complex exponentiation of a quotient. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ /\ C e. CC ) -> ( ( A / B ) ^c C ) = ( ( A ^c C ) / ( B ^c C ) ) )
Theorem	cxpmul 16157	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	rpcxpmul2 16158	Product of exponents law for complex exponentiation. Variation on cxpmul 16157 with more general conditions on A and B when C is a nonnegative integer. (Contributed by Mario Carneiro, 9-Aug-2014.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. NN0 ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	rpcxproot 16159	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. RR+ /\ N e. NN ) -> ( ( A ^c ( 1 / N ) ) ^ N ) = A )
Theorem	rpcxpmul2z 16160	Generalize rpcxpmul2 16158 to negative integers. (Contributed by Mario Carneiro, 23-Apr-2015.)
|- ( ( A e. RR+ /\ B e. CC /\ C e. ZZ ) -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	rpcxpmul2zd 16161	Generalize rpcxpmul2 16158 to negative integers. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. ZZ )   =>    |- ( ph -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	abscxp 16162	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	cxplt 16163	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 16164	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	rpcxple2 16165	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 8-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( A <_ B <-> ( A ^c C ) <_ ( B ^c C ) ) )
Theorem	rpcxplt2 16166	Ordering property for complex exponentiation. (Contributed by Mario Carneiro, 15-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ /\ C e. RR+ ) -> ( A < B <-> ( A ^c C ) < ( B ^c C ) ) )
Theorem	cxplt3 16167	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 16168	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	rpcxpsqrt 16169	The exponential function with exponent 1 / 2 exactly matches the square root function, and thus serves as a suitable generalization to other n-th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 16-Jun-2024.)
|- ( A e. RR+ -> ( A ^c ( 1 / 2 ) ) = ( sqr ` A ) )
Theorem	logsqrt 16170	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) )
Theorem	rpcxp0d 16171	Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A ^c 0 ) = 1 )
Theorem	rpcxp1d 16172	Value of the complex power function at one. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( A ^c 1 ) = A )
Theorem	1cxpd 16173	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	rpcncxpcld 16174	Closure of the complex power function. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. CC )   =>    |- ( ph -> ( A ^c B ) e. CC )
Theorem	cxpltd 16175	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 16176	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	rpcxpsqrtth 16177	Square root theorem over the complex numbers for the complex power function. Compare with resqrtth 11820. (Contributed by AV, 23-Dec-2022.)
|- ( A e. RR+ -> ( ( sqr ` A ) ^c 2 ) = A )
Theorem	cxprecd 16178	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	rpcxpmul2d 16179	Product of exponents law for complex exponentiation. Variation on cxpmul 16157 with more general conditions on A and B when C is a nonnegative integer. (Contributed by Mario Carneiro, 30-May-2016.)
|- ( ph -> A e. RR+ )   &    |- ( ph -> B e. CC )   &    |- ( ph -> C e. NN0 )   =>    |- ( ph -> ( A ^c ( B x. C ) ) = ( ( A ^c B ) ^ C ) )
Theorem	rpcxpcld 16180	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 16181	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 16182	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 16183	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 16184	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	cxpcom 16185	Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.)
|- ( ( A e. RR+ /\ B e. RR /\ C e. RR ) -> ( ( A ^c B ) ^c C ) = ( ( A ^c C ) ^c B ) )
Theorem	apcxp2 16186	Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.)
|- ( ( ( A e. RR+ /\ A # 1 ) /\ ( B e. RR /\ C e. RR ) ) -> ( B # C <-> ( A ^c B ) # ( A ^c C ) ) )
Theorem	rpabscxpbnd 16187	Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.)
|- ( ph -> A e. RR+ )   &    |- ( 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	efnthr 16188*	An equation involving an N-th power. The expression exp ( 2 pi _i / N ) is a way to write the primitive N-th root of unity with the smallest positive argument. We could write it as -u 1 ^c ( 2 / N ) except that we only support positive real numbers as the base for ^c. The converse is presumably also provable but we do not have a proof yet. (Contributed by Mario Carneiro, 23-Apr-2015.) (Revised by Jim Kingdon, 18-Sep-2026.)
|- ( ( A e. CC /\ N e. NN /\ B e. RR+ ) -> ( E. n e. ( 0 ... ( N - 1 ) ) A = ( ( B ^c ( 1 / N ) ) x. ( ( exp ` ( ( _i x. ( 2 x. pi ) ) / N ) ) ^ n ) ) -> ( A ^ N ) = B ) )
Theorem	ltexp2 16189	Ordering law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 5-Jun-2014.)
|- ( ( ( A e. RR /\ M e. ZZ /\ N e. ZZ ) /\ 1 < A ) -> ( M < N <-> ( A ^ M ) < ( A ^ N ) ) )
Theorem	ltexp2d 16190	Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
|- ( ph -> A e. RR )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. ZZ )   &    |- ( ph -> 1 < A )   =>    |- ( ph -> ( M < N <-> ( A ^ M ) < ( A ^ N ) ) )
11.2.4  Logarithms to an arbitrary base Define "log using an arbitrary base" function and then prove some of its properties. As with df-relog 16099 this is for real logarithms rather than complex logarithms. 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.
Syntax	clogb 16191	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 16192*	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 will only be useful where x is a positive real apart from one and where y is a positive real, so the choice of ( CC \ { 0 , 1 } ) and ( CC \ { 0 } ) is somewhat arbitrary (we adopt the definition used in set.mm). (Contributed by David A. Wheeler, 21-Jan-2017.)
|- logb = ( x e. ( CC \ { 0 , 1 } ) , y e. ( CC \ { 0 } ) |-> ( ( log ` y ) / ( log ` x ) ) )
Theorem	rplogbval 16193	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 Jim Kingdon, 3-Jul-2024.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR+ ) -> ( B logb X ) = ( ( log ` X ) / ( log ` B ) ) )
Theorem	rplogbcl 16194	General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR+ ) -> ( B logb X ) e. RR )
Theorem	rplogbid1 16195	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. RR+ /\ A # 1 ) -> ( A logb A ) = 1 )
Theorem	rplogb1 16196	The logarithm of 1 to an arbitrary base B is 0. Property 1(b) of [Cohen4] p. 361. See log1 16107. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Revised by Thierry Arnoux, 27-Sep-2017.)
|- ( ( B e. RR+ /\ B # 1 ) -> ( B logb 1 ) = 0 )
Theorem	rpelogb 16197	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. RR+ -> ( _e logb A ) = ( log ` A ) )
Theorem	rplogbchbase 16198	Change of base for logarithms. Property in [Cohen4] p. 367. (Contributed by AV, 11-Jun-2020.)
|- ( ( ( A e. RR+ /\ A # 1 ) /\ ( B e. RR+ /\ B # 1 ) /\ X e. RR+ ) -> ( A logb X ) = ( ( B logb X ) / ( B logb A ) ) )
Theorem	relogbval 16199	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	relogbzcl 16200	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 )