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

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

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

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

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

Theoremelni 6406 Membership in the class of positive integers. (Contributed by NM, 15-Aug-1995.)

Theorempinn 6407 A positive integer is a natural number. (Contributed by NM, 15-Aug-1995.)

Theorempion 6408 A positive integer is an ordinal number. (Contributed by NM, 23-Mar-1996.)

Theorempiord 6409 A positive integer is ordinal. (Contributed by NM, 29-Jan-1996.)

Theoremniex 6410 The class of positive integers is a set. (Contributed by NM, 15-Aug-1995.)

Theorem0npi 6411 The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995.)

Theoremelni2 6412 Membership in the class of positive integers. (Contributed by NM, 27-Nov-1995.)

Theorem1pi 6413 Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995.)

Theoremmulpiord 6415 Positive integer multiplication in terms of ordinal multiplication. (Contributed by NM, 27-Aug-1995.)

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

Theoremltpiord 6417 Positive integer 'less than' in terms of ordinal membership. (Contributed by NM, 6-Feb-1996.) (Revised by Mario Carneiro, 28-Apr-2015.)

Theoremltsopi 6418 Positive integer 'less than' is a strict ordering. (Contributed by NM, 8-Feb-1996.) (Proof shortened by Mario Carneiro, 10-Jul-2014.)

Theorempitric 6419 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)

Theorempitri3or 6420 Trichotomy for positive integers. (Contributed by Jim Kingdon, 21-Sep-2019.)

Theoremltdcpi 6421 Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
DECID

Theoremltrelpi 6422 Positive integer 'less than' is a relation on positive integers. (Contributed by NM, 8-Feb-1996.)

Theoremdmaddpi 6423 Domain of addition on positive integers. (Contributed by NM, 26-Aug-1995.)

Theoremdmmulpi 6424 Domain of multiplication on positive integers. (Contributed by NM, 26-Aug-1995.)

Theoremaddclpi 6425 Closure of addition of positive integers. (Contributed by NM, 18-Oct-1995.)

Theoremmulclpi 6426 Closure of multiplication of positive integers. (Contributed by NM, 18-Oct-1995.)

Theoremaddcompig 6427 Addition of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)

Theoremaddasspig 6428 Addition of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)

Theoremmulcompig 6429 Multiplication of positive integers is commutative. (Contributed by Jim Kingdon, 26-Aug-2019.)

Theoremmulasspig 6430 Multiplication of positive integers is associative. (Contributed by Jim Kingdon, 26-Aug-2019.)

Theoremdistrpig 6431 Multiplication of positive integers is distributive. (Contributed by Jim Kingdon, 26-Aug-2019.)

Theoremaddcanpig 6432 Addition cancellation law for positive integers. (Contributed by Jim Kingdon, 27-Aug-2019.)

Theoremmulcanpig 6433 Multiplication cancellation law for positive integers. (Contributed by Jim Kingdon, 29-Aug-2019.)

Theoremaddnidpig 6434 There is no identity element for addition on positive integers. (Contributed by NM, 28-Nov-1995.)

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

Theoremltapig 6436 Ordering property of addition for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)

Theoremltmpig 6437 Ordering property of multiplication for positive integers. (Contributed by Jim Kingdon, 31-Aug-2019.)

Theorem1lt2pi 6438 One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.)

Theoremnlt1pig 6439 No positive integer is less than one. (Contributed by Jim Kingdon, 31-Aug-2019.)

Theoremindpi 6440* Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.)

Theoremnnppipi 6441 A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.)

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 (df-plqqs 6447) works with the equivalence classes of these ordered pairs determined by the equivalence relation (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.)

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

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

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

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

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

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

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

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

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

Theoremdfplpq2 6452* Alternative definition of pre-addition on positive fractions. (Contributed by Jim Kingdon, 12-Sep-2019.)

Theoremdfmpq2 6453* Alternative definition of pre-multiplication on positive fractions. (Contributed by Jim Kingdon, 13-Sep-2019.)

Theoremenqbreq 6454 Equivalence relation for positive fractions in terms of positive integers. (Contributed by NM, 27-Aug-1995.)

Theoremenqbreq2 6455 Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)

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

Theoremenqeceq 6457 Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.)

Theoremenqex 6458 The equivalence relation for positive fractions exists. (Contributed by NM, 3-Sep-1995.)

Theoremenqdc 6459 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
DECID

Theoremenqdc1 6460 The equivalence relation for positive fractions is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
DECID

Theoremnqex 6461 The class of positive fractions exists. (Contributed by NM, 16-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)

Theorem0nnq 6462 The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995.) (Revised by Mario Carneiro, 27-Apr-2013.)

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

Theorem1nq 6464 The positive fraction 'one'. (Contributed by NM, 29-Oct-1995.)

Theoremmulcmpblnq 6466 Lemma showing compatibility of multiplication. (Contributed by NM, 27-Aug-1995.)

Theoremaddpipqqs 6468 Addition of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)

Theoremmulpipq2 6469 Multiplication of positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013.)

Theoremmulpipq 6470 Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.) (Revised by Mario Carneiro, 8-May-2013.)

Theoremmulpipqqs 6471 Multiplication of positive fractions in terms of positive integers. (Contributed by NM, 28-Aug-1995.)

Theoremordpipqqs 6472 Ordering of positive fractions in terms of positive integers. (Contributed by Jim Kingdon, 14-Sep-2019.)

Theoremaddclnq 6473 Closure of addition on positive fractions. (Contributed by NM, 29-Aug-1995.)

Theoremmulclnq 6474 Closure of multiplication on positive fractions. (Contributed by NM, 29-Aug-1995.)

Theoremdmaddpqlem 6475* Decomposition of a positive fraction into numerator and denominator. Lemma for dmaddpq 6477. (Contributed by Jim Kingdon, 15-Sep-2019.)

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

Theoremdmaddpq 6477 Domain of addition on positive fractions. (Contributed by NM, 24-Aug-1995.)

Theoremdmmulpq 6478 Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)

Theoremaddcomnqg 6479 Addition of positive fractions is commutative. (Contributed by Jim Kingdon, 15-Sep-2019.)

Theoremaddassnqg 6480 Addition of positive fractions is associative. (Contributed by Jim Kingdon, 16-Sep-2019.)

Theoremmulcomnqg 6481 Multiplication of positive fractions is commutative. (Contributed by Jim Kingdon, 17-Sep-2019.)

Theoremmulassnqg 6482 Multiplication of positive fractions is associative. (Contributed by Jim Kingdon, 17-Sep-2019.)

Theoremmulcanenq 6483 Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.)

Theoremmulcanenqec 6484 Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 17-Sep-2019.)

Theoremdistrnqg 6485 Multiplication of positive fractions is distributive. (Contributed by Jim Kingdon, 17-Sep-2019.)

Theorem1qec 6486 The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.)

Theoremmulidnq 6487 Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.)

Theoremrecexnq 6488* Existence of positive fraction reciprocal. (Contributed by Jim Kingdon, 20-Sep-2019.)

Theoremrecmulnqg 6489 Relationship between reciprocal and multiplication on positive fractions. (Contributed by Jim Kingdon, 19-Sep-2019.)

Theoremrecclnq 6490 Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)

Theoremrecidnq 6491 A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.)

Theoremrecrecnq 6492 Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.)

Theoremrec1nq 6493 Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.)

Theoremnqtri3or 6494 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)

Theoremltdcnq 6495 Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.)
DECID

Theoremltsonq 6496 'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.)

Theoremnqtric 6497 Trichotomy for positive fractions. (Contributed by Jim Kingdon, 21-Sep-2019.)

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

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

Theoremltanqi 6500 Ordering property of addition for positive fractions. One direction of ltanqg 6498. (Contributed by Jim Kingdon, 9-Dec-2019.)

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 >