P. 334 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33301-33400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	zlmodzxzldeplem1 33301	Lemma 1 for zlmodzxzldep 33305. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- F e. ( ZZ ^m { A , B } )
Theorem	zlmodzxzldeplem2 33302	Lemma 2 for zlmodzxzldep 33305. (Contributed by AV, 24-May-2019.) (Revised by AV, 30-Jul-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- F finSupp 0
Theorem	zlmodzxzldeplem3 33303	Lemma 3 for zlmodzxzldep 33305. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- ( F ( linC ` Z ) { A , B } ) = ( 0g ` Z )
Theorem	zlmodzxzldeplem4 33304*	Lemma 4 for zlmodzxzldep 33305. (Contributed by AV, 24-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   &    |- F = { <. A , 2 >. , <. B , -u 3 >. }   =>    |- E. y e. { A , B } ( F ` y ) =/= 0
Theorem	zlmodzxzldep 33305	{ A , B } is a linearly dependent set within the ZZ-module ZZ X. ZZ (see example in [Roman] p. 112). (Contributed by AV, 22-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- { A , B } linDepS Z
Theorem	ldepsnlinclem1 33306	Lemma 1 for ldepsnlinc 33309. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- ( F e. ( ( Base ` ℤring ) ^m { B } ) -> ( F ( linC ` Z ) { B } ) =/= A )
Theorem	ldepsnlinclem2 33307	Lemma 2 for ldepsnlinc 33309. (Contributed by AV, 25-May-2019.) (Revised by AV, 10-Jun-2019.)
|- Z = (ℤring freeLMod { 0 , 1 } )   &    |- A = { <. 0 , 3 >. , <. 1 , 6 >. }   &    |- B = { <. 0 , 2 >. , <. 1 , 4 >. }   =>    |- ( F e. ( ( Base ` ℤring ) ^m { A } ) -> ( F ( linC ` Z ) { A } ) =/= B )
21.25.12.5  Differences between (left) modules and (left) vector spaces
Theorem	lvecpsslmod 33308	The class of all (left) vector spaces is a proper subclass of the class of all (left) modules. Although it is obvious (and proven by lveclmod 17865) that every left vector space is a left module, there is (at least) one left module which is no left vector space, for example the zero module over the zero ring, see lmod1zrnlvec 33295. (Contributed by AV, 29-Apr-2019.)
|- LVec C. LMod
Theorem	ldepsnlinc 33309*	The reverse implication of islindeps2 33284 does not hold for arbitrary (left) modules, see note in [Roman] p. 112: "... if a nontrivial linear combination of the elements ... in an R-module M is 0, ... where not all of the coefficients are 0, then we cannot conclude ... that one of the elements ... is a linear combination of the others." This means that there is at least one left module having a linearly dependent subset in which there is at least one element which is not a linear combinantion of the other elements of this subset. Such a left module can be constructed by using zlmodzxzequa 33297 and zlmodzxznm 33298 (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
|- E. m e. LMod E. s e. ~P ( Base ` m ) ( s linDepS m /\ A. v e. s A. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) -> ( f ( linC ` m ) ( s \ { v } ) ) =/= v ) )
Theorem	ldepslinc 33310*	For (left) vector spaces, isldepslvec2 33286 provides an alternative definition of being a linearly dependent subset, whereas ldepsnlinc 33309 indicates that there is not an analogous alternative definition for arbitrary (left) modules. (Contributed by AV, 25-May-2019.) (Revised by AV, 30-Jul-2019.)
|- ( A. m e. LVec A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) /\ -. A. m e. LMod A. s e. ~P ( Base ` m ) ( s linDepS m <-> E. v e. s E. f e. ( ( Base ` (Scalar ` m ) ) ^m ( s \ { v } ) ) ( f finSupp ( 0g ` (Scalar ` m ) ) /\ ( f ( linC ` m ) ( s \ { v } ) ) = v ) ) )
21.25.13  Complexity theory
21.25.13.1  Auxiliary theorems
Theorem	offval0 33311*	Value of an operation applied to two functions. (Contributed by AV, 15-May-2020.)
|- ( ( F e. V /\ G e. W ) -> ( F oF R G ) = ( x e. ( dom F i^i dom G ) |-> ( ( F ` x ) R ( G ` x ) ) ) )
Theorem	suppdm 33312	If the range of a function does not contain the zero, the support of the function equals its domain. (Contributed by AV, 20-May-2020.)
|- ( ( ( Fun F /\ F e. V /\ Z e. W ) /\ Z e/ ran F ) -> ( F supp Z ) = dom F )
Theorem	eluz2gt1 33313	An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.)
|- ( N e. ( ZZ>= ` 2 ) -> 1 < N )
Theorem	eluz2n0 33314	An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.)
|- ( N e. ( ZZ>= ` 2 ) -> N =/= 0 )
Theorem	eluz2cnn0n1 33315	An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.)
|- ( B e. ( ZZ>= ` 2 ) -> B e. ( CC \ { 0 , 1 } ) )
Theorem	divge1b 33316	The ratio of a real number to a positive real number is greater than or equal to 1 iff the divisor (the positive real number) is less than or equal to the dividend (the real number). (Contributed by AV, 26-May-2020.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( A <_ B <-> 1 <_ ( B / A ) ) )
Theorem	divgt1b 33317	The ratio of a real number to a positive real number is greater than 1 iff the divisor (the positive real number) is less than the dividend (the real number). (Contributed by AV, 30-May-2020.)
|- ( ( A e. RR+ /\ B e. RR ) -> ( A < B <-> 1 < ( B / A ) ) )
Theorem	divlt1lt 33318	A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) < 1 <-> A < B ) )
Theorem	ltsubaddb 33319	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> ( A + D ) < ( B + C ) ) )
Theorem	ltsubsubb 33320	Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( A - C ) < ( B - D ) <-> ( A - B ) < ( C - D ) ) )
Theorem	ltsubadd2b 33321	Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. RR /\ D e. RR ) ) -> ( ( D - C ) < ( B - A ) <-> ( A + D ) < ( B + C ) ) )
Theorem	divsub1dir 33322	Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.)
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) - 1 ) = ( ( A - B ) / B ) )
Theorem	expnegico01 33323	An integer greater than 1 to the power of a negative integer is in the closed-below, open-above interval between 0 and 1. (Contributed by AV, 24-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ N < 0 ) -> ( B ^ N ) e. ( 0 [,) 1 ) )
Theorem	nn0rp0 33324	A nonnegative integer is a nonnegative real number. (Contributed by AV, 24-May-2020.)
|- ( N e. NN0 -> N e. ( 0 [,) +oo ) )
Theorem	elfzolborelfzop1 33325	An element of a half-open integer interval is either equal to the left bound of the interval or an element of a half-open integer interval with a left bound increased by 1. (Contributed by AV, 2-Jun-2020.)
|- ( K e. ( M..^ N ) -> ( K = M \/ K e. ( ( M + 1 )..^ N ) ) )
Theorem	3halfnz 33326	Three halfs is not an integer. (Contributed by AV, 2-Jun-2020.)
|- -. ( 3 / 2 ) e. ZZ
Theorem	pw2m1lepw2m1 33327	2 to the power of a positive integer decreased by 1 is less than or equal to 2 to the power of the integer minus 1. (Contributed by AV, 30-May-2020.)
|- ( I e. NN -> ( 2 ^ ( I - 1 ) ) <_ ( ( 2 ^ I ) - 1 ) )
Theorem	zgeltp1eq 33328	If an integer is between another integer and its successor, the integer is equal to the other integer. (Contributed by AV, 30-May-2020.)
|- ( ( I e. ZZ /\ A e. ZZ ) -> ( ( A <_ I /\ I < ( A + 1 ) ) -> I = A ) )
Theorem	zgtp1leeq 33329	If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.)
|- ( ( I e. ZZ /\ A e. ZZ ) -> ( ( ( A - 1 ) < I /\ I <_ A ) -> I = A ) )
Theorem	flsubz 33330	An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.)
|- ( ( A e. RR /\ N e. ZZ ) -> ( |_ ` ( A - N ) ) = ( ( |_ ` A ) - N ) )
21.25.13.2  The modulo (remainder) operation (extension)
Theorem	fldivmod 33331	Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) = ( ( A - ( A mod B ) ) / B ) )
Theorem	mod0mul 33332*	If an integer is 0 modulo a positive integer, this integer must be the product of another integer and the modulus. (Contributed by AV, 7-Jun-2020.)
|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) = 0 -> E. x e. ZZ A = ( x x. N ) ) )
Theorem	modn0mul 33333*	If an integer is not 0 modulo a positive integer, this integer must be the sum of the product of another integer and the modulus and a positive integer less than the modulus. (Contributed by AV, 7-Jun-2020.)
|- ( ( A e. ZZ /\ N e. NN ) -> ( ( A mod N ) =/= 0 -> E. x e. ZZ E. y e. ( 1..^ N ) A = ( ( x x. N ) + y ) ) )
Theorem	m1modmmod 33334	An integer decreased by 1 modulo a positive integer minus the integer modulo the same modulus is either -1 or the modulus minus 1. (Contributed by AV, 7-Jun-2020.)
|- ( ( A e. ZZ /\ N e. NN ) -> ( ( ( A - 1 ) mod N ) - ( A mod N ) ) = if ( ( A mod N ) = 0 , ( N - 1 ) , -u 1 ) )
Theorem	difmodm1lt 33335	The difference between an integer modulo a positive integer and the integer decreased by 1 modulo the same modulus is less than the modulus decreased by 1 (if the modulus is greater than 2). This theorem would not be valid for an odd A and N = 2, since ( ( A mod N ) - ( ( A - 1 ) mod N ) ) would be ( 1 - 0 ) = 1 which is not less than ( N - 1 ) = 1. (Contributed by AV, 6-Jun-2012.)
|- ( ( A e. ZZ /\ N e. NN /\ 2 < N ) -> ( ( A mod N ) - ( ( A - 1 ) mod N ) ) < ( N - 1 ) )
21.25.13.3  Even and odd integers
Theorem	nn0enne 33336	A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.)
|- ( N e. NN -> ( ( N / 2 ) e. NN0 <-> ( N / 2 ) e. NN ) )
Theorem	nn0o1gt2 33337	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( N = 1 \/ 2 < N ) )
Theorem	nno 33338	An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.)
|- ( ( N e. ( ZZ>= ` 2 ) /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN )
Theorem	nn0o 33339	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( ( N - 1 ) / 2 ) e. NN0 )
Theorem	nn0ob 33340	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
|- ( N e. NN0 -> ( ( ( N + 1 ) / 2 ) e. NN0 <-> ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	nn0onn0ex 33341*	For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> E. m e. NN0 N = ( ( 2 x. m ) + 1 ) )
Theorem	nn0enn0ex 33342*	For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.)
|- ( ( N e. NN0 /\ ( N / 2 ) e. NN0 ) -> E. m e. NN0 N = ( 2 x. m ) )
Theorem	nneop 33343	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N + 1 ) / 2 ) e. NN ) )
Theorem	nneom 33344	A positive integer is even or odd. (Contributed by AV, 30-May-2020.)
|- ( N e. NN -> ( ( N / 2 ) e. NN \/ ( ( N - 1 ) / 2 ) e. NN0 ) )
Theorem	nn0eo 33345	A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.)
|- ( N e. NN0 -> ( ( N / 2 ) e. NN0 \/ ( ( N + 1 ) / 2 ) e. NN0 ) )
Theorem	nnpw2even 33346	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.)
|- ( N e. NN -> ( ( 2 ^ N ) / 2 ) e. NN )
Theorem	zefldiv2 33347	The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.)
|- ( ( N e. ZZ /\ ( N / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( N / 2 ) )
Theorem	zofldiv2 33348	The floor of an odd integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.)
|- ( ( N e. ZZ /\ ( ( N + 1 ) / 2 ) e. ZZ ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
Theorem	nn0ofldiv2 33349	The floor of an odd nonnegative integer divided by 2 is equal to the integer first decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.) (Proof shortened by AV, 7-Jun-2020.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( ( N - 1 ) / 2 ) )
Theorem	flnn0div2ge 33350	The floor of a positive integer divided by 2 is greater than or equal to the integer decreased by 1 and then divided by 2. (Contributed by AV, 1-Jun-2020.)
|- ( N e. NN0 -> ( ( N - 1 ) / 2 ) <_ ( |_ ` ( N / 2 ) ) )
Theorem	flnn0ohalf 33351	The floor of the half of an odd positive integer is equal to the floor of the half of the integer decreased by 1. (Contributed by AV, 5-Jun-2012.)
|- ( ( N e. NN0 /\ ( ( N + 1 ) / 2 ) e. NN0 ) -> ( |_ ` ( N / 2 ) ) = ( |_ ` ( ( N - 1 ) / 2 ) ) )
21.25.13.4  The natural logarithm on complex numbers (extension)
Theorem	logge0b 33352	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 33353	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 33354	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 33355	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	logcxp0 33356	Logarithm of a complex power. Generalisation of logcxp 23137. (Contributed by AV, 22-May-2020.)
|- ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )
Theorem	regt1loggt0 33357	The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.)
|- ( B e. ( 1 (,) +oo ) -> 0 < ( log ` B ) )
21.25.13.5  Division of functions
Syntax	cfdiv 33358	Extend class notation with the division operator of two functions.
class /_f
Definition	df-fdiv 33359*	Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
|- /_f = ( f e. _V , g e. _V |-> ( ( f oF / g ) |` ( g supp 0 ) ) )
Theorem	fdivval 33360	The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.)
|- ( ( F e. V /\ G e. W ) -> ( F /_f G ) = ( ( F oF / G ) |` ( G supp 0 ) ) )
Theorem	fdivmpt 33361*	The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.)
|- ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) = ( x e. ( G supp 0 ) |-> ( ( F ` x ) / ( G ` x ) ) ) )
Theorem	fdivmptf 33362	The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.)
|- ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> CC )
Theorem	refdivmptf 33363	The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.)
|- ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F /_f G ) : ( G supp 0 ) --> RR )
Theorem	fdivpm 33364	The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.)
|- ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) -> ( F /_f G ) e. ( CC ^pm A ) )
Theorem	refdivpm 33365	The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.)
|- ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) -> ( F /_f G ) e. ( RR ^pm A ) )
Theorem	fdivmptfv 33366	The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.)
|- ( ( ( F : A --> CC /\ G : A --> CC /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F /_f G ) ` X ) = ( ( F ` X ) / ( G ` X ) ) )
Theorem	refdivmptfv 33367	The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.)
|- ( ( ( F : A --> RR /\ G : A --> RR /\ A e. V ) /\ X e. ( G supp 0 ) ) -> ( ( F /_f G ) ` X ) = ( ( F ` X ) / ( G ` X ) ) )
21.25.13.6  Upper bounds
Syntax	cbigo 33368	Extend class notation with the class of the "big-O" function.
class _O
Definition	df-bigo 33369*	Define the function "big-O", mapping a real function g to the set of real functions "of order g(x)". Definition in section 1.1 of [AhoHopUll] p. 2. This is a generalisation of "big-O of one", see df-o1 13315 and df-lo1 13316. As explained in the comment of df-o1 , any big-O can be represented in terms of O(1) and division, see elbigolo1 33378. (Contributed by AV, 15-May-2020.)
|- _O = ( g e. ( RR ^pm RR ) |-> { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( g ` y ) ) } )
Theorem	bigoval 33370*	Set of functions of order G(x). (Contributed by AV, 15-May-2020.)
|- ( G e. ( RR ^pm RR ) -> (_O ` G ) = { f e. ( RR ^pm RR ) | E. x e. RR E. m e. RR A. y e. ( dom f i^i ( x [,) +oo ) ) ( f ` y ) <_ ( m x. ( G ` y ) ) } )
Theorem	elbigofrcl 33371	Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.)
|- ( F e. (_O ` G ) -> G e. ( RR ^pm RR ) )
Theorem	elbigo 33372*	Properties of a function of order G(x). (Contributed by AV, 16-May-2020.)
|- ( F e. (_O ` G ) <-> ( F e. ( RR ^pm RR ) /\ G e. ( RR ^pm RR ) /\ E. x e. RR E. m e. RR A. y e. ( dom F i^i ( x [,) +oo ) ) ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
Theorem	elbigo2 33373*	Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.)
|- ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) ) -> ( F e. (_O ` G ) <-> E. x e. RR E. m e. RR A. y e. B ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) ) )
Theorem	elbigo2r 33374*	Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.)
|- ( ( ( G : A --> RR /\ A C_ RR ) /\ ( F : B --> RR /\ B C_ A ) /\ ( C e. RR /\ M e. RR /\ A. x e. B ( C <_ x -> ( F ` x ) <_ ( M x. ( G ` x ) ) ) ) ) -> F e. (_O ` G ) )
Theorem	elbigof 33375	A function of order G(x) is a function. (Contributed by AV, 18-May-2020.)
|- ( F e. (_O ` G ) -> F : dom F --> RR )
Theorem	elbigodm 33376	The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.)
|- ( F e. (_O ` G ) -> dom F C_ RR )
Theorem	elbigoimp 33377*	The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.)
|- ( ( F e. (_O ` G ) /\ F : A --> RR /\ A C_ dom G ) -> E. x e. RR E. m e. RR A. y e. A ( x <_ y -> ( F ` y ) <_ ( m x. ( G ` y ) ) ) )
Theorem	elbigolo1 33378	A function (into the positive reals) is of order G(x) iff the quotient of the function and G(x) (also a function into the positive reals) is an eventually upper bounded function. (Contributed by AV, 20-May-2020.)
|- ( ( A C_ RR /\ G : A --> RR+ /\ F : A --> RR+ ) -> ( F e. (_O ` G ) <-> ( F /_f G ) e. <_O(1) ) )
21.25.13.7  Logarithm to an arbitrary base (extension)
Theorem	rege1logbrege0 33379	The general logarithm, with a real base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
|- ( ( B e. ( 1 (,) +oo ) /\ X e. ( 1 [,) +oo ) ) -> 0 <_ ( B logb X ) )
Theorem	rege1logbzge0 33380	The general logarithm, with an integer base greater than 1, for a real number greater than or equal to 1 is greater than or equal to 0. (Contributed by AV, 25-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. ( 1 [,) +oo ) ) -> 0 <_ ( B logb X ) )
Theorem	fllogbd 33381	A real number is between the base of a logarithm to the power of the floor of the logarithm of the number and the base of the logarithm to the power of the floor of the logarithm of the number plus one. (Contributed by AV, 23-May-2020.)
|- ( ph -> B e. ( ZZ>= ` 2 ) )   &    |- ( ph -> X e. RR+ )   &    |- E = ( |_ ` ( B logb X ) )   =>    |- ( ph -> ( ( B ^ E ) <_ X /\ X < ( B ^ ( E + 1 ) ) ) )
Theorem	relogbmulbexp 33382	The logarithm of the product of a positive real number and the base to the power of a real number is the logarithm of the positive real number plus the real number. (Contributed by AV, 29-May-2020.)
|- ( ( B e. ( RR+ \ { 1 } ) /\ ( A e. RR+ /\ C e. RR ) ) -> ( B logb ( A x. ( B ^c C ) ) ) = ( ( B logb A ) + C ) )
Theorem	relogbdivb 33383	The logarithm of the quotient of a positive real number and the base is the logarithm of the number minus 1. (Contributed by AV, 29-May-2020.)
|- ( ( B e. ( RR+ \ { 1 } ) /\ A e. RR+ ) -> ( B logb ( A / B ) ) = ( ( B logb A ) - 1 ) )
Theorem	logbge0b 33384	The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( 0 <_ ( B logb X ) <-> 1 <_ X ) )
Theorem	logblt1b 33385	The logarithm of a number is less than 1 iff the number is less than the base of the logarithm. (Contributed by AV, 30-May-2020.)
|- ( ( B e. ( ZZ>= ` 2 ) /\ X e. RR+ ) -> ( ( B logb X ) < 1 <-> X < B ) )
21.25.13.8  The binary logarithm If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g. log2 = ( x e. ( CC \ { 0 } ) |-> ( 2 logb X ) ). Then we can write "( log2 ` x )" (analogous to ( log x ) for the natural logarithm) instead of ( 2 logb x ).
Theorem	fldivexpfllog2 33386	The floor of a positive real number divided by 2 to the power of the floor of the logarithm to base 2 of the number is 1. (Contributed by AV, 26-May-2020.)
|- ( X e. RR+ -> ( |_ ` ( X / ( 2 ^ ( |_ ` ( 2 logb X ) ) ) ) ) = 1 )
Theorem	nnlog2ge0lt1 33387	A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020.)
|- ( N e. NN -> ( N = 1 <-> ( 0 <_ ( 2 logb N ) /\ ( 2 logb N ) < 1 ) ) )
Theorem	logbpw2m1 33388	The floor of the binary logarithm of 2 to the power of a positive integer minus 1 is equal to the integer minus 1. (Contributed by AV, 31-May-2020.)
|- ( I e. NN -> ( |_ ` ( 2 logb ( ( 2 ^ I ) - 1 ) ) ) = ( I - 1 ) )
Theorem	fllog2 33389	The floor of the binary logarithm of 2 to the power of an element of a half-open integer interval bounded by powers of 2 is equal to the integer. (Contributed by AV, 31-May-2020.)
|- ( ( I e. NN0 /\ N e. ( ( 2 ^ I )..^ ( 2 ^ ( I + 1 ) ) ) ) -> ( |_ ` ( 2 logb N ) ) = I )
21.25.13.9  Binary length
Syntax	cblen 33390	Extend class notation with the class of the binary length function.
class #b
Definition	df-blen 33391	Define the binary length of an integer. Definition in section 1.3 of [AhoHopUll] p. 12. Although not restricted to integers, this definition is only meaningful for n e. ZZ or even for n e. CC. (Contributed by AV, 16-May-2020.)
|- #b = ( n e. _V |-> if ( n = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` n ) ) ) + 1 ) ) )
Theorem	blenval 33392	The binary length of an integer. (Contributed by AV, 20-May-2020.)
|- ( N e. V -> (#b ` N ) = if ( N = 0 , 1 , ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) ) )
Theorem	blen0 33393	The binary length of 0. (Contributed by AV, 20-May-2020.)
|- (#b ` 0 ) = 1
Theorem	blenn0 33394	The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.)
|- ( ( N e. V /\ N =/= 0 ) -> (#b ` N ) = ( ( |_ ` ( 2 logb ( abs ` N ) ) ) + 1 ) )
Theorem	blenre 33395	The binary length of a positive real number. (Contributed by AV, 20-May-2020.)
|- ( N e. RR+ -> (#b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
Theorem	blennn 33396	The binary length of a positive integer. (Contributed by AV, 21-May-2020.)
|- ( N e. NN -> (#b ` N ) = ( ( |_ ` ( 2 logb N ) ) + 1 ) )
Theorem	blennnelnn 33397	The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.)
|- ( N e. NN -> (#b ` N ) e. NN )
Theorem	blennn0elnn 33398	The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.)
|- ( N e. NN0 -> (#b ` N ) e. NN )
Theorem	blenpw2 33399	The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020.)
|- ( I e. NN0 -> (#b ` ( 2 ^ I ) ) = ( I + 1 ) )
Theorem	blenpw2m1 33400	The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.)
|- ( I e. NN -> (#b ` ( ( 2 ^ I ) - 1 ) ) = I )