Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description | ||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Theorem | ||||||||||||||
24-Oct-2021 | ax-ddkcomp 10114 | Axiom of Dedekind completeness for Dedekind real numbers: every nonempty upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 10114 should be used in place of construction specific results. In particular, axcaucvg 6974 should be proved from it. (Contributed by BJ, 24-Oct-2021.) | ||||||||||||
20-Oct-2021 | onunsnss 6355 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) | ||||||||||||
19-Oct-2021 | snon0 6356 | An ordinal which is a singleton is . (Contributed by Jim Kingdon, 19-Oct-2021.) | ||||||||||||
18-Oct-2021 | qdencn 10124 | The set of complex numbers whose real and imaginary parts are rational is dense in the complex plane. This is a two dimensional analogue to qdenre 9798 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqmulnn 9184 | Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | intqfrac 9181 | Break a number into its integer part and its fractional part. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | flqmod 9180 | The floor function expressed in terms of the modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqfrac 9179 | The fractional part of a number is the number modulo 1. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqdifz 9178 | The modulo operation differs from by an integer multiple of . (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqdiffl 9177 | The modulo operation differs from by an integer multiple of . (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqelico 9176 | Modular reduction produces a half-open interval. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqlt 9175 | The modulo operation is less than its second argument. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | modqge0 9174 | The modulo operation is nonnegative. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | negqmod0 9173 | is divisible by iff its negative is. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | mulqmod0 9172 | The product of an integer and a positive rational number is 0 modulo the positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | flqdiv 9163 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
18-Oct-2021 | intqfrac2 9161 | Decompose a real into integer and fractional parts. (Contributed by Jim Kingdon, 18-Oct-2021.) | ||||||||||||
17-Oct-2021 | modq0 9171 | is zero iff is evenly divisible by . (Contributed by Jim Kingdon, 17-Oct-2021.) | ||||||||||||
16-Oct-2021 | modqcld 9170 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) | ||||||||||||
16-Oct-2021 | flqpmodeq 9169 | Partition of a division into its integer part and the remainder. (Contributed by Jim Kingdon, 16-Oct-2021.) | ||||||||||||
16-Oct-2021 | modqcl 9168 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) | ||||||||||||
16-Oct-2021 | modqvalr 9167 | The value of the modulo operation (multiplication in reversed order). (Contributed by Jim Kingdon, 16-Oct-2021.) | ||||||||||||
16-Oct-2021 | modqval 9166 | The value of the modulo operation. The modulo congruence notation of number theory, (modulo ), can be expressed in our notation as . Definition 1 in Knuth, The Art of Computer Programming, Vol. I (1972), p. 38. Knuth uses "mod" for the operation and "modulo" for the congruence. Unlike Knuth, we restrict the second argument to positive numbers to simplify certain theorems. (This also gives us future flexibility to extend it to any one of several different conventions for a zero or negative second argument, should there be an advantage in doing so.) As with flqcl 9117 we only prove this for rationals although other particular kinds of real numbers may be possible. (Contributed by Jim Kingdon, 16-Oct-2021.) | ||||||||||||
15-Oct-2021 | qdenre 9798 | The rational numbers are dense in : any real number can be approximated with arbitrary precision by a rational number. For order theoretic density, see qbtwnre 9111. (Contributed by BJ, 15-Oct-2021.) | ||||||||||||
14-Oct-2021 | qbtwnrelemcalc 9110 | Lemma for qbtwnre 9111. Calculations involved in showing the constructed rational number is less than . (Contributed by Jim Kingdon, 14-Oct-2021.) | ||||||||||||
13-Oct-2021 | rebtwn2z 9109 |
A real number can be bounded by integers above and below which are two
apart.
The proof starts by finding two integers which are less than and greater than the given real number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.) | ||||||||||||
13-Oct-2021 | rebtwn2zlemshrink 9108 | Lemma for rebtwn2z 9109. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.) | ||||||||||||
13-Oct-2021 | rebtwn2zlemstep 9107 | Lemma for rebtwn2z 9109. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.) | ||||||||||||
11-Oct-2021 | flqeqceilz 9160 | A rational number is an integer iff its floor equals its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | flqleceil 9159 | The floor of a rational number is less than or equal to its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceilqidz 9158 | A rational number equals its ceiling iff it is an integer. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceilqle 9156 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceiqle 9155 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
11-Oct-2021 | ceilqm1lt 9154 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceiqm1l 9153 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
11-Oct-2021 | ceilqge 9152 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceiqge 9151 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
11-Oct-2021 | ceilqcl 9150 | Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
11-Oct-2021 | ceiqcl 9149 | The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
11-Oct-2021 | qdceq 9102 | Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
DECID | ||||||||||||||
11-Oct-2021 | qltlen 8575 | Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7621 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.) | ||||||||||||
10-Oct-2021 | ceilqval 9148 | The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
⌈ | ||||||||||||||
10-Oct-2021 | flqmulnn0 9141 | Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
10-Oct-2021 | flqzadd 9140 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
10-Oct-2021 | flqaddz 9139 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
10-Oct-2021 | flqge1nn 9136 | The floor of a number greater than or equal to 1 is a positive integer. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
10-Oct-2021 | flqge0nn0 9135 | The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
10-Oct-2021 | 4ap0 8015 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
# | ||||||||||||||
10-Oct-2021 | 3ap0 8012 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) | ||||||||||||
# | ||||||||||||||
9-Oct-2021 | flqbi2 9133 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
9-Oct-2021 | flqbi 9132 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
9-Oct-2021 | flqword2 9131 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
9-Oct-2021 | flqwordi 9130 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
9-Oct-2021 | flqltnz 9129 | If A is not an integer, then the floor of A is less than A. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
9-Oct-2021 | flqidz 9128 | A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqidm 9127 | The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqlt 9125 | The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqge 9124 | The floor function value is the greatest integer less than or equal to its argument. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qfracge0 9123 | The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qfraclt1 9122 | The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqltp1 9121 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqle 9120 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqcld 9119 | The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqlelt 9118 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | flqcl 9117 | The floor (greatest integer) function yields an integer when applied to a rational (closure law). It would presumably be possible to prove a similar result for some real numbers (for example, those apart from any integer), but not real numbers in general. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qbtwnz 9106 | There is a unique greatest integer less than or equal to a rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qbtwnzlemex 9105 |
Lemma for qbtwnz 9106. Existence of the integer.
The proof starts by finding two integers which are less than and greater than the given rational number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on rational number trichotomy, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qbtwnzlemshrink 9104 | Lemma for qbtwnz 9106. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qbtwnzlemstep 9103 | Lemma for qbtwnz 9106. Induction step. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
8-Oct-2021 | qltnle 9101 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.) | ||||||||||||
7-Oct-2021 | qlelttric 9100 | Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.) | ||||||||||||
6-Oct-2021 | qletric 9099 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) | ||||||||||||
6-Oct-2021 | qtri3or 9098 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) | ||||||||||||
3-Oct-2021 | reg3exmid 4304 | If any inhabited set satisfying df-wetr 4071 for has a minimal element, excluded middle follows. (Contributed by Jim Kingdon, 3-Oct-2021.) | ||||||||||||
3-Oct-2021 | reg3exmidlemwe 4303 | Lemma for reg3exmid 4304. Our counterexample satisfies . (Contributed by Jim Kingdon, 3-Oct-2021.) | ||||||||||||
2-Oct-2021 | reg2exmid 4261 | If any inhabited set has a minimal element (when expressed by ), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) | ||||||||||||
2-Oct-2021 | reg2exmidlema 4259 | Lemma for reg2exmid 4261. If has a minimal element (expressed by ), excluded middle follows. (Contributed by Jim Kingdon, 2-Oct-2021.) | ||||||||||||
30-Sep-2021 | fin0or 6343 | A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.) | ||||||||||||
30-Sep-2021 | wessep 4302 | A subset of a set well-ordered by set membership is well-ordered by set membership. (Contributed by Jim Kingdon, 30-Sep-2021.) | ||||||||||||
28-Sep-2021 | frind 4089 | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) | ||||||||||||
26-Sep-2021 | wetriext 4301 | A trichotomous well-order is extensional. (Contributed by Jim Kingdon, 26-Sep-2021.) | ||||||||||||
25-Sep-2021 | nnwetri 6354 | A natural number is well-ordered by . More specifically, this order both satisfies and is trichotomous. (Contributed by Jim Kingdon, 25-Sep-2021.) | ||||||||||||
23-Sep-2021 | wepo 4096 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) | ||||||||||||
23-Sep-2021 | df-wetr 4071 | Define the well-ordering predicate. It is unusual to define "well-ordering" in the absence of excluded middle, but we mean an ordering which is like the ordering which we have for ordinals (for example, it does not entail trichotomy because ordinals don't have that as seen at ordtriexmid 4247). Given excluded middle, well-ordering is usually defined to require trichotomy (and the defintion of is typically also different). (Contributed by Mario Carneiro and Jim Kingdon, 23-Sep-2021.) | ||||||||||||
22-Sep-2021 | frforeq3 4084 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) | ||||||||||||
FrFor FrFor | ||||||||||||||
22-Sep-2021 | frforeq2 4082 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) | ||||||||||||
FrFor FrFor | ||||||||||||||
22-Sep-2021 | frforeq1 4080 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) | ||||||||||||
FrFor FrFor | ||||||||||||||
22-Sep-2021 | df-frfor 4068 | Define the well-founded relation predicate where might be a proper class. By passing in we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.) | ||||||||||||
FrFor | ||||||||||||||
21-Sep-2021 | frirrg 4087 | A well-founded relation is irreflexive. This is the case where exists. (Contributed by Jim Kingdon, 21-Sep-2021.) | ||||||||||||
21-Sep-2021 | df-frind 4069 | Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via . (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.) | ||||||||||||
FrFor | ||||||||||||||
17-Sep-2021 | ontr2exmid 4250 | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) | ||||||||||||
16-Sep-2021 | nnsseleq 6079 | For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.) | ||||||||||||
15-Sep-2021 | fientri3 6353 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) | ||||||||||||
15-Sep-2021 | nntri2or2 6076 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.) | ||||||||||||
14-Sep-2021 | findcard2sd 6349 | Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.) | ||||||||||||
13-Sep-2021 | php5fin 6339 | A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.) | ||||||||||||
13-Sep-2021 | fiunsnnn 6338 | Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.) | ||||||||||||
12-Sep-2021 | fisbth 6340 | Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.) | ||||||||||||
11-Sep-2021 | diffisn 6350 | Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.) | ||||||||||||
10-Sep-2021 | fin0 6342 | A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.) | ||||||||||||
9-Sep-2021 | fidifsnid 6332 | If we remove a single element from a finite set then put it back in, we end up with the original finite set. This strengthens difsnss 3510 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.) | ||||||||||||
9-Sep-2021 | fidifsnen 6331 | All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.) | ||||||||||||
8-Sep-2021 | diffifi 6351 | Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.) | ||||||||||||
8-Sep-2021 | diffitest 6344 | If subtracting any set from a finite set gives a finite set, any proposition of the form is decidable. This is not a proof of full excluded middle, but it is close enough to show we won't be able to prove . (Contributed by Jim Kingdon, 8-Sep-2021.) | ||||||||||||
6-Sep-2021 | phpelm 6328 | Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.) | ||||||||||||
5-Sep-2021 | fidceq 6330 | Equality of members of a finite set is decidable. This may be counterintuitive: cannot any two sets be elements of a finite set? Well, to show, for example, that is finite would require showing it is equinumerous to or to but to show that you'd need to know or , respectively. (Contributed by Jim Kingdon, 5-Sep-2021.) | ||||||||||||
DECID | ||||||||||||||
5-Sep-2021 | phplem4on 6329 | Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.) | ||||||||||||
4-Sep-2021 | ex-ceil 9896 | Example for df-ceil 9115. (Contributed by AV, 4-Sep-2021.) | ||||||||||||
⌈ ⌈ | ||||||||||||||
3-Sep-2021 | 0elsucexmid 4289 | If the successor of any ordinal class contains the empty set, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2021.) | ||||||||||||
1-Sep-2021 | php5dom 6325 | A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.) | ||||||||||||
1-Sep-2021 | phplem4dom 6324 | Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.) | ||||||||||||
1-Sep-2021 | snnen2oprc 6323 | A singleton is never equinumerous with the ordinal number 2. If is a set, see snnen2og 6322. (Contributed by Jim Kingdon, 1-Sep-2021.) | ||||||||||||
1-Sep-2021 | snnen2og 6322 | A singleton is never equinumerous with the ordinal number 2. If is a proper class, see snnen2oprc 6323. (Contributed by Jim Kingdon, 1-Sep-2021.) | ||||||||||||
1-Sep-2021 | phplem3g 6319 | A natural number is equinumerous to its successor minus any element of the successor. Version of phplem3 6317 with unnecessary hypotheses removed. (Contributed by Jim Kingdon, 1-Sep-2021.) | ||||||||||||
31-Aug-2021 | nndifsnid 6080 | If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3510 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.) | ||||||||||||
30-Aug-2021 | carden2bex 6369 | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) | ||||||||||||
30-Aug-2021 | cardval3ex 6365 | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) | ||||||||||||
30-Aug-2021 | cardcl 6361 | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) | ||||||||||||
30-Aug-2021 | onintrab2im 4244 | An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.) | ||||||||||||
30-Aug-2021 | onintonm 4243 | The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.) | ||||||||||||
29-Aug-2021 | onintexmid 4297 | If the intersection (infimum) of an inhabited class of ordinal numbers belongs to the class, excluded middle follows. The hypothesis would be provable given excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Aug-2021.) | ||||||||||||
29-Aug-2021 | ordtri2or2exmid 4296 | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 29-Aug-2021.) | ||||||||||||
29-Aug-2021 | ordtri2or2exmidlem 4251 | A set which is if or if is an ordinal. (Contributed by Jim Kingdon, 29-Aug-2021.) | ||||||||||||
29-Aug-2021 | 2ordpr 4249 | Version of 2on 6009 with the definition of expanded and expressed in terms of . (Contributed by Jim Kingdon, 29-Aug-2021.) | ||||||||||||
25-Aug-2021 | nnap0d 7959 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.) | ||||||||||||
# | ||||||||||||||
24-Aug-2021 | climcaucn 9870 | A converging sequence of complex numbers is a Cauchy sequence. This is like climcau 9866 but adds the part that is complex. (Contributed by Jim Kingdon, 24-Aug-2021.) | ||||||||||||
24-Aug-2021 | climcvg1nlem 9868 | Lemma for climcvg1n 9869. We construct sequences of the real and imaginary parts of each term of , show those converge, and use that to show that converges. (Contributed by Jim Kingdon, 24-Aug-2021.) | ||||||||||||
23-Aug-2021 | climcvg1n 9869 | A Cauchy sequence of complex numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.) | ||||||||||||
23-Aug-2021 | climrecvg1n 9867 | A Cauchy sequence of real numbers converges, existence version. The rate of convergence is fixed: all terms after the nth term must be within of the nth term, where is a constant multiplier. (Contributed by Jim Kingdon, 23-Aug-2021.) | ||||||||||||
22-Aug-2021 | climserile 9865 | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
22-Aug-2021 | iserige0 9863 | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
22-Aug-2021 | iserile 9862 | Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
22-Aug-2021 | serile 9253 | Comparison of partial sums of two infinite series of reals. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
22-Aug-2021 | serige0 9252 | A finite sum of nonnegative terms is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.) | ||||||||||||
21-Aug-2021 | clim2iser2 9858 | The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.) | ||||||||||||
21-Aug-2021 | iseqdistr 9249 | The distributive property for series. (Contributed by Jim Kingdon, 21-Aug-2021.) | ||||||||||||
21-Aug-2021 | iseqhomo 9248 | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 21-Aug-2021.) | ||||||||||||
20-Aug-2021 | clim2iser 9857 | The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.) | ||||||||||||
20-Aug-2021 | iseqex 9213 | Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.) | ||||||||||||
20-Aug-2021 | frecex 5981 | Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.) | ||||||||||||
frec | ||||||||||||||
20-Aug-2021 | tfrfun 5955 | Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.) | ||||||||||||
recs | ||||||||||||||
19-Aug-2021 | iserclim0 9826 | The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
19-Aug-2021 | shftval4g 9438 | Value of a sequence shifted by . (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
19-Aug-2021 | iser0f 9251 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
19-Aug-2021 | iser0 9250 | The value of the partial sums in a zero-valued infinite series. (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
19-Aug-2021 | ovexg 5539 | Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.) | ||||||||||||
18-Aug-2021 | iseqid3s 9246 | A sequence that consists of zeroes up to sums to zero at . In this case by "zero" we mean whatever the identity is for the operation ). (Contributed by Jim Kingdon, 18-Aug-2021.) | ||||||||||||
18-Aug-2021 | iseqid3 9245 | A sequence that consists entirely of zeroes (or whatever the identity is for operation ) sums to zero. (Contributed by Jim Kingdon, 18-Aug-2021.) | ||||||||||||
18-Aug-2021 | iseqss 9226 | Specifying a larger universe for . As long as and are closed over , then any set which contains can be used as the last argument to . This theorem does not allow to be a proper class, however. It also currently requires that be closed over (as well as ). (Contributed by Jim Kingdon, 18-Aug-2021.) | ||||||||||||
17-Aug-2021 | iseqcaopr 9242 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.) | ||||||||||||
16-Aug-2021 | iseqcaopr3 9240 | Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.) | ||||||||||||
..^ | ||||||||||||||
16-Aug-2021 | iseq1p 9239 | Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.) | ||||||||||||
16-Aug-2021 | iseqsplit 9238 | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) | ||||||||||||
15-Aug-2021 | shftfibg 9421 | Value of a fiber of the relation . (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
15-Aug-2021 | ovshftex 9420 | Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
15-Aug-2021 | isermono 9237 | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
15-Aug-2021 | iserf 9233 | An infinite series of complex terms is a function from to . (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
15-Aug-2021 | iseqshft2 9232 | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
15-Aug-2021 | iseqfeq 9231 | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) | ||||||||||||
13-Aug-2021 | absdivapd 9791 | Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | absrpclapd 9784 | The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | absdivapzi 9750 | Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | absgt0ap 9695 | The absolute value of a number apart from zero is positive. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | recvalap 9693 | Reciprocal expressed with a real denominator. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | sqap0 9320 | A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
13-Aug-2021 | leltapd 7628 | '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
13-Aug-2021 | leltap 7615 | '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | abssubap0 9686 | If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | ltabs 9683 | A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
12-Aug-2021 | absext 9661 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
12-Aug-2021 | sq11ap 9414 | Analogue to sq11 9326 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
12-Aug-2021 | subap0d 7631 | Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
12-Aug-2021 | ltapd 7627 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | gtapd 7626 | 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | ltapi 7625 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | ltapii 7624 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | gtapii 7623 | 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
12-Aug-2021 | ltap 7622 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) | ||||||||||||
# | ||||||||||||||
11-Aug-2021 | absexpzap 9676 | Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# | ||||||||||||||
11-Aug-2021 | absdivap 9668 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# | ||||||||||||||
11-Aug-2021 | abs00ap 9660 | The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
11-Aug-2021 | absrpclap 9659 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# | ||||||||||||||
11-Aug-2021 | sqrt11ap 9636 | Analogue to sqrt11 9637 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
11-Aug-2021 | cjap0d 9548 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# # | ||||||||||||||
11-Aug-2021 | ap0gt0d 7630 | A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# | ||||||||||||||
11-Aug-2021 | ap0gt0 7629 | A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.) | ||||||||||||
# | ||||||||||||||
10-Aug-2021 | rersqrtthlem 9628 | Lemma for resqrtth 9629. (Contributed by Jim Kingdon, 10-Aug-2021.) | ||||||||||||
10-Aug-2021 | rersqreu 9626 | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) | ||||||||||||
10-Aug-2021 | rsqrmo 9625 | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) | ||||||||||||
9-Aug-2021 | resqrexlemoverl 9619 | Lemma for resqrex 9624. Every term in the sequence is an overestimate compared with the limit . Although this theorem is stated in terms of a particular sequence the proof could be adapted for any decreasing convergent sequence. (Contributed by Jim Kingdon, 9-Aug-2021.) | ||||||||||||
8-Aug-2021 | resqrexlemga 9621 | Lemma for resqrex 9624. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) | ||||||||||||
8-Aug-2021 | resqrexlemglsq 9620 | Lemma for resqrex 9624. The sequence formed by squaring each term of converges to . (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.) | ||||||||||||
8-Aug-2021 | recvguniqlem 9592 | Lemma for recvguniq 9593. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) | ||||||||||||
8-Aug-2021 | ifcldcd 3358 | Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) | ||||||||||||
DECID | ||||||||||||||
8-Aug-2021 | ifbothdc 3357 | A wff containing a conditional operator is true when both of its cases are true. (Contributed by Jim Kingdon, 8-Aug-2021.) | ||||||||||||
DECID | ||||||||||||||
7-Aug-2021 | resqrexlemsqa 9622 | Lemma for resqrex 9624. The square of a limit is . (Contributed by Jim Kingdon, 7-Aug-2021.) | ||||||||||||
7-Aug-2021 | resqrexlemgt0 9618 | Lemma for resqrex 9624. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) | ||||||||||||
7-Aug-2021 | recvguniq 9593 | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) | ||||||||||||
6-Aug-2021 | resqrexlemcvg 9617 | Lemma for resqrex 9624. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) | ||||||||||||
6-Aug-2021 | cvg1nlemcxze 9581 | Lemma for cvg1n 9585. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) | ||||||||||||
1-Aug-2021 | cvg1n 9585 |
Convergence of real sequences.
This is a version of caucvgre 9580 with a constant multiplier on the rate of convergence. That is, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 1-Aug-2021.) | ||||||||||||
1-Aug-2021 | cvg1nlemres 9584 | Lemma for cvg1n 9585. The original sequence has a limit (turns out it is the same as the limit of the modified sequence ). (Contributed by Jim Kingdon, 1-Aug-2021.) | ||||||||||||
1-Aug-2021 | cvg1nlemcau 9583 | Lemma for cvg1n 9585. By selecting spaced out terms for the modified sequence , the terms are within (without the constant ). (Contributed by Jim Kingdon, 1-Aug-2021.) | ||||||||||||
1-Aug-2021 | cvg1nlemf 9582 | Lemma for cvg1n 9585. The modified sequence is a sequence. (Contributed by Jim Kingdon, 1-Aug-2021.) | ||||||||||||
31-Jul-2021 | resqrexlemnm 9616 | Lemma for resqrex 9624. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) | ||||||||||||
31-Jul-2021 | resqrexlemdecn 9610 | Lemma for resqrex 9624. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) | ||||||||||||
30-Jul-2021 | resqrexlemnmsq 9615 | Lemma for resqrex 9624. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) | ||||||||||||
30-Jul-2021 | divmuldivapd 7806 | Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.) | ||||||||||||
# # | ||||||||||||||
29-Jul-2021 | resqrexlemcalc3 9614 | Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) | ||||||||||||
29-Jul-2021 | resqrexlemcalc2 9613 | Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) | ||||||||||||
29-Jul-2021 | resqrexlemcalc1 9612 | Lemma for resqrex 9624. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) | ||||||||||||
29-Jul-2021 | resqrexlemlo 9611 | Lemma for resqrex 9624. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) | ||||||||||||
29-Jul-2021 | resqrexlemdec 9609 | Lemma for resqrex 9624. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) | ||||||||||||
28-Jul-2021 | resqrexlemp1rp 9604 | Lemma for resqrex 9624. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) | ||||||||||||
28-Jul-2021 | resqrexlem1arp 9603 | Lemma for resqrex 9624. is a positive real (expressed in a way that will help apply iseqf 9224 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) | ||||||||||||
28-Jul-2021 | rpap0d 8628 | A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.) | ||||||||||||
# | ||||||||||||||
27-Jul-2021 | resqrexlemex 9623 | Lemma for resqrex 9624. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) | ||||||||||||
27-Jul-2021 | resqrexlemover 9608 | Lemma for resqrex 9624. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) | ||||||||||||
27-Jul-2021 | resqrexlemfp1 9607 | Lemma for resqrex 9624. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) | ||||||||||||
27-Jul-2021 | resqrexlemf1 9606 | Lemma for resqrex 9624. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) | ||||||||||||
27-Jul-2021 | resqrexlemf 9605 | Lemma for resqrex 9624. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) | ||||||||||||
23-Jul-2021 | iseqf 9224 | Range of the recursive sequence builder. (Contributed by Jim Kingdon, 23-Jul-2021.) | ||||||||||||
22-Jul-2021 | ialgrlemconst 9882 | Lemma for ialgr0 9883. Closure of a constant function, in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
22-Jul-2021 | ialgrlem1st 9881 | Lemma for ialgr0 9883. Expressing algrflemg 5851 in a form suitable for theorems such as iseq1 9222 or iseqfn 9221. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
22-Jul-2021 | algrflemg 5851 | Lemma for algrf and related theorems. (Contributed by Jim Kingdon, 22-Jul-2021.) | ||||||||||||
21-Jul-2021 | zmod1congr 9183 | Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.) | ||||||||||||
20-Jul-2021 | caucvgrelemcau 9579 | Lemma for caucvgre 9580. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) | ||||||||||||
20-Jul-2021 | caucvgrelemrec 9578 | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) | ||||||||||||
# | ||||||||||||||
19-Jul-2021 | caucvgre 9580 |
Convergence of real sequences.
A Cauchy sequence (as defined here, which has a rate of convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within of the nth term. (Contributed by Jim Kingdon, 19-Jul-2021.) | ||||||||||||
19-Jul-2021 | ax-caucvg 7004 |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 6974.
A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within of the nth term. This axiom should not be used directly; instead use caucvgre 9580 (which is the same, but stated in terms of the and notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) | ||||||||||||
18-Jul-2021 | mulnqpr 6675 | Multiplication of fractions embedded into positive reals. One can either multiply the fractions as fractions, or embed them into positive reals and multiply them as positive reals, and get the same result. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
18-Jul-2021 | mulnqprlemfu 6674 | Lemma for mulnqpr 6675. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
18-Jul-2021 | mulnqprlemfl 6673 | Lemma for mulnqpr 6675. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
18-Jul-2021 | mulnqprlemru 6672 | Lemma for mulnqpr 6675. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
18-Jul-2021 | mulnqprlemrl 6671 | Lemma for mulnqpr 6675. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
18-Jul-2021 | lt2mulnq 6503 | Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.) | ||||||||||||
17-Jul-2021 | recidpirqlemcalc 6933 | Lemma for recidpirq 6934. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) | ||||||||||||
17-Jul-2021 | recidpipr 6932 | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) | ||||||||||||
15-Jul-2021 | rereceu 6963 | The reciprocal from axprecex 6954 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) | ||||||||||||
15-Jul-2021 | recidpirq 6934 | A real number times its reciprocal is one, where reciprocal is expressed with . (Contributed by Jim Kingdon, 15-Jul-2021.) | ||||||||||||
15-Jul-2021 | recnnre 6927 | Embedding the reciprocal of a natural number into . (Contributed by Jim Kingdon, 15-Jul-2021.) | ||||||||||||
15-Jul-2021 | pitore 6926 | Embedding from to . Similar to pitonn 6924 but separate in the sense that we have not proved nnssre 7918 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) | ||||||||||||
15-Jul-2021 | pitoregt0 6925 | Embedding from to yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) | ||||||||||||
14-Jul-2021 | adddivflid 9134 | The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021.) | ||||||||||||
14-Jul-2021 | nnindnn 6967 | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 7930 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) | ||||||||||||
14-Jul-2021 | peano5nnnn 6966 | Peano's inductive postulate. This is a counterpart to peano5nni 7917 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) | ||||||||||||
14-Jul-2021 | peano2nnnn 6929 | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 7926 designed for real number axioms which involve to natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) | ||||||||||||
14-Jul-2021 | peano1nnnn 6928 | One is an element of . This is a counterpart to 1nn 7925 designed for real number axioms which involve natural numbers (notably, axcaucvg 6974). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) | ||||||||||||
14-Jul-2021 | addvalex 6920 | Existence of a sum. This is dependent on how we define so once we proceed to real number axioms we will replace it with theorems such as addcl 7006. (Contributed by Jim Kingdon, 14-Jul-2021.) | ||||||||||||
13-Jul-2021 | nntopi 6968 | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) | ||||||||||||
13-Jul-2021 | ltrennb 6930 | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 13-Jul-2021.) | ||||||||||||
12-Jul-2021 | ltrenn 6931 | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 12-Jul-2021.) | ||||||||||||
11-Jul-2021 | recriota 6964 | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) | ||||||||||||
11-Jul-2021 | elrealeu 6906 | The real number mapping in elreal 6905 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) | ||||||||||||
10-Jul-2021 | axcaucvglemres 6973 | Lemma for axcaucvg 6974. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) | ||||||||||||
10-Jul-2021 | axcaucvglemval 6971 | Lemma for axcaucvg 6974. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) | ||||||||||||
10-Jul-2021 | axcaucvglemcl 6969 | Lemma for axcaucvg 6974. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) | ||||||||||||
9-Jul-2021 | axcaucvglemcau 6972 | Lemma for axcaucvg 6974. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) | ||||||||||||
9-Jul-2021 | axcaucvglemf 6970 | Lemma for axcaucvg 6974. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) | ||||||||||||
8-Jul-2021 | fldiv4p1lem1div2 9147 | The floor of an integer equal to 3 or greater than 4, increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) | ||||||||||||
8-Jul-2021 | divfl0 9138 | The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021.) | ||||||||||||
8-Jul-2021 | div4p1lem1div2 8177 | An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) | ||||||||||||
8-Jul-2021 | axcaucvg 6974 |
Real number completeness axiom. A Cauchy sequence with a modulus of
convergence converges. This is basically Corollary 11.2.13 of [HoTT],
p. (varies). The HoTT book theorem has a modulus of convergence
(that is, a rate of convergence) specified by (11.2.9) in HoTT whereas
this theorem fixes the rate of convergence to say that all terms after
the nth term must be within of the nth term (it should
later
be able to prove versions of this theorem with a different fixed rate
or a modulus of convergence supplied as a hypothesis).
Because we are stating this axiom before we have introduced notations for or division, we use for the natural numbers and express a reciprocal in terms of . This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 7004. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) | ||||||||||||
7-Jul-2021 | ltadd1sr 6861 | Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.) | ||||||||||||
7-Jul-2021 | lteupri 6715 | The difference from ltexpri 6711 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) | ||||||||||||
4-Jul-2021 | caucvgsrlemasr 6874 | Lemma for caucvgsr 6886. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.) | ||||||||||||
3-Jul-2021 | caucvgsrlemoffres 6884 | Lemma for caucvgsr 6886. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) | ||||||||||||
3-Jul-2021 | caucvgsrlemoffgt1 6883 | Lemma for caucvgsr 6886. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) | ||||||||||||
3-Jul-2021 | caucvgsrlemoffcau 6882 | Lemma for caucvgsr 6886. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) | ||||||||||||
3-Jul-2021 | caucvgsrlemofff 6881 | Lemma for caucvgsr 6886. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) | ||||||||||||
3-Jul-2021 | caucvgsrlemoffval 6880 | Lemma for caucvgsr 6886. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) | ||||||||||||
2-Jul-2021 | caucvgsrlemcl 6873 | Lemma for caucvgsr 6886. Terms of the sequence from caucvgsrlemgt1 6879 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.) | ||||||||||||
29-Jun-2021 | ledivge1le 8652 | If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.) | ||||||||||||
29-Jun-2021 | divle1le 8651 | A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.) | ||||||||||||
29-Jun-2021 | caucvgsrlemfv 6875 | Lemma for caucvgsr 6886. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) | ||||||||||||
29-Jun-2021 | prsrriota 6872 | Mapping a restricted iota from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) | ||||||||||||
29-Jun-2021 | prsrlt 6871 | Mapping from positive real ordering to signed real ordering. (Contributed by Jim Kingdon, 29-Jun-2021.) | ||||||||||||
29-Jun-2021 | prsradd 6870 | Mapping from positive real addition to signed real addition. (Contributed by Jim Kingdon, 29-Jun-2021.) | ||||||||||||
25-Jun-2021 | caucvgsrlembound 6878 | Lemma for caucvgsr 6886. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.) | ||||||||||||
25-Jun-2021 | prsrpos 6869 | Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.) | ||||||||||||
25-Jun-2021 | prsrcl 6868 | Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.) | ||||||||||||
25-Jun-2021 | srpospr 6867 | Mapping from a signed real greater than zero to a positive real. (Contributed by Jim Kingdon, 25-Jun-2021.) | ||||||||||||
23-Jun-2021 | caucvgsrlemcau 6877 | Lemma for caucvgsr 6886. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) | ||||||||||||
23-Jun-2021 | caucvgsrlemf 6876 | Lemma for caucvgsr 6886. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) | ||||||||||||
22-Jun-2021 | caucvgsrlemgt1 6879 | Lemma for caucvgsr 6886. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.) | ||||||||||||
20-Jun-2021 | caucvgsr 6886 |
A Cauchy sequence of signed reals with a modulus of convergence
converges to a signed real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies). The HoTT book
theorem has a modulus of
convergence (that is, a rate of convergence) specified by (11.2.9) in
HoTT whereas this theorem fixes the rate of convergence to say that
all terms after the nth term must be within of the nth
term
(it should later be able to prove versions of this theorem with a
different fixed rate or a modulus of convergence supplied as a
hypothesis).
This is similar to caucvgprpr 6810 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 6885). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 6881). 3. Since a signed real (element of ) which is greater than zero can be mapped to a positive real (element of ), perform that mapping on each element of the sequence and invoke caucvgprpr 6810 to get a limit (see caucvgsrlemgt1 6879). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 6879). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 6884). (Contributed by Jim Kingdon, 20-Jun-2021.) | ||||||||||||
19-Jun-2021 | 2tnp1ge0ge0 9143 | Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021.) | ||||||||||||
19-Jun-2021 | caucvgsrlembnd 6885 | Lemma for caucvgsr 6886. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.) | ||||||||||||
19-Jun-2021 | caucvgprprlemclphr 6803 | Lemma for caucvgprpr 6810. The putative limit is a positive real. Like caucvgprprlemcl 6802 but without a distinct variable constraint between and . (Contributed by Jim Kingdon, 19-Jun-2021.) | ||||||||||||
19-Jun-2021 | ltnqpr 6691 | We can order fractions via or . (Contributed by Jim Kingdon, 19-Jun-2021.) | ||||||||||||
17-Jun-2021 | caucvgprprlemnbj 6791 | Lemma for caucvgprpr 6810. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) | ||||||||||||
16-Jun-2021 | caucvgprprlemexbt 6804 | Lemma for caucvgprpr 6810. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) | ||||||||||||
16-Jun-2021 | prplnqu 6718 | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) | ||||||||||||
15-Jun-2021 | caucvgprprlemexb 6805 | Lemma for caucvgprpr 6810. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) | ||||||||||||
5-Jun-2021 | caucvgprprlemaddq 6806 | Lemma for caucvgprpr 6810. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) | ||||||||||||
27-Mar-2021 | notnotd 560 | Deduction associated with notnot 559 and notnoti 574. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) | ||||||||||||
20-Mar-2021 | subfzo0 9097 | The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021.) | ||||||||||||
..^ ..^ | ||||||||||||||
3-Mar-2021 | caucvgprprlemval 6786 | Lemma for caucvgprpr 6810. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) | ||||||||||||
27-Feb-2021 | recnnpr 6646 | The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.) | ||||||||||||
12-Feb-2021 | caucvgprprlemnjltk 6789 | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) | ||||||||||||
12-Feb-2021 | caucvgprprlemnkeqj 6788 | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) | ||||||||||||
12-Feb-2021 | caucvgprprlemnkltj 6787 | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) | ||||||||||||
12-Feb-2021 | caucvgprprlemcbv 6785 | Lemma for caucvgprpr 6810. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) | ||||||||||||
8-Feb-2021 | caucvgprprlemloccalc 6782 | Lemma for caucvgprpr 6810. Rearranging some expressions for caucvgprprlemloc 6801. (Contributed by Jim Kingdon, 8-Feb-2021.) | ||||||||||||
5-Feb-2021 | fvinim0ffz 9096 | The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.) | ||||||||||||
..^ ..^ ..^ | ||||||||||||||
28-Jan-2021 | caucvgprprlemelu 6784 | Lemma for caucvgprpr 6810. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) | ||||||||||||
21-Jan-2021 | caucvgprprlemell 6783 | Lemma for caucvgprpr 6810. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) | ||||||||||||
20-Jan-2021 | caucvgprprlemnkj 6790 | Lemma for caucvgprpr 6810. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) | ||||||||||||
8-Jan-2021 | ltnqpri 6692 | We can order fractions via or . (Contributed by Jim Kingdon, 8-Jan-2021.) | ||||||||||||
29-Dec-2020 | caucvgprprlemmu 6793 | Lemma for caucvgprpr 6810. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) | ||||||||||||
29-Dec-2020 | caucvgprprlemml 6792 | Lemma for caucvgprpr 6810. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemloc 6801 | Lemma for caucvgprpr 6810. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemdisj 6800 | Lemma for caucvgprpr 6810. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemrnd 6799 | Lemma for caucvgprpr 6810. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemupu 6798 | Lemma for caucvgprpr 6810. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemopu 6797 | Lemma for caucvgprpr 6810. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemlol 6796 | Lemma for caucvgprpr 6810. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemopl 6795 | Lemma for caucvgprpr 6810. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
21-Dec-2020 | caucvgprprlemm 6794 | Lemma for caucvgprpr 6810. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) | ||||||||||||
29-Nov-2020 | nqpru 6650 | Comparing a fraction to a real can be done by whether it is an element of the upper cut, or by . (Contributed by Jim Kingdon, 29-Nov-2020.) | ||||||||||||
28-Nov-2020 | caucvgprprlemk 6781 | Lemma for caucvgprpr 6810. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) | ||||||||||||
25-Nov-2020 | caucvgprprlem2 6808 | Lemma for caucvgprpr 6810. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) | ||||||||||||
25-Nov-2020 | caucvgprprlem1 6807 | Lemma for caucvgprpr 6810. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) | ||||||||||||
25-Nov-2020 | archrecpr 6762 | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) | ||||||||||||
21-Nov-2020 | caucvgprprlemlim 6809 | Lemma for caucvgprpr 6810. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.) | ||||||||||||
21-Nov-2020 | caucvgprprlemcl 6802 | Lemma for caucvgprpr 6810. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) | ||||||||||||
17-Nov-2020 | pm3.2 126 | Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.) | ||||||||||||
14-Nov-2020 | caucvgprpr 6810 |
A Cauchy sequence of positive reals with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a given value , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This is similar to caucvgpr 6780 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 6760) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.) | ||||||||||||
27-Oct-2020 | bj-omssonALT 10088 | Alternate proof of bj-omsson 10087. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||
27-Oct-2020 | bj-omsson 10087 | Constructive proof of omsson 4335. See also bj-omssonALT 10088. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged. | ||||||||||||
27-Oct-2020 | bj-nnelon 10084 | A natural number is an ordinal. Constructive proof of nnon 4332. Can also be proved from bj-omssonALT 10088. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) | ||||||||||||
27-Oct-2020 | bj-nnord 10083 | A natural number is an ordinal. Constructive proof of nnord 4334. Can also be proved from bj-nnelon 10084 if the latter is proved from bj-omssonALT 10088. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) | ||||||||||||
27-Oct-2020 | bj-axempty2 10014 | Axiom of the empty set from bounded separation, alternate version to bj-axempty 10013. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3883 instead. (New usage is discouraged.) | ||||||||||||
25-Oct-2020 | bj-indind 10056 | If is inductive and is "inductive in ", then is inductive. (Contributed by BJ, 25-Oct-2020.) | ||||||||||||
Ind Ind | ||||||||||||||
25-Oct-2020 | bj-axempty 10013 | Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a non-empty universe. See axnul 3882. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3883 instead. (New usage is discouraged.) | ||||||||||||
25-Oct-2020 | bj-axemptylem 10012 | Lemma for bj-axempty 10013 and bj-axempty2 10014. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3883 instead. (New usage is discouraged.) | ||||||||||||
23-Oct-2020 | caucvgprlemnkj 6764 | Lemma for caucvgpr 6780. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) | ||||||||||||
20-Oct-2020 | caucvgprlemupu 6770 | Lemma for caucvgpr 6780. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) | ||||||||||||
20-Oct-2020 | caucvgprlemopu 6769 | Lemma for caucvgpr 6780. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) | ||||||||||||
20-Oct-2020 | caucvgprlemlol 6768 | Lemma for caucvgpr 6780. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) | ||||||||||||
20-Oct-2020 | caucvgprlemopl 6767 | Lemma for caucvgpr 6780. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) | ||||||||||||
18-Oct-2020 | caucvgprlemnbj 6765 | Lemma for caucvgpr 6780. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) | ||||||||||||
9-Oct-2020 | caucvgprlemladdfu 6775 | Lemma for caucvgpr 6780. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.) | ||||||||||||
9-Oct-2020 | caucvgprlemk 6763 | Lemma for caucvgpr 6780. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) | ||||||||||||
8-Oct-2020 | caucvgprlemladdrl 6776 | Lemma for caucvgpr 6780. Adding after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.) | ||||||||||||
3-Oct-2020 | caucvgprlem2 6778 | Lemma for caucvgpr 6780. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) | ||||||||||||
3-Oct-2020 | caucvgprlem1 6777 | Lemma for caucvgpr 6780. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) | ||||||||||||
3-Oct-2020 | ltnnnq 6521 | Ordering of positive integers via or is equivalent. (Contributed by Jim Kingdon, 3-Oct-2020.) | ||||||||||||
1-Oct-2020 | caucvgprlemlim 6779 | Lemma for caucvgpr 6780. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) | ||||||||||||
27-Sep-2020 | caucvgprlemloc 6773 | Lemma for caucvgpr 6780. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) | ||||||||||||
27-Sep-2020 | caucvgprlemdisj 6772 | Lemma for caucvgpr 6780. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) | ||||||||||||
27-Sep-2020 | caucvgprlemrnd 6771 | Lemma for caucvgpr 6780. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) | ||||||||||||
27-Sep-2020 | caucvgprlemm 6766 | Lemma for caucvgpr 6780. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) | ||||||||||||
27-Sep-2020 | archrecnq 6761 | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) | ||||||||||||
26-Sep-2020 | caucvgprlemcl 6774 | Lemma for caucvgpr 6780. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) | ||||||||||||
26-Aug-2020 | sqrt0rlem 9601 | Lemma for sqrt0 9602. (Contributed by Jim Kingdon, 26-Aug-2020.) | ||||||||||||
23-Aug-2020 | sqrtrval 9598 | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) | ||||||||||||
23-Aug-2020 | df-rsqrt 9596 |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) | ||||||||||||
19-Aug-2020 | addnqpr 6659 | Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.) | ||||||||||||
19-Aug-2020 | addnqprlemfu 6658 | Lemma for addnqpr 6659. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) | ||||||||||||
19-Aug-2020 | addnqprlemfl 6657 | Lemma for addnqpr 6659. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) | ||||||||||||
19-Aug-2020 | addnqprlemru 6656 | Lemma for addnqpr 6659. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) | ||||||||||||
19-Aug-2020 | addnqprlemrl 6655 | Lemma for addnqpr 6659. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) | ||||||||||||
15-Aug-2020 | caucvgprlemcanl 6742 | Lemma for cauappcvgprlemladdrl 6755. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) | ||||||||||||
4-Aug-2020 | cauappcvgprlemupu 6747 | Lemma for cauappcvgpr 6760. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) | ||||||||||||
4-Aug-2020 | cauappcvgprlemopu 6746 | Lemma for cauappcvgpr 6760. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) | ||||||||||||
4-Aug-2020 | cauappcvgprlemlol 6745 | Lemma for cauappcvgpr 6760. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) | ||||||||||||
4-Aug-2020 | cauappcvgprlemopl 6744 | Lemma for cauappcvgpr 6760. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) | ||||||||||||
18-Jul-2020 | cauappcvgprlemloc 6750 | Lemma for cauappcvgpr 6760. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) | ||||||||||||
18-Jul-2020 | cauappcvgprlemdisj 6749 | Lemma for cauappcvgpr 6760. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) | ||||||||||||
18-Jul-2020 | cauappcvgprlemrnd 6748 | Lemma for cauappcvgpr 6760. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) | ||||||||||||
18-Jul-2020 | cauappcvgprlemm 6743 | Lemma for cauappcvgpr 6760. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) | ||||||||||||
11-Jul-2020 | cauappcvgprlemladdrl 6755 | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) | ||||||||||||
11-Jul-2020 | cauappcvgprlemladdru 6754 | Lemma for cauappcvgprlemladd 6756. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) | ||||||||||||
11-Jul-2020 | cauappcvgprlemladdfl 6753 | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) | ||||||||||||
11-Jul-2020 | cauappcvgprlemladdfu 6752 | Lemma for cauappcvgprlemladd 6756. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) | ||||||||||||
8-Jul-2020 | nqprl 6649 | Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by . (Contributed by Jim Kingdon, 8-Jul-2020.) | ||||||||||||
24-Jun-2020 | nqprlu 6645 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) | ||||||||||||
23-Jun-2020 | cauappcvgprlem2 6758 | Lemma for cauappcvgpr 6760. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) | ||||||||||||
23-Jun-2020 | cauappcvgprlem1 6757 | Lemma for cauappcvgpr 6760. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) | ||||||||||||
23-Jun-2020 | cauappcvgprlemladd 6756 | Lemma for cauappcvgpr 6760. This takes and offsets it by the positive fraction . (Contributed by Jim Kingdon, 23-Jun-2020.) | ||||||||||||
20-Jun-2020 | cauappcvgprlemlim 6759 | Lemma for cauappcvgpr 6760. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) | ||||||||||||
20-Jun-2020 | cauappcvgprlemcl 6751 | Lemma for cauappcvgpr 6760. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) | ||||||||||||
19-Jun-2020 | cauappcvgpr 6760 |
A Cauchy approximation has a limit. A Cauchy approximation, here
, is similar
to a Cauchy sequence but is indexed by the desired
tolerance (that is, how close together terms needs to be) rather than
by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p.
(varies) with a few differences such as that we are proving the
existence of a limit without anything about how fast it converges
(that is, mere existence instead of existence, in HoTT terms), and
that the codomain of is
rather than . We
also
specify that every term needs to be larger than a fraction , to
avoid the case where we have positive terms which "converge"
to zero
(which is not a positive real).
This proof (including its lemmas) is similar to the proofs of caucvgpr 6780 and caucvgprpr 6810 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) | ||||||||||||
18-Jun-2020 | caucvgpr 6780 |
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
of the nth term (it should later be able
to prove versions
of this theorem with a different fixed rate or a modulus of
convergence supplied as a hypothesis). We also specify that every
term needs to be larger than a fraction , to avoid the case
where we have positive terms which "converge" to zero (which
is not a
positive real).
This proof (including its lemmas) is similar to the proofs of cauappcvgpr 6760 and caucvgprpr 6810. Reading cauappcvgpr 6760 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) | ||||||||||||
15-Jun-2020 | imdivapd 9575 | Imaginary part of a division. Related to remul2 9473. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
15-Jun-2020 | redivapd 9574 | Real part of a division. Related to remul2 9473. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
15-Jun-2020 | cjdivapd 9568 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
# | ||||||||||||||
15-Jun-2020 | riotaexg 5472 | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) | ||||||||||||
14-Jun-2020 | cjdivapi 9535 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
14-Jun-2020 | cjdivap 9509 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
14-Jun-2020 | cjap0 9507 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
14-Jun-2020 | cjap 9506 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
14-Jun-2020 | imdivap 9481 | Imaginary part of a division. Related to immul2 9480. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
14-Jun-2020 | redivap 9474 | Real part of a division. Related to remul2 9473. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
14-Jun-2020 | mulreap 9464 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) | ||||||||||||
# | ||||||||||||||
13-Jun-2020 | sqgt0apd 9408 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) | ||||||||||||
# | ||||||||||||||
13-Jun-2020 | reexpclzapd 9405 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) | ||||||||||||
# | ||||||||||||||
13-Jun-2020 | expdivapd 9395 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) | ||||||||||||
# | ||||||||||||||
13-Jun-2020 | sqdivapd 9394 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | expsubapd 9392 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | expm1apd 9391 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | expp1zapd 9390 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | exprecapd 9389 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | expnegapd 9388 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | expap0d 9387 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
12-Jun-2020 | expclzapd 9386 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | sqrecapd 9385 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | sqgt0api 9339 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
12-Jun-2020 | sqdivapi 9337 | Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | sqgt0ap 9322 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | sqdivap 9318 | Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | expdivap 9305 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | expm1ap 9304 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | expp1zap 9303 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | expsubap 9302 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
11-Jun-2020 | expmulzap 9301 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) | ||||||||||||
# | ||||||||||||||
10-Jun-2020 | expaddzap 9299 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# | ||||||||||||||
10-Jun-2020 | expaddzaplem 9298 | Lemma for expaddzap 9299. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# | ||||||||||||||
10-Jun-2020 | exprecap 9296 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# | ||||||||||||||
10-Jun-2020 | mulexpzap 9295 | Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
10-Jun-2020 | expap0i 9287 | Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
10-Jun-2020 | expap0 9285 | Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 9286 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
10-Jun-2020 | mvllmulapd 7809 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) | ||||||||||||
# | ||||||||||||||
9-Jun-2020 | expclzap 9280 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) | ||||||||||||
# | ||||||||||||||
9-Jun-2020 | expclzaplem 9279 | Closure law for integer exponentiation. Lemma for expclzap 9280 and expap0i 9287. (Contributed by Jim Kingdon, 9-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
9-Jun-2020 | reexpclzap 9275 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) | ||||||||||||
# | ||||||||||||||
9-Jun-2020 | neg1ap0 8026 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) | ||||||||||||
# | ||||||||||||||
8-Jun-2020 | expcl2lemap 9267 | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
8-Jun-2020 | expn1ap0 9265 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) | ||||||||||||
# | ||||||||||||||
8-Jun-2020 | expineg2 9264 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) | ||||||||||||
# | ||||||||||||||
8-Jun-2020 | expnegap0 9263 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) | ||||||||||||
# | ||||||||||||||
8-Jun-2020 | expinnval 9258 | Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.) | ||||||||||||
7-Jun-2020 | expival 9257 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) | ||||||||||||
# | ||||||||||||||
7-Jun-2020 | expivallem 9256 | Lemma for expival 9257. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingdon, 7-Jun-2020.) | ||||||||||||
# # | ||||||||||||||
7-Jun-2020 | df-iexp 9255 | Define exponentiation to nonnegative integer powers. This definition is not meant to be used directly; instead, exp0 9259 and expp1 9262 provide the standard recursive definition. The up-arrow notation is used by Donald Knuth for iterated exponentiation (Science 194, 1235-1242, 1976) and is convenient for us since we don't have superscripts. 10-Jun-2005: The definition was extended to include zero exponents, so that per the convention of Definition 10-4.1 of [Gleason] p. 134. 4-Jun-2014: The definition was extended to include negative integer exponents. The case gives the value , so we will avoid this case in our theorems. (Contributed by Jim Kingdon, 7-Jun-2020.) | ||||||||||||
7-Jun-2020 | halfge0 8141 | One-half is not negative. (Contributed by AV, 7-Jun-2020.) | ||||||||||||
4-Jun-2020 | iseqfveq 9230 | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) | ||||||||||||
3-Jun-2020 | iseqfeq2 9229 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) | ||||||||||||
3-Jun-2020 | iseqfveq2 9228 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) | ||||||||||||
1-Jun-2020 | iseqcl 9223 | Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.) | ||||||||||||
1-Jun-2020 | fzdcel 8904 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) | ||||||||||||
DECID | ||||||||||||||
1-Jun-2020 | fztri3or 8903 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) | ||||||||||||
1-Jun-2020 | zdclt 8318 | Integer is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.) | ||||||||||||
DECID | ||||||||||||||
31-May-2020 | iseqp1 9225 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.) | ||||||||||||
31-May-2020 | iseq1 9222 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.) | ||||||||||||
31-May-2020 | iseqovex 9219 | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) | ||||||||||||
31-May-2020 | frecuzrdgcl 9199 | Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 9185 for the description of as the mapping from to . (Contributed by Jim Kingdon, 31-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
30-May-2020 | iseqfn 9221 | The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | iseqval 9220 | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
frec | ||||||||||||||
30-May-2020 | nfiseq 9218 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | iseqeq4 9217 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | iseqeq3 9216 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | iseqeq2 9215 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | iseqeq1 9214 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
30-May-2020 | nffrec 5982 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
frec | ||||||||||||||
30-May-2020 | freceq2 5980 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
30-May-2020 | freceq1 5979 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
29-May-2020 | df-iseq 9212 |
Define a general-purpose operation that builds a recursive sequence
(i.e. a function on the positive integers or some other upper
integer set) whose value at an index is a function of its previous value
and the value of an input sequence at that index. This definition is
complicated, but fortunately it is not intended to be used directly.
Instead, the only purpose of this definition is to provide us with an
object that has the properties expressed by iseq1 9222 and iseqp1 9225.
Typically, those are the main theorems that would be used in practice.
The first operand in the parentheses is the operation that is applied to the previous value and the value of the input sequence (second operand). The operand to the left of the parenthesis is the integer to start from. For example, for the operation , an input sequence with values 1, 1/2, 1/4, 1/8,... would be transformed into the output sequence with values 1, 3/2, 7/4, 15/8,.., so that , 3/2, etc. In other words, transforms a sequence into an infinite series. Internally, the frec function generates as its values a set of ordered pairs starting at , with the first member of each pair incremented by one in each successive value. So, the range of frec is exactly the sequence we want, and we just extract the range and throw away the domain. (Contributed by Jim Kingdon, 29-May-2020.) | ||||||||||||
frec | ||||||||||||||
28-May-2020 | frecuzrdgsuc 9201 | Successor value of a recursive definition generator on upper integers. See comment in frec2uz0d 9185 for the description of as the mapping from to . (Contributed by Jim Kingdon, 28-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
27-May-2020 | frecuzrdg0 9200 | Initial value of a recursive definition generator on upper integers. See comment in frec2uz0d 9185 for the description of as the mapping from to . (Contributed by Jim Kingdon, 27-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
27-May-2020 | frecuzrdgrrn 9194 | The function (used in the definition of the recursive definition generator on upper integers) yields ordered pairs of integers and elements of . (Contributed by Jim Kingdon, 27-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
27-May-2020 | dffun5r 4914 | A way of proving a relation is a function, analogous to mo2r 1952. (Contributed by Jim Kingdon, 27-May-2020.) | ||||||||||||
26-May-2020 | frecuzrdgfn 9198 | The recursive definition generator on upper integers is a function. See comment in frec2uz0d 9185 for the description of as the mapping from to . (Contributed by Jim Kingdon, 26-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
26-May-2020 | frecuzrdglem 9197 | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
26-May-2020 | frecuzrdgrom 9196 | The function (used in the definition of the recursive definition generator on upper integers) is a function defined for all natural numbers. (Contributed by Jim Kingdon, 26-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
25-May-2020 | divlt1lt 8650 | A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.) | ||||||||||||
25-May-2020 | freccl 5993 | Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.) | ||||||||||||
frec | ||||||||||||||
24-May-2020 | frec2uzrdg 9195 | A helper lemma for the value of a recursive definition generator on upper integers (typically either or ) with characteristic function and initial value . This lemma shows that evaluating at an element of gives an ordered pair whose first element is the index (translated from to ). See comment in frec2uz0d 9185 which describes and the index translation. (Contributed by Jim Kingdon, 24-May-2020.) | ||||||||||||
frec frec | ||||||||||||||
21-May-2020 | fzofig 9208 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) | ||||||||||||
..^ | ||||||||||||||
21-May-2020 | fzfigd 9207 | Deduction form of fzfig 9206. (Contributed by Jim Kingdon, 21-May-2020.) | ||||||||||||
19-May-2020 | fzfig 9206 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) | ||||||||||||
19-May-2020 | frechashgf1o 9205 | maps one-to-one onto . (Contributed by Jim Kingdon, 19-May-2020.) | ||||||||||||
frec | ||||||||||||||
19-May-2020 | ssfiexmid 6336 | If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.) | ||||||||||||
19-May-2020 | enm 6294 | A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.) | ||||||||||||
18-May-2020 | frecfzen2 9204 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) | ||||||||||||
frec | ||||||||||||||
18-May-2020 | frecfzennn 9203 | The cardinality of a finite set of sequential integers. (See frec2uz0d 9185 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) | ||||||||||||
frec | ||||||||||||||
17-May-2020 | frec2uzisod 9193 | (see frec2uz0d 9185) is an isomorphism from natural ordinals to upper integers. (Contributed by Jim Kingdon, 17-May-2020.) | ||||||||||||
frec | ||||||||||||||
17-May-2020 | frec2uzf1od 9192 | (see frec2uz0d 9185) is a one-to-one onto mapping. (Contributed by Jim Kingdon, 17-May-2020.) | ||||||||||||
frec | ||||||||||||||
17-May-2020 | frec2uzrand 9191 | Range of (see frec2uz0d 9185). (Contributed by Jim Kingdon, 17-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uzlt2d 9190 | The mapping (see frec2uz0d 9185) preserves order. (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uzltd 9189 | Less-than relation for (see frec2uz0d 9185). (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uzuzd 9188 | The value (see frec2uz0d 9185) at an ordinal natural number is in the upper integers. (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uzsucd 9187 | The value of (see frec2uz0d 9185) at a successor. (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uzzd 9186 | The value of (see frec2uz0d 9185) is an integer. (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
16-May-2020 | frec2uz0d 9185 | The mapping is a one-to-one mapping from onto upper integers that will be used to construct a recursive definition generator. Ordinal natural number 0 maps to complex number (normally 0 for the upper integers or 1 for the upper integers ), 1 maps to + 1, etc. This theorem shows the value of at ordinal natural number zero. (Contributed by Jim Kingdon, 16-May-2020.) | ||||||||||||
frec | ||||||||||||||
15-May-2020 | nntri3 6075 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.) | ||||||||||||
14-May-2020 | rdgifnon2 5967 | The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.) | ||||||||||||
14-May-2020 | rdgtfr 5961 | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.) | ||||||||||||
13-May-2020 | frecfnom 5986 | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) | ||||||||||||
frec | ||||||||||||||
13-May-2020 | frecabex 5984 | The class abstraction from df-frec 5978 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) | ||||||||||||
8-May-2020 | tfr0 5937 | Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.) | ||||||||||||
recs | ||||||||||||||
7-May-2020 | frec0g 5983 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) | ||||||||||||
frec | ||||||||||||||
3-May-2020 | dcned 2212 | Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.) | ||||||||||||
DECID DECID | ||||||||||||||
2-May-2020 | ax-arch 7003 |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 6965.
This axiom should not be used directly; instead use arch 8178 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) | ||||||||||||
30-Apr-2020 | ltexnqi 6507 | Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.) | ||||||||||||
26-Apr-2020 | pitonnlem1p1 6922 | Lemma for pitonn 6924. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) | ||||||||||||
26-Apr-2020 | addnqpr1 6660 | Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6659. (Contributed by Jim Kingdon, 26-Apr-2020.) | ||||||||||||
26-Apr-2020 | addpinq1 6562 | Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.) | ||||||||||||
26-Apr-2020 | nnnq 6520 | The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.) | ||||||||||||
24-Apr-2020 | pitonnlem2 6923 | Lemma for pitonn 6924. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) | ||||||||||||
24-Apr-2020 | pitonnlem1 6921 | Lemma for pitonn 6924. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) | ||||||||||||
23-Apr-2020 | archsr 6866 | For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression , is the embedding of the positive integer into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.) | ||||||||||||
23-Apr-2020 | nnprlu 6651 | The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.) | ||||||||||||
22-Apr-2020 | axarch 6965 |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined . Unless we find another way to state it,
we'll just use the right hand side of dfnn2 7916 in stating what we mean by
"natural number" in the context of this axiom.
This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7003. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) | ||||||||||||
22-Apr-2020 | pitonn 6924 | Mapping from to . (Contributed by Jim Kingdon, 22-Apr-2020.) | ||||||||||||
22-Apr-2020 | archpr 6741 | For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer is embedded into the reals as described at nnprlu 6651. (Contributed by Jim Kingdon, 22-Apr-2020.) | ||||||||||||
20-Apr-2020 | fzo0m 9047 | A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.) | ||||||||||||
..^ | ||||||||||||||
20-Apr-2020 | fzom 9020 | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) | ||||||||||||
..^ ..^ | ||||||||||||||
18-Apr-2020 | eluzdc 8547 | Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.) | ||||||||||||
DECID | ||||||||||||||
17-Apr-2020 | zlelttric 8290 | Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.) | ||||||||||||
16-Apr-2020 | fznlem 8905 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) | ||||||||||||
15-Apr-2020 | fzm 8902 | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) | ||||||||||||
15-Apr-2020 | xpdom3m 6308 | A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.) | ||||||||||||
13-Apr-2020 | snfig 6291 | A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.) | ||||||||||||
13-Apr-2020 | en1bg 6280 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.) | ||||||||||||
10-Apr-2020 | negm 8550 | The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.) | ||||||||||||
8-Apr-2020 | zleloe 8292 | Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.) | ||||||||||||
7-Apr-2020 | zdcle 8317 | Integer is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.) | ||||||||||||
DECID | ||||||||||||||
5-Apr-2020 | divge1 8649 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) | ||||||||||||
4-Apr-2020 | ioorebasg 8844 | Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.) | ||||||||||||
30-Mar-2020 | icc0r 8795 | An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.) | ||||||||||||
30-Mar-2020 | ubioog 8783 | An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) | ||||||||||||
30-Mar-2020 | lbioog 8782 | An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) | ||||||||||||
29-Mar-2020 | iooidg 8778 | An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.) | ||||||||||||
27-Mar-2020 | zletric 8289 | Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.) | ||||||||||||
26-Mar-2020 | 4z 8275 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) | ||||||||||||
25-Mar-2020 | elfzmlbm 8988 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) | ||||||||||||
25-Mar-2020 | elfz0add 8979 | An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) | ||||||||||||
25-Mar-2020 | 2eluzge0 8517 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) | ||||||||||||
23-Mar-2020 | rpnegap 8615 | Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.) | ||||||||||||
# | ||||||||||||||
23-Mar-2020 | reapltxor 7580 | Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.) | ||||||||||||
# | ||||||||||||||
22-Mar-2020 | rpcnap0 8603 | A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) | ||||||||||||
# | ||||||||||||||
22-Mar-2020 | rpreap0 8601 | A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) | ||||||||||||
# | ||||||||||||||
22-Mar-2020 | rpap0 8599 | A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) | ||||||||||||
# | ||||||||||||||
20-Mar-2020 | qapne 8574 | Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.) | ||||||||||||
# | ||||||||||||||
20-Mar-2020 | divap1d 7776 | If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
20-Mar-2020 | apmul1 7764 | Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
19-Mar-2020 | divfnzn 8556 | Division restricted to is a function. Given excluded middle, it would be easy to prove this for . The key difference is that an element of is apart from zero, whereas being an element of implies being not equal to zero. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
19-Mar-2020 | div2negapd 7780 | Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | divneg2apd 7779 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | divnegapd 7778 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | divap0bd 7777 | A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
19-Mar-2020 | diveqap0ad 7775 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7661. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | diveqap1ad 7774 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7682. Generalization of diveqap1d 7773. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | diveqap1d 7773 | Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
19-Mar-2020 | diveqap0d 7772 | If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) | ||||||||||||
# | ||||||||||||||
15-Mar-2020 | nneoor 8340 | A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.) | ||||||||||||
14-Mar-2020 | zltlen 8319 | Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7621 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | zdceq 8316 | Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
DECID | ||||||||||||||
14-Mar-2020 | zapne 8315 | Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
# | ||||||||||||||
14-Mar-2020 | zltnle 8291 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | ztri3or 8288 | Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | ztri3or0 8287 | Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | zaddcllemneg 8284 | Lemma for zaddcl 8285. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | zaddcllempos 8282 | Lemma for zaddcl 8285. Special case in which is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
14-Mar-2020 | dcne 2216 | Decidable equality expressed in terms of . Basically the same as df-dc 743. (Contributed by Jim Kingdon, 14-Mar-2020.) | ||||||||||||
DECID | ||||||||||||||
9-Mar-2020 | 2muliap0 8149 | is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | iap0 8148 | The imaginary unit is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | 2ap0 8009 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | 1ne0 7983 | . See aso 1ap0 7581. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
9-Mar-2020 | redivclapi 7755 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | redivclapzi 7754 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | rerecclapi 7753 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | rerecclapzi 7752 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | divdivdivapi 7751 | Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
9-Mar-2020 | divadddivapi 7750 | Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
9-Mar-2020 | divmul13api 7749 | Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
9-Mar-2020 | divmuldivapi 7748 | Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
9-Mar-2020 | div11api 7747 | One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | div23api 7746 | A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | divdirapi 7745 | Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
9-Mar-2020 | divassapi 7744 | An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) | ||||||||||||
# | ||||||||||||||
8-Mar-2020 | nnap0 7943 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# | ||||||||||||||
8-Mar-2020 | divdivap2d 7797 | Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | divdivap1d 7796 | Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | dmdcanap2d 7795 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | dmdcanapd 7794 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | divcanap7d 7793 | Cancel equal divisors in a division. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | divcanap5rd 7792 | Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | divcanap5d 7791 | Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | divdiv32apd 7790 | Swap denominators in a division. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
8-Mar-2020 | div13apd 7789 | A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# | ||||||||||||||
8-Mar-2020 | div32apd 7788 | A commutative/associative law for division. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# | ||||||||||||||
8-Mar-2020 | divmulapd 7787 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) | ||||||||||||
# | ||||||||||||||
7-Mar-2020 | nn1gt1 7947 | A positive integer is either one or greater than one. This is for ; 0elnn 4340 is a similar theorem for (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) | ||||||||||||
5-Mar-2020 | crap0 7910 | The real representation of complex numbers is apart from zero iff one of its terms is apart from zero. (Contributed by Jim Kingdon, 5-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
3-Mar-2020 | rec11apd 7786 | Reciprocal is one-to-one. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | ddcanapd 7785 | Cancellation in a double division. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | divcanap6d 7784 | Cancellation of inverted fractions. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | recdivap2d 7783 | Division into a reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | recdivapd 7782 | The reciprocal of a ratio. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | divap0d 7781 | The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # # | ||||||||||||||
3-Mar-2020 | div0apd 7763 | Division into zero is zero. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
3-Mar-2020 | dividapd 7762 | A number divided by itself is one. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
3-Mar-2020 | recrecapd 7761 | A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
3-Mar-2020 | recidap2d 7760 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
3-Mar-2020 | recidapd 7759 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
3-Mar-2020 | recap0d 7758 | The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# # | ||||||||||||||
3-Mar-2020 | recclapd 7757 | Closure law for reciprocal. (Contributed by Jim Kingdon, 3-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | div11apd 7805 | One-to-one relationship for division. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | divsubdirapd 7804 | Distribution of division over subtraction. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | divdirapd 7803 | Distribution of division over addition. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | div23apd 7802 | A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | div12apd 7801 | A commutative/associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | divassapd 7800 | An associative law for division. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | divmulap3d 7799 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
2-Mar-2020 | divmulap2d 7798 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 2-Mar-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | prodgt0gt0 7817 | Infer that a multiplicand is positive from a positive multiplier and positive product. See prodgt0 7818 for the same theorem with replaced by the weaker condition . (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
29-Feb-2020 | redivclapd 7808 | Closure law for division of reals. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | rerecclapd 7807 | Closure law for reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divcanap4d 7771 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divcanap3d 7770 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divrecap2d 7769 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divrecapd 7768 | Relationship between division and reciprocal. Theorem I.9 of [Apostol] p. 18. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divcanap2d 7767 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divcanap1d 7766 | A cancellation law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divclapd 7765 | Closure law for division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
29-Feb-2020 | divdiv32api 7743 | Swap denominators in a division. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
29-Feb-2020 | divmulapi 7742 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 29-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divdiv23apzi 7741 | Swap denominators in a division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
28-Feb-2020 | divdirapzi 7740 | Distribution of division over addition. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divmulapzi 7739 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divassapzi 7738 | An associative law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | rec11apii 7737 | Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
28-Feb-2020 | divap0i 7736 | The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
28-Feb-2020 | divcanap4i 7735 | A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divcanap3i 7734 | A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divrecapi 7733 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divcanap1i 7732 | A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divcanap2i 7731 | A cancellation law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | divclapi 7730 | Closure law for division. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
28-Feb-2020 | rec11api 7729 | Reciprocal is one-to-one. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
28-Feb-2020 | ltleap 7621 | Less than in terms of non-strict order and apartness. (Contributed by Jim Kingdon, 28-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divcanap4zi 7728 | A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divcanap3zi 7727 | A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divrecapzi 7726 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divcanap2zi 7725 | A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divcanap1zi 7724 | A cancellation law for division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divclapzi 7723 | Closure law for division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | recidapzi 7715 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | recap0apzi 7714 | The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
27-Feb-2020 | recclapzi 7713 | Closure law for reciprocal. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | divneg2ap 7712 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | div2negap 7711 | Quotient of two negatives. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | negap0 7620 | A number is apart from zero iff its negative is apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
27-Feb-2020 | gt0ap0d 7619 | Positive implies apart from zero. Because of the way we define #, must be an element of , not just . (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | gt0ap0ii 7618 | Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | gt0ap0i 7617 | Positive means apart from zero (useful for ordering theorems involving division). (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
27-Feb-2020 | gt0ap0 7616 | Positive implies apart from zero. (Contributed by Jim Kingdon, 27-Feb-2020.) | ||||||||||||
# | ||||||||||||||
26-Feb-2020 | 2times 8038 | Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) | ||||||||||||
26-Feb-2020 | redivclap 7707 | Closure law for division of reals. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# | ||||||||||||||
26-Feb-2020 | rerecclap 7706 | Closure law for reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# | ||||||||||||||
26-Feb-2020 | conjmulap 7705 | Two numbers whose reciprocals sum to 1 are called "conjugates" and satisfy this relationship. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divsubdivap 7704 | Subtraction of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divadddivap 7703 | Addition of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | ddcanap 7702 | Cancellation in a double division. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | recdivap2 7701 | Division into a reciprocal. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divdivap2 7700 | Division by a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divdivap1 7699 | Division into a fraction. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | dmdcanap 7698 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divcanap7 7697 | Cancel equal divisors in a division. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divdiv32ap 7696 | Swap denominators in a division. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divcanap6 7695 | Cancellation of inverted fractions. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | recdivap 7694 | The reciprocal of a ratio. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divmuleqap 7693 | Cross-multiply in an equality of ratios. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divmul24ap 7692 | Swap the numerators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
26-Feb-2020 | divmul13ap 7691 | Swap the denominators in the product of two ratios. (Contributed by Jim Kingdon, 26-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
25-Feb-2020 | divcanap5 7690 | Cancellation of common factor in a ratio. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
25-Feb-2020 | divdivdivap 7689 | Division of two ratios. Theorem I.15 of [Apostol] p. 18. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
25-Feb-2020 | divmuldivap 7688 | Multiplication of two ratios. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
25-Feb-2020 | rec11rap 7687 | Mutual reciprocals. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
25-Feb-2020 | rec11ap 7686 | Reciprocal is one-to-one. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
25-Feb-2020 | recrecap 7685 | A number is equal to the reciprocal of its reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divnegap 7683 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | diveqap1 7682 | Equality in terms of unit ratio. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div0ap 7679 | Division into zero is zero. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | dividap 7678 | A number divided by itself is one. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div11ap 7677 | One-to-one relationship for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divcanap4 7676 | A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divcanap3 7675 | A cancellation law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divdirap 7674 | Distribution of division over addition. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div12ap 7673 | A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div13ap 7672 | A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div32ap 7671 | A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | div23ap 7670 | A commutative/associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divassap 7669 | An associative law for division. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
25-Feb-2020 | divrecap2 7668 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 25-Feb-2020.) | ||||||||||||
# | ||||||||||||||
24-Feb-2020 | conventions 9892 |
Unless there is a reason to diverge, we follow the conventions of
the Metamath Proof Explorer (aka "set.mm"). This list of
conventions is intended to be read in conjunction with the
corresponding conventions in the Metamath Proof Explorer, and
only the differences are described below.
Label naming conventions Here are a few of the label naming conventions:
The following table shows some commonly-used abbreviations in labels which are not found in the Metamath Proof Explorer, in alphabetical order. For each abbreviation we provide a mnenomic to help you remember it, the source theorem/assumption defining it, an expression showing what it looks like, whether or not it is a "syntax fragment" (an abbreviation that indicates a particular kind of syntax), and hyperlinks to label examples that use the abbreviation. The abbreviation is bolded if there is a df-NAME definition but the label fragment is not NAME.
(Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
24-Feb-2020 | divrecap 7667 | Relationship between division and reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# | ||||||||||||||
24-Feb-2020 | recidap2 7666 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# | ||||||||||||||
24-Feb-2020 | recidap 7665 | Multiplication of a number and its reciprocal. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# | ||||||||||||||
24-Feb-2020 | recap0 7664 | The reciprocal of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
24-Feb-2020 | mulap0bbd 7641 | A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7639 and consequence of mulap0bd 7638. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
24-Feb-2020 | mulap0bad 7640 | A factor of a complex number apart from zero is apart from zero. Partial converse of mulap0d 7639 and consequence of mulap0bd 7638. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
24-Feb-2020 | mulap0bd 7638 | The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
24-Feb-2020 | mulap0b 7636 | The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
24-Feb-2020 | mulap0r 7606 | A product apart from zero. Lemma 2.13 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
24-Feb-2020 | 1ap0 7581 | One is apart from zero. (Contributed by Jim Kingdon, 24-Feb-2020.) | ||||||||||||
# | ||||||||||||||
23-Feb-2020 | mulap0d 7639 | The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
23-Feb-2020 | mulap0i 7637 | The product of two numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 23-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
23-Feb-2020 | mulext 7605 | Strong extensionality for multiplication. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5521. For us, it is proved a different way. (Contributed by Jim Kingdon, 23-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
23-Feb-2020 | mulreim 7595 | Complex multiplication in terms of real and imaginary parts. (Contributed by Jim Kingdon, 23-Feb-2020.) | ||||||||||||
22-Feb-2020 | divap0 7663 | The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
22-Feb-2020 | divap0b 7662 | The ratio of numbers apart from zero is apart from zero. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
22-Feb-2020 | diveqap0 7661 | A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divcanap1 7660 | A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divcanap2 7659 | A cancellation law for division. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | recclap 7658 | Closure law for reciprocal. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divclap 7657 | Closure law for division. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divmulap3 7656 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divmulap2 7655 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | divmulap 7654 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# | ||||||||||||||
22-Feb-2020 | mulap0 7635 | The product of two numbers apart from zero is apart from zero. Lemma 2.15 of [Geuvers], p. 6. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
22-Feb-2020 | mulext2 7604 | Right extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
22-Feb-2020 | mulext1 7603 | Left extensionality for complex multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
22-Feb-2020 | remulext2 7591 | Right extensionality for real multiplication. (Contributed by Jim Kingdon, 22-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
21-Feb-2020 | divvalap 7653 | Value of division: the (unique) element such that . This is meaningful only when is apart from zero. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | receuap 7650 | Existential uniqueness of reciprocals. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanapi 7648 | Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanap2 7647 | Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanap 7646 | Cancellation law for multiplication (full theorem form). (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanap2ad 7645 | Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcanap2d 7643. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanapad 7644 | Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcanapd 7642. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanap2d 7643 | Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | mulcanapd 7642 | Cancellation law for multiplication. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | apne 7614 | Apartness implies negated equality. We cannot in general prove the converse, which is the whole point of having separate notations for apartness and negated equality. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
21-Feb-2020 | apti 7613 | Complex apartness is tight. (Contributed by Jim Kingdon, 21-Feb-2020.) | ||||||||||||
# | ||||||||||||||
20-Feb-2020 | recexap 7634 | Existence of reciprocal of nonzero complex number. (Contributed by Jim Kingdon, 20-Feb-2020.) | ||||||||||||
# | ||||||||||||||
20-Feb-2020 | recexaplem2 7633 | Lemma for recexap 7634. (Contributed by Jim Kingdon, 20-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
19-Feb-2020 | remulext1 7590 | Left extensionality for multiplication. (Contributed by Jim Kingdon, 19-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
18-Feb-2020 | ax-pre-mulext 7002 |
Strong extensionality of multiplication (expressed in terms of ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 6962
(Contributed by Jim Kingdon, 18-Feb-2020.) | ||||||||||||
18-Feb-2020 | axpre-mulext 6962 |
Strong extensionality of multiplication (expressed in terms of
).
Axiom for real and complex numbers, derived from set theory.
This construction-dependent theorem should not be referenced directly;
instead, use ax-pre-mulext 7002.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) | ||||||||||||
18-Feb-2020 | mulextsr1 6865 | Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.) | ||||||||||||
18-Feb-2020 | ltmprr 6740 | Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.) | ||||||||||||
17-Feb-2020 | mulextsr1lem 6864 | Lemma for mulextsr1 6865. (Contributed by Jim Kingdon, 17-Feb-2020.) | ||||||||||||
17-Feb-2020 | addextpr 6719 | Strong extensionality of addition (ordering version). This is similar to addext 7601 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.) | ||||||||||||
16-Feb-2020 | apadd2 7600 | Addition respects apartness. (Contributed by Jim Kingdon, 16-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
16-Feb-2020 | apcotr 7598 | Apartness is cotransitive. (Contributed by Jim Kingdon, 16-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
16-Feb-2020 | apsym 7597 | Apartness is symmetric. This theorem for real numbers is part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
16-Feb-2020 | apirr 7596 | Apartness is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2020.) | ||||||||||||
# | ||||||||||||||
16-Feb-2020 | reapcotr 7589 | Real apartness is cotransitive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
15-Feb-2020 | addext 7601 | Strong extensionality for addition. Given excluded middle, apartness would be equivalent to negated equality and this would follow readily (for all operations) from oveq12 5521. For us, it is proved a different way. (Contributed by Jim Kingdon, 15-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
14-Feb-2020 | apneg 7602 | Negation respects apartness. (Contributed by Jim Kingdon, 14-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
13-Feb-2020 | apadd1 7599 | Addition respects apartness. Analogue of addcan 7191 for apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
13-Feb-2020 | reapneg 7588 | Real negation respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
13-Feb-2020 | reapadd1 7587 | Real addition respects apartness. (Contributed by Jim Kingdon, 13-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
12-Feb-2020 | apreim 7594 | Complex apartness in terms of real and imaginary parts. (Contributed by Jim Kingdon, 12-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
8-Feb-2020 | reapmul1 7586 | Multiplication of both sides of real apartness by a real number apart from zero. Special case of apmul1 7764. (Contributed by Jim Kingdon, 8-Feb-2020.) | ||||||||||||
# # # | ||||||||||||||
8-Feb-2020 | reapmul1lem 7585 | Lemma for reapmul1 7586. (Contributed by Jim Kingdon, 8-Feb-2020.) | ||||||||||||
# # | ||||||||||||||
7-Feb-2020 | apsqgt0 7592 | The square of a real number apart from zero is positive. (Contributed by Jim Kingdon, 7-Feb-2020.) | ||||||||||||
# | ||||||||||||||
6-Feb-2020 | recexgt0 7571 | Existence of reciprocal of positive real number. (Contributed by Jim Kingdon, 6-Feb-2020.) | ||||||||||||
6-Feb-2020 | ax-precex 6994 | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6954. (Contributed by Jim Kingdon, 6-Feb-2020.) | ||||||||||||
6-Feb-2020 | axprecex 6954 |
Existence of positive reciprocal of positive real number. Axiom for
real and complex numbers, derived from set theory. This
construction-dependent theorem should not be referenced directly;
instead, use ax-precex 6994.
In treatments which assume excluded middle, the condition is generally replaced by , and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.) | ||||||||||||
6-Feb-2020 | recexgt0sr 6858 | The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) | ||||||||||||
1-Feb-2020 | reaplt 7579 | Real apartness in terms of less than. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 1-Feb-2020.) | ||||||||||||
# | ||||||||||||||
31-Jan-2020 | apreap 7578 | Complex apartness and real apartness agree on the real numbers. (Contributed by Jim Kingdon, 31-Jan-2020.) | ||||||||||||
# #ℝ | ||||||||||||||
30-Jan-2020 | rereim 7577 | Decomposition of a real number into real part (itself) and imaginary part (zero). (Contributed by Jim Kingdon, 30-Jan-2020.) | ||||||||||||
30-Jan-2020 | reapti 7570 | Real apartness is tight. Beyond the development of apartness itself, proofs should use apti 7613. (Contributed by Jim Kingdon, 30-Jan-2020.) (New usage is discouraged.) | ||||||||||||
#ℝ | ||||||||||||||
29-Jan-2020 | recexre 7569 | Existence of reciprocal of real number. (Contributed by Jim Kingdon, 29-Jan-2020.) | ||||||||||||
#ℝ | ||||||||||||||
29-Jan-2020 | reapval 7567 | Real apartness in terms of classes. Beyond the development of # itself, proofs should use reaplt 7579 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 29-Jan-2020.) | ||||||||||||
#ℝ | ||||||||||||||
29-Jan-2020 | axapti 7090 | Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 6999 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.) | ||||||||||||
29-Jan-2020 | ax-pre-apti 6999 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6959. (Contributed by Jim Kingdon, 29-Jan-2020.) | ||||||||||||
29-Jan-2020 | axpre-apti 6959 |
Apartness of reals is tight. Axiom for real and complex numbers,
derived from set theory. This construction-dependent theorem should not
be referenced directly; instead, use ax-pre-apti 6999.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) | ||||||||||||
29-Jan-2020 | aptisr 6863 | Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.) | ||||||||||||
28-Jan-2020 | aptipr 6739 | Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.) | ||||||||||||
28-Jan-2020 | aptiprlemu 6738 | Lemma for aptipr 6739. (Contributed by Jim Kingdon, 28-Jan-2020.) | ||||||||||||
28-Jan-2020 | aptiprleml 6737 | Lemma for aptipr 6739. (Contributed by Jim Kingdon, 28-Jan-2020.) | ||||||||||||
27-Jan-2020 | bj-dcbi 10048 | Equivalence property for DECID. TODO: solve conflict with dcbi 844; minimize dcbii 747 and dcbid 748 with it, as well as theorems using those. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) | ||||||||||||
DECID DECID | ||||||||||||||
27-Jan-2020 | bj-notbid 10047 | Deduction form of bj-notbi 10045. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) | ||||||||||||
27-Jan-2020 | bj-notbii 10046 | Inference associated with bj-notbi 10045. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) | ||||||||||||
27-Jan-2020 | bj-notbi 10045 | Equivalence property for negation. TODO: minimize all theorems using notbid 592 and notbii 594. (Contributed by BJ, 27-Jan-2020.) (Proof modification is discouraged.) | ||||||||||||
26-Jan-2020 | df-ap 7573 |
Define complex apartness. Definition 6.1 of [Geuvers], p. 17.
Two numbers are considered apart if it is possible to separate them. One common usage is that we can divide by a number if it is apart from zero (see for example recclap 7658 which says that a number apart from zero has a reciprocal). The defining characteristics of an apartness are irreflexivity (apirr 7596), symmetry (apsym 7597), and cotransitivity (apcotr 7598). Apartness implies negated equality, as seen at apne 7614, and the converse would also follow if we assumed excluded middle. In addition, apartness of complex numbers is tight, which means that two numbers which are not apart are equal (apti 7613). (Contributed by Jim Kingdon, 26-Jan-2020.) | ||||||||||||
# #ℝ #ℝ | ||||||||||||||
26-Jan-2020 | reapirr 7568 | Real apartness is irreflexive. Part of Definition 11.2.7(v) of [HoTT], p. (varies). Beyond the development of # itself, proofs should use apirr 7596 instead. (Contributed by Jim Kingdon, 26-Jan-2020.) | ||||||||||||
#ℝ | ||||||||||||||
26-Jan-2020 | df-reap 7566 | Define real apartness. Definition in Section 11.2.1 of [HoTT], p. (varies). Although #ℝ is an apartness relation on the reals (see df-ap 7573 for more discussion of apartness relations), for our purposes it is just a stepping stone to defining # which is an apartness relation on complex numbers. On the reals, #ℝ and # agree (apreap 7578). (Contributed by Jim Kingdon, 26-Jan-2020.) | ||||||||||||
#ℝ | ||||||||||||||
26-Jan-2020 | gt0add 7564 | A positive sum must have a positive addend. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by Jim Kingdon, 26-Jan-2020.) | ||||||||||||
17-Jan-2020 | addcom 7150 | Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.) | ||||||||||||
17-Jan-2020 | ax-addcom 6984 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6944. Proofs should normally use addcom 7150 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) | ||||||||||||
17-Jan-2020 | axaddcom 6944 |
Addition commutes. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 6984 be used later.
Instead, use addcom 7150.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) | ||||||||||||
16-Jan-2020 | addid1 7151 | is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.) | ||||||||||||
16-Jan-2020 | ax-0id 6992 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 6952.
Proofs should normally use addid1 7151 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) | ||||||||||||
16-Jan-2020 | ax0id 6952 |
is an identity element
for real addition. Axiom for real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-0id 6992.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.) | ||||||||||||
15-Jan-2020 | axltwlin 7087 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6997 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) | ||||||||||||
15-Jan-2020 | axltirr 7086 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6996 with ordering on the extended reals. New proofs should use ltnr 7095 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) | ||||||||||||
14-Jan-2020 | 2pwuninelg 5898 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.) | ||||||||||||
13-Jan-2020 | 1re 7026 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) | ||||||||||||
13-Jan-2020 | ax-1re 6978 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6938. Proofs should use 1re 7026 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) | ||||||||||||
13-Jan-2020 | ax1re 6938 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 6978.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6977 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) | ||||||||||||
12-Jan-2020 | ax-pre-ltwlin 6997 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6957. (Contributed by Jim Kingdon, 12-Jan-2020.) | ||||||||||||
12-Jan-2020 | ax-pre-ltirr 6996 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6996. (Contributed by Jim Kingdon, 12-Jan-2020.) | ||||||||||||
12-Jan-2020 | ax-0lt1 6990 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6950. Proofs should normally use 0lt1 7141 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) | ||||||||||||
12-Jan-2020 | axpre-ltwlin 6957 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6997. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) | ||||||||||||
12-Jan-2020 | axpre-ltirr 6956 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6996. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) | ||||||||||||
12-Jan-2020 | ax0lt1 6950 |
0 is less than 1. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-0lt1 6990.
The version of this axiom in the Metamath Proof Explorer reads ; here we change it to . The proof of from in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) | ||||||||||||
8-Jan-2020 | ecidg 6170 | A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.) | ||||||||||||
5-Jan-2020 | elfzom1elp1fzo 9058 | Membership of an integer incremented by one in a half-open range of nonnegative integers. (Contributed by Alexander van der Vekens, 24-Jun-2018.) (Proof shortened by AV, 5-Jan-2020.) | ||||||||||||
..^ ..^ | ||||||||||||||
5-Jan-2020 | 1idsr 6853 | 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.) | ||||||||||||
4-Jan-2020 | nn0ge2m1nn 8242 | If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.) | ||||||||||||
4-Jan-2020 | distrsrg 6844 | Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.) | ||||||||||||
3-Jan-2020 | mulasssrg 6843 | Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.) | ||||||||||||
3-Jan-2020 | mulcomsrg 6842 | Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.) | ||||||||||||
3-Jan-2020 | addasssrg 6841 | Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.) | ||||||||||||
3-Jan-2020 | addcomsrg 6840 | Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.) | ||||||||||||
3-Jan-2020 | caovlem2d 5693 | Rearrangement of expression involving multiplication () and addition (). (Contributed by Jim Kingdon, 3-Jan-2020.) | ||||||||||||
2-Jan-2020 | bj-d0clsepcl 10049 | Δ0-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) | ||||||||||||
DECID | ||||||||||||||
2-Jan-2020 | ax-bj-d0cl 10044 | Axiom for Δ0-classical logic. (Contributed by BJ, 2-Jan-2020.) | ||||||||||||
BOUNDED DECID | ||||||||||||||
1-Jan-2020 | mulcmpblnrlemg 6825 | Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.) | ||||||||||||
31-Dec-2019 | eceq1d 6142 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) | ||||||||||||
30-Dec-2019 | mulsrmo 6829 | There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) | ||||||||||||
30-Dec-2019 | addsrmo 6828 | There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) | ||||||||||||
30-Dec-2019 | prsrlem1 6827 | Decomposing signed reals into positive reals. Lemma for addsrpr 6830 and mulsrpr 6831. (Contributed by Jim Kingdon, 30-Dec-2019.) | ||||||||||||
29-Dec-2019 | bj-omelon 10086 | The set is an ordinal. Constructive proof of omelon 4331. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
29-Dec-2019 | bj-omord 10085 | The set is an ordinal. Constructive proof of ordom 4329. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
29-Dec-2019 | bj-omtrans2 10082 | The set is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
29-Dec-2019 | bj-omtrans 10081 |
The set is
transitive. A natural number is included in
.
Constructive proof of elnn 4328.
The idea is to use bounded induction with the formula . This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
29-Dec-2019 | ltrnqg 6518 | Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6519. (Contributed by Jim Kingdon, 29-Dec-2019.) | ||||||||||||
29-Dec-2019 | rec1nq 6493 | Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.) | ||||||||||||
28-Dec-2019 | recexprlemupu 6726 | The upper cut of is upper. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | recexprlemopu 6725 | The upper cut of is open. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | recexprlemlol 6724 | The lower cut of is lower. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | recexprlemopl 6723 | The lower cut of is open. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | prmuloc2 6665 | Positive reals are multiplicatively located. This is a variation of prmuloc 6664 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio , there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | 1pru 6654 | The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
28-Dec-2019 | 1prl 6653 | The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemex 6735 | is the reciprocal of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemss1u 6734 | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemss1l 6733 | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlem1ssu 6732 | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlem1ssl 6731 | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlempr 6730 | is a positive real. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemloc 6729 | is located. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemdisj 6728 | is disjoint. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemrnd 6727 | is rounded. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemm 6722 | is inhabited. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemelu 6721 | Membership in the upper cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
27-Dec-2019 | recexprlemell 6720 | Membership in the lower cut of . Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.) | ||||||||||||
26-Dec-2019 | ltaprg 6717 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.) | ||||||||||||
26-Dec-2019 | prarloc2 6602 | A Dedekind cut is arithmetically located. This is a variation of prarloc 6601 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance , there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.) | ||||||||||||
25-Dec-2019 | addcanprlemu 6713 | Lemma for addcanprg 6714. (Contributed by Jim Kingdon, 25-Dec-2019.) | ||||||||||||
25-Dec-2019 | addcanprleml 6712 | Lemma for addcanprg 6714. (Contributed by Jim Kingdon, 25-Dec-2019.) | ||||||||||||
24-Dec-2019 | addcanprg 6714 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) | ||||||||||||
23-Dec-2019 | ltprordil 6687 | If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.) | ||||||||||||
22-Dec-2019 | bj-findis 10104 | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 10072 for a bounded version not requiring ax-setind 4262. See finds 4323 for a proof in IZF. From this version, it is easy to prove of finds 4323, finds2 4324, finds1 4325. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
21-Dec-2019 | ltexprlemupu 6702 | The upper cut of our constructed difference is upper. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
21-Dec-2019 | ltexprlemopu 6701 | The upper cut of our constructed difference is open. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
21-Dec-2019 | ltexprlemlol 6700 | The lower cut of our constructed difference is lower. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
21-Dec-2019 | ltexprlemopl 6699 | The lower cut of our constructed difference is open. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
21-Dec-2019 | ltexprlemelu 6697 | Element in upper cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
21-Dec-2019 | ltexprlemell 6696 | Element in lower cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemru 6710 | Lemma for ltexpri 6711. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemfu 6709 | Lemma for ltexpri 6711. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemrl 6708 | Lemma for ltexpri 6711. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemfl 6707 | Lemma for ltexpri 6711. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlempr 6706 | Our constructed difference is a positive real. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemloc 6705 | Our constructed difference is located. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemdisj 6704 | Our constructed difference is disjoint. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemrnd 6703 | Our constructed difference is rounded. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
17-Dec-2019 | ltexprlemm 6698 | Our constructed difference is inhabited. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.) | ||||||||||||
16-Dec-2019 | bj-sbime 9913 | A strengthening of sbie 1674 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
16-Dec-2019 | bj-sbimeh 9912 | A strengthening of sbieh 1673 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
16-Dec-2019 | bj-sbimedh 9911 | A strengthening of sbiedh 1670 (same proof). (Contributed by BJ, 16-Dec-2019.) | ||||||||||||
16-Dec-2019 | ltsopr 6694 | Positive real 'less than' is a weak linear order (in the sense of df-iso 4034). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.) | ||||||||||||
15-Dec-2019 | ltpopr 6693 | Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6694. (Contributed by Jim Kingdon, 15-Dec-2019.) | ||||||||||||
15-Dec-2019 | ltdfpr 6604 | More convenient form of df-iltp 6568. (Contributed by Jim Kingdon, 15-Dec-2019.) | ||||||||||||
15-Dec-2019 | prdisj 6590 | A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.) | ||||||||||||
13-Dec-2019 | 1idpru 6689 | Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.) | ||||||||||||
13-Dec-2019 | 1idprl 6688 | Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.) | ||||||||||||
13-Dec-2019 | gtnqex 6648 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) | ||||||||||||
13-Dec-2019 | ltnqex 6647 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) | ||||||||||||
13-Dec-2019 | sotritrieq 4062 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrprg 6686 | Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem5pru 6685 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem5prl 6684 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem4pru 6683 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem4prl 6682 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem1pru 6681 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | distrlem1prl 6680 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
12-Dec-2019 | ltdcnq 6495 | Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
DECID | ||||||||||||||
12-Dec-2019 | ltdcpi 6421 | Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) | ||||||||||||
DECID | ||||||||||||||
11-Dec-2019 | sublt0d 7561 | When a subtraction gives a negative result. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | mulassprg 6679 | Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | mulcomprg 6678 | Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | addassprg 6677 | Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | addcomprg 6676 | Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | genpassg 6624 | Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | genpassu 6623 | Associativity of upper cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | genpassl 6622 | Associativity of lower cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | preqlu 6570 | Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | fssd 5055 | Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | iffalsed 3341 | Value of the conditional operator when its first argument is false. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | iftrued 3338 | Value of the conditional operator when its first argument is true. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | neneq 2227 | From inequality to non equality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
11-Dec-2019 | neqne 2214 | From non equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.) | ||||||||||||
10-Dec-2019 | mullocprlem 6668 | Calculations for mullocpr 6669. (Contributed by Jim Kingdon, 10-Dec-2019.) | ||||||||||||
10-Dec-2019 | mulnqpru 6667 | Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) | ||||||||||||
10-Dec-2019 | mulnqprl 6666 | Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) | ||||||||||||
9-Dec-2019 | prmuloclemcalc 6663 | Calculations for prmuloc 6664. (Contributed by Jim Kingdon, 9-Dec-2019.) | ||||||||||||
9-Dec-2019 | appdiv0nq 6662 | Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6661 in which is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.) | ||||||||||||
9-Dec-2019 | ltmnqi 6501 | Ordering property of multiplication for positive fractions. One direction of ltmnqg 6499. (Contributed by Jim Kingdon, 9-Dec-2019.) | ||||||||||||
9-Dec-2019 | ltanqi 6500 | Ordering property of addition for positive fractions. One direction of ltanqg 6498. (Contributed by Jim Kingdon, 9-Dec-2019.) | ||||||||||||
8-Dec-2019 | bj-nn0sucALT 10103 | Alternate proof of bj-nn0suc 10089, also constructive but from ax-inf2 10101, hence requiring ax-bdsetind 10093. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||
8-Dec-2019 | bj-omex2 10102 | Using bounded set induction and the strong axiom of infinity, is a set, that is, we recover ax-infvn 10066 (see bj-2inf 10062 for the equivalence of the latter with bj-omex 10067). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) | ||||||||||||
8-Dec-2019 | bj-inf2vn2 10100 | A sufficient condition for to be a set; unbounded version of bj-inf2vn 10099. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
8-Dec-2019 | bj-inf2vn 10099 | A sufficient condition for to be a set. See bj-inf2vn2 10100 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
8-Dec-2019 | bj-inf2vnlem4 10098 | Lemma for bj-inf2vn2 10100. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind | ||||||||||||||
8-Dec-2019 | bj-inf2vnlem3 10097 | Lemma for bj-inf2vn 10099. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED BOUNDED Ind | ||||||||||||||
8-Dec-2019 | bj-inf2vnlem2 10096 | Lemma for bj-inf2vnlem3 10097 and bj-inf2vnlem4 10098. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind | ||||||||||||||
8-Dec-2019 | bj-inf2vnlem1 10095 | Lemma for bj-inf2vn 10099. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind | ||||||||||||||
8-Dec-2019 | bj-bdcel 9957 | Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.) | ||||||||||||
BOUNDED BOUNDED | ||||||||||||||
8-Dec-2019 | bj-ex 9902 | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1489 and 19.9ht 1532 or 19.23ht 1386). (Proof modification is discouraged.) | ||||||||||||
8-Dec-2019 | mullocpr 6669 | Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both and are positive, not just ). (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | prmuloc 6664 | Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | appdivnq 6661 | Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where and are positive, as well as ). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | nqprxx 6644 | The canonical embedding of the rationals into the reals, expressed with the same variable for the lower and upper cuts. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | nqprloc 6643 | A cut produced from a rational is located. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | nqprdisj 6642 | A cut produced from a rational is disjoint. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | nqprrnd 6641 | A cut produced from a rational is rounded. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | nqprm 6640 | A cut produced from a rational is inhabited. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | mpvlu 6637 | Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
8-Dec-2019 | plpvlu 6636 | Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) | ||||||||||||
7-Dec-2019 | addlocprlemeqgt 6630 | Lemma for addlocpr 6634. This is a step used in both the and cases. (Contributed by Jim Kingdon, 7-Dec-2019.) | ||||||||||||
7-Dec-2019 | addnqprulem 6626 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) | ||||||||||||
7-Dec-2019 | addnqprllem 6625 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) | ||||||||||||
7-Dec-2019 | lt2addnq 6502 | Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.) | ||||||||||||
6-Dec-2019 | addlocprlem 6633 | Lemma for addlocpr 6634. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.) | ||||||||||||
6-Dec-2019 | addlocprlemgt 6632 | Lemma for addlocpr 6634. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) | ||||||||||||
6-Dec-2019 | addlocprlemeq 6631 | Lemma for addlocpr 6634. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) | ||||||||||||
6-Dec-2019 | addlocprlemlt 6629 | Lemma for addlocpr 6634. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) | ||||||||||||
5-Dec-2019 | addlocpr 6634 | Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6601 to both and , and uses nqtri3or 6494 rather than prloc 6589 to decide whether is too big to be in the lower cut of (and deduce that if it is, then must be in the upper cut). What the two proofs have in common is that they take the difference between and to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.) | ||||||||||||
5-Dec-2019 | addnqpru 6628 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) | ||||||||||||
5-Dec-2019 | addnqprl 6627 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) | ||||||||||||
5-Dec-2019 | genpmu 6616 | The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.) | ||||||||||||
5-Dec-2019 | genpelxp 6609 | Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.) | ||||||||||||
3-Dec-2019 | addassnq0lemcl 6559 | A natural number closure law. Lemma for addassnq0 6560. (Contributed by Jim Kingdon, 3-Dec-2019.) | ||||||||||||
3-Dec-2019 | nndir 6069 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) | ||||||||||||
1-Dec-2019 | nnanq0 6556 | Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.) | ||||||||||||
~Q0 ~Q0 +Q0 ~Q0 | ||||||||||||||
1-Dec-2019 | archnqq 6515 | For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.) | ||||||||||||
30-Nov-2019 | bj-2inf 10062 | Two formulations of the axiom of infinity (see ax-infvn 10066 and bj-omex 10067) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind Ind | ||||||||||||||
30-Nov-2019 | bj-om 10061 | A set is equal to if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind Ind | ||||||||||||||
30-Nov-2019 | bj-ssom 10060 | A characterization of subclasses of . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | bj-omssind 10059 | is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | bj-omind 10058 | is an inductive class. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | bj-dfom 10057 | Alternate definition of , as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | bj-indint 10055 | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind Ind | ||||||||||||||
30-Nov-2019 | bj-bdind 10054 | Boundedness of the formula "the setvar is an inductive class". (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
BOUNDED Ind | ||||||||||||||
30-Nov-2019 | bj-indeq 10053 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind Ind | ||||||||||||||
30-Nov-2019 | bj-indsuc 10052 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | df-bj-ind 10051 | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
Ind | ||||||||||||||
30-Nov-2019 | bj-bdsucel 10002 | Boundedness of the formula "the successor of the setvar belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
BOUNDED | ||||||||||||||
30-Nov-2019 | bj-bd0el 9988 | Boundedness of the formula "the empty set belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
BOUNDED | ||||||||||||||
30-Nov-2019 | bj-sseq 9931 | If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.) | ||||||||||||
30-Nov-2019 | nqpnq0nq 6551 | A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.) | ||||||||||||
Q0 +Q0 | ||||||||||||||
30-Nov-2019 | mulclnq0 6550 | Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.) | ||||||||||||
Q0 Q0 ·Q0 Q0 | ||||||||||||||
30-Nov-2019 | prarloclemarch 6516 | A version of the Archimedean property. This variation is "stronger" than archnqq 6515 in the sense that we provide an integer which is larger than a given rational even after being multiplied by a second rational . (Contributed by Jim Kingdon, 30-Nov-2019.) | ||||||||||||
29-Nov-2019 | bj-elssuniab 9930 | Version of elssuni 3608 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
29-Nov-2019 | bj-intabssel1 9929 | Version of intss1 3630 using a class abstraction and implicit substitution. Closed form of intmin3 3642. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
29-Nov-2019 | bj-intabssel 9928 | Version of intss1 3630 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) | ||||||||||||
29-Nov-2019 | nq02m 6563 | Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.) | ||||||||||||
Q0 ~Q0 ·Q0 +Q0 | ||||||||||||||
29-Nov-2019 | distnq0r 6561 | Multiplication of non-negative fractions is distributive. Version of distrnq0 6557 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.) | ||||||||||||
Q0 Q0 Q0 +Q0 ·Q0 ·Q0 +Q0 ·Q0 | ||||||||||||||
29-Nov-2019 | addassnq0 6560 | Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.) | ||||||||||||
Q0 Q0 Q0 +Q0 +Q0 +Q0 +Q0 | ||||||||||||||
29-Nov-2019 | addclnq0 6549 | Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.) | ||||||||||||
Q0 Q0 +Q0 Q0 | ||||||||||||||
29-Nov-2019 | mulcanenq0ec 6543 | Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.) | ||||||||||||
~Q0 ~Q0 | ||||||||||||||
28-Nov-2019 | ax-bdsetind 10093 | Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.) | ||||||||||||
BOUNDED | ||||||||||||||
28-Nov-2019 | bj-peano4 10080 | Remove from peano4 4320 dependency on ax-setind 4262. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
28-Nov-2019 | bj-nnen2lp 10079 |
A version of en2lp 4278 for natural numbers, which does not require
ax-setind 4262.
Note: using this theorem and bj-nnelirr 10078, one can remove dependency on ax-setind 4262 from nntri2 6073 and nndcel 6078; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
27-Nov-2019 | mulcomnq0 6558 | Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.) | ||||||||||||
Q0 Q0 ·Q0 ·Q0 | ||||||||||||||
27-Nov-2019 | distrnq0 6557 | Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.) | ||||||||||||
Q0 Q0 Q0 ·Q0 +Q0 ·Q0 +Q0 ·Q0 | ||||||||||||||
25-Nov-2019 | prcunqu 6583 | An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.) | ||||||||||||
25-Nov-2019 | prarloclemarch2 6517 | Like prarloclemarch 6516 but the integer must be at least two, and there is also added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6601. (Contributed by Jim Kingdon, 25-Nov-2019.) | ||||||||||||
25-Nov-2019 | subhalfnqq 6512 | There is a number which is less than half of any positive fraction. The case where is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6508). (Contributed by Jim Kingdon, 25-Nov-2019.) | ||||||||||||
24-Nov-2019 | bj-nnelirr 10078 | A natural number does not belong to itself. Version of elirr 4266 for natural numbers, which does not require ax-setind 4262. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
24-Nov-2019 | bdcriota 10003 | A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.) | ||||||||||||
BOUNDED BOUNDED | ||||||||||||||
24-Nov-2019 | nq0nn 6540 | Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.) | ||||||||||||
Q0 ~Q0 | ||||||||||||||
24-Nov-2019 | enq0eceq 6535 | Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.) | ||||||||||||
~Q0 ~Q0 | ||||||||||||||
24-Nov-2019 | dfplq0qs 6528 | Addition on non-negative fractions. This definition is similar to df-plq0 6525 but expands Q0 (Contributed by Jim Kingdon, 24-Nov-2019.) | ||||||||||||
+Q0 ~Q0 ~Q0 ~Q0 ~Q0 ~Q0 | ||||||||||||||
23-Nov-2019 | addnq0mo 6545 | There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.) | ||||||||||||
~Q0 ~Q0 ~Q0 ~Q0 ~Q0 | ||||||||||||||
23-Nov-2019 | nnnq0lem1 6544 | Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6547 and mulnnnq0 6548. (Contributed by Jim Kingdon, 23-Nov-2019.) | ||||||||||||
~Q0 ~Q0 ~Q0 ~Q0 ~Q0 ~Q0 ~Q0 ~Q0 | ||||||||||||||
23-Nov-2019 | addcmpblnq0 6541 | Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.) | ||||||||||||
~Q0 | ||||||||||||||
23-Nov-2019 | ee8anv 1810 | Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.) | ||||||||||||
23-Nov-2019 | 19.42vvvv 1790 | Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.) | ||||||||||||
22-Nov-2019 | bdsetindis 10094 | Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
22-Nov-2019 | setindis 10092 | Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) | ||||||||||||
22-Nov-2019 | setindf 10091 | Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) | ||||||||||||
22-Nov-2019 | setindft 10090 | Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) | ||||||||||||
22-Nov-2019 | bj-nntrans2 10077 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
22-Nov-2019 | bj-nntrans 10076 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
22-Nov-2019 | bdfind 10071 | Bounded induction (principle of induction when is assumed to be bounded), proved from basic constructive axioms. See find 4322 for a nonconstructive proof of the general case. See findset 10070 for a proof when is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
22-Nov-2019 | findset 10070 | Bounded induction (principle of induction when is assumed to be a set) allowing a proof from basic constructive axioms. See find 4322 for a nonconstructive proof of the general case. See bdfind 10071 for a proof when is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
22-Nov-2019 | cbvrald 9927 | Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.) | ||||||||||||
22-Nov-2019 | addnnnq0 6547 | Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.) | ||||||||||||
~Q0 +Q0 ~Q0 ~Q0 | ||||||||||||||
22-Nov-2019 | dfmq0qs 6527 | Multiplication on non-negative fractions. This definition is similar to df-mq0 6526 but expands Q0 (Contributed by Jim Kingdon, 22-Nov-2019.) | ||||||||||||
·Q0 ~Q0 ~Q0 ~Q0 ~Q0 ~Q0 | ||||||||||||||
22-Nov-2019 | neqned 2213 | If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2226. One-way deduction form of df-ne 2206. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2255. (Revised by Wolf Lammen, 22-Nov-2019.) | ||||||||||||
21-Nov-2019 | bj-findes 10106 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 10104 for explanations. From this version, it is easy to prove findes 4326. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
21-Nov-2019 | bj-findisg 10105 | Version of bj-findis 10104 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 10104 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
21-Nov-2019 | bj-bdfindes 10074 | Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 10072 for explanations. From this version, it is easy to prove the bounded version of findes 4326. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
21-Nov-2019 | bj-bdfindisg 10073 | Version of bj-bdfindis 10072 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 10072 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
21-Nov-2019 | bj-bdfindis 10072 | Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4323 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4323, finds2 4324, finds1 4325. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) | ||||||||||||
BOUNDED | ||||||||||||||
21-Nov-2019 | bdeqsuc 10001 | Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
BOUNDED | ||||||||||||||
21-Nov-2019 | bdop 9995 | The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
BOUNDED | ||||||||||||||
21-Nov-2019 | bdeq0 9987 | Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.) | ||||||||||||
BOUNDED |
Copyright terms: Public domain | W3C HTML validation [external] |