P. 153 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 15201-15300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	logdivlti 15201	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 15202	Closure of the natural logarithm function. (Contributed by Mario Carneiro, 29-May-2016.)
|- ( ph -> A e. RR+ )   =>    |- ( ph -> ( log ` A ) e. RR )
Theorem	reeflogd 15203	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 15204	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 15205	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 15206	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 15207	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 15208	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 15209	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 15210	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 15211	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 15212	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 15213	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	rpcxpef 15214	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 15215	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 15216	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 15217	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 15218	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 15219	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. RR+ -> ( A ^c 1 ) = A )
Theorem	1cxp 15220	Value of the complex power function at one. (Contributed by Mario Carneiro, 2-Aug-2014.)
|- ( A e. CC -> ( 1 ^c A ) = 1 )
Theorem	ecxp 15221	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 15222	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 15223	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 15224	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 15225	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 15226	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 15227	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 15228	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 15229	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 15230	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 15231	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 15232	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 15233	Product of exponents law for complex exponentiation. Variation on cxpmul 15232 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 15234	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	abscxp 15235	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 15236	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 15237	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 15238	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 15239	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 15240	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 15241	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 15242	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 15243	Logarithm of a square root. (Contributed by Mario Carneiro, 5-May-2016.)
|- ( A e. RR+ -> ( log ` ( sqr ` A ) ) = ( ( log ` A ) / 2 ) )
Theorem	rpcxp0d 15244	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 15245	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 15246	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 15247	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 15248	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 15249	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 15250	Square root theorem over the complex numbers for the complex power function. Compare with resqrtth 11213. (Contributed by AV, 23-Dec-2022.)
|- ( A e. RR+ -> ( ( sqr ` A ) ^c 2 ) = A )
Theorem	cxprecd 15251	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 15252	Product of exponents law for complex exponentiation. Variation on cxpmul 15232 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 15253	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 15254	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 15255	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 15256	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 15257	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 15258	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 15259	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 15260	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	ltexp2 15261	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 15262	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 15178 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 15263	Extend class notation to include the logarithm generalized to an arbitrary base.
class logb
Definition	df-logb 15264*	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 15265	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 15266	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 15267	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 15268	The logarithm of 1 to an arbitrary base B is 0. Property 1(b) of [Cohen4] p. 361. See log1 15186. (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 15269	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 15270	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 15271	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 15272	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	rplogbreexp 15273	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. RR+ /\ B # 1 ) /\ C e. RR+ /\ E e. RR ) -> ( B logb ( C ^c E ) ) = ( E x. ( B logb C ) ) )
Theorem	rplogbzexp 15274	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. RR+ /\ B # 1 ) /\ C e. RR+ /\ N e. ZZ ) -> ( B logb ( C ^ N ) ) = ( N x. ( B logb C ) ) )
Theorem	rprelogbmul 15275	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. RR+ /\ B # 1 ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A x. C ) ) = ( ( B logb A ) + ( B logb C ) ) )
Theorem	rprelogbmulexp 15276	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. RR+ /\ B # 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	rprelogbdiv 15277	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. RR+ /\ B # 1 ) /\ ( A e. RR+ /\ C e. RR+ ) ) -> ( B logb ( A / C ) ) = ( ( B logb A ) - ( B logb C ) ) )
Theorem	relogbexpap 15278	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 15279	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 15280	Logarithm of a reciprocal changes sign. 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 15281	The general logarithm function is monotone/increasing. See logleb 15195. (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 15282	The general logarithm function is strictly monotone/increasing. Property 2 of [Cohen4] p. 377. See logltb 15194. (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 ) ) )
Theorem	rplogbcxp 15283	Identity law for the general logarithm for real numbers. (Contributed by AV, 22-May-2020.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR ) -> ( B logb ( B ^c X ) ) = X )
Theorem	rpcxplogb 15284	Identity law for the general logarithm. (Contributed by AV, 22-May-2020.)
|- ( ( B e. RR+ /\ B # 1 /\ X e. RR+ ) -> ( B ^c ( B logb X ) ) = X )
Theorem	relogbcxpbap 15285	The logarithm is the inverse of the exponentiation. Observation in [Cohen4] p. 348. (Contributed by AV, 11-Jun-2020.)
|- ( ( ( B e. RR+ /\ B # 1 ) /\ X e. RR+ /\ Y e. RR ) -> ( ( B logb X ) = Y <-> ( B ^c Y ) = X ) )
Theorem	logbgt0b 15286	The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.)
|- ( ( A e. RR+ /\ ( B e. RR+ /\ 1 < B ) ) -> ( 0 < ( B logb A ) <-> 1 < A ) )
Theorem	logbgcd1irr 15287	The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, ( 2 logb 9 ) e. ( RR \ QQ ). (Contributed by AV, 29-Dec-2022.)
|- ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) /\ ( X gcd B ) = 1 ) -> ( B logb X ) e. ( RR \ QQ ) )
Theorem	logbgcd1irraplemexp 15288	Lemma for logbgcd1irrap 15290. Apartness of X ^ N and B ^ M. (Contributed by Jim Kingdon, 11-Jul-2024.)
|- ( ph -> X e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( X gcd B ) = 1 )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( X ^ N ) # ( B ^ M ) )
Theorem	logbgcd1irraplemap 15289	Lemma for logbgcd1irrap 15290. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.)
|- ( ph -> X e. ( ZZ>= ` 2 ) )   &    |- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> ( X gcd B ) = 1 )   &    |- ( ph -> M e. ZZ )   &    |- ( ph -> N e. NN )   =>    |- ( ph -> ( B logb X ) # ( M / N ) )
Theorem	logbgcd1irrap 15290	The logarithm of an integer greater than 1 to an integer base greater than 1 is irrational (in the sense of being apart from any rational number) if the argument and the base are relatively prime. For example, ( 2 logb 9 ) # Q where Q is rational. (Contributed by AV, 29-Dec-2022.)
|- ( ( ( X e. ( ZZ>= ` 2 ) /\ B e. ( ZZ>= ` 2 ) ) /\ ( ( X gcd B ) = 1 /\ Q e. QQ ) ) -> ( B logb X ) # Q )
Theorem	2logb9irr 15291	Example for logbgcd1irr 15287. The logarithm of nine to base two is not rational. Also see 2logb9irrap 15297 which says that it is irrational (in the sense of being apart from any rational number). (Contributed by AV, 29-Dec-2022.)
|- ( 2 logb 9 ) e. ( RR \ QQ )
Theorem	logbprmirr 15292	The logarithm of a prime to a different prime base is not rational. For example, ( 2 logb 3 ) e. ( RR \ QQ ) (see 2logb3irr 15293). (Contributed by AV, 31-Dec-2022.)
|- ( ( X e. Prime /\ B e. Prime /\ X =/= B ) -> ( B logb X ) e. ( RR \ QQ ) )
Theorem	2logb3irr 15293	Example for logbprmirr 15292. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.)
|- ( 2 logb 3 ) e. ( RR \ QQ )
Theorem	2logb9irrALT 15294	Alternate proof of 2logb9irr 15291: The logarithm of nine to base two is not rational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.)
|- ( 2 logb 9 ) e. ( RR \ QQ )
Theorem	sqrt2cxp2logb9e3 15295	The square root of two to the power of the logarithm of nine to base two is three. ( sqr ` 2 ) and ( 2 logb 9 ) are not rational (see sqrt2irr0 12357 resp. 2logb9irr 15291), satisfying the statement in 2irrexpq 15296. (Contributed by AV, 29-Dec-2022.)
|- ( ( sqr ` 2 ) ^c ( 2 logb 9 ) ) = 3
Theorem	2irrexpq 15296*	There exist real numbers a and b which are not rational such that ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named non-rational numbers ( sqr ` 2 ) and ( 2 logb 9 ), see sqrt2irr0 12357, 2logb9irr 15291 and sqrt2cxp2logb9e3 15295. Therefore, this proof is acceptable/usable in intuitionistic logic. For a theorem which is the same but proves that a and b are irrational (in the sense of being apart from any rational number), see 2irrexpqap 15298. (Contributed by AV, 23-Dec-2022.)
|- E. a e. ( RR \ QQ ) E. b e. ( RR \ QQ ) ( a ^c b ) e. QQ
Theorem	2logb9irrap 15297	Example for logbgcd1irrap 15290. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.)
|- ( Q e. QQ -> ( 2 logb 9 ) # Q )
Theorem	2irrexpqap 15298*	There exist real numbers a and b which are irrational (in the sense of being apart from any rational number) such that ( a ^ b ) is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers ( sqr ` 2 ) and ( 2 logb 9 ), see sqrt2irrap 12373, 2logb9irrap 15297 and sqrt2cxp2logb9e3 15295. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.)
|- E. a e. RR E. b e. RR ( A. p e. QQ a # p /\ A. q e. QQ b # q /\ ( a ^c b ) e. QQ )
11.2.5  Quartic binomial expansion
Theorem	binom4 15299	Work out a quartic binomial. (You would think that by this point it would be faster to use binom 11666, but it turns out to be just as much work to put it into this form after clearing all the sums and calculating binomial coefficients.) (Contributed by Mario Carneiro, 6-May-2015.)
|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 4 ) = ( ( ( A ^ 4 ) + ( 4 x. ( ( A ^ 3 ) x. B ) ) ) + ( ( 6 x. ( ( A ^ 2 ) x. ( B ^ 2 ) ) ) + ( ( 4 x. ( A x. ( B ^ 3 ) ) ) + ( B ^ 4 ) ) ) ) )
11.3  Basic number theory
11.3.1  Wilson's theorem
Theorem	wilthlem1 15300	The only elements that are equal to their own inverses in the multiplicative group of nonzero elements in ZZ / P ZZ are 1 and -u 1 == P - 1. (Note that from prmdiveq 12429, ( N ^ ( P - 2 ) ) mod P is the modular inverse of N in ZZ / P ZZ. (Contributed by Mario Carneiro, 24-Jan-2015.)
|- ( ( P e. Prime /\ N e. ( 1 ... ( P - 1 ) ) ) -> ( N = ( ( N ^ ( P - 2 ) ) mod P ) <-> ( N = 1 \/ N = ( P - 1 ) ) ) )