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  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  Basic number theory
PART 12  GUIDES AND MISCELLANEA
      12.1  Guides (conventions, explanations, and examples)
PART 13  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​13.1  Mathboxes for user contributions
      13.2  Mathbox for BJ
      13.3  Mathbox for Jim Kingdon
      13.4  Mathbox for Mykola Mostovenko
      13.5  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 615
            1.2.6  Logical disjunction   wo 709
            1.2.7  Stable propositions   wstab 831
            1.2.8  Decidable propositions   wdc 835
            ​*1.2.9  Theorems of decidable propositions   const 853
            1.2.10  Miscellaneous theorems of propositional calculus   pm5.21nd 917
            1.2.11  Abbreviated conjunction and disjunction of three wff's   w3o 979
            1.2.12  True and false constants   wal 1362
                  ​*1.2.12.1  Universal quantifier for use by df-tru   wal 1362
                  ​*1.2.12.2  Equality predicate for use by df-tru   cv 1363
                  1.2.12.3  Define the true and false constants   wtru 1365
            1.2.13  Logical 'xor'   wxo 1386
            ​*1.2.14  Truth tables: Operations on true and false constants   truantru 1412
            ​*1.2.15  Stoic logic indemonstrables (Chrysippus of Soli)   mptnan 1434
            1.2.16  Logical implication (continued)   syl6an 1445
      ​1.3  Predicate calculus mostly without distinct variables
            ​*1.3.1  Universal quantifier (continued)   ax-5 1461
            ​*1.3.2  Equality predicate (continued)   weq 1517
            1.3.3  Axiom ax-17 - first use of the $d distinct variable statement   ax-17 1540
            1.3.4  Introduce Axiom of Existence   ax-i9 1544
            1.3.5  Additional intuitionistic axioms   ax-ial 1548
            1.3.6  Predicate calculus including ax-4, without distinct variables   spi 1550
            1.3.7  The existential quantifier   19.8a 1604
            1.3.8  Equality theorems without distinct variables   a9e 1710
            1.3.9  Axioms ax-10 and ax-11   ax10o 1729
            1.3.10  Substitution (without distinct variables)   wsb 1776
            1.3.11  Theorems using axiom ax-11   equs5a 1808
      ​1.4  Predicate calculus with distinct variables
            1.4.1  Derive the axiom of distinct variables ax-16   spimv 1825
            1.4.2  Derive the obsolete axiom of variable substitution ax-11o   ax11o 1836
            1.4.3  More theorems related to ax-11 and substitution   albidv 1838
            1.4.4  Predicate calculus with distinct variables (cont.)   ax16i 1872
            1.4.5  More substitution theorems   hbs1 1957
            1.4.6  Existential uniqueness   weu 2045
            ​*1.4.7  Aristotelian logic: Assertic syllogisms   barbara 2143
      ​​*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 2178
            2.1.2  Class abstractions (a.k.a. class builders)   cab 2182
                  2.1.2.1  Elementary properties of class abstractions   eqabdv 2325
            2.1.3  Class form not-free predicate   wnfc 2326
            2.1.4  Negated equality and membership   wne 2367
                  2.1.4.1  Negated equality   wne 2367
                  2.1.4.2  Negated membership   wnel 2462
            2.1.5  Restricted quantification   wral 2475
            2.1.6  The universal class   cvv 2763
            ​*2.1.7  Conditional equality (experimental)   wcdeq 2972
            2.1.8  Russell's Paradox   ru 2988
            2.1.9  Proper substitution of classes for sets   wsbc 2989
            2.1.10  Proper substitution of classes for sets into classes   csb 3084
            2.1.11  Define basic set operations and relations   cdif 3154
            2.1.12  Subclasses and subsets   df-ss 3170
            2.1.13  The difference, union, and intersection of two classes   dfdif3 3273
                  2.1.13.1  The difference of two classes   dfdif3 3273
                  2.1.13.2  The union of two classes   elun 3304
                  2.1.13.3  The intersection of two classes   elin 3346
                  2.1.13.4  Combinations of difference, union, and intersection of two classes   unabs 3394
                  2.1.13.5  Class abstractions with difference, union, and intersection of two classes   symdifxor 3429
                  2.1.13.6  Restricted uniqueness with difference, union, and intersection   reuss2 3443
            2.1.14  The empty set   c0 3450
            2.1.15  Conditional operator   cif 3561
            2.1.16  Power classes   cpw 3605
            2.1.17  Unordered and ordered pairs   csn 3622
            2.1.18  The union of a class   cuni 3839
            2.1.19  The intersection of a class   cint 3874
            2.1.20  Indexed union and intersection   ciun 3916
            2.1.21  Disjointness   wdisj 4010
            2.1.22  Binary relations   wbr 4033
            2.1.23  Ordered-pair class abstractions (class builders)   copab 4093
            2.1.24  Transitive classes   wtr 4131
      ​2.2  IZF Set Theory - add the Axioms of Collection and Separation
            2.2.1  Introduce the Axiom of Collection   ax-coll 4148
            2.2.2  Introduce the Axiom of Separation   ax-sep 4151
            2.2.3  Derive the Null Set Axiom   zfnuleu 4157
            2.2.4  Theorems requiring subset and intersection existence   nalset 4163
            2.2.5  Theorems requiring empty set existence   class2seteq 4196
            2.2.6  Collection principle   bnd 4205
      ​2.3  IZF Set Theory - add the Axioms of Power Sets and Pairing
            2.3.1  Introduce the Axiom of Power Sets   ax-pow 4207
            2.3.2  A notation for excluded middle   wem 4227
            2.3.3  Axiom of Pairing   ax-pr 4242
            2.3.4  Ordered pair theorem   opm 4267
            2.3.5  Ordered-pair class abstractions (cont.)   opabid 4290
            2.3.6  Power class of union and intersection   pwin 4317
            2.3.7  Epsilon and identity relations   cep 4322
            ​*2.3.8  Partial and total orderings   wpo 4329
            2.3.9  Founded and set-like relations   wfrfor 4362
            2.3.10  Ordinals   word 4397
      ​2.4  IZF Set Theory - add the Axiom of Union
            2.4.1  Introduce the Axiom of Union   ax-un 4468
            2.4.2  Ordinals (continued)   ordon 4522
      ​2.5  IZF Set Theory - add the Axiom of Set Induction
            2.5.1  The ZF Axiom of Foundation would imply Excluded Middle   regexmidlemm 4568
            2.5.2  Introduce the Axiom of Set Induction   ax-setind 4573
            2.5.3  Transfinite induction   tfi 4618
      ​2.6  IZF Set Theory - add the Axiom of Infinity
            2.6.1  Introduce the Axiom of Infinity   ax-iinf 4624
            2.6.2  The natural numbers   com 4626
            2.6.3  Peano's postulates   peano1 4630
            2.6.4  Finite induction (for finite ordinals)   find 4635
            2.6.5  The Natural Numbers (continued)   nn0suc 4640
            2.6.6  Relations   cxp 4661
            2.6.7  Definite description binder (inverted iota)   cio 5217
            2.6.8  Functions   wfun 5252
            2.6.9  Cantor's Theorem   canth 5875
            2.6.10  Restricted iota (description binder)   crio 5876
            2.6.11  Operations   co 5922
            2.6.12  Maps-to notation   elmpocl 6118
            2.6.13  Function operation   cof 6133
            2.6.14  Functions (continued)   resfunexgALT 6165
            2.6.15  First and second members of an ordered pair   c1st 6196
            ​*2.6.16  Special maps-to operations   opeliunxp2f 6296
            2.6.17  Function transposition   ctpos 6302
            2.6.18  Undefined values   pwuninel2 6340
            2.6.19  Functions on ordinals; strictly monotone ordinal functions   iunon 6342
            2.6.20  "Strong" transfinite recursion   crecs 6362
            2.6.21  Recursive definition generator   crdg 6427
            2.6.22  Finite recursion   cfrec 6448
            2.6.23  Ordinal arithmetic   c1o 6467
            2.6.24  Natural number arithmetic   nna0 6532
            2.6.25  Equivalence relations and classes   wer 6589
            2.6.26  The mapping operation   cmap 6707
            2.6.27  Infinite Cartesian products   cixp 6757
            2.6.28  Equinumerosity   cen 6797
            2.6.29  Equinumerosity (cont.)   xpf1o 6905
            2.6.30  Pigeonhole Principle   phplem1 6913
            2.6.31  Finite sets   fict 6929
            2.6.32  Schroeder-Bernstein Theorem   sbthlem1 7023
            2.6.33  Finite intersections   cfi 7034
            2.6.34  Supremum and infimum   csup 7048
            2.6.35  Ordinal isomorphism   ordiso2 7101
            2.6.36  Disjoint union   cdju 7103
                  2.6.36.1  Disjoint union   cdju 7103
                  ​*2.6.36.2  Left and right injections of a disjoint union   cinl 7111
                  2.6.36.3  Universal property of the disjoint union   djuss 7136
                  2.6.36.4  Dominance and equinumerosity properties of disjoint union   djudom 7159
                  2.6.36.5  Older definition temporarily kept for comparison, to be deleted   cdjud 7168
                  2.6.36.6  Countable sets   0ct 7173
            ​*2.6.37  The one-point compactification of the natural numbers   xnninf 7185
            2.6.38  Omniscient sets   comni 7200
            2.6.39  Markov's principle   cmarkov 7217
            2.6.40  Weakly omniscient sets   cwomni 7229
            2.6.41  Cardinal numbers   ccrd 7246
            2.6.42  Axiom of Choice equivalents   wac 7272
            2.6.43  Cardinal number arithmetic   endjudisj 7277
            2.6.44  Ordinal trichotomy   exmidontriimlem1 7288
            2.6.45  Excluded middle and the power set of a singleton   pw1on 7293
            2.6.46  Apartness relations   wap 7314
​​*PART 3  CHOICE PRINCIPLES
      ​3.1  Countable Choice and Dependent Choice
            3.1.1  Introduce Countable Choice   wacc 7329
​​*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 7339
            4.1.2  Final derivation of real and complex number postulates   axcnex 7926
            4.1.3  Real and complex number postulates restated as axioms   ax-cnex 7970
      ​4.2  Derive the basic properties from the field axioms
            4.2.1  Some deductions from the field axioms for complex numbers   cnex 8003
            4.2.2  Infinity and the extended real number system   cpnf 8058
            4.2.3  Restate the ordering postulates with extended real "less than"   axltirr 8093
            4.2.4  Ordering on reals   lttr 8100
            4.2.5  Initial properties of the complex numbers   mul12 8155
      ​4.3  Real and complex numbers - basic operations
            4.3.1  Addition   add12 8184
            4.3.2  Subtraction   cmin 8197
            4.3.3  Multiplication   kcnktkm1cn 8409
            4.3.4  Ordering on reals (cont.)   ltadd2 8446
            4.3.5  Real Apartness   creap 8601
            4.3.6  Complex Apartness   cap 8608
            4.3.7  Reciprocals   recextlem1 8678
            4.3.8  Division   cdiv 8699
            4.3.9  Ordering on reals (cont.)   ltp1 8871
            4.3.10  Suprema   lbreu 8972
            4.3.11  Imaginary and complex number properties   crap0 8985
            4.3.12  Function operation analogue theorems   ofnegsub 8989
      ​4.4  Integer sets
            4.4.1  Positive integers (as a subset of complex numbers)   cn 8990
            4.4.2  Principle of mathematical induction   nnind 9006
            ​*4.4.3  Decimal representation of numbers   c2 9041
            ​*4.4.4  Some properties of specific numbers   neg1cn 9095
            4.4.5  Simple number properties   halfcl 9217
            4.4.6  The Archimedean property   arch 9246
            4.4.7  Nonnegative integers (as a subset of complex numbers)   cn0 9249
            ​*4.4.8  Extended nonnegative integers   cxnn0 9312
            4.4.9  Integers (as a subset of complex numbers)   cz 9326
            4.4.10  Decimal arithmetic   cdc 9457
            4.4.11  Upper sets of integers   cuz 9601
            4.4.12  Rational numbers (as a subset of complex numbers)   cq 9693
            4.4.13  Complex numbers as pairs of reals   cnref1o 9725
      ​4.5  Order sets
            4.5.1  Positive reals (as a subset of complex numbers)   crp 9728
            4.5.2  Infinity and the extended real number system (cont.)   cxne 9844
            4.5.3  Real number intervals   cioo 9963
            4.5.4  Finite intervals of integers   cfz 10083
            ​*4.5.5  Finite intervals of nonnegative integers   elfz2nn0 10187
            4.5.6  Half-open integer ranges   cfzo 10217
            4.5.7  Rational numbers (cont.)   qtri3or 10330
      ​4.6  Elementary integer functions
            4.6.1  The floor and ceiling functions   cfl 10358
            4.6.2  The modulo (remainder) operation   cmo 10414
            4.6.3  Miscellaneous theorems about integers   frec2uz0d 10491
            4.6.4  Strong induction over upper sets of integers   uzsinds 10536
            4.6.5  The infinite sequence builder "seq"   cseq 10539
            4.6.6  Integer powers   cexp 10630
            4.6.7  Ordered pair theorem for nonnegative integers   nn0le2msqd 10811
            4.6.8  Factorial function   cfa 10817
            4.6.9  The binomial coefficient operation   cbc 10839
            4.6.10  The ` # ` (set size) function   chash 10867
      ​​*4.7  Words over a set
            4.7.1  Definitions and basic theorems   cword 10935
      ​4.8  Elementary real and complex functions
            4.8.1  The "shift" operation   cshi 10979
            4.8.2  Real and imaginary parts; conjugate   ccj 11004
            4.8.3  Sequence convergence   caucvgrelemrec 11144
            4.8.4  Square root; absolute value   csqrt 11161
            4.8.5  The maximum of two real numbers   maxcom 11368
            4.8.6  The minimum of two real numbers   mincom 11394
            4.8.7  The maximum of two extended reals   xrmaxleim 11409
            4.8.8  The minimum of two extended reals   xrnegiso 11427
      ​4.9  Elementary limits and convergence
            4.9.1  Limits   cli 11443
            4.9.2  Finite and infinite sums   csu 11518
            4.9.3  The binomial theorem   binomlem 11648
            4.9.4  Infinite sums (cont.)   isumshft 11655
            4.9.5  Miscellaneous converging and diverging sequences   divcnv 11662
            4.9.6  Arithmetic series   arisum 11663
            4.9.7  Geometric series   expcnvap0 11667
            4.9.8  Ratio test for infinite series convergence   cvgratnnlembern 11688
            4.9.9  Mertens' theorem   mertenslemub 11699
            4.9.10  Finite and infinite products   prodf 11703
                  4.9.10.1  Product sequences   prodf 11703
                  4.9.10.2  Non-trivial convergence   ntrivcvgap 11713
                  4.9.10.3  Complex products   cprod 11715
                  4.9.10.4  Finite products   fprodseq 11748
      ​4.10  Elementary trigonometry
            4.10.1  The exponential, sine, and cosine functions   ce 11807
                  4.10.1.1  The circle constant (tau = 2 pi)   ctau 11940
            4.10.2  _e is irrational   eirraplem 11942
​​*PART 5  ELEMENTARY NUMBER THEORY
      ​5.1  Elementary properties of divisibility
            5.1.1  The divides relation   cdvds 11952
            ​*5.1.2  Even and odd numbers   evenelz 12032
            5.1.3  The division algorithm   divalglemnn 12083
            5.1.4  Bit sequences   cbits 12105
            5.1.5  The greatest common divisor operator   cgcd 12120
            5.1.6  Bézout's identity   bezoutlemnewy 12163
            5.1.7  Decidable sets of integers   nnmindc 12201
            5.1.8  Algorithms   nn0seqcvgd 12209
            5.1.9  Euclid's Algorithm   eucalgval2 12221
            ​*5.1.10  The least common multiple   clcm 12228
            ​*5.1.11  Coprimality and Euclid's lemma   coprmgcdb 12256
            5.1.12  Cancellability of congruences   congr 12268
      ​5.2  Elementary prime number theory
            ​*5.2.1  Elementary properties   cprime 12275
            ​*5.2.2  Coprimality and Euclid's lemma (cont.)   coprm 12312
            5.2.3  Non-rationality of square root of 2   sqrt2irrlem 12329
            5.2.4  Properties of the canonical representation of a rational   cnumer 12349
            5.2.5  Euler's theorem   codz 12376
            5.2.6  Arithmetic modulo a prime number   modprm1div 12416
            5.2.7  Pythagorean Triples   coprimeprodsq 12426
            5.2.8  The prime count function   cpc 12453
            5.2.9  Pocklington's theorem   prmpwdvds 12524
            5.2.10  Infinite primes theorem   infpnlem1 12528
            5.2.11  Fundamental theorem of arithmetic   1arithlem1 12532
            5.2.12  Lagrange's four-square theorem   cgz 12538
            5.2.13  Decimal arithmetic (cont.)   dec2dvds 12580
      ​5.3  Cardinality of real and complex number subsets
            5.3.1  Countability of integers and rationals   oddennn 12609
​PART 6  BASIC STRUCTURES
      ​6.1  Extensible structures
            ​*6.1.1  Basic definitions   cstr 12674
            6.1.2  Slot definitions   cplusg 12755
            6.1.3  Definition of the structure product   crest 12910
            6.1.4  Definition of the structure quotient   cimas 12942
​PART 7  BASIC ALGEBRAIC STRUCTURES
      ​7.1  Monoids
            ​*7.1.1  Magmas   cplusf 12996
            ​*7.1.2  Identity elements   mgmidmo 13015
            ​*7.1.3  Iterated sums in a magma   fngsum 13031
            ​*7.1.4  Semigroups   csgrp 13044
            ​*7.1.5  Definition and basic properties of monoids   cmnd 13057
            7.1.6  Monoid homomorphisms and submonoids   cmhm 13089
            ​*7.1.7  Iterated sums in a monoid   gsumvallem2 13125
      ​7.2  Groups
            7.2.1  Definition and basic properties   cgrp 13132
            ​*7.2.2  Group multiple operation   cmg 13249
            7.2.3  Subgroups and Quotient groups   csubg 13297
            7.2.4  Elementary theory of group homomorphisms   cghm 13370
            7.2.5  Abelian groups   ccmn 13414
                  7.2.5.1  Definition and basic properties   ccmn 13414
                  7.2.5.2  Group sum operation   gsumfzreidx 13467
      ​7.3  Rings
            7.3.1  Multiplicative Group   cmgp 13476
            ​*7.3.2  Non-unital rings ("rngs")   crng 13488
            ​*7.3.3  Ring unity (multiplicative identity)   cur 13515
            7.3.4  Semirings   csrg 13519
            7.3.5  Definition and basic properties of unital rings   crg 13552
            7.3.6  Opposite ring   coppr 13623
            7.3.7  Divisibility   cdsr 13642
            7.3.8  Ring homomorphisms   crh 13706
            7.3.9  Nonzero rings and zero rings   cnzr 13735
            7.3.10  Local rings   clring 13746
            7.3.11  Subrings   csubrng 13753
                  7.3.11.1  Subrings of non-unital rings   csubrng 13753
                  7.3.11.2  Subrings of unital rings   csubrg 13773
            7.3.12  Left regular elements and domains   crlreg 13811
      ​7.4  Division rings and fields
            7.4.1  Ring apartness   capr 13836
      ​7.5  Left modules
            7.5.1  Definition and basic properties   clmod 13843
            7.5.2  Subspaces and spans in a left module   clss 13908
      ​7.6  Subring algebras and ideals
            7.6.1  Subring algebras   csra 13989
            7.6.2  Ideals and spans   clidl 14023
            7.6.3  Two-sided ideals and quotient rings   c2idl 14055
            7.6.4  Principal ideal rings. Divisibility in the integers   rspsn 14090
      ​7.7  The complex numbers as an algebraic extensible structure
            7.7.1  Definition and basic properties   cpsmet 14091
            ​*7.7.2  Ring of integers   czring 14146
            7.7.3  Algebraic constructions based on the complex numbers   czrh 14167
​​*PART 8  BASIC LINEAR ALGEBRA
      ​8.1  Abstract multivariate polynomials
            8.1.1  Definition and basic properties   cmps 14217
​PART 9  BASIC TOPOLOGY
      ​9.1  Topology
            ​*9.1.1  Topological spaces   ctop 14233
                  9.1.1.1  Topologies   ctop 14233
                  9.1.1.2  Topologies on sets   ctopon 14246
                  9.1.1.3  Topological spaces   ctps 14266
            9.1.2  Topological bases   ctb 14278
            9.1.3  Examples of topologies   distop 14321
            9.1.4  Closure and interior   ccld 14328
            9.1.5  Neighborhoods   cnei 14374
            9.1.6  Subspace topologies   restrcl 14403
            9.1.7  Limits and continuity in topological spaces   ccn 14421
            9.1.8  Product topologies   ctx 14488
            9.1.9  Continuous function-builders   cnmptid 14517
            9.1.10  Homeomorphisms   chmeo 14536
      ​9.2  Metric spaces
            9.2.1  Pseudometric spaces   psmetrel 14558
            9.2.2  Basic metric space properties   cxms 14572
            9.2.3  Metric space balls   blfvalps 14621
            9.2.4  Open sets of a metric space   mopnrel 14677
            9.2.5  Continuity in metric spaces   metcnp3 14747
            9.2.6  Topology on the reals   qtopbasss 14757
            9.2.7  Topological definitions using the reals   ccncf 14806
​PART 10  BASIC REAL AND COMPLEX ANALYSIS
      ​10.1  Continuity
            10.1.1  Dedekind cuts   dedekindeulemuub 14853
            10.1.2  Intermediate value theorem   ivthinclemlm 14870
      ​10.2  Derivatives
            10.2.1  Real and complex differentiation   climc 14890
                  10.2.1.1  Derivatives of functions of one complex or real variable   climc 14890
​PART 11  BASIC REAL AND COMPLEX FUNCTIONS
      ​11.1  Polynomials
            11.1.1  Elementary properties of complex polynomials   cply 14964
      ​11.2  Basic trigonometry
            11.2.1  The exponential, sine, and cosine functions (cont.)   efcn 15004
            11.2.2  Properties of pi = 3.14159...   pilem1 15015
            11.2.3  The natural logarithm on complex numbers   clog 15092
            ​*11.2.4  Logarithms to an arbitrary base   clogb 15179
            11.2.5  Quartic binomial expansion   binom4 15215
      ​11.3  Basic number theory
            11.3.1  Wilson's theorem   wilthlem1 15216
            11.3.2  Number-theoretical functions   csgm 15217
            11.3.3  Perfect Number Theorem   mersenne 15233
            ​*11.3.4  Quadratic residues and the Legendre symbol   clgs 15238
            ​*11.3.5  Gauss' Lemma   gausslemma2dlem0a 15290
            11.3.6  Quadratic reciprocity   lgseisenlem1 15311
            11.3.7  All primes 4n+1 are the sum of two squares   2sqlem1 15355
​PART 12  GUIDES AND MISCELLANEA
      ​12.1  Guides (conventions, explanations, and examples)
            ​*12.1.1  Conventions   conventions 15367
            12.1.2  Definitional examples   ex-or 15368
​PART 13  SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
      ​13.1  Mathboxes for user contributions
            13.1.1  Mathbox guidelines   mathbox 15378
      ​13.2  Mathbox for BJ
            13.2.1  Propositional calculus   bj-nnsn 15379
                  ​*13.2.1.1  Stable formulas   bj-trst 15385
                  13.2.1.2  Decidable formulas   bj-trdc 15398
            13.2.2  Predicate calculus   bj-ex 15408
            13.2.3  Set theorey miscellaneous   bj-el2oss1o 15420
            ​*13.2.4  Extensionality   bj-vtoclgft 15421
            ​*13.2.5  Decidability of classes   wdcin 15439
            13.2.6  Disjoint union   djucllem 15446
            13.2.7  Miscellaneous   funmptd 15449
            ​*13.2.8  Constructive Zermelo--Fraenkel set theory (CZF): Bounded formulas and classes   wbd 15458
                  *13.2.8.1  Bounded formulas   wbd 15458
                  ​*13.2.8.2  Bounded classes   wbdc 15486
            ​*13.2.9  CZF: Bounded separation   ax-bdsep 15530
                  13.2.9.1  Delta_0-classical logic   ax-bj-d0cl 15570
                  13.2.9.2  Inductive classes and the class of natural number ordinals   wind 15572
                  ​*13.2.9.3  The first three Peano postulates   bj-peano2 15585
            ​*13.2.10  CZF: Infinity   ax-infvn 15587
                  *13.2.10.1  The set of natural number ordinals   ax-infvn 15587
                  ​*13.2.10.2  Peano's fifth postulate   bdpeano5 15589
                  ​*13.2.10.3  Bounded induction and Peano's fourth postulate   findset 15591
            ​*13.2.11  CZF: Set induction   setindft 15611
                  *13.2.11.1  Set induction   setindft 15611
                  ​*13.2.11.2  Full induction   bj-findis 15625
            ​*13.2.12  CZF: Strong collection   ax-strcoll 15628
            ​*13.2.13  CZF: Subset collection   ax-sscoll 15633
            13.2.14  Real numbers   ax-ddkcomp 15635
      ​13.3  Mathbox for Jim Kingdon
            13.3.1  Propositional and predicate logic   nnnotnotr 15636
            13.3.2  Natural numbers   1dom1el 15637
            13.3.3  The power set of a singleton   pwtrufal 15642
            13.3.4  Omniscience of NN+oo   0nninf 15648
            13.3.5  Schroeder-Bernstein Theorem   exmidsbthrlem 15666
            13.3.6  Real and complex numbers   qdencn 15671
            ​*13.3.7  Analytic omniscience principles   trilpolemclim 15680
            13.3.8  Supremum and infimum   supfz 15715
            13.3.9  Circle constant   taupi 15717
      ​13.4  Mathbox for Mykola Mostovenko
      ​13.5  Mathbox for David A. Wheeler
            13.5.1  Testable propositions   dftest 15719
            ​*13.5.2  Allsome quantifier   walsi 15720