HomeHome Intuitionistic Logic Explorer
Theorem List (p. 83 of 102)
< 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 - 8201-8300   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem5nn0 8201 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |-  5  e.  NN0
 
Theorem6nn0 8202 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |-  6  e.  NN0
 
Theorem7nn0 8203 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |-  7  e.  NN0
 
Theorem8nn0 8204 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |-  8  e.  NN0
 
Theorem9nn0 8205 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |-  9  e.  NN0
 
Theorem10nn0 8206 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
 |- 
 10  e.  NN0
 
Theoremnn0ge0 8207 A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.)
 |-  ( N  e.  NN0  -> 
 0  <_  N )
 
Theoremnn0nlt0 8208 A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
 |-  ( A  e.  NN0  ->  -.  A  <  0 )
 
Theoremnn0ge0i 8209 Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  N  e.  NN0   =>    |-  0  <_  N
 
Theoremnn0le0eq0 8210 A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005.)
 |-  ( N  e.  NN0  ->  ( N  <_  0  <->  N  =  0
 ) )
 
Theoremnn0p1gt0 8211 A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
 |-  ( N  e.  NN0  -> 
 0  <  ( N  +  1 ) )
 
Theoremnnnn0addcl 8212 A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 |-  ( ( M  e.  NN  /\  N  e.  NN0 )  ->  ( M  +  N )  e.  NN )
 
Theoremnn0nnaddcl 8213 A nonnegative integer plus a positive integer is a positive integer. (Contributed by NM, 22-Dec-2005.)
 |-  ( ( M  e.  NN0  /\  N  e.  NN )  ->  ( M  +  N )  e.  NN )
 
Theorem0mnnnnn0 8214 The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
 |-  ( N  e.  NN  ->  ( 0  -  N )  e/  NN0 )
 
Theoremun0addcl 8215 If  S is closed under addition, then so is  S  u.  { 0 }. (Contributed by Mario Carneiro, 17-Jul-2014.)
 |-  ( ph  ->  S  C_ 
 CC )   &    |-  T  =  ( S  u.  { 0 } )   &    |-  ( ( ph  /\  ( M  e.  S  /\  N  e.  S ) )  ->  ( M  +  N )  e.  S )   =>    |-  ( ( ph  /\  ( M  e.  T  /\  N  e.  T )
 )  ->  ( M  +  N )  e.  T )
 
Theoremun0mulcl 8216 If  S is closed under multiplication, then so is  S  u.  { 0 }. (Contributed by Mario Carneiro, 17-Jul-2014.)
 |-  ( ph  ->  S  C_ 
 CC )   &    |-  T  =  ( S  u.  { 0 } )   &    |-  ( ( ph  /\  ( M  e.  S  /\  N  e.  S ) )  ->  ( M  x.  N )  e.  S )   =>    |-  ( ( ph  /\  ( M  e.  T  /\  N  e.  T )
 )  ->  ( M  x.  N )  e.  T )
 
Theoremnn0addcl 8217 Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
 |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  ->  ( M  +  N )  e.  NN0 )
 
Theoremnn0mulcl 8218 Closure of multiplication of nonnegative integers. (Contributed by NM, 22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
 |-  ( ( M  e.  NN0  /\  N  e.  NN0 )  ->  ( M  x.  N )  e.  NN0 )
 
Theoremnn0addcli 8219 Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  M  e.  NN0   &    |-  N  e.  NN0   =>    |-  ( M  +  N )  e.  NN0
 
Theoremnn0mulcli 8220 Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  M  e.  NN0   &    |-  N  e.  NN0   =>    |-  ( M  x.  N )  e.  NN0
 
Theoremnn0p1nn 8221 A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
 |-  ( N  e.  NN0  ->  ( N  +  1
 )  e.  NN )
 
Theorempeano2nn0 8222 Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  NN0  ->  ( N  +  1
 )  e.  NN0 )
 
Theoremnnm1nn0 8223 A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.)
 |-  ( N  e.  NN  ->  ( N  -  1
 )  e.  NN0 )
 
Theoremelnn0nn 8224 The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 |-  ( N  e.  NN0  <->  ( N  e.  CC  /\  ( N  +  1 )  e.  NN ) )
 
Theoremelnnnn0 8225 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)
 |-  ( N  e.  NN  <->  ( N  e.  CC  /\  ( N  -  1 )  e. 
 NN0 ) )
 
Theoremelnnnn0b 8226 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)
 |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  0  <  N ) )
 
Theoremelnnnn0c 8227 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)
 |-  ( N  e.  NN  <->  ( N  e.  NN0  /\  1  <_  N ) )
 
Theoremnn0addge1 8228 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 |-  ( ( A  e.  RR  /\  N  e.  NN0 )  ->  A  <_  ( A  +  N )
 )
 
Theoremnn0addge2 8229 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 |-  ( ( A  e.  RR  /\  N  e.  NN0 )  ->  A  <_  ( N  +  A )
 )
 
Theoremnn0addge1i 8230 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 |-  A  e.  RR   &    |-  N  e.  NN0   =>    |-  A  <_  ( A  +  N )
 
Theoremnn0addge2i 8231 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
 |-  A  e.  RR   &    |-  N  e.  NN0   =>    |-  A  <_  ( N  +  A )
 
Theoremnn0le2xi 8232 A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  N  e.  NN0   =>    |-  N  <_  ( 2  x.  N )
 
Theoremnn0lele2xi 8233 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
 |-  M  e.  NN0   &    |-  N  e.  NN0   =>    |-  ( N  <_  M  ->  N  <_  ( 2  x.  M ) )
 
Theoremnn0supp 8234 Two ways to write the support of a function on  NN0. (Contributed by Mario Carneiro, 29-Dec-2014.)
 |-  ( F : I --> NN0  ->  ( `' F " ( _V  \  {
 0 } ) )  =  ( `' F " NN ) )
 
Theoremnnnn0d 8235 A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN )   =>    |-  ( ph  ->  A  e.  NN0 )
 
Theoremnn0red 8236 A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN0 )   =>    |-  ( ph  ->  A  e.  RR )
 
Theoremnn0cnd 8237 A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN0 )   =>    |-  ( ph  ->  A  e.  CC )
 
Theoremnn0ge0d 8238 A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN0 )   =>    |-  ( ph  ->  0  <_  A )
 
Theoremnn0addcld 8239 Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN0 )   &    |-  ( ph  ->  B  e.  NN0 )   =>    |-  ( ph  ->  ( A  +  B )  e.  NN0 )
 
Theoremnn0mulcld 8240 Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
 |-  ( ph  ->  A  e.  NN0 )   &    |-  ( ph  ->  B  e.  NN0 )   =>    |-  ( ph  ->  ( A  x.  B )  e. 
 NN0 )
 
Theoremnn0readdcl 8241 Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
 |-  ( ( A  e.  NN0  /\  B  e.  NN0 )  ->  ( A  +  B )  e.  RR )
 
Theoremnn0ge2m1nn 8242 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
 |-  ( ( N  e.  NN0  /\  2  <_  N ) 
 ->  ( N  -  1
 )  e.  NN )
 
Theoremnn0ge2m1nn0 8243 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
 |-  ( ( N  e.  NN0  /\  2  <_  N ) 
 ->  ( N  -  1
 )  e.  NN0 )
 
Theoremnn0nndivcl 8244 Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
 |-  ( ( K  e.  NN0  /\  L  e.  NN )  ->  ( K  /  L )  e.  RR )
 
3.4.8  Integers (as a subset of complex numbers)
 
Syntaxcz 8245 Extend class notation to include the class of integers.
 class  ZZ
 
Definitiondf-z 8246 Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.)
 |- 
 ZZ  =  { n  e.  RR  |  ( n  =  0  \/  n  e.  NN  \/  -u n  e.  NN ) }
 
Theoremelz 8247 Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
 |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  =  0  \/  N  e.  NN  \/  -u N  e.  NN )
 ) )
 
Theoremnnnegz 8248 The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
 |-  ( N  e.  NN  -> 
 -u N  e.  ZZ )
 
Theoremzre 8249 An integer is a real. (Contributed by NM, 8-Jan-2002.)
 |-  ( N  e.  ZZ  ->  N  e.  RR )
 
Theoremzcn 8250 An integer is a complex number. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  ZZ  ->  N  e.  CC )
 
Theoremzrei 8251 An integer is a real number. (Contributed by NM, 14-Jul-2005.)
 |-  A  e.  ZZ   =>    |-  A  e.  RR
 
Theoremzssre 8252 The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
 |- 
 ZZ  C_  RR
 
Theoremzsscn 8253 The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
 |- 
 ZZ  C_  CC
 
Theoremzex 8254 The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
 |- 
 ZZ  e.  _V
 
Theoremelnnz 8255 Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
 |-  ( N  e.  NN  <->  ( N  e.  ZZ  /\  0  <  N ) )
 
Theorem0z 8256 Zero is an integer. (Contributed by NM, 12-Jan-2002.)
 |-  0  e.  ZZ
 
Theorem0zd 8257 Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
 |-  ( ph  ->  0  e.  ZZ )
 
Theoremelnn0z 8258 Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  NN0  <->  ( N  e.  ZZ  /\  0  <_  N ) )
 
Theoremelznn0nn 8259 Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
 |-  ( N  e.  ZZ  <->  ( N  e.  NN0  \/  ( N  e.  RR  /\  -u N  e.  NN ) ) )
 
Theoremelznn0 8260 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  e.  NN0  \/  -u N  e.  NN0 ) ) )
 
Theoremelznn 8261 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
 |-  ( N  e.  ZZ  <->  ( N  e.  RR  /\  ( N  e.  NN  \/  -u N  e.  NN0 )
 ) )
 
Theoremnnssz 8262 Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)
 |- 
 NN  C_  ZZ
 
Theoremnn0ssz 8263 Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)
 |- 
 NN0  C_  ZZ
 
Theoremnnz 8264 A positive integer is an integer. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  NN  ->  N  e.  ZZ )
 
Theoremnn0z 8265 A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  NN0  ->  N  e.  ZZ )
 
Theoremnnzi 8266 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 |-  N  e.  NN   =>    |-  N  e.  ZZ
 
Theoremnn0zi 8267 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 |-  N  e.  NN0   =>    |-  N  e.  ZZ
 
Theoremelnnz1 8268 Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 |-  ( N  e.  NN  <->  ( N  e.  ZZ  /\  1  <_  N ) )
 
Theoremnnzrab 8269 Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
 |- 
 NN  =  { x  e.  ZZ  |  1  <_  x }
 
Theoremnn0zrab 8270 Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
 |- 
 NN0  =  { x  e.  ZZ  |  0  <_  x }
 
Theorem1z 8271 One is an integer. (Contributed by NM, 10-May-2004.)
 |-  1  e.  ZZ
 
Theorem1zzd 8272 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
 |-  ( ph  ->  1  e.  ZZ )
 
Theorem2z 8273 Two is an integer. (Contributed by NM, 10-May-2004.)
 |-  2  e.  ZZ
 
Theorem3z 8274 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
 |-  3  e.  ZZ
 
Theorem4z 8275 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
 |-  4  e.  ZZ
 
Theoremznegcl 8276 Closure law for negative integers. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  ZZ  -> 
 -u N  e.  ZZ )
 
Theoremneg1z 8277 -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
 |-  -u 1  e.  ZZ
 
Theoremznegclb 8278 A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
 |-  ( A  e.  CC  ->  ( A  e.  ZZ  <->  -u A  e.  ZZ ) )
 
Theoremnn0negz 8279 The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
 |-  ( N  e.  NN0  ->  -u N  e.  ZZ )
 
Theoremnn0negzi 8280 The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
 |-  N  e.  NN0   =>    |-  -u N  e.  ZZ
 
Theorempeano2z 8281 Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
 |-  ( N  e.  ZZ  ->  ( N  +  1 )  e.  ZZ )
 
Theoremzaddcllempos 8282 Lemma for zaddcl 8285. Special case in which  N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 |-  ( ( M  e.  ZZ  /\  N  e.  NN )  ->  ( M  +  N )  e.  ZZ )
 
Theorempeano2zm 8283 "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
 |-  ( N  e.  ZZ  ->  ( N  -  1
 )  e.  ZZ )
 
Theoremzaddcllemneg 8284 Lemma for zaddcl 8285. Special case in which  -u N is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
 |-  ( ( M  e.  ZZ  /\  N  e.  RR  /\  -u N  e.  NN )  ->  ( M  +  N )  e.  ZZ )
 
Theoremzaddcl 8285 Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  +  N )  e.  ZZ )
 
Theoremzsubcl 8286 Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  -  N )  e.  ZZ )
 
Theoremztri3or0 8287 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
 |-  ( N  e.  ZZ  ->  ( N  <  0  \/  N  =  0  \/  0  <  N ) )
 
Theoremztri3or 8288 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  \/  M  =  N  \/  N  <  M ) )
 
Theoremzletric 8289 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  <_  B  \/  B  <_  A ) )
 
Theoremzlelttric 8290 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  <_  B  \/  B  <  A ) )
 
Theoremzltnle 8291 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  <  B  <->  -.  B  <_  A )
 )
 
Theoremzleloe 8292 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
 |-  ( ( A  e.  ZZ  /\  B  e.  ZZ )  ->  ( A  <_  B  <-> 
 ( A  <  B  \/  A  =  B ) ) )
 
Theoremznnnlt1 8293 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
 |-  ( N  e.  ZZ  ->  ( -.  N  e.  NN 
 <->  N  <  1 ) )
 
Theoremzletr 8294 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
 |-  ( ( J  e.  ZZ  /\  K  e.  ZZ  /\  L  e.  ZZ )  ->  ( ( J  <_  K 
 /\  K  <_  L )  ->  J  <_  L ) )
 
Theoremzrevaddcl 8295 Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
 |-  ( N  e.  ZZ  ->  ( ( M  e.  CC  /\  ( M  +  N )  e.  ZZ ) 
 <->  M  e.  ZZ )
 )
 
Theoremznnsub 8296 The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7952.) (Contributed by NM, 11-May-2004.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <-> 
 ( N  -  M )  e.  NN )
 )
 
Theoremzmulcl 8297 Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  x.  N )  e.  ZZ )
 
Theoremzltp1le 8298 Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <-> 
 ( M  +  1 )  <_  N )
 )
 
Theoremzleltp1 8299 Integer ordering relation. (Contributed by NM, 10-May-2004.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <_  N  <->  M  <  ( N  +  1 ) ) )
 
Theoremzlem1lt 8300 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
 |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <_  N  <-> 
 ( M  -  1
 )  <  N )
 )
    < 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-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
  Copyright terms: Public domain < Previous  Next >