TOC of Theorem List - Intuitionistic Logic Explorer

Table of Contents Summary

PART 1  INTUITIONISTIC 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
      1.5  First-order logic with one non-logical binary predicate
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  CHOICE PRINCIPLES
      3.1  Countable Choice and Dependent Choice
PART 4  REAL AND COMPLEX NUMBERS
      4.1  Construction and axiomatization of real and complex numbers
      4.2  Derive the basic properties from the field axioms
      4.3  Real and complex numbers - basic operations
      4.4  Integer sets
      4.5  Order sets
      4.6  Elementary integer functions
      4.7  Words over a set
      4.8  Elementary real and complex functions
      4.9  Elementary limits and convergence
      4.10  Elementary trigonometry
PART 5  ELEMENTARY NUMBER THEORY
      5.1  Elementary properties of divisibility
      5.2  Elementary prime number theory
      5.3  Cardinality of real and complex number subsets
PART 6  BASIC STRUCTURES
      6.1  Extensible structures
PART 7  BASIC ALGEBRAIC STRUCTURES
      7.1  Monoids
      7.2  Groups
      7.3  Rings
      7.4  Division rings and fields
      7.5  Left modules
      7.6  Subring algebras and ideals
      7.7  The complex numbers as an algebraic extensible structure
PART 8  BASIC LINEAR ALGEBRA
      8.1  Associative algebras
      8.2  Abstract multivariate polynomials
PART 9  BASIC TOPOLOGY
      9.1  Topology
      9.2  Metric spaces
PART 10  BASIC REAL AND COMPLEX ANALYSIS
      10.1  Continuity
      10.2  Derivatives
PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      11.1  Polynomials
      11.2  Basic trigonometry
      11.3  Pell equations
      11.4  Basic number theory
PART 12  GRAPH THEORY
      12.1  Vertices and edges
      12.2  Undirected graphs
      12.3  Walks, paths and cycles
      12.4  Eulerian paths and the Konigsberg Bridge problem
PART 13  GUIDES AND MISCELLANEA
      13.1  Guides (conventions, explanations, and examples)
PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
      14.2  Mathbox for Matthew House
      14.3  Mathbox for BJ
      14.4  Mathbox for Jim Kingdon
      14.5  Mathbox for Mykola Mostovenko
      14.6  Mathbox for David A. Wheeler

Detailed Table of Contents
(* means the section header has a description)

​​*PART 1  INTUITIONISTIC FIRST-ORDER LOGIC WITH EQUALITY
      ​*1.1  Pre-logic
            *1.1.1  Inferences for assisting proof development   idi 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-mp 5
            ​*1.2.3  Logical implication   mp2b 8
            1.2.4  Logical conjunction and logical equivalence   wa 104
            1.2.5  Logical negation (intuitionistic)   ax-in1 623
            1.2.6  Logical disjunction   wo 720
            1.2.7  Stable propositions   wstab 842
            1.2.8  Decidable propositions   wdc 846
            ​*1.2.9  Theorems of decidable propositions   const 864
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 928
            ​*1.2.11  The conditional operator for propositions   wif 990
            1.2.12  Abbreviated conjunction and disjunction of three wff's   w3o 1008
            1.2.13  True and false constants   wal 1400
                  ​*1.2.13.1  Universal quantifier for use by df-tru   wal 1400
                  ​*1.2.13.2  Equality predicate for use by df-tru   cv 1401
                  1.2.13.3  Define the true and false constants   wtru 1403
            1.2.14  Logical 'xor'   wxo 1424
            ​*1.2.15  Truth tables: Operations on true and false constants   truantru 1450
            ​*1.2.16  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1472
            1.2.17  Logical implication (continued)   syl6an 1483
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1500
            ​*1.3.2  Equality predicate (continued)   weq 1556
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1579
            1.3.4  Introduce Axiom of Existence   ax-i9 1583
            1.3.5  Additional intuitionistic axioms   ax-ial 1587
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1589
            1.3.7  The existential quantifier   19.8a 1643
            1.3.8  Equality theorems without distinct variables   a9e 1748
            1.3.9  Axioms ax-10 and ax-11   ax10o 1767
            1.3.10  Substitution (without distinct variables)   wsb 1815
            1.3.11  Theorems using axiom ax-11   equs5a 1847
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1864
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1875
            1.4.3  More theorems related to ax-11 and substitution   albidv 1877
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1911
            1.4.5  More substitution theorems   hbs1 1998
            1.4.6  Existential uniqueness   weu 2086
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2185
      ​​*1.5  First-order logic with one non-logical binary predicate
​​*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 2220
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2224
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2369
            2.1.3  Class form not-free predicate   wnfc 2379
            2.1.4  Negated equality and membership   wne 2420
                  2.1.4.1  Negated equality   wne 2420
                  2.1.4.2  Negated membership   wnel 2515
            2.1.5  Restricted quantification   wral 2528
            2.1.6  The universal class   cvv 2821
            ​*2.1.7  Conditional equality (experimental)   wcdeq 3034
            2.1.8  Russell's Paradox   ru 3050
            2.1.9  Proper substitution of classes for sets   wsbc 3051
            2.1.10  Proper substitution of classes for sets into classes   csb 3147
            2.1.11  Define basic set operations and relations   cdif 3217
            2.1.12  Subclasses and subsets   df-ss 3233
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3339
                  2.1.13.1  The difference of two classes   dfdif3 3339
                  2.1.13.2  The union of two classes   elun 3370
                  2.1.13.3  The intersection of two classes   elin 3412
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3462
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3497
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3513
            2.1.14  The empty set   c0 3520
            2.1.15  Conditional operator   cif 3638
            2.1.16  Power classes   cpw 3688
            2.1.17  Unordered and ordered pairs   csn 3709
            2.1.18  The union of a class   cuni 3935
            2.1.19  The intersection of a class   cint 3970
            2.1.20  Indexed union and intersection   ciun 4012
            2.1.21  Disjointness   wdisj 4106
            2.1.22  Binary relations   wbr 4130
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4191
            2.1.24  Transitive classes   wtr 4229
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4246
            2.2.2  Introduce the Axiom of Separation   ax-sep 4249
            2.2.3  Derive the Null Set Axiom   zfnuleu 4257
            2.2.4  Theorems requiring subset and intersection existence   nalset 4263
            2.2.5  Theorems requiring empty set existence   class2seteq 4300
            2.2.6  Collection principle   bnd 4309
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4311
            2.3.2  A notation for excluded middle   wem 4331
            2.3.3  Axiom of Pairing   ax-pr 4346
            2.3.4  Ordered pair theorem   opm 4374
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4398
            2.3.6  Power class of union and intersection   pwin 4427
            2.3.7  Epsilon and identity relations   cep 4432
            ​*2.3.8  Partial and total orderings   wpo 4439
            2.3.9  Founded and set-like relations   wfrfor 4472
            2.3.10  Ordinals   word 4507
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4578
            2.4.2  Ordinals (continued)   ordon 4633
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4679
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4684
            2.5.3  Transfinite induction   tfi 4729
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4735
            2.6.2  The natural numbers   com 4737
            2.6.3  Peano's postulates   peano1 4741
            2.6.4  Finite induction (for finite ordinals)   find 4746
            2.6.5  The Natural Numbers (continued)   nn0suc 4751
            2.6.6  Relations   cxp 4772
            2.6.7  Definite description binder (inverted iota)   cio 5335
            2.6.8  Functions   wfun 5371
            2.6.9  Cantor's Theorem   canth 6036
            2.6.10  Restricted iota (description binder)   crio 6037
            2.6.11  Operations   co 6085
            2.6.12  Maps-to notation   elmpocl 6284
            2.6.13  Function operation   cof 6300
            2.6.14  Functions (continued)   resfunexgALT 6337
            2.6.15  First and second members of an ordered pair   c1st 6372
            ​*2.6.16  The support of functions   csupp 6475
            ​*2.6.17  Special maps-to operations   opeliunxp2f 6509
            2.6.18  Function transposition   ctpos 6515
            2.6.19  Undefined values   pwuninel2 6553
            2.6.20  Functions on ordinals; strictly monotone ordinal functions   iunon 6555
            2.6.21  "Strong" transfinite recursion   crecs 6575
            2.6.22  Recursive definition generator   crdg 6640
            2.6.23  Finite recursion   cfrec 6661
            2.6.24  Ordinal arithmetic   c1o 6680
            2.6.25  Natural number arithmetic   nna0 6747
            2.6.26  Equivalence relations and classes   wer 6804
            2.6.27  The mapping operation   cmap 6922
            2.6.28  Infinite Cartesian products   cixp 6980
            2.6.29  Equinumerosity   cen 7020
            2.6.30  Equinumerosity (cont.)   xpf1o 7144
            2.6.31  Pigeonhole Principle   phplem1 7153
            2.6.32  Finite sets   fict 7170
            2.6.33  Schroeder-Bernstein Theorem   sbthlem1 7274
            2.6.34  Finitely supported functions   cfsupp 7285
            2.6.35  Finite intersections   cfi 7302
            2.6.36  The sizes of sets   2omap 7319
            2.6.37  Supremum and infimum   csup 7323
            2.6.38  Ordinal isomorphism   ordiso2 7376
            2.6.39  Disjoint union   cdju 7378
                  2.6.39.1  Disjoint union   cdju 7378
                  ​*2.6.39.2  Left and right injections of a disjoint union   cinl 7386
                  2.6.39.3  Universal property of the disjoint union   djuss 7411
                  2.6.39.4  Dominance and equinumerosity properties of disjoint union   djudom 7434
                  2.6.39.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7443
                  2.6.39.6  Countable sets   0ct 7448
            ​*2.6.40  The one-point compactification of the natural numbers   xnninf 7460
            2.6.41  Omniscient sets   comni 7475
            2.6.42  Markov's principle   cmarkov 7492
            2.6.43  Weakly omniscient sets   cwomni 7504
            2.6.44  Cardinal numbers   ccrd 7523
            2.6.45  Axiom of Choice equivalents   wac 7562
            2.6.46  Cardinal number arithmetic   endjudisj 7567
            2.6.47  Ordinal trichotomy   exmidontriimlem1 7578
            2.6.48  Excluded middle and the power set of a singleton   iftrueb01 7583
            2.6.49  Apartness relations   wap 7608
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7629
​​*PART 4  REAL AND COMPLEX NUMBERS
      ​4.1  Construction and axiomatization of real and complex numbers
            4.1.1  Dedekind-cut construction of real and complex numbers   cnpi 7640
            4.1.2  Final derivation of real and complex number postulates   axcnex 8227
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 8271
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8304
            4.2.2  Infinity and the extended real number system   cpnf 8358
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8393
            4.2.4  Ordering on reals   lttr 8400
            4.2.5  Initial properties of the complex numbers   mul12 8457
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8486
            4.3.2  Subtraction   cmin 8499
            4.3.3  Multiplication   kcnktkm1cn 8712
            4.3.4  Ordering on reals (cont.)   ltadd2 8749
            4.3.5  Real Apartness   creap 8905
            4.3.6  Complex Apartness   cap 8912
            4.3.7  Reciprocals   recextlem1 8982
            4.3.8  Division   cdiv 9005
            4.3.9  Ordering on reals (cont.)   ltp1 9177
            4.3.10  Suprema   lbreu 9278
            4.3.11  Imaginary and complex number properties   crap0 9291
            4.3.12  Function operation analogue theorems   ofnegsub 9295
            ​*4.3.13  Indicator Functions   cind 9296
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 9307
            4.4.2  Principle of mathematical induction   nnind 9323
            ​*4.4.3  Decimal representation of numbers   c2 9358
            ​*4.4.4  Some properties of specific numbers   neg1cn 9412
            4.4.5  Simple number properties   halfcl 9536
            4.4.6  The Archimedean property   arch 9565
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9568
            ​*4.4.8  Extended nonnegative integers   cxnn0 9635
            4.4.9  Integers (as a subset of complex numbers)   cz 9649
            4.4.10  Decimal arithmetic   cdc 9782
            4.4.11  Upper sets of integers   cuz 9931
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 10029
            4.4.13  Complex numbers as pairs of reals   cnref1o 10062
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 10065
            4.5.2  Infinity and the extended real number system (cont.)   cxne 10182
            4.5.3  Real number intervals   cioo 10301
            4.5.4  Finite intervals of integers   cfz 10422
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10530
            4.5.6  Half-open integer ranges   cfzo 10560
            4.5.7  Rational numbers (cont.)   qtri3or 10686
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10714
            4.6.2  The modulo (remainder) operation   cmo 10774
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10851
            4.6.4  Strong induction over upper sets of integers   uzsinds 10896
            4.6.5  The infinite sequence builder "seq"   cseq 10899
            4.6.6  Integer powers   cexp 10990
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 11173
            4.6.8  Factorial function   cfa 11179
            4.6.9  The binomial coefficient operation   cbc 11201
            4.6.10  The ` # ` (set size) function   chash 11230
                  4.6.10.1  Proper unordered pairs and triples (sets of size 2 and 3)   hash2en 11311
                  4.6.10.2  Functions with a domain containing at least two different elements   fundm2domnop0 11316
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 11320
            4.7.2  Last symbol of a word   clsw 11365
            4.7.3  Concatenations of words   cconcat 11374
            4.7.4  Singleton words   cs1 11399
            4.7.5  Concatenations with singleton words   ccatws1cl 11416
            4.7.6  Subwords/substrings   csubstr 11433
            4.7.7  Prefixes of a word   cpfx 11460
            4.7.8  Subwords of subwords   swrdswrdlem 11492
            4.7.9  Subwords and concatenations   pfxcctswrd 11498
            4.7.10  Subwords of concatenations   swrdccatfn 11512
            4.7.11  Longer string literals   cs2 11537
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 11595
            4.8.2  Real and imaginary parts; conjugate   ccj 11620
            4.8.3  Sequence convergence   caucvgrelemrec 11761
            4.8.4  Square root; absolute value   csqrt 11778
            4.8.5  The maximum of two real numbers   maxcom 11986
            4.8.6  The minimum of two real numbers   mincom 12013
            4.8.7  The maximum of two extended reals   xrmaxleim 12029
            4.8.8  The minimum of two extended reals   xrnegiso 12047
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 12063
            4.9.2  Finite and infinite sums   csu 12138
            4.9.3  The binomial theorem   binomlem 12269
            4.9.4  Infinite sums (cont.)   isumshft 12276
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 12283
            4.9.6  Arithmetic series   arisum 12284
            4.9.7  Geometric series   expcnvap0 12288
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 12309
            4.9.9  Mertens' theorem   mertenslemub 12320
            4.9.10  Finite and infinite products   prodf 12324
                  4.9.10.1  Product sequences   prodf 12324
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 12334
                  4.9.10.3  Complex products   cprod 12336
                  4.9.10.4  Finite products   fprodseq 12369
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 12428
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 12561
            4.10.2  _e is irrational   eirraplem 12563
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 12573
            ​*5.1.2  Even and odd numbers   evenelz 12653
            5.1.3  The division algorithm   divalglemnn 12704
            5.1.4  Bit sequences   cbits 12726
            5.1.5  The greatest common divisor operator   cgcd 12749
            5.1.6  Bézout's identity   bezoutlemnewy 12792
            5.1.7  Decidable sets of integers   nnmindc 12830
            5.1.8  Algorithms   nn0seqcvgd 12838
            5.1.9  Euclid's Algorithm   eucalgval2 12850
            ​*5.1.10  The least common multiple   clcm 12857
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12885
            5.1.12  Cancellability of congruences   congr 12897
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12904
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12942
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12959
            5.2.4  Properties of the canonical representation of a rational   cnumer 12980
            5.2.5  Euler's theorem   codz 13009
            5.2.6  Arithmetic modulo a prime number   modprm1div 13049
            5.2.7  Pythagorean Triples   coprimeprodsq 13059
            5.2.8  The prime count function   cpc 13086
            5.2.9  Pocklington's theorem   prmpwdvds 13157
            5.2.10  Infinite primes theorem   infpnlem1 13161
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 13165
            5.2.12  Lagrange's four-square theorem   cgz 13171
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 13213
            5.2.14  Specific prime numbers   prmlem0 13243
            5.2.15  Very large primes   1259lem1 13265
            5.2.16  Bertrand's Ballot Problem   ballotfilemofi 13271
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 13335
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 13400
            6.1.2  Slot definitions   cplusg 13484
            6.1.3  Various definitions used by the structure product   crest 13646
            6.1.4  Definition of the structure quotient   cimas 13675
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 13726
            ​*7.1.2  Identity elements   mgmidmo 13745
            7.1.3  Iterated sums in a magma   fngzsum 13761
            ​*7.1.4  Semigroups   csgrp 13769
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13782
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13817
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13853
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13858
            ​*7.2.2  Group multiple operation   cmg 13975
            7.2.3  Subgroups and Quotient groups   csubg 14023
            7.2.4  Elementary theory of group homomorphisms   cghm 14096
            7.2.5  Centralizers and centers   ccntz 14140
            7.2.6  Abelian groups   ccmn 14171
                  7.2.6.1  Definition and basic properties   ccmn 14171
                  7.2.6.2  Group sum operation   gzsumreidx 14225
            7.2.7  Finite group sum over unordered finite set   cgsu 14234
            7.2.8  Structure product   cprds 14253
            7.2.9  Binary product on structures   cxps 14283
            7.2.10  Structure power   cpws 14286
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 14301
            ​*7.3.2  Non-unital rings ("rngs")   crng 14315
            ​*7.3.3  Ring unity (multiplicative identity)   cur 14346
            7.3.4  Semirings   csrg 14351
            7.3.5  Definition and basic properties of unital rings   crg 14384
            7.3.6  Opposite ring   coppr 14456
            7.3.7  Divisibility   cdsr 14476
            7.3.8  Ring homomorphisms   crh 14541
            7.3.9  Nonzero rings and zero rings   cnzr 14570
            7.3.10  Local rings   clring 14581
            7.3.11  Subrings   csubrng 14589
                  7.3.11.1  Subrings of non-unital rings   csubrng 14589
                  7.3.11.2  Subrings of unital rings   csubrg 14609
            7.3.12  Left regular elements and domains   crlreg 14647
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 14673
            7.4.2  Definition and basic properties   cdr 14686
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 14707
            7.5.2  Subspaces and spans in a left module   clss 14773
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 14854
            7.6.2  Ideals and spans   clidl 14888
            7.6.3  Two-sided ideals and quotient rings   c2idl 14920
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14955
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14956
            ​*7.7.2  Ring of integers   czring 15009
            7.7.3  Algebraic constructions based on the complex numbers   czrh 15030
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Associative algebras
            8.1.1  Definition and basic properties   casa 15080
      ​8.2  Abstract multivariate polynomials
            8.2.1  Definition and basic properties   cmps 15129
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 15189
                  9.1.1.1  Topologies   ctop 15189
                  9.1.1.2  Topologies on sets   ctopon 15202
                  9.1.1.3  Topological spaces   ctps 15222
            9.1.2  Topological bases   ctb 15234
            9.1.3  Examples of topologies   distop 15277
            9.1.4  Closure and interior   ccld 15284
            9.1.5  Neighborhoods   cnei 15330
            9.1.6  Subspace topologies   restrcl 15359
            9.1.7  Limits and continuity in topological spaces   ccn 15377
            9.1.8  Product topologies   ctx 15444
            9.1.9  Continuous function-builders   cnmptid 15473
            9.1.10  Homeomorphisms   chmeo 15492
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 15514
            9.2.2  Basic metric space properties   cxms 15528
            9.2.3  Metric space balls   blfvalps 15577
            9.2.4  Open sets of a metric space   mopnrel 15633
            9.2.5  Continuity in metric spaces   metcnp3 15703
            9.2.6  Topology on the reals   qtopbasss 15713
            9.2.7  Topological definitions using the reals   ccncf 15762
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 15809
            10.1.2  Intermediate value theorem   ivthinclemlm 15826
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 15846
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 15846
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 15920
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15960
            11.2.2  Properties of pi = 3.14159...   pilem1 15972
            11.2.3  The natural logarithm on complex numbers   clog 16049
            ​*11.2.4  Logarithms to an arbitrary base   clogb 16140
            11.2.5  Quartic binomial expansion   binom4 16180
            11.2.6  Logarithms (cont.)   log2tlbndlog2 16181
            11.2.7  The Birthday Problem   log2ublem1 16182
      ​11.3  Pell equations
            11.3.1  Pell equations 1: A nontrivial solution always exists   pellexlem1 16190
      ​11.4  Basic number theory
            11.4.1  Wilson's theorem   wilthlem1 16193
            11.4.2  Number-theoretical functions   ccht 16194
            11.4.3  Perfect Number Theorem   mersenne 16258
            11.4.4  Bertrand's postulate   bcctr 16263
            ​*11.4.5  Quadratic residues and the Legendre symbol   clgs 16282
            ​*11.4.6  Gauss' Lemma   gausslemma2dlem0a 16334
            11.4.7  Quadratic reciprocity   lgseisenlem1 16355
            11.4.8  All primes 4n+1 are the sum of two squares   2sqlem1 16399
​PART 12  GRAPH THEORY
      ​12.1  Vertices and edges
            12.1.1  The edge function extractor for extensible structures   cedgf 16411
            12.1.2  Vertices and indexed edges   cvtx 16419
                  12.1.2.1  Definitions and basic properties   cvtx 16419
                  12.1.2.2  The vertices and edges of a graph represented as ordered pair   opvtxval 16428
                  12.1.2.3  The vertices and edges of a graph represented as extensible structure   funvtxdm2domval 16436
                  12.1.2.4  Degenerated cases of representations of graphs   vtxval0 16460
            12.1.3  Edges as range of the edge function   cedg 16464
      ​12.2  Undirected graphs
            12.2.1  Undirected hypergraphs   cuhgr 16474
            12.2.2  Undirected pseudographs and multigraphs   cupgr 16498
            ​*12.2.3  Loop-free graphs   umgrislfupgrenlem 16537
            12.2.4  Edges as subsets of vertices of graphs   uhgredgiedgb 16541
            ​*12.2.5  Undirected simple graphs   cuspgr 16560
            12.2.6  Examples for graphs   usgr0e 16639
            12.2.7  Subgraphs   csubgr 16660
            12.2.8  Vertex degree   cvtxdg 16693
      ​12.3  Walks, paths and cycles
            12.3.1  Walks   cwlks 16724
            12.3.2  Trails   ctrls 16787
            12.3.3  Closed walks as words   cclwwlk 16798
                  12.3.3.1  Closed walks as words   cclwwlk 16798
                  12.3.3.2  Closed walks of a fixed length as words   cclwwlkn 16810
                  12.3.3.3  Closed walks on a vertex of a fixed length as words   cclwwlknon 16833
      ​12.4  Eulerian paths and the Konigsberg Bridge problem
            ​*12.4.1  Eulerian paths   ceupth 16849
            ​*12.4.2  The Königsberg Bridge problem   konigsbergvtx 16889
​PART 13  GUIDES AND MISCELLANEA
      ​13.1  Guides (conventions, explanations, and examples)
            ​*13.1.1  Conventions   conventions 16901
            13.1.2  Definitional examples   ex-or 16902
​PART 14  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​14.1  Mathboxes for user contributions
            14.1.1  Mathbox guidelines   mathbox 16912
      ​14.2  Mathbox for Matthew House
      ​14.3  Mathbox for BJ
            14.3.1  Propositional calculus   bj-nnsn 16927
                  ​*14.3.1.1  Stable formulas   bj-trst 16933
                  14.3.1.2  Decidable formulas   bj-trdc 16946
            14.3.2  Predicate calculus   bj-ex 16956
            14.3.3  Set theorey miscellaneous   bj-el2oss1o 16968
            ​*14.3.4  Extensionality   bj-vtoclgft 16969
            ​*14.3.5  Decidability of classes   wdcin 16987
            14.3.6  Disjoint union   djucllem 16994
            14.3.7  Miscellaneous   funmptd 16997
            ​*14.3.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 17004
                  *14.3.8.1  Bounded formulas   wbd 17004
                  ​*14.3.8.2  Bounded classes   wbdc 17032
            ​*14.3.9  CZF: Bounded separation   ax-bdsep 17076
                  14.3.9.1  Delta_0-classical logic   ax-bj-d0cl 17116
                  14.3.9.2  Inductive classes and the class of natural number ordinals   wind 17118
                  ​*14.3.9.3  The first three Peano postulates   bj-peano2 17131
            ​*14.3.10  CZF: Infinity   ax-infvn 17133
                  *14.3.10.1  The set of natural number ordinals   ax-infvn 17133
                  ​*14.3.10.2  Peano's fifth postulate   bdpeano5 17135
                  ​*14.3.10.3  Bounded induction and Peano's fourth postulate   findset 17137
            ​*14.3.11  CZF: Set induction   setindft 17157
                  *14.3.11.1  Set induction   setindft 17157
                  ​*14.3.11.2  Full induction   bj-findis 17171
            ​*14.3.12  CZF: Strong collection   ax-strcoll 17174
            ​*14.3.13  CZF: Subset collection   ax-sscoll 17179
            14.3.14  Real numbers   ax-ddkcomp 17181
      ​14.4  Mathbox for Jim Kingdon
            14.4.1  Propositional and predicate logic   nnnotnotr 17182
            14.4.2  The sizes of sets   ss1oel2o 17183
            14.4.3  The power set of a singleton   pwtrufal 17193
            14.4.4  Weak excluded middle   wwem 17206
            14.4.5  Omniscience of NN+oo   0nninf 17213
            14.4.6  Schroeder-Bernstein Theorem   exmidsbthrlem 17233
            14.4.7  Real and complex numbers   qdencn 17238
            ​*14.4.8  Analytic omniscience principles   trilpolemclim 17252
            14.4.9  Supremum and infimum   supfz 17288
            14.4.10  Circle constant   taupi 17290
      ​14.5  Mathbox for Mykola Mostovenko
      ​14.6  Mathbox for David A. Wheeler
            14.6.1  Testable propositions   dftest 17292
            ​*14.6.2  Allsome quantifier   wals 17293
            ​*14.6.3  Allsome one quantifier   walseu 17327