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 | ||
18-Oct-2021 | qdencn 10097 | 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 9772 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
15-Oct-2021 | qdenre 9772 | 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 9109. (Contributed by BJ, 15-Oct-2021.) |
14-Oct-2021 | qbtwnrelemcalc 9108 | Lemma for qbtwnre 9109. Calculations involved in showing the constructed rational number is less than . (Contributed by Jim Kingdon, 14-Oct-2021.) |
13-Oct-2021 | rebtwn2z 9107 |
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 9106 | Lemma for rebtwn2z 9107. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.) |
13-Oct-2021 | rebtwn2zlemstep 9105 | Lemma for rebtwn2z 9107. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.) |
11-Oct-2021 | flqeqceilz 9158 | A rational number is an integer iff its floor equals its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⌈ | ||
11-Oct-2021 | flqleceil 9157 | 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 9156 | A rational number equals its ceiling iff it is an integer. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⌈ | ||
11-Oct-2021 | ceilqle 9154 | 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 9153 | 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 9152 | 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 9151 | 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 9150 | 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 9149 | 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 9148 | Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.) |
⌈ | ||
11-Oct-2021 | ceiqcl 9147 | The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.) |
11-Oct-2021 | qdceq 9100 | Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.) |
DECID | ||
11-Oct-2021 | qltlen 8573 | Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7619 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.) |
10-Oct-2021 | ceilqval 9146 | The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⌈ | ||
10-Oct-2021 | flqmulnn0 9139 | Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.) |
10-Oct-2021 | flqzadd 9138 | 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 9137 | 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 9134 | 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 9133 | 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 8013 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
10-Oct-2021 | 3ap0 8010 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
# | ||
9-Oct-2021 | flqbi2 9131 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
9-Oct-2021 | flqbi 9130 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
9-Oct-2021 | flqword2 9129 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
9-Oct-2021 | flqwordi 9128 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
9-Oct-2021 | flqltnz 9127 | 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 9126 | A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.) |
8-Oct-2021 | flqidm 9125 | The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqlt 9123 | The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqge 9122 | 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 9121 | The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | qfraclt1 9120 | The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqltp1 9119 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqle 9118 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqcld 9117 | The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqlelt 9116 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | flqcl 9115 | 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 9104 | 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 9103 |
Lemma for qbtwnz 9104. 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 9102 | Lemma for qbtwnz 9104. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | qbtwnzlemstep 9101 | Lemma for qbtwnz 9104. Induction step. (Contributed by Jim Kingdon, 8-Oct-2021.) |
8-Oct-2021 | qltnle 9099 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.) |
7-Oct-2021 | qlelttric 9098 | Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.) |
6-Oct-2021 | qletric 9097 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) |
6-Oct-2021 | qtri3or 9096 | 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 9870 | Example for df-ceil 9113. (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 6367 | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
30-Aug-2021 | cardval3ex 6363 | The value of . (Contributed by Jim Kingdon, 30-Aug-2021.) |
30-Aug-2021 | cardcl 6359 | 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.) |
Copyright terms: Public domain | W3C HTML validation [external] |