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 | ||
15-Feb-2024 | dedekindicclemeu 12673 | Lemma for dedekindicc 12674. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlu 12672 | Lemma for dedekindicc 12674. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlub 12671 | Lemma for dedekindicc 12674. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemloc 12670 | Lemma for dedekindicc 12674. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemub 12669 | Lemma for dedekindicc 12674. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemuub 12668 | Lemma for dedekindicc 12674. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.) |
14-Feb-2024 | suplociccex 12667 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7801 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
14-Feb-2024 | suplociccreex 12666 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7801 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
2-Feb-2024 | dedekindeulemuub 12659 | Lemma for dedekindeu 12665. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.) |
31-Jan-2024 | dedekindeulemeu 12664 | Lemma for dedekindeu 12665. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlu 12663 | Lemma for dedekindeu 12665. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlub 12662 | Lemma for dedekindeu 12665. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemloc 12661 | Lemma for dedekindeu 12665. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemub 12660 | Lemma for dedekindeu 12665. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
30-Jan-2024 | axsuploc 7801 | An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 7705 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
24-Jan-2024 | axpre-suploclemres 7673 | Lemma for axpre-suploc 7674. The result. The proof just needs to define as basically the same set as (but expressed as a subset of rather than a subset of ), and apply suplocsr 7581. (Contributed by Jim Kingdon, 24-Jan-2024.) |
23-Jan-2024 | ax-pre-suploc 7705 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. Although this and ax-caucvg 7704 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7704. (Contributed by Jim Kingdon, 23-Jan-2024.) |
23-Jan-2024 | axpre-suploc 7674 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7705. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
22-Jan-2024 | suplocsr 7581 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
21-Jan-2024 | bj-el2oss1o 12792 | Shorter proof of el2oss1o 12999 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
21-Jan-2024 | ltm1sr 7549 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
19-Jan-2024 | suplocsrlempr 7579 | Lemma for suplocsr 7581. The set has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
18-Jan-2024 | suplocsrlemb 7578 | Lemma for suplocsr 7581. The set is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
16-Jan-2024 | suplocsrlem 7580 | Lemma for suplocsr 7581. The set has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
14-Jan-2024 | suplocexprlemlub 7496 | Lemma for suplocexpr 7497. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
14-Jan-2024 | suplocexprlemub 7495 | Lemma for suplocexpr 7497. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
9-Jan-2024 | suplocexprlemloc 7493 | Lemma for suplocexpr 7497. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemdisj 7492 | Lemma for suplocexpr 7497. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemru 7491 | Lemma for suplocexpr 7497. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemrl 7489 | Lemma for suplocexpr 7497. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlem2b 7486 | Lemma for suplocexpr 7497. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemell 7485 | Lemma for suplocexpr 7497. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
7-Jan-2024 | suplocexpr 7497 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemex 7494 | Lemma for suplocexpr 7497. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemmu 7490 | Lemma for suplocexpr 7497. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemml 7488 | Lemma for suplocexpr 7497. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemss 7487 | Lemma for suplocexpr 7497. is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.) |
5-Jan-2024 | dedekindicc 12674 | A Dedekind cut identifies a unique real number. Similar to df-inp 7238 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.) |
5-Jan-2024 | dedekindeu 12665 | A Dedekind cut identifies a unique real number. Similar to df-inp 7238 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.) |
31-Dec-2023 | dvmptsubcn 12737 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | dvmptnegcn 12736 | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | dvmptcmulcn 12735 | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | brm 3946 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
30-Dec-2023 | dvmptccn 12731 | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
30-Dec-2023 | dvmptidcn 12730 | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
25-Dec-2023 | ctfoex 6969 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
23-Dec-2023 | enct 11841 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | enctlem 11840 | Lemma for enct 11841. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | omct 6968 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
21-Dec-2023 | dvcoapbr 12723 | The chain rule for derivatives at a point. The # # hypothesis constrains what functions work for . (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 21-Dec-2023.) |
# # | ||
19-Dec-2023 | apsscn 8371 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
19-Dec-2023 | aprcl 8370 | Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
18-Dec-2023 | limccoap 12699 | Composition of two limits. This theorem is only usable in the case where # implies R(x) # so it is less general than might appear at first. (Contributed by Mario Carneiro, 29-Dec-2016.) (Revised by Jim Kingdon, 18-Dec-2023.) |
# # # # lim # lim # lim | ||
16-Dec-2023 | cnreim 10690 | Complex apartness in terms of real and imaginary parts. See also apreim 8328 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
14-Dec-2023 | cnopnap 12658 | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
# | ||
14-Dec-2023 | cnovex 12260 | The class of all continuous functions from a topology to another is a set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
13-Dec-2023 | reopnap 12602 | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
# | ||
12-Dec-2023 | cnopncntop 12601 | The set of complex numbers is open with respect to the standard topology on complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.) |
12-Dec-2023 | unicntopcntop 12600 | The underlying set of the standard topology on the complex numbers is the set of complex numbers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by Jim Kingdon, 12-Dec-2023.) |
4-Dec-2023 | bj-pm2.18st 12769 | Clavius law for stable formulas. See pm2.18dc 823. (Contributed by BJ, 4-Dec-2023.) |
STAB | ||
4-Dec-2023 | bj-nnclavius 12761 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
2-Dec-2023 | dvmulxx 12720 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 12718. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.) |
1-Dec-2023 | dvmulxxbr 12718 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 12720. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.) |
29-Nov-2023 | subctctexmid 13007 | If every subcountable set is countable and Markov's principle holds, excluded middle follows. Proposition 2.6 of [BauerSwan], p. 14:4. The proof is taken from that paper. (Contributed by Jim Kingdon, 29-Nov-2023.) |
⊔ Markov EXMID | ||
29-Nov-2023 | ismkvnex 6995 | The predicate of being Markov stated in terms of double negation and comparison with . (Contributed by Jim Kingdon, 29-Nov-2023.) |
Markov | ||
28-Nov-2023 | exmid1stab 13006 | If any proposition is stable, excluded middle follows. We are thinking of as a proposition and as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.) |
STAB EXMID | ||
28-Nov-2023 | ccfunen 7043 | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
CCHOICE | ||
27-Nov-2023 | df-cc 7042 | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7026 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
26-Nov-2023 | offeq 5961 | Convert an identity of the operation to the analogous identity on the function operation. (Contributed by Jim Kingdon, 26-Nov-2023.) |
25-Nov-2023 | dvaddxx 12719 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 12717. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
25-Nov-2023 | dvaddxxbr 12717 | The sum rule for derivatives at a point. That is, if the derivative of at is and the derivative of at is , then the derivative of the pointwise sum of those two functions at is . (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
25-Nov-2023 | dcnn 816 | Decidability of the negation of a proposition is equivalent to decidability of its double negation. See also dcn 810. The relation between dcn 810 and dcnn 816 is analogous to that between notnot 601 and notnotnot 606 (and directly stems from it). Using the notion of "testable proposition" (proposition whose negation is decidable), dcnn 816 means that a proposition is testable if and only if its negation is testable, and dcn 810 means that decidability implies testability. (Contributed by David A. Wheeler, 6-Dec-2018.) (Proof shortened by BJ, 25-Nov-2023.) |
DECID DECID | ||
24-Nov-2023 | bj-dcst 12778 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) |
DECID STAB STAB | ||
24-Nov-2023 | bj-nnbidc 12773 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 12764. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-dcstab 12772 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
DECID STAB | ||
24-Nov-2023 | bj-fadc 12771 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-trdc 12770 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-stal 12768 | The universal quantification of stable formula is stable. See bj-stim 12765 for implication, stabnot 801 for negation, and bj-stan 12766 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-stand 12767 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 12766. Its proof is shorter, so one could prove it first and then bj-stan 12766 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stan 12766 | The conjunction of two stable formulas is stable. See bj-stim 12765 for implication, stabnot 801 for negation, and bj-stal 12768 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stim 12765 | A conjunction with a stable consequent is stable. See stabnot 801 for negation and bj-stan 12766 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-nnbist 12764 | If a formula is not refutable, then it is stable if and only if it is provable. By double-negation translation, if is a classical tautology, then is an intuitionistic tautology. Therefore, if is a classical tautology, then is intuitionistically equivalent to its stability (and to its decidability, see bj-nnbidc 12773). (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-fast 12763 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-trst 12762 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-nnal 12760 | The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnan 12759 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnim 12758 | The double negation of an implication implies the implication with the consequent doubly negated. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnsn 12756 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) |
22-Nov-2023 | ofvalg 5957 | Evaluate a function operation at a point. (Contributed by Mario Carneiro, 20-Jul-2014.) (Revised by Jim Kingdon, 22-Nov-2023.) |
21-Nov-2023 | exmidac 7029 | The axiom of choice implies excluded middle. See acexmid 5739 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
21-Nov-2023 | exmidaclem 7028 | Lemma for exmidac 7029. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
CHOICE EXMID | ||
21-Nov-2023 | exmid1dc 4091 | A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4085 or ordtriexmid 4405. In this context can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.) |
DECID EXMID | ||
20-Nov-2023 | acfun 7027 | A convenient form of choice. The goal here is to state choice as the existence of a choice function on a set of inhabited sets, while making full use of our notation around functions and function values. (Contributed by Jim Kingdon, 20-Nov-2023.) |
CHOICE | ||
18-Nov-2023 | condc 821 |
Contraposition of a decidable proposition.
This theorem swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This theorem (without the decidability condition, of course) is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103) and is Axiom A3 of [Margaris] p. 49. We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. (Contributed by Jim Kingdon, 13-Mar-2018.) (Proof shortened by BJ, 18-Nov-2023.) |
DECID | ||
18-Nov-2023 | const 820 | Contraposition of a stable proposition. See comment of condc 821. (Contributed by BJ, 18-Nov-2023.) |
STAB | ||
18-Nov-2023 | stdcn 815 | A formula is stable if and only if the decidability of its negation implies its decidability. Note that the right-hand side of this biconditional is the converse of dcn 810. (Contributed by BJ, 18-Nov-2023.) |
STAB DECID DECID | ||
17-Nov-2023 | cnplimclemr 12690 | Lemma for cnplimccntop 12691. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾_{t} lim | ||
17-Nov-2023 | cnplimclemle 12689 | Lemma for cnplimccntop 12691. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾_{t} lim # | ||
14-Nov-2023 | limccnp2cntop 12698 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Nov-2023.) |
↾_{t} lim lim lim | ||
10-Nov-2023 | rpmaxcl 10935 | The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.) |
Copyright terms: Public domain | W3C HTML validation [external] |