HomeHome Intuitionistic Logic Explorer
Theorem List (p. 91 of 95)
< 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 - 9001-9100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremneg1sqe1 9001  -u 1 squared is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 -u 1 ^ 2  1
 
Theoremsq2 9002 The square of 2 is 4. (Contributed by NM, 22-Aug-1999.)
 2 ^ 2  4
 
Theoremsq3 9003 The square of 3 is 9. (Contributed by NM, 26-Apr-2006.)
 3 ^ 2  9
 
Theoremcu2 9004 The cube of 2 is 8. (Contributed by NM, 2-Aug-2004.)
 2 ^ 3  8
 
Theoremirec 9005 The reciprocal of  _i. (Contributed by NM, 11-Oct-1999.)
 1  _i  -u _i
 
Theoremi2 9006  _i squared. (Contributed by NM, 6-May-1999.)
 _i ^ 2  -u 1
 
Theoremi3 9007  _i cubed. (Contributed by NM, 31-Jan-2007.)
 _i ^ 3  -u _i
 
Theoremi4 9008  _i to the fourth power. (Contributed by NM, 31-Jan-2007.)
 _i ^ 4  1
 
Theoremnnlesq 9009 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 9010 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 9011 Factor the difference of two squares. (Contributed by NM, 21-Feb-2008.)
 CC  CC 
 ^ 2  -  ^ 2  +  x.  -
 
Theoremsubsq2 9012 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 9013 The square of a binomial. (Contributed by NM, 11-Aug-1999.)
 CC   &     CC   =>     +  ^ 2  ^ 2  +  2  x.  x.  +  ^ 2
 
Theoremsubsqi 9014 Factor the difference of two squares. (Contributed by NM, 7-Feb-2005.)
 CC   &     CC   =>     ^
 2  -  ^ 2  +  x.  -
 
Theorembinom2 9015 The square of a binomial. (Contributed by FL, 10-Dec-2006.)
 CC  CC  +  ^
 2  ^
 2  + 
 2  x.  x.  + 
 ^ 2
 
Theorembinom21 9016 Special case of binom2 9015 where  1. (Contributed by Scott Fenton, 11-May-2014.)
 CC  +  1 ^ 2  ^ 2  +  2  x.  +  1
 
Theorembinom2sub 9017 Expand the square of a subtraction. (Contributed by Scott Fenton, 10-Jun-2013.)
 CC  CC 
 -  ^
 2  ^
 2  - 
 2  x.  x.  + 
 ^ 2
 
Theorembinom2subi 9018 Expand the square of a subtraction. (Contributed by Scott Fenton, 13-Jun-2013.)
 CC   &     CC   =>     -  ^ 2  ^ 2 
 -  2  x.  x.  +  ^ 2
 
Theorembinom3 9019 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 9020 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 9021 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 9022 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 9023 Variation of Bernoulli's inequality bernneq 9022. (Contributed by NM, 18-Oct-2007.)
 RR  N  NN0  0  <_ 
 -  1  x.  N  +  1  <_  ^ N
 
Theorembernneq3 9024 A corollary of bernneq 9022. (Contributed by Mario Carneiro, 11-Mar-2014.)
 P  ZZ>= `  2  N  NN0  N  <  P ^ N
 
Theoremexpnbnd 9025* Exponentiation with a mantissa greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)
 RR  RR  1  <  k  NN  <  ^
 k
 
Theoremexpnlbnd 9026* 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 9027* 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 9028 Value of a complex number raised to the 0th power. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 0  1
 
Theoremexp1d 9029 Value of a complex number raised to the first power. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 1
 
Theoremexpeq0d 9030 Positive integer exponentiation is 0 iff its mantissa is 0. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     N  NN   &     ^ N  0   =>     0
 
Theoremsqvald 9031 Value of square. Inference version. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 2  x.
 
Theoremsqcld 9032 Closure of square. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   =>     ^ 2 
 CC
 
Theoremsqeq0d 9033 A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     ^ 2  0   =>     0
 
Theoremexpcld 9034 Closure law for nonnegative integer exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     N  NN0   =>     ^ N 
 CC
 
Theoremexpp1d 9035 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 9036 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 9037 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 9038 Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   =>     1 
 ^ 2  1  ^ 2
 
Theoremexpclzapd 9039 Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N 
 CC
 
Theoremexpap0d 9040 Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N #  0
 
Theoremexpnegapd 9041 Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ -u N  1  ^ N
 
Theoremexprecapd 9042 Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     1 
 ^ N  1  ^ N
 
Theoremexpp1zapd 9043 Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N  +  1  ^ N  x.
 
Theoremexpm1apd 9044 Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   =>     ^ N  -  1  ^ N
 
Theoremexpsubapd 9045 Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.)
 CC   &    #  0   &     N  ZZ   &     M  ZZ   =>     ^ M  -  N  ^ M  ^ N
 
Theoremsqmuld 9046 Distribution of square over multiplication. (Contributed by Mario Carneiro, 28-May-2016.)
 CC   &     CC   =>     x.  ^ 2  ^
 2  x.  ^ 2
 
Theoremsqdivapd 9047 Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   =>    
 ^ 2  ^
 2  ^ 2
 
Theoremexpdivapd 9048 Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.)
 CC   &     CC   &    #  0   &     N  NN0   =>    
 ^ N  ^ N 
 ^ N
 
Theoremmulexpd 9049 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.)
 CC   &     CC   &     N  NN0   =>     x.  ^ N  ^ N  x.  ^ N
 
Theorem0expd 9050 Value of zero raised to a positive integer power. (Contributed by Mario Carneiro, 28-May-2016.)
 N  NN   =>    
 0 ^ N  0
 
Theoremreexpcld 9051 Closure of exponentiation of reals. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     N  NN0   =>     ^ N 
 RR
 
Theoremexpge0d 9052 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     N  NN0   &     0  <_    =>     0  <_  ^ N
 
Theoremexpge1d 9053 Nonnegative integer exponentiation with a nonnegative mantissa is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     N  NN0   &     1  <_    =>     1  <_  ^ N
 
Theoremnnsqcld 9054 The naturals are closed under squaring. (Contributed by Mario Carneiro, 28-May-2016.)
 NN   =>     ^ 2 
 NN
 
Theoremnnexpcld 9055 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
 NN   &     N  NN0   =>     ^ N 
 NN
 
Theoremnn0expcld 9056 Closure of exponentiation of nonnegative integers. (Contributed by Mario Carneiro, 28-May-2016.)
 NN0   &     N  NN0   =>     ^ N 
 NN0
 
Theoremrpexpcld 9057 Closure law for exponentiation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.)
 RR+   &     N  ZZ   =>     ^ N  RR+
 
Theoremreexpclzapd 9058 Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   &     N  ZZ   =>     ^ N 
 RR
 
Theoremresqcld 9059 Closure of square in reals. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   =>     ^ 2 
 RR
 
Theoremsqge0d 9060 A square of a real is nonnegative. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   =>     0  <_  ^ 2
 
Theoremsqgt0apd 9061 The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.)
 RR   &    #  0   =>     0  <  ^ 2
 
Theoremleexp2ad 9062 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     1  <_    &     N  ZZ>= `  M   =>     ^ M  <_  ^ N
 
Theoremleexp2rd 9063 Ordering relationship for exponentiation. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     M  NN0   &     N  ZZ>= `  M   &     0  <_    &     <_  1   =>     ^ N  <_  ^ M
 
Theoremlt2sqd 9064 The square function on nonnegative reals is strictly monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     0  <_    &     0  <_    =>     < 
 ^ 2  <  ^ 2
 
Theoremle2sqd 9065 The square function on nonnegative reals is monotonic. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     0  <_    &     0  <_    =>     <_ 
 ^ 2  <_  ^ 2
 
Theoremsq11d 9066 The square function is one-to-one for nonnegative reals. (Contributed by Mario Carneiro, 28-May-2016.)
 RR   &     RR   &     0  <_    &     0  <_    &     ^ 2  ^ 2   =>   
 
3.6  Elementary real and complex functions
 
3.6.1  Real and imaginary parts; conjugate
 
Syntaxccj 9067 Extend class notation to include complex conjugate function.

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

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

 Im
 
Definitiondf-cj 9070* Define the complex conjugate function. See cjcli 9141 for its closure and cjval 9073 for its value. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
 *  CC  |->  iota_  CC  +  RR  _i  x.  -  RR
 
Definitiondf-re 9071 Define a function whose value is the real part of a complex number. See reval 9077 for its value, recli 9139 for its closure, and replim 9087 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
 Re  CC  |->  +  * `
  2
 
Definitiondf-im 9072 Define a function whose value is the imaginary part of a complex number. See imval 9078 for its value, imcli 9140 for its closure, and replim 9087 for its use in decomposing a complex number. (Contributed by NM, 9-May-1999.)
 Im  CC  |->  Re
 `  _i
 
Theoremcjval 9073* The value of the conjugate of a complex number. (Contributed by Mario Carneiro, 6-Nov-2013.)
 CC  * `  iota_  CC  +  RR  _i  x.  -  RR
 
Theoremcjth 9074 The defining property of the complex conjugate. (Contributed by Mario Carneiro, 6-Nov-2013.)
 CC  +  * `  RR  _i  x.  -  * ` 
 RR
 
Theoremcjf 9075 Domain and codomain of the conjugate function. (Contributed by Mario Carneiro, 6-Nov-2013.)
 * : CC --> CC
 
Theoremcjcl 9076 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.)
 CC  * `  CC
 
Theoremreval 9077 The value of the real part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
 CC  Re `  +  * `  2
 
Theoremimval 9078 The value of the imaginary part of a complex number. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
 CC  Im `  Re `  _i
 
Theoremimre 9079 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.)
 CC  Im `  Re `  -u _i  x.
 
Theoremreim 9080 The real part of a complex number in terms of the imaginary part function. (Contributed by Mario Carneiro, 31-Mar-2015.)
 CC  Re `  Im `  _i  x.
 
Theoremrecl 9081 The real part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
 CC  Re `  RR
 
Theoremimcl 9082 The imaginary part of a complex number is real. (Contributed by NM, 9-May-1999.) (Revised by Mario Carneiro, 6-Nov-2013.)
 CC  Im `  RR
 
Theoremref 9083 Domain and codomain of the real part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
 Re : CC --> RR
 
Theoremimf 9084 Domain and codomain of the imaginary part function. (Contributed by Paul Chapman, 22-Oct-2007.) (Revised by Mario Carneiro, 6-Nov-2013.)
 Im : CC --> RR
 
Theoremcrre 9085 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.)
 RR  RR  Re `  +  _i  x.
 
Theoremcrim 9086 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.)
 RR  RR  Im `  +  _i  x.
 
Theoremreplim 9087 Reconstruct a complex number from its real and imaginary parts. (Contributed by NM, 10-May-1999.) (Revised by Mario Carneiro, 7-Nov-2013.)
 CC  Re `  +  _i  x.  Im `
 
Theoremremim 9088 Value of the conjugate of a complex number. The value is the real part minus  _i 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.)
 CC  * `  Re `  -  _i  x.  Im `
 
Theoremreim0 9089 The imaginary part of a real number is 0. (Contributed by NM, 18-Mar-2005.) (Revised by Mario Carneiro, 7-Nov-2013.)
 RR  Im `  0
 
Theoremreim0b 9090 A number is real iff its imaginary part is 0. (Contributed by NM, 26-Sep-2005.)
 CC  RR  Im `  0
 
Theoremrereb 9091 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.)
 CC  RR  Re `
 
Theoremmulreap 9092 A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.)
 CC  RR #  0  RR  x. 
 RR
 
Theoremrere 9093 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.)
 RR  Re `
 
Theoremcjreb 9094 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.)
 CC  RR  * `
 
Theoremrecj 9095 Real part of a complex conjugate. (Contributed by Mario Carneiro, 14-Jul-2014.)
 CC  Re `  * `  Re `
 
Theoremreneg 9096 Real part of negative. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
 CC  Re `  -u  -u Re
 `
 
Theoremreadd 9097 Real part distributes over addition. (Contributed by NM, 17-Mar-2005.) (Revised by Mario Carneiro, 14-Jul-2014.)
 CC  CC  Re `  +  Re `  +  Re `
 
Theoremresub 9098 Real part distributes over subtraction. (Contributed by NM, 17-Mar-2005.)
 CC  CC  Re `  -  Re ` 
 -  Re `
 
Theoremremullem 9099 Lemma for remul 9100, immul 9107, and cjmul 9113. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
 CC  CC  Re
 `  x.  Re `  x.  Re ` 
 -  Im
 `  x.  Im `  Im `  x.  Re `  x.  Im `  +  Im
 `  x.  Re `  * `  x.  * `  x.  * `
 
Theoremremul 9100 Real part of a product. (Contributed by NM, 28-Jul-1999.) (Revised by Mario Carneiro, 14-Jul-2014.)
 CC  CC  Re `  x.  Re `  x.  Re `  -  Im `  x.  Im `
    < 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-9400 95 9401-9457
  Copyright terms: Public domain < Previous  Next >