Home | Metamath
Proof Explorer Theorem List (p. 424 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eluz2cnn0n1 42301 | An integer greater than 1 is a complex number not equal to 0 or 1. (Contributed by AV, 23-May-2020.) |
Theorem | divge1b 42302 | 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.) |
Theorem | divgt1b 42303 | 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.) |
Theorem | ltsubaddb 42304 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
Theorem | ltsubsubb 42305 | Equivalence for the "less than" relation between differences. (Contributed by AV, 6-Jun-2020.) |
Theorem | ltsubadd2b 42306 | Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020.) |
Theorem | divsub1dir 42307 | Distribution of division over subtraction by 1. (Contributed by AV, 6-Jun-2020.) |
Theorem | expnegico01 42308 | 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.) |
Theorem | elfzolborelfzop1 42309 | 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 lower bound increased by 1. (Contributed by AV, 2-Jun-2020.) |
..^ ..^ | ||
Theorem | pw2m1lepw2m1 42310 | 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.) |
Theorem | zgtp1leeq 42311 | If an integer is between another integer and its predecessor, the integer is equal to the other integer. (Contributed by AV, 7-Jun-2020.) |
Theorem | flsubz 42312 | An integer can be moved in and out of the floor of a difference. (Contributed by AV, 29-May-2020.) |
Theorem | fldivmod 42313 | Expressing the floor of a division by the modulo operator. (Contributed by AV, 6-Jun-2020.) |
Theorem | mod0mul 42314* | 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.) |
Theorem | modn0mul 42315* | 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.) |
..^ | ||
Theorem | m1modmmod 42316 | 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.) |
Theorem | difmodm1lt 42317 | 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 and , since would be which is not less than . (Contributed by AV, 6-Jun-2012.) |
Theorem | nn0onn0ex 42318* | 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.) |
Theorem | nn0enn0ex 42319* | 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.) |
Theorem | nneop 42320 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
Theorem | nneom 42321 | A positive integer is even or odd. (Contributed by AV, 30-May-2020.) |
Theorem | nn0eo 42322 | A nonnegative integer is even or odd. (Contributed by AV, 27-May-2020.) |
Theorem | nnpw2even 42323 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) |
Theorem | zefldiv2 42324 | The floor of an even integer divided by 2 is equal to the integer divided by 2. (Contributed by AV, 7-Jun-2020.) |
Theorem | zofldiv2 42325 | 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.) |
Theorem | nn0ofldiv2 42326 | 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.) |
Theorem | flnn0div2ge 42327 | 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.) |
Theorem | flnn0ohalf 42328 | 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.) |
Theorem | logcxp0 42329 | Logarithm of a complex power. Generalisation of logcxp 24415. (Contributed by AV, 22-May-2020.) |
Theorem | regt1loggt0 42330 | The natural logarithm for a real number greater than 1 is greater than 0. (Contributed by AV, 25-May-2020.) |
Syntax | cfdiv 42331 | Extend class notation with the division operator of two functions. |
/_f | ||
Definition | df-fdiv 42332* | Define the division of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
/_f supp | ||
Theorem | fdivval 42333 | The quotient of two functions into the complex numbers. (Contributed by AV, 15-May-2020.) |
/_f supp | ||
Theorem | fdivmpt 42334* | The quotient of two functions into the complex numbers as mapping. (Contributed by AV, 16-May-2020.) |
/_f supp | ||
Theorem | fdivmptf 42335 | The quotient of two functions into the complex numbers is a function into the complex numbers. (Contributed by AV, 16-May-2020.) |
/_f supp | ||
Theorem | refdivmptf 42336 | The quotient of two functions into the real numbers is a function into the real numbers. (Contributed by AV, 16-May-2020.) |
/_f supp | ||
Theorem | fdivpm 42337 | The quotient of two functions into the complex numbers is a partial function. (Contributed by AV, 16-May-2020.) |
/_f | ||
Theorem | refdivpm 42338 | The quotient of two functions into the real numbers is a partial function. (Contributed by AV, 16-May-2020.) |
/_f | ||
Theorem | fdivmptfv 42339 | The function value of a quotient of two functions into the complex numbers. (Contributed by AV, 19-May-2020.) |
supp /_f | ||
Theorem | refdivmptfv 42340 | The function value of a quotient of two functions into the real numbers. (Contributed by AV, 19-May-2020.) |
supp /_f | ||
Syntax | cbigo 42341 | Extend class notation with the class of the "big-O" function. |
_O | ||
Definition | df-bigo 42342* | 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 14221 and df-lo1 14222. As explained in the comment of df-o1 , any big-O can be represented in terms of and division, see elbigolo1 42351. (Contributed by AV, 15-May-2020.) |
_O | ||
Theorem | bigoval 42343* | Set of functions of order G(x). (Contributed by AV, 15-May-2020.) |
_O | ||
Theorem | elbigofrcl 42344 | Reverse closure of the "big-O" function. (Contributed by AV, 16-May-2020.) |
_O | ||
Theorem | elbigo 42345* | Properties of a function of order G(x). (Contributed by AV, 16-May-2020.) |
_O | ||
Theorem | elbigo2 42346* | Properties of a function of order G(x) under certain assumptions. (Contributed by AV, 17-May-2020.) |
_O | ||
Theorem | elbigo2r 42347* | Sufficient condition for a function to be of order G(x). (Contributed by AV, 18-May-2020.) |
_O | ||
Theorem | elbigof 42348 | A function of order G(x) is a function. (Contributed by AV, 18-May-2020.) |
_O | ||
Theorem | elbigodm 42349 | The domain of a function of order G(x) is a subset of the reals. (Contributed by AV, 18-May-2020.) |
_O | ||
Theorem | elbigoimp 42350* | The defining property of a function of order G(x). (Contributed by AV, 18-May-2020.) |
_O | ||
Theorem | elbigolo1 42351 | 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.) |
_O /_f | ||
Theorem | rege1logbrege0 42352 | 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.) |
logb | ||
Theorem | rege1logbzge0 42353 | 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.) |
logb | ||
Theorem | fllogbd 42354 | 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.) |
logb | ||
Theorem | relogbmulbexp 42355 | 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.) |
logb logb | ||
Theorem | relogbdivb 42356 | 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.) |
logb logb | ||
Theorem | logbge0b 42357 | The logarithm of a number is nonnegative iff the number is greater than or equal to 1. (Contributed by AV, 30-May-2020.) |
logb | ||
Theorem | logblt1b 42358 | 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.) |
logb | ||
If the binary logarithm is used more often, a separate symbol/definition could be provided for it, e.g. log2 = logb . Then we can write "( log2 ` x )" (analogous to for the natural logarithm) instead of logb . | ||
Theorem | fldivexpfllog2 42359 | 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.) |
logb | ||
Theorem | nnlog2ge0lt1 42360 | A positive integer is 1 iff its binary logarithm is between 0 and 1. (Contributed by AV, 30-May-2020.) |
logb logb | ||
Theorem | logbpw2m1 42361 | 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.) |
logb | ||
Theorem | fllog2 42362 | 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.) |
..^ logb | ||
Syntax | cblen 42363 | Extend class notation with the class of the binary length function. |
#b | ||
Definition | df-blen 42364 | 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 or even for . (Contributed by AV, 16-May-2020.) |
#b logb | ||
Theorem | blenval 42365 | The binary length of an integer. (Contributed by AV, 20-May-2020.) |
#b logb | ||
Theorem | blen0 42366 | The binary length of 0. (Contributed by AV, 20-May-2020.) |
#b | ||
Theorem | blenn0 42367 | The binary length of a "number" not being 0. (Contributed by AV, 20-May-2020.) |
#b logb | ||
Theorem | blenre 42368 | The binary length of a positive real number. (Contributed by AV, 20-May-2020.) |
#b logb | ||
Theorem | blennn 42369 | The binary length of a positive integer. (Contributed by AV, 21-May-2020.) |
#b logb | ||
Theorem | blennnelnn 42370 | The binary length of a positive integer is a positive integer. (Contributed by AV, 25-May-2020.) |
#b | ||
Theorem | blennn0elnn 42371 | The binary length of a nonnegative integer is a positive integer. (Contributed by AV, 28-May-2020.) |
#b | ||
Theorem | blenpw2 42372 | The binary length of a power of 2 is the exponent plus 1. (Contributed by AV, 30-May-2020.) |
#b | ||
Theorem | blenpw2m1 42373 | The binary length of a power of 2 minus 1 is the exponent. (Contributed by AV, 31-May-2020.) |
#b | ||
Theorem | nnpw2blen 42374 | A positive integer is between 2 to the power of its binary length minus 1 and 2 to the power of its binary length. (Contributed by AV, 31-May-2020.) |
#b #b | ||
Theorem | nnpw2blenfzo 42375 | A positive integer is between 2 to the power of the binary length of the integer minus 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.) |
#b ..^#b | ||
Theorem | nnpw2blenfzo2 42376 | A positive integer is either 2 to the power of the binary length of the integer minus 1, or between 2 to the power of the binary length of the integer minus 1, increased by 1, and 2 to the power of the binary length of the integer. (Contributed by AV, 2-Jun-2020.) |
#b #b ..^#b | ||
Theorem | nnpw2pmod 42377 | Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
#b #b | ||
Theorem | blen1 42378 | The binary length of 1. (Contributed by AV, 21-May-2020.) |
#b | ||
Theorem | blen2 42379 | The binary length of 2. (Contributed by AV, 21-May-2020.) |
#b | ||
Theorem | nnpw2p 42380* | Every positive integer can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
..^ | ||
Theorem | nnpw2pb 42381* | A number is a positive integer iff it can be represented as the sum of a power of 2 and a "remainder" smaller than the power. (Contributed by AV, 31-May-2020.) |
..^ | ||
Theorem | blen1b 42382 | The binary length of a nonnegative integer is 1 if the integer is 0 or 1. (Contributed by AV, 30-May-2020.) |
#b | ||
Theorem | blennnt2 42383 | The binary length of a positive integer, doubled and increased by 1, is the binary length of the integer plus 1. (Contributed by AV, 30-May-2010.) |
#b #b | ||
Theorem | nnolog2flm1 42384 | The floor of the binary logarithm of an odd integer greater than 1 is the floor of the binary logarithm of the integer decreased by 1. (Contributed by AV, 2-Jun-2020.) |
logb logb | ||
Theorem | blennn0em1 42385 | The binary length of the half of an even positive integer is the binary length of the integer minus 1. (Contributed by AV, 30-May-2010.) |
#b #b | ||
Theorem | blennngt2o2 42386 | The binary length of an odd integer greater than 1 is the binary length of the half of the integer decreased by 1, increased by 1. (Contributed by AV, 3-Jun-2020.) |
#b #b | ||
Theorem | blengt1fldiv2p1 42387 | The binary length of an integer greater than 1 is the binary length of the integer divided by 2, increased by one. (Contributed by AV, 3-Jun-2020.) |
#b #b | ||
Theorem | blennn0e2 42388 | The binary length of an even positive integer is the binary length of the half of the integer, increased by 1. (Contributed by AV, 29-May-2020.) |
#b #b | ||
Generalisation of df-bits 15144. In contrast to digit, bits are defined for integers only. The equivalence of both definitions for integers is shown in dig2bits 42408: digit 2 ) N ) = 1 <-> K e. ( bits . | ||
Syntax | cdig 42389 | Extend class notation with the class of the digit extraction operation. |
digit | ||
Definition | df-dig 42390* | Definition of an operation to obtain the th digit of a nonnegative real number in the positional system with base . corresponds to the first digit of the fractional part (for the first digit after the decimal point), corresponds to the last digit of the integer part (for the first digit before the decimal point). See also digit1 12998. Examples (not formal): ( 234.567 ( digit ` 10 ) 0 ) = 4; ( 2.567 ( digit ` 10 ) -2 ) = 6; ( 2345.67 ( digit ` 10 ) 2 ) = 3. (Contributed by AV, 16-May-2020.) |
digit | ||
Theorem | digfval 42391* | Operation to obtain the th digit of a nonnegative real number in the positional system with base . (Contributed by AV, 23-May-2020.) |
digit | ||
Theorem | digval 42392 | The th digit of a nonnegative real number in the positional system with base . (Contributed by AV, 23-May-2020.) |
digit | ||
Theorem | digvalnn0 42393 | The th digit of a nonnegative real number in the positional system with base is a nonnegative integer. (Contributed by AV, 28-May-2020.) |
digit | ||
Theorem | nn0digval 42394 | The th digit of a nonnegative real number in the positional system with base . (Contributed by AV, 23-May-2020.) |
digit | ||
Theorem | dignn0fr 42395 | The digits of the fractional part of a nonnegative integer are 0. (Contributed by AV, 23-May-2020.) |
digit | ||
Theorem | dignn0ldlem 42396 | Lemma for dignnld 42397. (Contributed by AV, 25-May-2020.) |
logb | ||
Theorem | dignnld 42397 | The leading digits of a positive integer are 0. (Contributed by AV, 25-May-2020.) |
logb digit | ||
Theorem | dig2nn0ld 42398 | The leading digits of a positive integer in a binary system are 0. (Contributed by AV, 25-May-2020.) |
#b digit | ||
Theorem | dig2nn1st 42399 | The first (relevant) digit of a positive integer in a binary system is 1. (Contributed by AV, 26-May-2020.) |
#b digit | ||
Theorem | dig0 42400 | All digits of 0 are 0. (Contributed by AV, 24-May-2020.) |
digit |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |