Home Intuitionistic Logic ExplorerTheorem 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

Theorem List for Intuitionistic Logic Explorer - 9601-9700   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremfac4 9601 The factorial of 4. (Contributed by Mario Carneiro, 18-Jun-2015.)
;

Theoremfacnn2 9602 Value of the factorial function expressed recursively. (Contributed by NM, 2-Dec-2004.)

Theoremfaccl 9603 Closure of the factorial function. (Contributed by NM, 2-Dec-2004.)

Theoremfaccld 9604 Closure of the factorial function, deduction version of faccl 9603. (Contributed by Glauco Siliprandi, 5-Apr-2020.)

Theoremfacne0 9605 The factorial function is nonzero. (Contributed by NM, 26-Apr-2005.)

Theoremfacdiv 9606 A positive integer divides the factorial of an equal or larger number. (Contributed by NM, 2-May-2005.)

Theoremfacndiv 9607 No positive integer (greater than one) divides the factorial plus one of an equal or larger number. (Contributed by NM, 3-May-2005.)

Theoremfacwordi 9608 Ordering property of factorial. (Contributed by NM, 9-Dec-2005.)

Theoremfaclbnd 9609 A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)

Theoremfaclbnd2 9610 A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005.)

Theoremfaclbnd3 9611 A lower bound for the factorial function. (Contributed by NM, 19-Dec-2005.)

Theoremfaclbnd6 9612 Geometric lower bound for the factorial function, where N is usually held constant. (Contributed by Paul Chapman, 28-Dec-2007.)

Theoremfacubnd 9613 An upper bound for the factorial function. (Contributed by Mario Carneiro, 15-Apr-2016.)

Theoremfacavg 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.)

3.6.8  The binomial coefficient operation

Syntaxcbc 9615 Extend class notation to include the binomial coefficient operation (combinatorial choose operation).

Definitiondf-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.)

Theorembcval 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.)

Theorembcval2 9618 Value of the binomial coefficient, choose , in its standard domain. (Contributed by NM, 9-Jun-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)

Theorembcval3 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.)

Theorembcval4 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.)

Theorembcrpcl 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.)

Theorembccmpl 9622 "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 5-Mar-2014.)

Theorembcn0 9623 choose 0 is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)

Theorembc0k 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.)

Theorembcnn 9625 choose is 1. Remark in [Gleason] p. 296. (Contributed by NM, 17-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)

Theorembcn1 9626 Binomial coefficient: choose . (Contributed by NM, 21-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)

Theorembcnp1n 9627 Binomial coefficient: choose . (Contributed by NM, 20-Jun-2005.) (Revised by Mario Carneiro, 8-Nov-2013.)

Theorembcm1k 9628 The proportion of one binomial coefficient to another with decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)

Theorembcp1n 9629 The proportion of one binomial coefficient to another with increased by 1. (Contributed by Mario Carneiro, 10-Mar-2014.)

Theorembcp1nk 9630 The proportion of one binomial coefficient to another with and increased by 1. (Contributed by Mario Carneiro, 16-Jan-2015.)

Theoremibcval5 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.)

Theorembcn2 9632 Binomial coefficient: choose . (Contributed by Mario Carneiro, 22-May-2014.)

Theorembcp1m1 9633 Compute the binomial coefficient of over (Contributed by Scott Fenton, 11-May-2014.) (Revised by Mario Carneiro, 22-May-2014.)

Theorembcpasc 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.)

Theorembccl 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.)

Theorembccl2 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.)

Theorembcn2m1 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.)

Theorembcn2p1 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.)

Theorempermnn 9639 The number of permutations of objects from a collection of objects is a positive integer. (Contributed by Jason Orendorff, 24-Jan-2007.)

Theorembcnm1 9640 The binomial coefficent of is . (Contributed by Scott Fenton, 16-May-2014.)

Theorem4bc3eq4 9641 The value of four choose three. (Contributed by Scott Fenton, 11-Jun-2016.)

Theorem4bc2eq6 9642 The value of four choose two. (Contributed by Scott Fenton, 9-Jan-2017.)

3.7  Elementary real and complex functions

3.7.1  The "shift" operation

Syntaxcshi 9643 Extend class notation with function shifter.

Definitiondf-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.)

Theoremshftlem 9645* Two ways to write a shifted set . (Contributed by Mario Carneiro, 3-Nov-2013.)

Theoremshftuz 9646* A shift of the upper integers. (Contributed by Mario Carneiro, 5-Nov-2013.)

Theoremshftfvalg 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.)

Theoremovshftex 9648 Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.)

Theoremshftfibg 9649 Value of a fiber of the relation . (Contributed by Jim Kingdon, 15-Aug-2021.)

Theoremshftfval 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.)

Theoremshftdm 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.)

Theoremshftfib 9652 Value of a fiber of the relation . (Contributed by Mario Carneiro, 4-Nov-2013.)

Theoremshftfn 9653* Functionality and domain of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 3-Nov-2013.)

Theoremshftval 9654 Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 4-Nov-2013.)

Theoremshftval2 9655 Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftval3 9656 Value of a sequence shifted by . (Contributed by NM, 20-Jul-2005.)

Theoremshftval4 9657 Value of a sequence shifted by . (Contributed by NM, 18-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftval5 9658 Value of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftf 9659* Functionality of a shifted sequence. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theorem2shfti 9660 Composite shift operations. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftidt2 9661 Identity law for the shift operation. (Contributed by Mario Carneiro, 5-Nov-2013.)

Theoremshftidt 9662 Identity law for the shift operation. (Contributed by NM, 19-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftcan1 9663 Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftcan2 9664 Cancellation law for the shift operation. (Contributed by NM, 4-Aug-2005.) (Revised by Mario Carneiro, 5-Nov-2013.)

Theoremshftvalg 9665 Value of a sequence shifted by . (Contributed by Scott Fenton, 16-Dec-2017.)

Theoremshftval4g 9666 Value of a sequence shifted by . (Contributed by Jim Kingdon, 19-Aug-2021.)

3.7.2  Real and imaginary parts; conjugate

Syntaxccj 9667 Extend class notation to include complex conjugate function.

Syntaxcre 9668 Extend class notation to include real part of a complex number.

Syntaxcim 9669 Extend class notation to include imaginary part of a complex number.

Definitiondf-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.)

Definitiondf-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.)

Definitiondf-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.)

Theoremcjval 9673* The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)

Theoremcjth 9674 The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)

Theoremcjf 9675 Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)

Theoremcjcl 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.)

Theoremreval 9677 The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremimval 9678 The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremimre 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.)

Theoremreim 9680 The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)

Theoremrecl 9681 The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremimcl 9682 The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremref 9683 Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremimf 9684 Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)

Theoremcrre 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.)

Theoremcrim 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.)

Theoremreplim 9687 Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)

Theoremremim 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.)

Theoremreim0 9689 The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)

Theoremreim0b 9690 A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)

Theoremrereb 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.)

Theoremmulreap 9692 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
#

Theoremrere 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.)

Theoremcjreb 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.)

Theoremrecj 9695 Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)

Theoremreneg 9696 Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)

Theoremreadd 9697 Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)

Theoremresub 9698 Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)

Theoremremullem 9699 Lemma for remul 9700, immul 9707, and cjmul 9713. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)

Theoremremul 9700 Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >