HomeHome Intuitionistic Logic Explorer
Theorem List (Table of Contents)
< Wrap  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page:  Detailed Table of Contents  Page List

Table of Contents Summary
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      1.1  Pre-logic
      1.2  Propositional calculus
      1.3  Predicate calculus mostly without distinct variables
      1.4  Predicate calculus with distinct variables
PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
      2.2  IZF Set Theory - add the Axioms of Collection and Separation
      2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
      2.4  IZF Set Theory - add the Axiom of Union
      2.5  IZF Set Theory - add the Axiom of Set Induction
      2.6  IZF Set Theory - add the Axiom of Infinity
PART 3  REAL AND COMPLEX NUMBERS
      3.1  Construction and axiomatization of real and complex numbers
      3.2  Derive the basic properties from the field axioms
      3.3  Real and complex numbers - basic operations
      3.4  Integer sets
      3.5  Order sets
      3.6  Elementary integer functions
      3.7  Elementary real and complex functions
      3.8  Elementary limits and convergence
PART 4  ELEMENTARY NUMBER THEORY
      4.1  Elementary properties of divisibility
      4.2  Elementary prime number theory
      4.3  Cardinality of real and complex number subsets
PART 5  GUIDES AND MISCELLANEA
      5.1  Guides (conventions, explanations, and examples)
PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      6.1  Mathboxes for user contributions
      6.2  Mathbox for BJ
      6.3  Mathbox for Jim Kingdon
      6.4  Mathbox for Mykola Mostovenko
      6.5  Mathbox for David A. Wheeler

Detailed Table of Contents
(* means the section header has a description)
PART 1  FIRST ORDER LOGIC WITH EQUALITY
      *1.1  Pre-logic
            *1.1.1  Inferences for assisting proof development   a1ii 1
      1.2  Propositional calculus
            1.2.1  Recursively define primitive wffs for propositional calculus   wn 3
            1.2.2  Propositional logic axioms for implication   ax-1 5
            *1.2.3  Logical implication   mp2b 8
            1.2.4  Logical conjunction and logical equivalence   wa 102
            1.2.5  Logical negation (intuitionistic)   ax-in1 577
            1.2.6  Logical disjunction   wo 662
            1.2.7  Stable propositions   wstab 773
            1.2.8  Decidable propositions   wdc 778
            *1.2.9  Theorems of decidable propositions   condc 785
            1.2.10  Testable propositions   dftest 858
            1.2.11  Miscellaneous theorems of propositional calculus   pm5.21nd 861
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 921
            1.2.13  True and false constants   wal 1285
                  *1.2.13.1  Universal quantifier for use by df-tru   wal 1285
                  *1.2.13.2  Equality predicate for use by df-tru   cv 1286
                  1.2.13.3  Define the true and false constants   wtru 1288
            1.2.14  Logical 'xor'   wxo 1309
            *1.2.15  Truth tables: Operations on true and false constants   truantru 1335
            *1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1357
            1.2.17  Logical implication (continued)   syl6an 1366
      1.3  Predicate calculus mostly without distinct variables
            *1.3.1  Universal quantifier (continued)   ax-5 1379
            *1.3.2  Equality predicate (continued)   weq 1435
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1462
            1.3.4  Introduce Axiom of Existence   ax-i9 1466
            1.3.5  Additional intuitionistic axioms   ax-ial 1470
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1472
            1.3.7  The existential quantifier   19.8a 1525
            1.3.8  Equality theorems without distinct variables   a9e 1629
            1.3.9  Axioms ax-10 and ax-11   ax10o 1647
            1.3.10  Substitution (without distinct variables)   wsb 1689
            1.3.11  Theorems using axiom ax-11   equs5a 1719
      1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1736
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1747
            1.4.3  More theorems related to ax-11 and substitution   albidv 1749
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1783
            1.4.5  More substitution theorems   hbs1 1859
            1.4.6  Existential uniqueness   weu 1945
            *1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2043
*PART 2  SET THEORY
      2.1  IZF Set Theory - start with the Axiom of Extensionality
            2.1.1  Introduce the Axiom of Extensionality   ax-ext 2067
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2071
            2.1.3  Class form not-free predicate   wnfc 2212
            2.1.4  Negated equality and membership   wne 2251
                  2.1.4.1  Negated equality   wne 2251
                  2.1.4.2  Negated membership   wnel 2346
            2.1.5  Restricted quantification   wral 2355
            2.1.6  The universal class   cvv 2615
            *2.1.7  Conditional equality (experimental)   wcdeq 2812
            2.1.8  Russell's Paradox   ru 2828
            2.1.9  Proper substitution of classes for sets   wsbc 2829
            2.1.10  Proper substitution of classes for sets into classes   csb 2922
            2.1.11  Define basic set operations and relations   cdif 2985
            2.1.12  Subclasses and subsets   df-ss 3001
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3099
                  2.1.13.1  The difference of two classes   dfdif3 3099
                  2.1.13.2  The union of two classes   elun 3130
                  2.1.13.3  The intersection of two classes   elin 3172
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3219
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3254
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3268
            2.1.14  The empty set   c0 3275
            2.1.15  Conditional operator   cif 3379
            2.1.16  Power classes   cpw 3415
            2.1.17  Unordered and ordered pairs   csn 3431
            2.1.18  The union of a class   cuni 3636
            2.1.19  The intersection of a class   cint 3671
            2.1.20  Indexed union and intersection   ciun 3713
            2.1.21  Disjointness   wdisj 3801
            2.1.22  Binary relations   wbr 3820
            2.1.23  Ordered-pair class abstractions (class builders)   copab 3873
            2.1.24  Transitive classes   wtr 3911
      2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 3929
            2.2.2  Introduce the Axiom of Separation   ax-sep 3932
            2.2.3  Derive the Null Set Axiom   zfnuleu 3938
            2.2.4  Theorems requiring subset and intersection existence   nalset 3944
            2.2.5  Theorems requiring empty set existence   class2seteq 3973
            2.2.6  Collection principle   bnd 3982
      2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 3984
            2.3.2  A notation for excluded middle   wem 4003
            2.3.3  Axiom of Pairing   ax-pr 4010
            2.3.4  Ordered pair theorem   opm 4035
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4058
            2.3.6  Power class of union and intersection   pwin 4083
            2.3.7  Epsilon and identity relations   cep 4088
            2.3.8  Partial and complete ordering   wpo 4095
            2.3.9  Founded and set-like relations   wfrfor 4128
            2.3.10  Ordinals   word 4163
      2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4234
            2.4.2  Ordinals (continued)   ordon 4276
      2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4321
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4326
            2.5.3  Transfinite induction   tfi 4370
      2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4376
            2.6.2  The natural numbers (i.e. finite ordinals)   com 4378
            2.6.3  Peano's postulates   peano1 4382
            2.6.4  Finite induction (for finite ordinals)   find 4387
            2.6.5  The Natural Numbers (continued)   nn0suc 4392
            2.6.6  Relations   cxp 4409
            2.6.7  Definite description binder (inverted iota)   cio 4944
            2.6.8  Functions   wfun 4975
            2.6.9  Restricted iota (description binder)   crio 5568
            2.6.10  Operations   co 5613
            2.6.11  Maps-to notation   elmpt2cl 5799
            2.6.12  Function operation   cof 5811
            2.6.13  Functions (continued)   resfunexgALT 5838
            2.6.14  First and second members of an ordered pair   c1st 5866
            *2.6.15  Special maps-to operations   mpt2xopn0yelv 5958
            2.6.16  Function transposition   ctpos 5963
            2.6.17  Undefined values   pwuninel2 6001
            2.6.18  Functions on ordinals; strictly monotone ordinal functions   iunon 6003
            2.6.19  "Strong" transfinite recursion   crecs 6023
            2.6.20  Recursive definition generator   crdg 6088
            2.6.21  Finite recursion   cfrec 6109
            2.6.22  Ordinal arithmetic   c1o 6128
            2.6.23  Natural number arithmetic   nna0 6189
            2.6.24  Equivalence relations and classes   wer 6241
            2.6.25  The mapping operation   cmap 6357
            2.6.26  Equinumerosity   cen 6407
            2.6.27  Equinumerosity (cont.)   xpf1o 6512
            2.6.28  Pigeonhole Principle   phplem1 6520
            2.6.29  Finite sets   fict 6536
            2.6.30  Schroeder-Bernstein Theorem   sbthlem1 6610
            2.6.31  Supremum and infimum   csup 6621
            2.6.32  Ordinal isomorphism   ordiso2 6672
            2.6.33  Disjoint union   cdju 6674
                  2.6.33.1  Disjoint union   cdju 6674
                  *2.6.33.2  Left and right injections of a disjoint union   cinl 6681
                  2.6.33.3  Universal property of the disjoint union   djuss 6705
                  2.6.33.4  Older definition temporarily kept for comparison, to be deleted   cdjud 6726
            2.6.34  Omniscient sets   comni 6732
            2.6.35  Cardinal numbers   ccrd 6751
*PART 3  REAL AND COMPLEX NUMBERS
      3.1  Construction and axiomatization of real and complex numbers
            3.1.1  Dedekind-cut construction of real and complex numbers   cnpi 6775
            3.1.2  Final derivation of real and complex number postulates   axcnex 7340
            3.1.3  Real and complex number postulates restated as axioms   ax-cnex 7380
      3.2  Derive the basic properties from the field axioms
            3.2.1  Some deductions from the field axioms for complex numbers   cnex 7410
            3.2.2  Infinity and the extended real number system   cpnf 7463
            3.2.3  Restate the ordering postulates with extended real "less than"   axltirr 7497
            3.2.4  Ordering on reals   lttr 7503
            3.2.5  Initial properties of the complex numbers   mul12 7555
      3.3  Real and complex numbers - basic operations
            3.3.1  Addition   add12 7584
            3.3.2  Subtraction   cmin 7597
            3.3.3  Multiplication   kcnktkm1cn 7805
            3.3.4  Ordering on reals (cont.)   ltadd2 7841
            3.3.5  Real Apartness   creap 7992
            3.3.6  Complex Apartness   cap 7999
            3.3.7  Reciprocals   recextlem1 8059
            3.3.8  Division   cdiv 8078
            3.3.9  Ordering on reals (cont.)   ltp1 8240
            3.3.10  Suprema   lbreu 8341
            3.3.11  Imaginary and complex number properties   crap0 8353
      3.4  Integer sets
            3.4.1  Positive integers (as a subset of complex numbers)   cn 8357
            3.4.2  Principle of mathematical induction   nnind 8373
            *3.4.3  Decimal representation of numbers   c2 8407
            *3.4.4  Some properties of specific numbers   neg1cn 8462
            3.4.5  Simple number properties   halfcl 8575
            3.4.6  The Archimedean property   arch 8603
            3.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 8606
            *3.4.8  Extended nonnegative integers   cxnn0 8669
            3.4.9  Integers (as a subset of complex numbers)   cz 8683
            3.4.10  Decimal arithmetic   cdc 8809
            3.4.11  Upper sets of integers   cuz 8951
            3.4.12  Rational numbers (as a subset of complex numbers)   cq 9036
            3.4.13  Complex numbers as pairs of reals   cnref1o 9065
      3.5  Order sets
            3.5.1  Positive reals (as a subset of complex numbers)   crp 9066
            3.5.2  Infinity and the extended real number system (cont.)   cxne 9172
            3.5.3  Real number intervals   cioo 9238
            3.5.4  Finite intervals of integers   cfz 9356
            *3.5.5  Finite intervals of nonnegative integers   elfz2nn0 9456
            3.5.6  Half-open integer ranges   cfzo 9481
            3.5.7  Rational numbers (cont.)   qtri3or 9582
      3.6  Elementary integer functions
            3.6.1  The floor and ceiling functions   cfl 9603
            3.6.2  The modulo (remainder) operation   cmo 9657
            3.6.3  Miscellaneous theorems about integers   frec2uz0d 9734
            3.6.4  Strong induction over upper sets of integers   uzsinds 9776
            3.6.5  The infinite sequence builder "seq"   cseq 9779
            3.6.6  Integer powers   cexp 9853
            3.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10024
            3.6.8  Factorial function   cfa 10030
            3.6.9  The binomial coefficient operation   cbc 10052
            3.6.10  The ` # ` (set size) function   chash 10080
      3.7  Elementary real and complex functions
            3.7.1  The "shift" operation   cshi 10145
            3.7.2  Real and imaginary parts; conjugate   ccj 10169
            3.7.3  Sequence convergence   caucvgrelemrec 10308
            3.7.4  Square root; absolute value   csqrt 10325
            3.7.5  The maximum of two real numbers   maxcom 10532
            3.7.6  The minimum of two real numbers   mincom 10555
      3.8  Elementary limits and convergence
            3.8.1  Limits   cli 10561
            3.8.2  Finite and infinite sums   csu 10634
*PART 4  ELEMENTARY NUMBER THEORY
      4.1  Elementary properties of divisibility
            4.1.1  The divides relation   cdvds 10678
            *4.1.2  Even and odd numbers   evenelz 10749
            4.1.3  The division algorithm   divalglemnn 10800
            4.1.4  The greatest common divisor operator   cgcd 10820
            4.1.5  Bézout's identity   bezoutlemnewy 10867
            4.1.6  Algorithms   nn0seqcvgd 10905
            4.1.7  Euclid's Algorithm   eucalgval2 10917
            *4.1.8  The least common multiple   clcm 10924
            *4.1.9  Coprimality and Euclid's lemma   coprmgcdb 10952
            4.1.10  Cancellability of congruences   congr 10964
      4.2  Elementary prime number theory
            *4.2.1  Elementary properties   cprime 10971
            *4.2.2  Coprimality and Euclid's lemma (cont.)   coprm 11005
            4.2.3  Non-rationality of square root of 2   sqrt2irrlem 11022
            4.2.4  Properties of the canonical representation of a rational   cnumer 11041
            4.2.5  Euler's theorem   cphi 11068
      4.3  Cardinality of real and complex number subsets
            4.3.1  Countability of integers and rationals   oddennn 11087
PART 5  GUIDES AND MISCELLANEA
      5.1  Guides (conventions, explanations, and examples)
            *5.1.1  Conventions   conventions 11094
            5.1.2  Definitional examples   ex-or 11095
PART 6  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES)
      6.1  Mathboxes for user contributions
            6.1.1  Mathbox guidelines   mathbox 11104
      6.2  Mathbox for BJ
            6.2.1  Propositional calculus   nnexmid 11105
            6.2.2  Predicate calculus   bj-ex 11108
            *6.2.3  Extensionality   bj-vtoclgft 11120
            *6.2.4  Dedidability of classes   wdcin 11138
            6.2.5  Disjoint union   djucllem 11145
            *6.2.6  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 11148
                  *6.2.6.1  Bounded formulas   wbd 11148
                  *6.2.6.2  Bounded classes   wbdc 11176
            *6.2.7  CZF: Bounded separation   ax-bdsep 11220
                  6.2.7.1  Delta_0-classical logic   ax-bj-d0cl 11260
                  6.2.7.2  Inductive classes and the class of natural numbers (finite ordinals)   wind 11266
                  *6.2.7.3  The first three Peano postulates   bj-peano2 11279
            *6.2.8  CZF: Infinity   ax-infvn 11281
                  *6.2.8.1  The set of natural numbers (finite ordinals)   ax-infvn 11281
                  *6.2.8.2  Peano's fifth postulate   bdpeano5 11283
                  *6.2.8.3  Bounded induction and Peano's fourth postulate   findset 11285
            *6.2.9  CZF: Set induction   setindft 11305
                  *6.2.9.1  Set induction   setindft 11305
                  *6.2.9.2  Full induction   bj-findis 11319
            *6.2.10  CZF: Strong collection   ax-strcoll 11322
            *6.2.11  CZF: Subset collection   ax-sscoll 11327
            6.2.12  Real numbers   ax-ddkcomp 11329
      6.3  Mathbox for Jim Kingdon
            6.3.1  Natural numbers   0lt2o 11330
            6.3.2  Omniscience of NN+oo   0nninf 11338
            6.3.3  Schroeder-Bernstein Theorem   exmidsbthrlem 11357
            6.3.4  Real and complex numbers   qdencn 11360
      6.4  Mathbox for Mykola Mostovenko
      6.5  Mathbox for David A. Wheeler
            *6.5.1  Allsome quantifier   walsi 11362

    < Wrap  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-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11370
  Copyright terms: Public domain < Wrap  Next >