Home | Intuitionistic Logic Explorer Theorem List (p. 97 of 106) | < 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 | fac4 9601 | The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.) |
; | ||
Theorem | facnn2 9602 | Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccl 9603 | Closure of the factorial function. (Contributed by NM, 2-Dec-2004.) |
Theorem | faccld 9604 | Closure of the factorial function, deduction version of faccl 9603. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | facne0 9605 | The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.) |
Theorem | facdiv 9606 | A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.) |
Theorem | facndiv 9607 | 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 9608 | Ordering property of factorial. (Contributed by NM, 9-Dec-2005.) |
Theorem | faclbnd 9609 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd2 9610 | A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.) |
Theorem | faclbnd3 9611 | A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.) |
Theorem | faclbnd6 9612 | Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.) |
Theorem | facubnd 9613 | An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.) |
Theorem | facavg 9614 | 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 9615 | Extend class notation to include the binomial coefficient operation (combinatorial choose operation). |
Definition | df-bc 9616* |
Define the binomial coefficient operation. For example,
(ex-bc 10282).
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 9617 | 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 9618 for the value in the standard domain. (Contributed by NM, 10-Jul-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | bcval2 9618 | 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 9619 | 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 9620 | 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 9621 | Closure of the binomial coefficient in the positive reals. (This is mostly a lemma before we have bccl2 9636.) (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bccmpl 9622 | "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 9623 | choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bc0k 9624 | The binomial coefficient " 0 choose " is 0 for a positive integer K. Note that (see bcn0 9623). (Contributed by Alexander van der Vekens, 1-Jan-2018.) |
Theorem | bcnn 9625 | choose is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcn1 9626 | Binomial coefficient: choose . (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcnp1n 9627 | Binomial coefficient: choose . (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.) |
Theorem | bcm1k 9628 | The proportion of one binomial coefficient to another with decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bcp1n 9629 | The proportion of one binomial coefficient to another with increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.) |
Theorem | bcp1nk 9630 | The proportion of one binomial coefficient to another with and increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.) |
Theorem | ibcval5 9631 | 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 9632 | Binomial coefficient: choose . (Contributed by Mario Carneiro, 22-May-2014.) |
Theorem | bcp1m1 9633 | Compute the binomial coefficient of over (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.) |
Theorem | bcpasc 9634 | 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 9635 | 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 9636 | 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 9637 | 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 9638 | 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 9639 | The number of permutations of objects from a collection of objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.) |
Theorem | bcnm1 9640 | The binomial coefficent of is . (Contributed by Scott Fenton, 16-May-2014.) |
Theorem | 4bc3eq4 9641 | The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.) |
Theorem | 4bc2eq6 9642 | The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.) |
Syntax | cshi 9643 | Extend class notation with function shifter. |
Definition | df-shft 9644* | Define a function shifter. This operation offsets the value argument of a function (ordinarily on a subset of ) and produces a new function on . See shftval 9654 for its value. (Contributed by NM, 20-Jul-2005.) |
Theorem | shftlem 9645* | Two ways to write a shifted set . (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | shftuz 9646* | A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftfvalg 9647* | The value of the sequence shifter operation is a function on . is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | ovshftex 9648 | Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.) |
Theorem | shftfibg 9649 | Value of a fiber of the relation . (Contributed by Jim Kingdon, 15-Aug-2021.) |
Theorem | shftfval 9650* | The value of the sequence shifter operation is a function on . is ordinarily an integer. (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | shftdm 9651* | Domain of a relation shifted by . The set on the right is more commonly notated as (meaning add to every element of ). (Contributed by Mario Carneiro, 3-Nov-2013.) |
Theorem | shftfib 9652 | Value of a fiber of the relation . (Contributed by Mario Carneiro, 4-Nov-2013.) |
Theorem | shftfn 9653* | Functionality and domain of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | shftval 9654 | Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.) |
Theorem | shftval2 9655 | Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftval3 9656 | Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) |
Theorem | shftval4 9657 | Value of a sequence shifted by . (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftval5 9658 | Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftf 9659* | Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | 2shfti 9660 | Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftidt2 9661 | Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftidt 9662 | Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftcan1 9663 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftcan2 9664 | Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.) |
Theorem | shftvalg 9665 | Value of a sequence shifted by . (Contributed by Scott Fenton, 16-Dec-2017.) |
Theorem | shftval4g 9666 | Value of a sequence shifted by . (Contributed by Jim Kingdon, 19-Aug-2021.) |
Syntax | ccj 9667 | Extend class notation to include complex conjugate function. |
Syntax | cre 9668 | Extend class notation to include real part of a complex number. |
Syntax | cim 9669 | Extend class notation to include imaginary part of a complex number. |
Definition | df-cj 9670* | Define the complex conjugate function. See cjcli 9741 for its closure and cjval 9673 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Definition | df-re 9671 | Define a function whose value is the real part of a complex number. See reval 9677 for its value, recli 9739 for its closure, and replim 9687 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
Definition | df-im 9672 | Define a function whose value is the imaginary part of a complex number. See imval 9678 for its value, imcli 9740 for its closure, and replim 9687 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.) |
Theorem | cjval 9673* | The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.) |
Theorem | cjth 9674 | The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.) |
Theorem | cjf 9675 | Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.) |
Theorem | cjcl 9676 | The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | reval 9677 | The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | imval 9678 | The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | imre 9679 | The imaginary part of a complex number in terms of the real part function. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | reim 9680 | The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.) |
Theorem | recl 9681 | The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | imcl 9682 | The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | ref 9683 | Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | imf 9684 | Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.) |
Theorem | crre 9685 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | crim 9686 | The real part of a complex number representation. Definition 10-3.1 of [Gleason] p. 132. (Contributed by NM, 12-May-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | replim 9687 | Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | remim 9688 | Value of the conjugate of a complex number. The value is the real part minus times the imaginary part. Definition 10-3.2 of [Gleason] p. 132. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | reim0 9689 | The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.) |
Theorem | reim0b 9690 | A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.) |
Theorem | rereb 9691 | A number is real iff it equals its real part. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 20-Aug-2008.) |
Theorem | mulreap 9692 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) |
# | ||
Theorem | rere 9693 | A real number equals its real part. One direction of Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by Paul Chapman, 7-Sep-2007.) |
Theorem | cjreb 9694 | A number is real iff it equals its complex conjugate. Proposition 10-3.4(f) of [Gleason] p. 133. (Contributed by NM, 2-Jul-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
Theorem | recj 9695 | Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.) |
Theorem | reneg 9696 | Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
Theorem | readd 9697 | Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.) |
Theorem | resub 9698 | Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.) |
Theorem | remullem 9699 | Lemma for remul 9700, immul 9707, and cjmul 9713. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
Theorem | remul 9700 | Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |