HomeHome Intuitionistic Logic Explorer
Theorem List (p. 90 of 94)
< 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 - 8901-9000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremexpap0i 8901 Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  N  ZZ  ^ N #  0
 
Theoremexpgt0 8902 Nonnegative integer exponentiation with a positive mantissa is positive. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
 RR  N  ZZ  0  <  0  < 
 ^ N
 
Theoremexpnegzap 8903 Value of a complex number raised to a negative power. (Contributed by Mario Carneiro, 4-Jun-2014.)
 CC #  0  N  ZZ  ^ -u N  1  ^ N
 
Theorem0exp 8904 Value of zero raised to a positive integer power. (Contributed by NM, 19-Aug-2004.)
 N  NN  0 ^ N  0
 
Theoremexpge0 8905 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by NM, 16-Dec-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
 RR  N  NN0  0  <_  0  <_  ^ N
 
Theoremexpge1 8906 Nonnegative integer exponentiation with a mantissa greater than or equal to 1 is greater than or equal to 1. (Contributed by NM, 21-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
 RR  N  NN0  1  <_  1  <_  ^ N
 
Theoremexpgt1 8907 Positive integer exponentiation with a mantissa greater than 1 is greater than 1. (Contributed by NM, 13-Feb-2005.) (Revised by Mario Carneiro, 4-Jun-2014.)
 RR  N  NN  1  <  1  < 
 ^ N
 
Theoremmulexp 8908 Positive integer exponentiation of a product. Proposition 10-4.2(c) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 13-Feb-2005.)
 CC  CC  N  NN0  x.  ^ N 
 ^ N  x.  ^ N
 
Theoremmulexpzap 8909 Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  CC #  0  N  ZZ  x. 
 ^ N  ^ N  x.  ^ N
 
Theoremexprecap 8910 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  N  ZZ  1  ^ N  1  ^ N
 
Theoremexpadd 8911 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by NM, 30-Nov-2004.)
 CC  M  NN0  N  NN0  ^ M  +  N  ^ M  x.  ^ N
 
Theoremexpaddzaplem 8912 Lemma for expaddzap 8913. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  M  RR  -u M  NN  N  NN0  ^ M  +  N  ^ M  x.  ^ N
 
Theoremexpaddzap 8913 Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  +  N 
 ^ M  x.  ^ N
 
Theoremexpmul 8914 Product of exponents law for positive integer exponentiation. Proposition 10-4.2(b) of [Gleason] p. 135, restricted to nonnegative integer exponents. (Contributed by NM, 4-Jan-2006.)
 CC  M  NN0  N  NN0  ^ M  x.  N 
 ^ M ^ N
 
Theoremexpmulzap 8915 Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  x.  N 
 ^ M ^ N
 
Theoremexpsubap 8916 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  M  ZZ  N  ZZ  ^ M  -  N 
 ^ M  ^ N
 
Theoremexpp1zap 8917 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  N  ZZ  ^ N  +  1  ^ N  x.
 
Theoremexpm1ap 8918 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC #  0  N  ZZ  ^ N  -  1 
 ^ N
 
Theoremexpdivap 8919 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0  N  NN0  ^ N 
 ^ N  ^ N
 
Theoremltexp2a 8920 Ordering relationship for exponentiation. (Contributed by NM, 2-Aug-2006.) (Revised by Mario Carneiro, 4-Jun-2014.)
 RR  M  ZZ  N  ZZ  1  <  M  <  N  ^ M 
 <  ^ N
 
Theoremleexp2a 8921 Weak ordering relationship for exponentiation. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 5-Jun-2014.)
 RR  1  <_  N  ZZ>= `  M  ^ M  <_  ^ N
 
Theoremleexp2r 8922 Weak ordering relationship for exponentiation. (Contributed by Paul Chapman, 14-Jan-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
 RR  M  NN0  N  ZZ>= `  M  0  <_  <_  1 
 ^ N  <_  ^ M
 
Theoremleexp1a 8923 Weak mantissa ordering relationship for exponentiation. (Contributed by NM, 18-Dec-2005.)
 RR  RR  N  NN0  0 
 <_  <_  ^ N  <_  ^ N
 
Theoremexple1 8924 Nonnegative integer exponentiation with a mantissa between 0 and 1 inclusive is less than or equal to 1. (Contributed by Paul Chapman, 29-Dec-2007.) (Revised by Mario Carneiro, 5-Jun-2014.)
 RR  0  <_  <_  1  N  NN0 
 ^ N  <_ 
 1
 
Theoremexpubnd 8925 An upper bound on  ^ N when  2  <_ . (Contributed by NM, 19-Dec-2005.)
 RR  N  NN0  2  <_  ^ N  <_  2 ^ N  x.  -  1 ^ N
 
Theoremsqval 8926 Value of the square of a complex number. (Contributed by Raph Levien, 10-Apr-2004.)
 CC  ^ 2  x.
 
Theoremsqneg 8927 The square of the negative of a number.) (Contributed by NM, 15-Jan-2006.)
 CC  -u ^ 2  ^ 2
 
Theoremsqsubswap 8928 Swap the order of subtraction in a square. (Contributed by Scott Fenton, 10-Jun-2013.)
 CC  CC 
 -  ^
 2  -  ^ 2
 
Theoremsqcl 8929 Closure of square. (Contributed by NM, 10-Aug-1999.)
 CC  ^ 2  CC
 
Theoremsqmul 8930 Distribution of square over multiplication. (Contributed by NM, 21-Mar-2008.)
 CC  CC  x.  ^
 2  ^ 2  x.  ^
 2
 
Theoremsqeq0 8931 A number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006.)
 CC  ^
 2  0  0
 
Theoremsqdivap 8932 Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.)
 CC  CC #  0 
 ^ 2  ^
 2  ^ 2
 
Theoremsqne0 8933 A number is nonzero iff its square is nonzero. (Contributed by NM, 11-Mar-2006.)
 CC  ^
 2  =/=  0  =/=  0
 
Theoremresqcl 8934 Closure of the square of a real number. (Contributed by NM, 18-Oct-1999.)
 RR  ^ 2  RR
 
Theoremsqgt0ap 8935 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.)
 RR #  0  0  < 
 ^ 2
 
Theoremnnsqcl 8936 The naturals are closed under squaring. (Contributed by Scott Fenton, 29-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 NN  ^ 2  NN
 
Theoremzsqcl 8937 Integers are closed under squaring. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
 ZZ  ^ 2  ZZ
 
Theoremqsqcl 8938 The square of a rational is rational. (Contributed by Stefan O'Rear, 15-Sep-2014.)
 QQ  ^ 2  QQ
 
Theoremsq11 8939 The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001.) (Proof shortened by Mario Carneiro, 28-May-2016.)
 RR  0  <_  RR  0  <_  ^ 2  ^ 2
 
Theoremlt2sq 8940 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 24-Feb-2006.)
 RR  0  <_  RR  0  <_  < 
 ^ 2  <  ^ 2
 
Theoremle2sq 8941 The square function on nonnegative reals is monotonic. (Contributed by NM, 18-Oct-1999.)
 RR  0  <_  RR  0  <_  <_ 
 ^ 2  <_  ^ 2
 
Theoremle2sq2 8942 The square of a 'less than or equal to' ordering. (Contributed by NM, 21-Mar-2008.)
 RR  0  <_  RR  <_  ^ 2 
 <_  ^ 2
 
Theoremsqge0 8943 A square of a real is nonnegative. (Contributed by NM, 18-Oct-1999.)
 RR  0  <_  ^ 2
 
Theoremzsqcl2 8944 The square of an integer is a nonnegative integer. (Contributed by Mario Carneiro, 18-Apr-2014.) (Revised by Mario Carneiro, 14-Jul-2014.)
 ZZ  ^ 2  NN0
 
Theoremsumsqeq0 8945 Two real numbers are equal to 0 iff their Euclidean norm is. (Contributed by NM, 29-Apr-2005.) (Revised by Stefan O'Rear, 5-Oct-2014.) (Proof shortened by Mario Carneiro, 28-May-2016.)
 RR  RR  0  0  ^ 2  +  ^
 2  0
 
Theoremsqvali 8946 Value of square. Inference version. (Contributed by NM, 1-Aug-1999.)
 CC   =>     ^ 2  x.
 
Theoremsqcli 8947 Closure of square. (Contributed by NM, 2-Aug-1999.)
 CC   =>     ^ 2  CC
 
Theoremsqeq0i 8948 A number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999.)
 CC   =>     ^
 2  0  0
 
Theoremsqmuli 8949 Distribution of square over multiplication. (Contributed by NM, 3-Sep-1999.)
 CC   &     CC   =>     x.  ^ 2 
 ^ 2  x.  ^ 2
 
Theoremsqdivapi 8950 Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &     CC   &    #  0   =>     ^ 2 
 ^ 2  ^ 2
 
Theoremresqcli 8951 Closure of square in reals. (Contributed by NM, 2-Aug-1999.)
 RR   =>     ^ 2  RR
 
Theoremsqgt0api 8952 The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.)
 RR   =>    #  0  0  < 
 ^ 2
 
Theoremsqge0i 8953 A square of a real is nonnegative. (Contributed by NM, 3-Aug-1999.)
 RR   =>     0  <_  ^ 2
 
Theoremlt2sqi 8954 The square function on nonnegative reals is strictly monotonic. (Contributed by NM, 12-Sep-1999.)
 RR   &     RR   =>     0  <_  0  <_  <  ^ 2 
 <  ^ 2
 
Theoremle2sqi 8955 The square function on nonnegative reals is monotonic. (Contributed by NM, 12-Sep-1999.)
 RR   &     RR   =>     0  <_  0  <_  <_  ^ 2 
 <_  ^ 2
 
Theoremsq11i 8956 The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999.)
 RR   &     RR   =>     0  <_  0  <_ 
 ^ 2  ^ 2
 
Theoremsq0 8957 The square of 0 is 0. (Contributed by NM, 6-Jun-2006.)
 0 ^ 2  0
 
Theoremsq0i 8958 If a number is zero, its square is zero. (Contributed by FL, 10-Dec-2006.)
 0  ^ 2  0
 
Theoremsq0id 8959 If a number is zero, its square is zero. Deduction form of sq0i 8958. Converse of sqeq0d 8993. (Contributed by David Moews, 28-Feb-2017.)
 0   =>     ^ 2  0
 
Theoremsq1 8960 The square of 1 is 1. (Contributed by NM, 22-Aug-1999.)
 1 ^ 2  1
 
Theoremneg1sqe1 8961  -u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 -u 1 ^ 2  1
 
Theoremsq2 8962 The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
 2 ^ 2  4
 
Theoremsq3 8963 The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
 3 ^ 2  9
 
Theoremcu2 8964 The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
 2 ^ 3  8
 
Theoremirec 8965 The reciprocal of  _i. (Contributed by NM, 11-Oct-1999.)
 1  _i  -u _i
 
Theoremi2 8966  _i squared. (Contributed by NM, 6-May-1999.)
 _i ^ 2  -u 1
 
Theoremi3 8967  _i cubed. (Contributed by NM, 31-Jan-2007.)
 _i ^ 3  -u _i
 
Theoremi4 8968  _i to the fourth power. (Contributed by NM, 31-Jan-2007.)
 _i ^ 4  1
 
Theoremnnlesq 8969 A positive integer is less than or equal to its square. (Contributed by NM, 15-Sep-1999.) (Revised by Mario Carneiro, 12-Sep-2015.)
 N  NN  N  <_  N ^ 2
 
Theoremexpnass 8970 A counterexample showing that exponentiation is not associative. (Contributed by Stefan Allan and Gérard Lang, 21-Sep-2010.)
 3 ^
 3 ^ 3  <  3 ^ 3 ^ 3
 
Theoremsubsq 8971 Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
 CC  CC 
 ^ 2  -  ^ 2  +  x.  -
 
Theoremsubsq2 8972 Express the difference of the squares of two numbers as a polynomial in the difference of the numbers. (Contributed by NM, 21-Feb-2008.)
 CC  CC 
 ^ 2  -  ^ 2  -  ^ 2  +  2  x.  x.  -
 
Theorembinom2i 8973 The square of a binomial. (Contributed by NM, 11-Aug-1999.)
 CC   &     CC   =>     +  ^ 2  ^ 2  +  2  x.  x.  +  ^ 2
 
Theoremsubsqi 8974 Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
 CC   &     CC   =>     ^
 2  -  ^ 2  +  x.  -
 
Theorembinom2 8975 The square of a binomial. (Contributed by FL, 10-Dec-2006.)
 CC  CC  +  ^
 2  ^
 2  + 
 2  x.  x.  + 
 ^ 2
 
Theorembinom21 8976 Special case of binom2 8975 where  1. (Contributed by Scott Fenton, 11-May-2014.)
 CC  +  1 ^ 2  ^ 2  +  2  x.  +  1
 
Theorembinom2sub 8977 Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
 CC  CC 
 -  ^
 2  ^
 2  - 
 2  x.  x.  + 
 ^ 2
 
Theorembinom2subi 8978 Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
 CC   &     CC   =>     -  ^ 2  ^ 2 
 -  2  x.  x.  +  ^ 2
 
Theorembinom3 8979 The cube of a binomial. (Contributed by Mario Carneiro, 24-Apr-2015.)
 CC  CC  +  ^
 3  ^
 3  + 
 3  x.  ^ 2  x.  +  3  x.  x.  ^
 2  +  ^
 3
 
Theoremzesq 8980 An integer is even iff its square is even. (Contributed by Mario Carneiro, 12-Sep-2015.)
 N  ZZ  N  2  ZZ  N ^ 2  2 
 ZZ
 
Theoremnnesq 8981 A positive integer is even iff its square is even. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
 N  NN  N  2  NN  N ^ 2  2 
 NN
 
Theorembernneq 8982 Bernoulli's inequality, due to Johan Bernoulli (1667-1748). (Contributed by NM, 21-Feb-2005.)
 RR  N  NN0  -u 1  <_  1  +  x.  N 
 <_  1  +  ^ N
 
Theorembernneq2 8983 Variation of Bernoulli's inequality bernneq 8982. (Contributed by NM, 18-Oct-2007.)
 RR  N  NN0  0  <_ 
 -  1  x.  N  +  1  <_  ^ N
 
Theorembernneq3 8984 A corollary of bernneq 8982. (Contributed by Mario Carneiro, 11-Mar-2014.)
 P  ZZ>= `  2  N  NN0  N  <  P ^ N
 
Theoremexpnbnd 8985* Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
 RR  RR  1  <  k  NN  <  ^
 k
 
Theoremexpnlbnd 8986* The reciprocal of exponentiation with a mantissa greater than 1 has no lower bound. (Contributed by NM, 18-Jul-2008.)
 RR+  RR  1  <  k  NN  1 
 ^ k 
 <
 
Theoremexpnlbnd2 8987* 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.)
 RR+  RR  1  <  j  NN  k  ZZ>= `  j 1  ^ k  <
 
Theoremexp0d 8988 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 0  1
 
Theoremexp1d 8989 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 1
 
Theoremexpeq0d 8990 Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     N  NN   &     ^ N  0   =>     0
 
Theoremsqvald 8991 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 2  x.
 
Theoremsqcld 8992 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 2 
 CC
 
Theoremsqeq0d 8993 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     ^ 2  0   =>     0
 
Theoremexpcld 8994 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     N  NN0   =>     ^ N 
 CC
 
Theoremexpp1d 8995 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.)
 CC   &     N  NN0   =>     ^ N  +  1  ^ N  x.
 
Theoremexpaddd 8996 Sum of exponents law for nonnegative integer exponentiation. Proposition 10-4.2(a) of [Gleason] p. 135. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     N  NN0   &     M  NN0   =>     ^ M  +  N  ^ M  x.  ^ N
 
Theoremexpmuld 8997 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.)
 CC   &     N  NN0   &     M  NN0   =>     ^ M  x.  N  ^ M ^ N
 
Theoremsqrecapd 8998 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   =>     1 
 ^ 2  1  ^ 2
 
Theoremexpclzapd 8999 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N 
 CC
 
Theoremexpap0d 9000 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N #  0
    < Previous  Next >

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-9381
  Copyright terms: Public domain < Previous  Next >