Home | Intuitionistic Logic Explorer Theorem List (p. 105 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | binom2i 10401 | The square of a binomial. (Contributed by NM, 11-Aug-1999.) |
Theorem | subsqi 10402 | Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.) |
Theorem | binom2 10403 | The square of a binomial. (Contributed by FL, 10-Dec-2006.) |
Theorem | binom21 10404 | Special case of binom2 10403 where . (Contributed by Scott Fenton, 11-May-2014.) |
Theorem | binom2sub 10405 | Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.) |
Theorem | binom2sub1 10406 | Special case of binom2sub 10405 where . (Contributed by AV, 2-Aug-2021.) |
Theorem | binom2subi 10407 | Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.) |
Theorem | mulbinom2 10408 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
Theorem | binom3 10409 | The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.) |
Theorem | zesq 10410 | An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.) |
Theorem | nnesq 10411 | A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) |
Theorem | bernneq 10412 | Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.) |
Theorem | bernneq2 10413 | Variation of Bernoulli's inequality bernneq 10412. (Contributed by NM, 18-Oct-2007.) |
Theorem | bernneq3 10414 | A corollary of bernneq 10412. (Contributed by Mario Carneiro, 11-Mar-2014.) |
Theorem | expnbnd 10415* | Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.) |
Theorem | expnlbnd 10416* | The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) |
Theorem | expnlbnd2 10417* | The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
Theorem | exp0d 10418 | Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | exp1d 10419 | Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expeq0d 10420 | Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqvald 10421 | Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqcld 10422 | Closure of square. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqeq0d 10423 | A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expcld 10424 | Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expp1d 10425 | Value of a complex number raised to a nonnegative integer power plus one. Part of Definition 10-4.1 of [Gleason] p. 134. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expaddd 10426 | Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expmuld 10427 | Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqrecapd 10428 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expclzapd 10429 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expap0d 10430 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# # | ||
Theorem | expnegapd 10431 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | exprecapd 10432 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expp1zapd 10433 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expm1apd 10434 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expsubapd 10435 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | sqmuld 10436 | Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqdivapd 10437 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | expdivapd 10438 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | mulexpd 10439 | Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | 0expd 10440 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | reexpcld 10441 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expge0d 10442 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expge1d 10443 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqoddm1div8 10444 | 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.) |
Theorem | nnsqcld 10445 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nnexpcld 10446 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nn0expcld 10447 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpexpcld 10448 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | reexpclzapd 10449 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | resqcld 10450 | Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqge0d 10451 | A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqgt0apd 10452 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | leexp2ad 10453 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | leexp2rd 10454 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lt2sqd 10455 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | le2sqd 10456 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sq11d 10457 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sq11ap 10458 | Analogue to sq11 10365 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.) |
# # | ||
Theorem | sq10 10459 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
; ;; | ||
Theorem | sq10e99m1 10460 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
; ; | ||
Theorem | 3dec 10461 | 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.) |
;; ; ; | ||
Theorem | expcanlem 10462 | Lemma for expcan 10463. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.) |
Theorem | expcan 10463 | Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
Theorem | expcand 10464 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nn0le2msqd 10465 | The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthlem1d 10466 | A rather pretty lemma for nn0opth2 10470. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthlem2d 10467 | Lemma for nn0opth2 10470. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthd 10468 | 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 3536 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opth2d 10469 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 10468. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opth2 10470 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 10468. (Contributed by NM, 22-Jul-2004.) |
Syntax | cfa 10471 | Extend class notation to include the factorial of nonnegative integers. |
Definition | df-fac 10472 | Define the factorial function on nonnegative integers. For example, because (ex-fac 12940). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.) |
Theorem | facnn 10473 | Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac0 10474 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac1 10475 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | facp1 10476 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac2 10477 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
Theorem | fac3 10478 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
Theorem | fac4 10479 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
; | ||
Theorem | facnn2 10480 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccl 10481 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccld 10482 | Closure of the factorial function, deduction version of faccl 10481. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | facne0 10483 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
Theorem | facdiv 10484 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
Theorem | facndiv 10485 | No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.) |
Theorem | facwordi 10486 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
Theorem | faclbnd 10487 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd2 10488 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd3 10489 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
Theorem | faclbnd6 10490 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
Theorem | facubnd 10491 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
Theorem | facavg 10492 | 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.) |
Syntax | cbc 10493 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
Definition | df-bc 10494* |
Define the binomial coefficient operation. For example,
(ex-bc 12941).
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". is read " choose ." Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when does not hold. (Contributed by NM, 10-Jul-2005.) |
Theorem | bcval 10495 | 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 does not hold. See bcval2 10496 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | bcval2 10496 | Value of the binomial coefficient, choose , in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | bcval3 10497 | 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.) |
Theorem | bcval4 10498 | 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.) |
Theorem | bcrpcl 10499 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 10514.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bccmpl 10500 | "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |