Home | Intuitionistic Logic Explorer Theorem List (p. 97 of 108) | < 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 | expeq0d 9601 | Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqvald 9602 | Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqcld 9603 | Closure of square. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqeq0d 9604 | A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expcld 9605 | Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expp1d 9606 | 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 9607 | 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 9608 | 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 9609 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expclzapd 9610 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expap0d 9611 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# # | ||
Theorem | expnegapd 9612 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | exprecapd 9613 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expp1zapd 9614 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expm1apd 9615 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | expsubapd 9616 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
# | ||
Theorem | sqmuld 9617 | Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqdivapd 9618 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | expdivapd 9619 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | mulexpd 9620 | 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 9621 | Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | reexpcld 9622 | Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expge0d 9623 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | expge1d 9624 | Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqoddm1div8 9625 | 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 9626 | The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nnexpcld 9627 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nn0expcld 9628 | Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpexpcld 9629 | Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | reexpclzapd 9630 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | resqcld 9631 | Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqge0d 9632 | A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sqgt0apd 9633 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
# | ||
Theorem | leexp2ad 9634 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | leexp2rd 9635 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lt2sqd 9636 | The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | le2sqd 9637 | The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sq11d 9638 | The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | sq11ap 9639 | Analogue to sq11 9548 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.) |
# # | ||
Theorem | sq10 9640 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
; ;; | ||
Theorem | sq10e99m1 9641 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
; ; | ||
Theorem | 3dec 9642 | 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 9643 | Lemma for expcan 9644. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.) |
Theorem | expcan 9644 | Cancellation law for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.) |
Theorem | expcand 9645 | Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nn0le2msqd 9646 | The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthlem1d 9647 | A rather pretty lemma for nn0opth2 9651. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthlem2d 9648 | Lemma for nn0opth2 9651. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opthd 9649 | 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 3407 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opth2d 9650 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 9649. (Contributed by Jim Kingdon, 31-Oct-2021.) |
Theorem | nn0opth2 9651 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See nn0opthd 9649. (Contributed by NM, 22-Jul-2004.) |
Syntax | cfa 9652 | Extend class notation to include the factorial of nonnegative integers. |
Definition | df-fac 9653 | Define the factorial function on nonnegative integers. For example, because (ex-fac 10565). In the literature, the factorial function is written as a postscript exclamation point. (Contributed by NM, 2-Dec-2004.) |
Theorem | facnn 9654 | Value of the factorial function for positive integers. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac0 9655 | The factorial of 0. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac1 9656 | The factorial of 1. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | facp1 9657 | The factorial of a successor. (Contributed by NM, 2-Dec-2004.) (Revised by Mario Carneiro, 13-Jul-2013.) |
Theorem | fac2 9658 | The factorial of 2. (Contributed by NM, 17-Mar-2005.) |
Theorem | fac3 9659 | The factorial of 3. (Contributed by NM, 17-Mar-2005.) |
Theorem | fac4 9660 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
; | ||
Theorem | facnn2 9661 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccl 9662 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccld 9663 | Closure of the factorial function, deduction version of faccl 9662. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | facne0 9664 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
Theorem | facdiv 9665 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
Theorem | facndiv 9666 | 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 9667 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
Theorem | faclbnd 9668 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd2 9669 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd3 9670 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
Theorem | faclbnd6 9671 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
Theorem | facubnd 9672 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
Theorem | facavg 9673 | 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 9674 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
Definition | df-bc 9675* |
Define the binomial coefficient operation. For example,
(ex-bc 10566).
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 9676 | 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 9677 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | bcval2 9677 | 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 9678 | 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 9679 | 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 9680 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 9695.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bccmpl 9681 | "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.) |
Theorem | bcn0 9682 | choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bc0k 9683 | The binomial coefficient " 0 choose " is 0 for a positive integer K. Note that (see bcn0 9682). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
Theorem | bcnn 9684 | choose is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcn1 9685 | Binomial coefficient: choose . (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcnp1n 9686 | Binomial coefficient: choose . (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcm1k 9687 | The proportion of one binomial coefficient to another with decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bcp1n 9688 | The proportion of one binomial coefficient to another with increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bcp1nk 9689 | The proportion of one binomial coefficient to another with and increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Theorem | ibcval5 9690 | Write out the top and bottom parts of the binomial coefficient explicitly. In this form, it is valid even for , although it is no longer valid for nonpositive . (Contributed by Jim Kingdon, 6-Nov-2021.) |
Theorem | bcn2 9691 | Binomial coefficient: choose . (Contributed by Mario Carneiro, 22-May-2014.) |
Theorem | bcp1m1 9692 | Compute the binomial coefficient of over (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
Theorem | bcpasc 9693 | 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.) |
Theorem | bccl 9694 | A binomial coefficient, in its extended domain, is a nonnegative integer. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 9-Nov-2013.) |
Theorem | bccl2 9695 | A binomial coefficient, in its standard domain, is a positive integer. (Contributed by NM, 3-Jan-2006.) (Revised by Mario Carneiro, 10-Mar-2014.) |
Theorem | bcn2m1 9696 | Compute the binomial coefficient " choose 2 " from " choose 2 ": (N-1) + ( (N-1) 2 ) = ( N 2 ). (Contributed by Alexander van der Vekens, 7-Jan-2018.) |
Theorem | bcn2p1 9697 | Compute the binomial coefficient " choose 2 " from " choose 2 ": N + ( N 2 ) = ( (N+1) 2 ). (Contributed by Alexander van der Vekens, 8-Jan-2018.) |
Theorem | permnn 9698 | The number of permutations of objects from a collection of objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.) |
Theorem | bcnm1 9699 | The binomial coefficent of is . (Contributed by Scott Fenton, 16-May-2014.) |
Theorem | 4bc3eq4 9700 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |