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