![]() |
Metamath
Proof Explorer Theorem List (p. 143 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | expnlbnd 14201* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ (1 / (๐ตโ๐)) < ๐ด) | ||
Theorem | expnlbnd2 14202* | The reciprocal of exponentiation with a base greater than 1 has no positive lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
โข ((๐ด โ โ+ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ โ๐ โ (โคโฅโ๐)(1 / (๐ตโ๐)) < ๐ด) | ||
Theorem | expmulnbnd 14203* | Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
โข ((๐ด โ โ โง ๐ต โ โ โง 1 < ๐ต) โ โ๐ โ โ0 โ๐ โ (โคโฅโ๐)(๐ด ยท ๐) < (๐ตโ๐)) | ||
Theorem | digit2 14204 | Two ways to express the ๐พ th digit in the decimal (when base ๐ต = 10) expansion of a number ๐ด. ๐พ = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 25-Dec-2008.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = ((โโ((๐ตโ๐พ) ยท ๐ด)) โ (๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))))) | ||
Theorem | digit1 14205 | Two ways to express the ๐พ th digit in the decimal expansion of a number ๐ด (when base ๐ต = 10). ๐พ = 1 corresponds to the first digit after the decimal point. (Contributed by NM, 3-Jan-2009.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐พ โ โ) โ ((โโ((๐ตโ๐พ) ยท ๐ด)) mod ๐ต) = (((โโ((๐ตโ๐พ) ยท ๐ด)) mod (๐ตโ๐พ)) โ ((๐ต ยท (โโ((๐ตโ(๐พ โ 1)) ยท ๐ด))) mod (๐ตโ๐พ)))) | ||
Theorem | modexp 14206 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) |
โข (((๐ด โ โค โง ๐ต โ โค) โง (๐ถ โ โ0 โง ๐ท โ โ+) โง (๐ด mod ๐ท) = (๐ต mod ๐ท)) โ ((๐ดโ๐ถ) mod ๐ท) = ((๐ตโ๐ถ) mod ๐ท)) | ||
Theorem | discr1 14207* | A nonnegative quadratic form has nonnegative leading coefficient. (Contributed by Mario Carneiro, 4-Jun-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ โ) โ 0 โค (((๐ด ยท (๐ฅโ2)) + (๐ต ยท ๐ฅ)) + ๐ถ)) & โข ๐ = if(1 โค (((๐ต + if(0 โค ๐ถ, ๐ถ, 0)) + 1) / -๐ด), (((๐ต + if(0 โค ๐ถ, ๐ถ, 0)) + 1) / -๐ด), 1) โ โข (๐ โ 0 โค ๐ด) | ||
Theorem | discr 14208* | If a quadratic polynomial with real coefficients is nonnegative for all values, then its discriminant is nonpositive. (Contributed by NM, 10-Aug-1999.) (Revised by Mario Carneiro, 4-Jun-2014.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ ๐ถ โ โ) & โข ((๐ โง ๐ฅ โ โ) โ 0 โค (((๐ด ยท (๐ฅโ2)) + (๐ต ยท ๐ฅ)) + ๐ถ)) โ โข (๐ โ ((๐ตโ2) โ (4 ยท (๐ด ยท ๐ถ))) โค 0) | ||
Theorem | expnngt1 14209 | If an integer power with a positive integer base is greater than 1, then the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
โข ((๐ด โ โ โง ๐ต โ โค โง 1 < (๐ดโ๐ต)) โ ๐ต โ โ) | ||
Theorem | expnngt1b 14210 | An integer power with an integer base greater than 1 is greater than 1 iff the exponent is positive. (Contributed by AV, 28-Dec-2022.) |
โข ((๐ด โ (โคโฅโ2) โง ๐ต โ โค) โ (1 < (๐ดโ๐ต) โ ๐ต โ โ)) | ||
Theorem | sqoddm1div8 14211 | A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ โ โค โง ๐ = ((2 ยท ๐) + 1)) โ (((๐โ2) โ 1) / 8) = ((๐ ยท (๐ + 1)) / 2)) | ||
Theorem | nnsqcld 14212 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ (๐ดโ2) โ โ) | ||
Theorem | nnexpcld 14213 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ๐) โ โ) | ||
Theorem | nn0expcld 14214 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ0) & โข (๐ โ ๐ โ โ0) โ โข (๐ โ (๐ดโ๐) โ โ0) | ||
Theorem | rpexpcld 14215 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ๐) โ โ+) | ||
Theorem | ltexp2rd 14216 | The power of a positive number smaller than 1 decreases as its exponent increases. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ+) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ด < 1) โ โข (๐ โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) | ||
Theorem | reexpclzd 14217 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) & โข (๐ โ ๐ โ โค) โ โข (๐ โ (๐ดโ๐) โ โ) | ||
Theorem | sqgt0d 14218 | The square of a nonzero real is positive. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ด โ 0) โ โข (๐ โ 0 < (๐ดโ2)) | ||
Theorem | ltexp2d 14219 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ 1 < ๐ด) โ โข (๐ โ (๐ < ๐ โ (๐ดโ๐) < (๐ดโ๐))) | ||
Theorem | leexp2d 14220 | Ordering law for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ 1 < ๐ด) โ โข (๐ โ (๐ โค ๐ โ (๐ดโ๐) โค (๐ดโ๐))) | ||
Theorem | expcand 14221 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ 1 < ๐ด) & โข (๐ โ (๐ดโ๐) = (๐ดโ๐)) โ โข (๐ โ ๐ = ๐) | ||
Theorem | leexp2ad 14222 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ 1 โค ๐ด) & โข (๐ โ ๐ โ (โคโฅโ๐)) โ โข (๐ โ (๐ดโ๐) โค (๐ดโ๐)) | ||
Theorem | leexp2rd 14223 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ (โคโฅโ๐)) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ ๐ด โค 1) โ โข (๐ โ (๐ดโ๐) โค (๐ดโ๐)) | ||
Theorem | lt2sqd 14224 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ต) โ โข (๐ โ (๐ด < ๐ต โ (๐ดโ2) < (๐ตโ2))) | ||
Theorem | le2sqd 14225 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ต) โ โข (๐ โ (๐ด โค ๐ต โ (๐ดโ2) โค (๐ตโ2))) | ||
Theorem | sq11d 14226 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
โข (๐ โ ๐ด โ โ) & โข (๐ โ ๐ต โ โ) & โข (๐ โ 0 โค ๐ด) & โข (๐ โ 0 โค ๐ต) & โข (๐ โ (๐ดโ2) = (๐ตโ2)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | mulsubdivbinom2 14227 | The square of a binomial with factor minus a number divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โง (๐ถ โ โ โง ๐ถ โ 0)) โ (((((๐ถ ยท ๐ด) + ๐ต)โ2) โ ๐ท) / ๐ถ) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + (((๐ตโ2) โ ๐ท) / ๐ถ))) | ||
Theorem | muldivbinom2 14228 | The square of a binomial with factor divided by a nonzero number. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ ((((๐ถ ยท ๐ด) + ๐ต)โ2) / ๐ถ) = (((๐ถ ยท (๐ดโ2)) + (2 ยท (๐ด ยท ๐ต))) + ((๐ตโ2) / ๐ถ))) | ||
Theorem | sq10 14229 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
โข (;10โ2) = ;;100 | ||
Theorem | sq10e99m1 14230 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
โข (;10โ2) = (;99 + 1) | ||
Theorem | 3dec 14231 | A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข ;;๐ด๐ต๐ถ = ((((;10โ2) ยท ๐ด) + (;10 ยท ๐ต)) + ๐ถ) | ||
Theorem | nn0le2msqi 14232 | The square function on nonnegative integers is monotonic. (Contributed by Raph Levien, 10-Dec-2002.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (๐ด โค ๐ต โ (๐ด ยท ๐ด) โค (๐ต ยท ๐ต)) | ||
Theorem | nn0opthlem1 14233 | A rather pretty lemma for nn0opthi 14235. (Contributed by Raph Levien, 10-Dec-2002.) |
โข ๐ด โ โ0 & โข ๐ถ โ โ0 โ โข (๐ด < ๐ถ โ ((๐ด ยท ๐ด) + (2 ยท ๐ด)) < (๐ถ ยท ๐ถ)) | ||
Theorem | nn0opthlem2 14234 | Lemma for nn0opthi 14235. (Contributed by Raph Levien, 10-Dec-2002.) (Revised by Scott Fenton, 8-Sep-2010.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 โ โข ((๐ด + ๐ต) < ๐ถ โ ((๐ถ ยท ๐ถ) + ๐ท) โ (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต)) | ||
Theorem | nn0opthi 14235 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers ๐ด and ๐ต by (((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต). If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 4635 that works for any set. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Scott Fenton, 8-Sep-2010.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 โ โข ((((๐ด + ๐ต) ยท (๐ด + ๐ต)) + ๐ต) = (((๐ถ + ๐ท) ยท (๐ถ + ๐ท)) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) | ||
Theorem | nn0opth2i 14236 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthi 14235. (Contributed by NM, 22-Jul-2004.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 & โข ๐ท โ โ0 โ โข ((((๐ด + ๐ต)โ2) + ๐ต) = (((๐ถ + ๐ท)โ2) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท)) | ||
Theorem | nn0opth2 14237 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthi 14235. (Contributed by NM, 22-Jul-2004.) |
โข (((๐ด โ โ0 โง ๐ต โ โ0) โง (๐ถ โ โ0 โง ๐ท โ โ0)) โ ((((๐ด + ๐ต)โ2) + ๐ต) = (((๐ถ + ๐ท)โ2) + ๐ท) โ (๐ด = ๐ถ โง ๐ต = ๐ท))) | ||
Syntax | cfa 14238 | Extend class notation to include the factorial of nonnegative integers. |
class ! | ||
Definition | df-fac 14239 | Define the factorial function on nonnegative integers. For example, (!โ5) = 120 because 1 ยท 2 ยท 3 ยท 4 ยท 5 = 120 (ex-fac 29972). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.) |
โข ! = ({โจ0, 1โฉ} โช seq1( ยท , I )) | ||
Theorem | facnn 14240 | Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
โข (๐ โ โ โ (!โ๐) = (seq1( ยท , I )โ๐)) | ||
Theorem | fac0 14241 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
โข (!โ0) = 1 | ||
Theorem | fac1 14242 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
โข (!โ1) = 1 | ||
Theorem | facp1 14243 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
โข (๐ โ โ0 โ (!โ(๐ + 1)) = ((!โ๐) ยท (๐ + 1))) | ||
Theorem | fac2 14244 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
โข (!โ2) = 2 | ||
Theorem | fac3 14245 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
โข (!โ3) = 6 | ||
Theorem | fac4 14246 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
โข (!โ4) = ;24 | ||
Theorem | facnn2 14247 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
โข (๐ โ โ โ (!โ๐) = ((!โ(๐ โ 1)) ยท ๐)) | ||
Theorem | faccl 14248 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
โข (๐ โ โ0 โ (!โ๐) โ โ) | ||
Theorem | faccld 14249 | Closure of the factorial function, deduction version of faccl 14248. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
โข (๐ โ ๐ โ โ0) โ โข (๐ โ (!โ๐) โ โ) | ||
Theorem | facmapnn 14250 | The factorial function restricted to positive integers is a mapping from the positive integers to the positive integers. (Contributed by AV, 8-Aug-2020.) |
โข (๐ โ โ โฆ (!โ๐)) โ (โ โm โ) | ||
Theorem | facne0 14251 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
โข (๐ โ โ0 โ (!โ๐) โ 0) | ||
Theorem | facdiv 14252 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
โข ((๐ โ โ0 โง ๐ โ โ โง ๐ โค ๐) โ ((!โ๐) / ๐) โ โ) | ||
Theorem | facndiv 14253 | No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.) |
โข (((๐ โ โ0 โง ๐ โ โ) โง (1 < ๐ โง ๐ โค ๐)) โ ยฌ (((!โ๐) + 1) / ๐) โ โค) | ||
Theorem | facwordi 14254 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
โข ((๐ โ โ0 โง ๐ โ โ0 โง ๐ โค ๐) โ (!โ๐) โค (!โ๐)) | ||
Theorem | faclbnd 14255 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
โข ((๐ โ โ0 โง ๐ โ โ0) โ (๐โ(๐ + 1)) โค ((๐โ๐) ยท (!โ๐))) | ||
Theorem | faclbnd2 14256 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
โข (๐ โ โ0 โ ((2โ๐) / 2) โค (!โ๐)) | ||
Theorem | faclbnd3 14257 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
โข ((๐ โ โ0 โง ๐ โ โ0) โ (๐โ๐) โค ((๐โ๐) ยท (!โ๐))) | ||
Theorem | faclbnd4lem1 14258 | Lemma for faclbnd4 14262. Prepare the induction step. (Contributed by NM, 20-Dec-2005.) |
โข ๐ โ โ & โข ๐พ โ โ0 & โข ๐ โ โ0 โ โข ((((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (๐โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐))) | ||
Theorem | faclbnd4lem2 14259 | Lemma for faclbnd4 14262. Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 14258 to antecedents. (Contributed by NM, 23-Dec-2005.) |
โข ((๐ โ โ0 โง ๐พ โ โ0 โง ๐ โ โ) โ ((((๐ โ 1)โ๐พ) ยท (๐โ(๐ โ 1))) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ(๐ โ 1))) โ ((๐โ(๐พ + 1)) ยท (๐โ๐)) โค (((2โ((๐พ + 1)โ2)) ยท (๐โ(๐ + (๐พ + 1)))) ยท (!โ๐)))) | ||
Theorem | faclbnd4lem3 14260 | Lemma for faclbnd4 14262. The ๐ = 0 case. (Contributed by NM, 23-Dec-2005.) |
โข (((๐ โ โ0 โง ๐พ โ โ0) โง ๐ = 0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) | ||
Theorem | faclbnd4lem4 14261 | Lemma for faclbnd4 14262. Prove the 0 < ๐ case by induction on ๐พ. (Contributed by NM, 19-Dec-2005.) |
โข ((๐ โ โ โง ๐พ โ โ0 โง ๐ โ โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) | ||
Theorem | faclbnd4 14262 | Variant of faclbnd5 14263 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005.) |
โข ((๐ โ โ0 โง ๐พ โ โ0 โง ๐ โ โ0) โ ((๐โ๐พ) ยท (๐โ๐)) โค (((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ))) ยท (!โ๐))) | ||
Theorem | faclbnd5 14263 | The factorial function grows faster than powers and exponentiations. If we consider ๐พ and ๐ to be constants, the right-hand side of the inequality is a constant times ๐-factorial. (Contributed by NM, 24-Dec-2005.) |
โข ((๐ โ โ0 โง ๐พ โ โ0 โง ๐ โ โ) โ ((๐โ๐พ) ยท (๐โ๐)) < ((2 ยท ((2โ(๐พโ2)) ยท (๐โ(๐ + ๐พ)))) ยท (!โ๐))) | ||
Theorem | faclbnd6 14264 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
โข ((๐ โ โ0 โง ๐ โ โ0) โ ((!โ๐) ยท ((๐ + 1)โ๐)) โค (!โ(๐ + ๐))) | ||
Theorem | facubnd 14265 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
โข (๐ โ โ0 โ (!โ๐) โค (๐โ๐)) | ||
Theorem | facavg 14266 | The product of two factorials is greater than or equal to the factorial of (the floor of) their average. (Contributed by NM, 9-Dec-2005.) |
โข ((๐ โ โ0 โง ๐ โ โ0) โ (!โ(โโ((๐ + ๐) / 2))) โค ((!โ๐) ยท (!โ๐))) | ||
Syntax | cbc 14267 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
class C | ||
Definition | df-bc 14268* |
Define the binomial coefficient operation. For example,
(5C3) = 10 (ex-bc 29973).
In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". The expression (๐C๐พ) is read "๐ choose ๐พ". Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 โค ๐ โค ๐ does not hold. (Contributed by NM, 10-Jul-2005.) |
โข C = (๐ โ โ0, ๐ โ โค โฆ if(๐ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐)) ยท (!โ๐))), 0)) | ||
Theorem | bcval 14269 | Value of the binomial coefficient, ๐ choose ๐พ. Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 โค ๐พ โค ๐ does not hold. See bcval2 14270 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
โข ((๐ โ โ0 โง ๐พ โ โค) โ (๐C๐พ) = if(๐พ โ (0...๐), ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ))), 0)) | ||
Theorem | bcval2 14270 | Value of the binomial coefficient, ๐ choose ๐พ, in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) = ((!โ๐) / ((!โ(๐ โ ๐พ)) ยท (!โ๐พ)))) | ||
Theorem | bcval3 14271 | Value of the binomial coefficient, ๐ choose ๐พ, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
โข ((๐ โ โ0 โง ๐พ โ โค โง ยฌ ๐พ โ (0...๐)) โ (๐C๐พ) = 0) | ||
Theorem | bcval4 14272 | Value of the binomial coefficient, ๐ choose ๐พ, outside of its standard domain. Remark in [Gleason] p. 295. (Contributed by NM, 14-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
โข ((๐ โ โ0 โง ๐พ โ โค โง (๐พ < 0 โจ ๐ < ๐พ)) โ (๐C๐พ) = 0) | ||
Theorem | bcrpcl 14273 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 14288.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) โ โ+) | ||
Theorem | bccmpl 14274 | "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.) |
โข ((๐ โ โ0 โง ๐พ โ โค) โ (๐C๐พ) = (๐C(๐ โ ๐พ))) | ||
Theorem | bcn0 14275 | ๐ choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
โข (๐ โ โ0 โ (๐C0) = 1) | ||
Theorem | bc0k 14276 | The binomial coefficient " 0 choose ๐พ " is 0 for a positive integer K. Note that (0C0) = 1 (see bcn0 14275). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
โข (๐พ โ โ โ (0C๐พ) = 0) | ||
Theorem | bcnn 14277 | ๐ choose ๐ is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
โข (๐ โ โ0 โ (๐C๐) = 1) | ||
Theorem | bcn1 14278 | Binomial coefficient: ๐ choose 1. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
โข (๐ โ โ0 โ (๐C1) = ๐) | ||
Theorem | bcnp1n 14279 | Binomial coefficient: ๐ + 1 choose ๐. (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
โข (๐ โ โ0 โ ((๐ + 1)C๐) = (๐ + 1)) | ||
Theorem | bcm1k 14280 | The proportion of one binomial coefficient to another with ๐พ decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
โข (๐พ โ (1...๐) โ (๐C๐พ) = ((๐C(๐พ โ 1)) ยท ((๐ โ (๐พ โ 1)) / ๐พ))) | ||
Theorem | bcp1n 14281 | The proportion of one binomial coefficient to another with ๐ increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
โข (๐พ โ (0...๐) โ ((๐ + 1)C๐พ) = ((๐C๐พ) ยท ((๐ + 1) / ((๐ + 1) โ ๐พ)))) | ||
Theorem | bcp1nk 14282 | The proportion of one binomial coefficient to another with ๐ and ๐พ increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.) |
โข (๐พ โ (0...๐) โ ((๐ + 1)C(๐พ + 1)) = ((๐C๐พ) ยท ((๐ + 1) / (๐พ + 1)))) | ||
Theorem | bcval5 14283 | Write out the top and bottom parts of the binomial coefficient (๐C๐พ) = (๐ ยท (๐ โ 1) ยท ... ยท ((๐ โ ๐พ) + 1)) / ๐พ! explicitly. In this form, it is valid even for ๐ < ๐พ, although it is no longer valid for nonpositive ๐พ. (Contributed by Mario Carneiro, 22-May-2014.) |
โข ((๐ โ โ0 โง ๐พ โ โ) โ (๐C๐พ) = ((seq((๐ โ ๐พ) + 1)( ยท , I )โ๐) / (!โ๐พ))) | ||
Theorem | bcn2 14284 | Binomial coefficient: ๐ choose 2. (Contributed by Mario Carneiro, 22-May-2014.) |
โข (๐ โ โ0 โ (๐C2) = ((๐ ยท (๐ โ 1)) / 2)) | ||
Theorem | bcp1m1 14285 | Compute the binomial coefficient of (๐ + 1) over (๐ โ 1) (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
โข (๐ โ โ0 โ ((๐ + 1)C(๐ โ 1)) = (((๐ + 1) ยท ๐) / 2)) | ||
Theorem | bcpasc 14286 | Pascal's rule for the binomial coefficient, generalized to all integers ๐พ. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.) |
โข ((๐ โ โ0 โง ๐พ โ โค) โ ((๐C๐พ) + (๐C(๐พ โ 1))) = ((๐ + 1)C๐พ)) | ||
Theorem | bccl 14287 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.) |
โข ((๐ โ โ0 โง ๐พ โ โค) โ (๐C๐พ) โ โ0) | ||
Theorem | bccl2 14288 | A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.) |
โข (๐พ โ (0...๐) โ (๐C๐พ) โ โ) | ||
Theorem | bcn2m1 14289 | Compute the binomial coefficient "๐ choose 2 " from "(๐ โ 1) choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.) |
โข (๐ โ โ โ ((๐ โ 1) + ((๐ โ 1)C2)) = (๐C2)) | ||
Theorem | bcn2p1 14290 | Compute the binomial coefficient "(๐ + 1) choose 2 " from "๐ choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.) |
โข (๐ โ โ0 โ (๐ + (๐C2)) = ((๐ + 1)C2)) | ||
Theorem | permnn 14291 | The number of permutations of ๐ โ ๐ objects from a collection of ๐ objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.) |
โข (๐ โ (0...๐) โ ((!โ๐) / (!โ๐ )) โ โ) | ||
Theorem | bcnm1 14292 | The binomial coefficent of (๐ โ 1) is ๐. (Contributed by Scott Fenton, 16-May-2014.) |
โข (๐ โ โ0 โ (๐C(๐ โ 1)) = ๐) | ||
Theorem | 4bc3eq4 14293 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
โข (4C3) = 4 | ||
Theorem | 4bc2eq6 14294 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
โข (4C2) = 6 | ||
Syntax | chash 14295 | Extend the definition of a class to include the set size function. |
class โฏ | ||
Definition | df-hash 14296 | Define the set size function โฏ, which gives the cardinality of a finite set as a member of โ0, and assigns all infinite sets the value +โ. For example, (โฏโ{0, 1, 2}) = 3 (ex-hash 29974). (Contributed by Paul Chapman, 22-Jun-2011.) |
โข โฏ = (((rec((๐ฅ โ V โฆ (๐ฅ + 1)), 0) โพ ฯ) โ card) โช ((V โ Fin) ร {+โ})) | ||
Theorem | hashkf 14297 | The finite part of the size function maps all finite sets to their cardinality, as members of โ0. (Contributed by Mario Carneiro, 13-Sep-2013.) (Revised by Mario Carneiro, 26-Dec-2014.) |
โข ๐บ = (rec((๐ฅ โ V โฆ (๐ฅ + 1)), 0) โพ ฯ) & โข ๐พ = (๐บ โ card) โ โข ๐พ:Finโถโ0 | ||
Theorem | hashgval 14298* | The value of the โฏ function in terms of the mapping ๐บ from ฯ to โ0. The proof avoids the use of ax-ac 10458. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 26-Dec-2014.) |
โข ๐บ = (rec((๐ฅ โ V โฆ (๐ฅ + 1)), 0) โพ ฯ) โ โข (๐ด โ Fin โ (๐บโ(cardโ๐ด)) = (โฏโ๐ด)) | ||
Theorem | hashginv 14299* | The converse of ๐บ maps the size function's value to card. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 15-Sep-2013.) |
โข ๐บ = (rec((๐ฅ โ V โฆ (๐ฅ + 1)), 0) โพ ฯ) โ โข (๐ด โ Fin โ (โก๐บโ(โฏโ๐ด)) = (cardโ๐ด)) | ||
Theorem | hashinf 14300 | The value of the โฏ function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014.) |
โข ((๐ด โ ๐ โง ยฌ ๐ด โ Fin) โ (โฏโ๐ด) = +โ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |