HomeHome Intuitionistic Logic Explorer
Theorem List (p. 65 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 - 6401-6500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Syntaxcltr 6401 Signed real ordering relation.
 class  <R
 
Definitiondf-ni 6402 Define the class of positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 15-Aug-1995.)
 |- 
 N.  =  ( om  \  { (/) } )
 
Definitiondf-pli 6403 Define addition on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
 |- 
 +N  =  (  +o  |`  ( N.  X.  N. ) )
 
Definitiondf-mi 6404 Define multiplication on positive integers. This is a "temporary" set used in the construction of complex numbers and is intended to be used only by the construction. (Contributed by NM, 26-Aug-1995.)
 |- 
 .N  =  (  .o  |`  ( N.  X.  N. ) )
 
Definitiondf-lti 6405 Define 'less than' on positive integers. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by NM, 6-Feb-1996.)
 |- 
 <N  =  (  _E  i^i  ( N.  X.  N. ) )
 
Theoremelni 6406 Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.)
 |-  ( A  e.  N.  <->  ( A  e.  om  /\  A  =/= 
 (/) ) )
 
Theorempinn 6407 A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)
 |-  ( A  e.  N.  ->  A  e.  om )
 
Theorempion 6408 A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.)
 |-  ( A  e.  N.  ->  A  e.  On )
 
Theorempiord 6409 A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)
 |-  ( A  e.  N.  ->  Ord  A )
 
Theoremniex 6410 The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)
 |- 
 N.  e.  _V
 
Theorem0npi 6411 The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)
 |- 
 -.  (/)  e.  N.
 
Theoremelni2 6412 Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)
 |-  ( A  e.  N.  <->  ( A  e.  om  /\  (/)  e.  A ) )
 
Theorem1pi 6413 Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)
 |- 
 1o  e.  N.
 
Theoremaddpiord 6414 Positive integer addition in terms of ordinal addition. (Contributed by NM, 27-Aug-1995.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  +N  B )  =  ( A  +o  B ) )
 
Theoremmulpiord 6415 Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  .N  B )  =  ( A  .o  B ) )
 
Theoremmulidpi 6416 1 is an identity element for multiplication on positive integers. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.)
 |-  ( A  e.  N.  ->  ( A  .N  1o )  =  A )
 
Theoremltpiord 6417 Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  <N  B  <->  A  e.  B )
 )
 
Theoremltsopi 6418 Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)
 |- 
 <N  Or  N.
 
Theorempitric 6419 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  <N  B  <->  -.  ( A  =  B  \/  B  <N  A )
 ) )
 
Theorempitri3or 6420 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  <N  B  \/  A  =  B  \/  B  <N  A )
 )
 
Theoremltdcpi 6421 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  -> DECID  A  <N  B )
 
Theoremltrelpi 6422 Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)
 |- 
 <N  C_  ( N.  X.  N. )
 
Theoremdmaddpi 6423 Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)
 |- 
 dom  +N  =  ( N.  X.  N. )
 
Theoremdmmulpi 6424 Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)
 |- 
 dom  .N  =  ( N.  X.  N. )
 
Theoremaddclpi 6425 Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  +N  B )  e.  N. )
 
Theoremmulclpi 6426 Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  .N  B )  e.  N. )
 
Theoremaddcompig 6427 Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  +N  B )  =  ( B  +N  A ) )
 
Theoremaddasspig 6428 Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( ( A  +N  B )  +N  C )  =  ( A  +N  ( B  +N  C ) ) )
 
Theoremmulcompig 6429 Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  .N  B )  =  ( B  .N  A ) )
 
Theoremmulasspig 6430 Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( ( A  .N  B )  .N  C )  =  ( A  .N  ( B  .N  C ) ) )
 
Theoremdistrpig 6431 Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( A  .N  ( B  +N  C ) )  =  ( ( A  .N  B )  +N  ( A  .N  C ) ) )
 
Theoremaddcanpig 6432 Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( ( A  +N  B )  =  ( A  +N  C )  <->  B  =  C ) )
 
Theoremmulcanpig 6433 Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( ( A  .N  B )  =  ( A  .N  C )  <->  B  =  C ) )
 
Theoremaddnidpig 6434 There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  -.  ( A  +N  B )  =  A )
 
Theoremltexpi 6435* Ordering on positive integers in terms of existence of sum. (Contributed by NM, 15-Mar-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N. )  ->  ( A  <N  B  <->  E. x  e.  N.  ( A  +N  x )  =  B )
 )
 
Theoremltapig 6436 Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( A  <N  B  <->  ( C  +N  A )  <N  ( C  +N  B ) ) )
 
Theoremltmpig 6437 Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  ( A  <N  B  <->  ( C  .N  A )  <N  ( C  .N  B ) ) )
 
Theorem1lt2pi 6438 One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)
 |- 
 1o  <N  ( 1o  +N  1o )
 
Theoremnlt1pig 6439 No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)
 |-  ( A  e.  N.  ->  -.  A  <N  1o )
 
Theoremindpi 6440* Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)
 |-  ( x  =  1o  ->  ( ph  <->  ps ) )   &    |-  ( x  =  y  ->  (
 ph 
 <->  ch ) )   &    |-  ( x  =  ( y  +N  1o )  ->  ( ph 
 <-> 
 th ) )   &    |-  ( x  =  A  ->  (
 ph 
 <->  ta ) )   &    |-  ps   &    |-  (
 y  e.  N.  ->  ( ch  ->  th )
 )   =>    |-  ( A  e.  N.  ->  ta )
 
Theoremnnppipi 6441 A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)
 |-  ( ( A  e.  om 
 /\  B  e.  N. )  ->  ( A  +o  B )  e.  N. )
 
Definitiondf-plpq 6442* Define pre-addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. This "pre-addition" operation works directly with ordered pairs of integers. The actual positive fraction addition  +Q (df-plqqs 6447) works with the equivalence classes of these ordered pairs determined by the equivalence relation  ~Q (df-enq 6445). (Analogous remarks apply to the other "pre-" operations in the complex number construction that follows.) From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 28-Aug-1995.)
 |- 
 +pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |-> 
 <. ( ( ( 1st `  x )  .N  ( 2nd `  y ) )  +N  ( ( 1st `  y )  .N  ( 2nd `  x ) ) ) ,  ( ( 2nd `  x )  .N  ( 2nd `  y
 ) ) >. )
 
Definitiondf-mpq 6443* Define pre-multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 28-Aug-1995.)
 |- 
 .pQ  =  ( x  e.  ( N.  X.  N. ) ,  y  e.  ( N.  X.  N. )  |-> 
 <. ( ( 1st `  x )  .N  ( 1st `  y
 ) ) ,  (
 ( 2nd `  x )  .N  ( 2nd `  y
 ) ) >. )
 
Definitiondf-ltpq 6444* Define pre-ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 28-Aug-1995.)
 |- 
 <pQ  =  { <. x ,  y >.  |  ( ( x  e.  ( N. 
 X.  N. )  /\  y  e.  ( N.  X.  N. ) )  /\  ( ( 1st `  x )  .N  ( 2nd `  y
 ) )  <N  ( ( 1st `  y )  .N  ( 2nd `  x ) ) ) }
 
Definitiondf-enq 6445* Define equivalence relation for positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.)
 |- 
 ~Q  =  { <. x ,  y >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X. 
 N. ) )  /\  E. z E. w E. v E. u ( ( x  =  <. z ,  w >.  /\  y  = 
 <. v ,  u >. ) 
 /\  ( z  .N  u )  =  ( w  .N  v ) ) ) }
 
Definitiondf-nqqs 6446 Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.)
 |- 
 Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
 
Definitiondf-plqqs 6447* Define addition on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.3 of [Gleason] p. 117. (Contributed by NM, 24-Aug-1995.)
 |- 
 +Q  =  { <. <. x ,  y >. ,  z >.  |  (
 ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ] 
 ~Q  /\  y  =  [ <. u ,  f >. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  +pQ  <. u ,  f >. ) ]  ~Q  ) ) }
 
Definitiondf-mqqs 6448* Define multiplication on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.4 of [Gleason] p. 119. (Contributed by NM, 24-Aug-1995.)
 |- 
 .Q  =  { <. <. x ,  y >. ,  z >.  |  (
 ( x  e.  Q.  /\  y  e.  Q. )  /\  E. w E. v E. u E. f ( ( x  =  [ <. w ,  v >. ] 
 ~Q  /\  y  =  [ <. u ,  f >. ]  ~Q  )  /\  z  =  [ ( <. w ,  v >.  .pQ  <. u ,  f >. ) ]  ~Q  ) ) }
 
Definitiondf-1nqqs 6449 Define positive fraction constant 1. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 29-Oct-1995.)
 |- 
 1Q  =  [ <. 1o ,  1o >. ]  ~Q
 
Definitiondf-rq 6450* Define reciprocal on positive fractions. It means the same thing as one divided by the argument (although we don't define full division since we will never need it). This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.5 of [Gleason] p. 119, who uses an asterisk to denote this unary operation. (Contributed by Jim Kingdon, 20-Sep-2019.)
 |- 
 *Q  =  { <. x ,  y >.  |  ( x  e.  Q.  /\  y  e.  Q.  /\  ( x  .Q  y )  =  1Q ) }
 
Definitiondf-ltnqqs 6451* Define ordering relation on positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. Similar to Definition 5 of [Suppes] p. 162. (Contributed by NM, 13-Feb-1996.)
 |- 
 <Q  =  { <. x ,  y >.  |  ( ( x  e.  Q.  /\  y  e.  Q. )  /\  E. z E. w E. v E. u ( ( x  =  [ <. z ,  w >. ] 
 ~Q  /\  y  =  [ <. v ,  u >. ]  ~Q  )  /\  ( z  .N  u )  <N  ( w  .N  v ) ) ) }
 
Theoremdfplpq2 6452* Alternative definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)
 |- 
 +pQ  =  { <. <. x ,  y >. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) 
 /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  = 
 <. ( ( w  .N  f )  +N  (
 v  .N  u )
 ) ,  ( v  .N  f ) >. ) ) }
 
Theoremdfmpq2 6453* Alternative definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)
 |- 
 .pQ  =  { <. <. x ,  y >. ,  z >.  |  ( ( x  e.  ( N.  X.  N. )  /\  y  e.  ( N.  X.  N. ) ) 
 /\  E. w E. v E. u E. f ( ( x  =  <. w ,  v >.  /\  y  =  <. u ,  f >. )  /\  z  = 
 <. ( w  .N  u ) ,  ( v  .N  f ) >. ) ) }
 
Theoremenqbreq 6454 Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( <. A ,  B >.  ~Q  <. C ,  D >.  <-> 
 ( A  .N  D )  =  ( B  .N  C ) ) )
 
Theoremenqbreq2 6455 Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
 |-  ( ( A  e.  ( N.  X.  N. )  /\  B  e.  ( N. 
 X.  N. ) )  ->  ( A  ~Q  B  <->  ( ( 1st `  A )  .N  ( 2nd `  B ) )  =  ( ( 1st `  B )  .N  ( 2nd `  A ) ) ) )
 
Theoremenqer 6456 The equivalence relation for positive fractions is an equivalence relation. Proposition 9-2.1 of [Gleason] p. 117. (Contributed by NM, 27-Aug-1995.) (Revised by Mario Carneiro, 6-Jul-2015.)
 |- 
 ~Q  Er  ( N.  X. 
 N. )
 
Theoremenqeceq 6457 Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( [ <. A ,  B >. ]  ~Q  =  [ <. C ,  D >. ] 
 ~Q 
 <->  ( A  .N  D )  =  ( B  .N  C ) ) )
 
Theoremenqex 6458 The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)
 |- 
 ~Q  e.  _V
 
Theoremenqdc 6459 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  -> DECID  <. A ,  B >.  ~Q  <. C ,  D >. )
 
Theoremenqdc1 6460 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  C  e.  ( N.  X.  N. ) )  -> DECID  <. A ,  B >.  ~Q  C )
 
Theoremnqex 6461 The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
 |- 
 Q.  e.  _V
 
Theorem0nnq 6462 The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)
 |- 
 -.  (/)  e.  Q.
 
Theoremltrelnq 6463 Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)
 |- 
 <Q  C_  ( Q.  X.  Q. )
 
Theorem1nq 6464 The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)
 |- 
 1Q  e.  Q.
 
Theoremaddcmpblnq 6465 Lemma showing compatibility of addition. (Contributed by NM, 27-Aug-1995.)
 |-  ( ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. )
 )  /\  ( ( F  e.  N.  /\  G  e.  N. )  /\  ( R  e.  N.  /\  S  e.  N. ) ) ) 
 ->  ( ( ( A  .N  D )  =  ( B  .N  C )  /\  ( F  .N  S )  =  ( G  .N  R ) ) 
 ->  <. ( ( A  .N  G )  +N  ( B  .N  F ) ) ,  ( B  .N  G ) >.  ~Q 
 <. ( ( C  .N  S )  +N  ( D  .N  R ) ) ,  ( D  .N  S ) >. ) )
 
Theoremmulcmpblnq 6466 Lemma showing compatibility of multiplication. (Contributed by NM, 27-Aug-1995.)
 |-  ( ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. )
 )  /\  ( ( F  e.  N.  /\  G  e.  N. )  /\  ( R  e.  N.  /\  S  e.  N. ) ) ) 
 ->  ( ( ( A  .N  D )  =  ( B  .N  C )  /\  ( F  .N  S )  =  ( G  .N  R ) ) 
 ->  <. ( A  .N  F ) ,  ( B  .N  G ) >.  ~Q 
 <. ( C  .N  R ) ,  ( D  .N  S ) >. ) )
 
Theoremaddpipqqslem 6467 Lemma for addpipqqs 6468. (Contributed by Jim Kingdon, 11-Sep-2019.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  <. ( ( A  .N  D )  +N  ( B  .N  C ) ) ,  ( B  .N  D ) >.  e.  ( N.  X.  N. ) )
 
Theoremaddpipqqs 6468 Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( [ <. A ,  B >. ]  ~Q  +Q  [ <. C ,  D >. ] 
 ~Q  )  =  [ <. ( ( A  .N  D )  +N  ( B  .N  C ) ) ,  ( B  .N  D ) >. ]  ~Q  )
 
Theoremmulpipq2 6469 Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)
 |-  ( ( A  e.  ( N.  X.  N. )  /\  B  e.  ( N. 
 X.  N. ) )  ->  ( A  .pQ  B )  =  <. ( ( 1st `  A )  .N  ( 1st `  B ) ) ,  ( ( 2nd `  A )  .N  ( 2nd `  B ) )
 >. )
 
Theoremmulpipq 6470 Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( <. A ,  B >.  .pQ  <. C ,  D >. )  =  <. ( A  .N  C ) ,  ( B  .N  D ) >. )
 
Theoremmulpipqqs 6471 Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( [ <. A ,  B >. ]  ~Q  .Q  [ <. C ,  D >. ] 
 ~Q  )  =  [ <. ( A  .N  C ) ,  ( B  .N  D ) >. ]  ~Q  )
 
Theoremordpipqqs 6472 Ordering of positive fractions in terms of positive integers. (Contributed by Jim Kingdon, 14-Sep-2019.)
 |-  ( ( ( A  e.  N.  /\  B  e.  N. )  /\  ( C  e.  N.  /\  D  e.  N. ) )  ->  ( [ <. A ,  B >. ]  ~Q  <Q  [ <. C ,  D >. ]  ~Q  <->  ( A  .N  D )  <N  ( B  .N  C ) ) )
 
Theoremaddclnq 6473 Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  +Q  B )  e.  Q. )
 
Theoremmulclnq 6474 Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  .Q  B )  e.  Q. )
 
Theoremdmaddpqlem 6475* Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 6477. (Contributed by Jim Kingdon, 15-Sep-2019.)
 |-  ( x  e.  Q.  ->  E. w E. v  x  =  [ <. w ,  v >. ]  ~Q  )
 
Theoremnqpi 6476* Decomposition of a positive fraction into numerator and denominator. Similar to dmaddpqlem 6475 but also shows that the numerator and denominator are positive integers. (Contributed by Jim Kingdon, 20-Sep-2019.)
 |-  ( A  e.  Q.  ->  E. w E. v
 ( ( w  e. 
 N.  /\  v  e.  N. )  /\  A  =  [ <. w ,  v >. ]  ~Q  ) )
 
Theoremdmaddpq 6477 Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)
 |- 
 dom  +Q  =  ( Q.  X.  Q. )
 
Theoremdmmulpq 6478 Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)
 |- 
 dom  .Q  =  ( Q.  X.  Q. )
 
Theoremaddcomnqg 6479 Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  +Q  B )  =  ( B  +Q  A ) )
 
Theoremaddassnqg 6480 Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( ( A  +Q  B )  +Q  C )  =  ( A  +Q  ( B  +Q  C ) ) )
 
Theoremmulcomnqg 6481 Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  .Q  B )  =  ( B  .Q  A ) )
 
Theoremmulassnqg 6482 Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( ( A  .Q  B )  .Q  C )  =  ( A  .Q  ( B  .Q  C ) ) )
 
Theoremmulcanenq 6483 Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  -> 
 <. ( A  .N  B ) ,  ( A  .N  C ) >.  ~Q  <. B ,  C >. )
 
Theoremmulcanenqec 6484 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)
 |-  ( ( A  e.  N. 
 /\  B  e.  N.  /\  C  e.  N. )  ->  [ <. ( A  .N  B ) ,  ( A  .N  C ) >. ] 
 ~Q  =  [ <. B ,  C >. ]  ~Q  )
 
Theoremdistrnqg 6485 Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( A  .Q  ( B  +Q  C ) )  =  ( ( A  .Q  B )  +Q  ( A  .Q  C ) ) )
 
Theorem1qec 6486 The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)
 |-  ( A  e.  N.  ->  1Q  =  [ <. A ,  A >. ]  ~Q  )
 
Theoremmulidnq 6487 Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)
 |-  ( A  e.  Q.  ->  ( A  .Q  1Q )  =  A )
 
Theoremrecexnq 6488* Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)
 |-  ( A  e.  Q.  ->  E. y ( y  e.  Q.  /\  ( A  .Q  y )  =  1Q ) )
 
Theoremrecmulnqg 6489 Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( ( *Q `  A )  =  B  <->  ( A  .Q  B )  =  1Q ) )
 
Theoremrecclnq 6490 Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
 |-  ( A  e.  Q.  ->  ( *Q `  A )  e.  Q. )
 
Theoremrecidnq 6491 A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)
 |-  ( A  e.  Q.  ->  ( A  .Q  ( *Q `  A ) )  =  1Q )
 
Theoremrecrecnq 6492 Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)
 |-  ( A  e.  Q.  ->  ( *Q `  ( *Q `  A ) )  =  A )
 
Theoremrec1nq 6493 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)
 |-  ( *Q `  1Q )  =  1Q
 
Theoremnqtri3or 6494 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  <Q  B  \/  A  =  B  \/  B  <Q  A )
 )
 
Theoremltdcnq 6495 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  -> DECID  A  <Q  B )
 
Theoremltsonq 6496 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)
 |- 
 <Q  Or  Q.
 
Theoremnqtric 6497 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q. )  ->  ( A  <Q  B  <->  -.  ( A  =  B  \/  B  <Q  A )
 ) )
 
Theoremltanqg 6498 Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( A  <Q  B  <->  ( C  +Q  A )  <Q  ( C  +Q  B ) ) )
 
Theoremltmnqg 6499 Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by Jim Kingdon, 22-Sep-2019.)
 |-  ( ( A  e.  Q. 
 /\  B  e.  Q.  /\  C  e.  Q. )  ->  ( A  <Q  B  <->  ( C  .Q  A )  <Q  ( C  .Q  B ) ) )
 
Theoremltanqi 6500 Ordering property of addition for positive fractions. One direction of ltanqg 6498. (Contributed by Jim Kingdon, 9-Dec-2019.)
 |-  ( ( A  <Q  B 
 /\  C  e.  Q. )  ->  ( C  +Q  A )  <Q  ( C  +Q  B ) )
    < 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 >