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 | ||
9-Dec-2024 | nninfwlpoim 7154 | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
ℕ∞ ℕ∞ DECID WOmni | ||
8-Dec-2024 | nninfwlpoimlemdc 7153 | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
ℕ∞ ℕ∞ DECID DECID | ||
8-Dec-2024 | nninfwlpoimlemginf 7152 | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
8-Dec-2024 | nninfwlpoimlemg 7151 | Lemma for nninfwlpoim 7154. (Contributed by Jim Kingdon, 8-Dec-2024.) |
ℕ∞ | ||
7-Dec-2024 | nninfwlpor 7150 | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
WOmni ℕ∞ ℕ∞ DECID | ||
7-Dec-2024 | nninfwlporlem 7149 | Lemma for nninfwlpor 7150. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
WOmni DECID | ||
6-Dec-2024 | nninfwlporlemd 7148 | Given two countably infinite sequences of zeroes and ones, they are equal if and only if a sequence formed by pointwise comparing them is all ones. (Contributed by Jim Kingdon, 6-Dec-2024.) |
3-Dec-2024 | nninfwlpo 7155 | Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.) |
ℕ∞ ℕ∞ DECID WOmni | ||
3-Dec-2024 | nninfdcinf 7147 | The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.) |
WOmni ℕ∞ DECID | ||
28-Nov-2024 | basmexd 12475 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
22-Nov-2024 | eliotaeu 5187 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) |
22-Nov-2024 | eliota 5186 | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) |
18-Nov-2024 | basmex 12474 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
11-Nov-2024 | bj-con1st 13786 | Contraposition when the antecedent is a negated stable proposition. See con1dc 851. (Contributed by BJ, 11-Nov-2024.) |
STAB | ||
11-Nov-2024 | const 847 | Contraposition when the antecedent is a negated stable proposition. See comment of condc 848. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.) |
STAB | ||
4-Nov-2024 | lgsfvalg 13700 | Value of the function which defines the Legendre symbol at the primes. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by Jim Kingdon, 4-Nov-2024.) |
1-Nov-2024 | qsqeqor 10586 | The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.) |
29-Oct-2024 | fiubnn 10765 | A finite set of natural numbers has an upper bound which is a a natural number. (Contributed by Jim Kingdon, 29-Oct-2024.) |
29-Oct-2024 | fiubz 10764 | A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.) |
29-Oct-2024 | fiubm 10763 | Lemma for fiubz 10764 and fiubnn 10765. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.) |
27-Oct-2024 | bj-nnst 13778 | Double negation of stability of a formula. Intuitionistic logic refutes unstability (but does not prove stability) of any formula. This theorem can also be proved in classical refutability calculus (see https://us.metamath.org/mpeuni/bj-peircestab.html) but not in minimal calculus (see https://us.metamath.org/mpeuni/bj-stabpeirce.html). See nnnotnotr 14025 for the version not using the definition of stability. (Contributed by BJ, 9-Oct-2019.) Prove it in -intuitionistic calculus with definitions (uses of ax-ia1 105, ax-ia2 106, ax-ia3 107 are via sylibr 133, necessary for definition unpackaging), and in -intuitionistic calculus, following a discussion with Jim Kingdon. (Revised by BJ, 27-Oct-2024.) |
STAB | ||
27-Oct-2024 | bj-imnimnn 13773 | If a formula is implied by both a formula and its negation, then it is not refutable. There is another proof using the inference associated with bj-nnclavius 13772 as its last step. (Contributed by BJ, 27-Oct-2024.) |
25-Oct-2024 | nnwosdc 11994 | Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.) |
DECID | ||
23-Oct-2024 | nnwodc 11991 | Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.) |
DECID | ||
22-Oct-2024 | uzwodc 11992 | Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.) |
DECID | ||
21-Oct-2024 | nnnotnotr 14025 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 845, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.) |
20-Oct-2024 | isprm5lem 12095 | Lemma for isprm5 12096. The interesting direction (showing that one only needs to check prime divisors up to the square root of ). (Contributed by Jim Kingdon, 20-Oct-2024.) |
17-Oct-2024 | elnndc 9571 | Membership of an integer in is decidable. (Contributed by Jim Kingdon, 17-Oct-2024.) |
DECID | ||
14-Oct-2024 | 2zinfmin 11206 | Two ways to express the minimum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 14-Oct-2024.) |
inf | ||
14-Oct-2024 | mingeb 11205 | Equivalence of and being equal to the minimum of two reals. (Contributed by Jim Kingdon, 14-Oct-2024.) |
inf | ||
13-Oct-2024 | pcxnn0cl 12264 | Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.) |
NN0* | ||
13-Oct-2024 | xnn0letri 9760 | Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) |
NN0* NN0* | ||
13-Oct-2024 | xnn0dcle 9759 | Decidability of for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) |
NN0* NN0* DECID | ||
9-Oct-2024 | nn0leexp2 10645 | Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.) |
8-Oct-2024 | pclemdc 12242 | Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.) |
DECID | ||
8-Oct-2024 | elnn0dc 9570 | Membership of an integer in is decidable. (Contributed by Jim Kingdon, 8-Oct-2024.) |
DECID | ||
7-Oct-2024 | pclemub 12241 | Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.) |
7-Oct-2024 | pclem0 12240 | Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Jim Kingdon, 7-Oct-2024.) |
7-Oct-2024 | nn0ltexp2 10644 | Special case of ltexp2 13654 which we use here because we haven't yet defined df-rpcxp 13574 which is used in the current proof of ltexp2 13654. (Contributed by Jim Kingdon, 7-Oct-2024.) |
6-Oct-2024 | suprzcl2dc 11910 | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) |
DECID | ||
5-Oct-2024 | zsupssdc 11909 | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
DECID | ||
5-Oct-2024 | suprzubdc 11907 | The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
DECID | ||
1-Oct-2024 | infex2g 7011 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
inf | ||
30-Sep-2024 | unbendc 12409 | An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.) |
DECID | ||
30-Sep-2024 | prmdc 12084 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
DECID | ||
30-Sep-2024 | dcfi 6958 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
DECID DECID | ||
29-Sep-2024 | ssnnct 12402 | A decidable subset of is countable. (Contributed by Jim Kingdon, 29-Sep-2024.) |
DECID ⊔ | ||
29-Sep-2024 | ssnnctlemct 12401 | Lemma for ssnnct 12402. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
frec DECID ⊔ | ||
28-Sep-2024 | nninfdcex 11908 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
DECID | ||
27-Sep-2024 | infregelbex 9557 | Any lower bound of a set of real numbers with an infimum is less than or equal to the infimum. (Contributed by Jim Kingdon, 27-Sep-2024.) |
inf | ||
26-Sep-2024 | nninfdclemp1 12405 | Lemma for nninfdc 12408. Each element of the sequence is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.) |
DECID inf | ||
26-Sep-2024 | nnminle 11990 | The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 11989. (Contributed by Jim Kingdon, 26-Sep-2024.) |
DECID inf | ||
25-Sep-2024 | nninfdclemcl 12403 | Lemma for nninfdc 12408. (Contributed by Jim Kingdon, 25-Sep-2024.) |
DECID inf | ||
24-Sep-2024 | nninfdclemlt 12406 | Lemma for nninfdc 12408. The function from nninfdclemf 12404 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nninfdc 12408 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID | ||
23-Sep-2024 | nninfdclemf1 12407 | Lemma for nninfdc 12408. The function from nninfdclemf 12404 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nninfdclemf 12404 | Lemma for nninfdc 12408. A function from the natural numbers into . (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nnmindc 11989 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
19-Sep-2024 | ssomct 12400 | A decidable subset of is countable. (Contributed by Jim Kingdon, 19-Sep-2024.) |
DECID ⊔ | ||
14-Sep-2024 | nnpredlt 4608 | The predecessor (see nnpredcl 4607) of a nonzero natural number is less than (see df-iord 4351) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
13-Sep-2024 | nninfisollemeq 7108 | Lemma for nninfisol 7109. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
13-Sep-2024 | nninfisollemne 7107 | Lemma for nninfisol 7109. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
13-Sep-2024 | nninfisollem0 7106 | Lemma for nninfisol 7109. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ∞ DECID | ||
12-Sep-2024 | nninfisol 7109 | Finite elements of ℕ∞ are isolated. That is, given a natural number and any element of ℕ∞, it is decidable whether the natural number (when converted to an element of ℕ∞) is equal to the given element of ℕ∞. Stated in an online post by Martin Escardo. One way to understand this theorem is that you do not need to look at an unbounded number of elements of the sequence to decide whether it is equal to (in fact, you only need to look at two elements and tells you where to look). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
ℕ∞ DECID | ||
7-Sep-2024 | eulerthlemfi 12182 | Lemma for eulerth 12187. The set is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.) |
..^ | ||
7-Sep-2024 | modqexp 10602 | Exponentiation property of the modulo operation, see theorem 5.2(c) in [ApostolNT] p. 107. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.) |
5-Sep-2024 | eulerthlemh 12185 | Lemma for eulerth 12187. A permutation of . (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemth 12186 | Lemma for eulerth 12187. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlema 12184 | Lemma for eulerth 12187. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemrprm 12183 | Lemma for eulerth 12187. and are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
30-Aug-2024 | fprodap0f 11599 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 11584 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020.) (Revised by Jim Kingdon, 30-Aug-2024.) |
# # | ||
28-Aug-2024 | fprodrec 11592 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
# | ||
26-Aug-2024 | exmidontri2or 7220 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | exmidontri 7216 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | ontri2orexmidim 4556 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4555. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
26-Aug-2024 | ontriexmidim 4506 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4505. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
25-Aug-2024 | onntri2or 7223 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | onntri3or 7222 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | csbcow 3060 | Composition law for chained substitutions into a class. Version of csbco 3059 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvreuvw 2702 | Version of cbvreuv 2698 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvrexvw 2701 | Version of cbvrexv 2697 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvralvw 2700 | Version of cbvralv 2696 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvabw 2293 | Version of cbvab 2294 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | nfsbv 1940 | If is not free in , it is not free in when is distinct from and . Version of nfsb 1939 requiring more disjoint variables. (Contributed by Wolf Lammen, 7-Feb-2023.) Remove disjoint variable condition on . (Revised by Steven Nguyen, 13-Aug-2023.) Reduce axiom usage. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvexvw 1913 | Change bound variable. See cbvexv 1911 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvalvw 1912 | Change bound variable. See cbvalv 1910 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1441. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | nfal 1569 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1503. (Revised by Gino Giotto, 25-Aug-2024.) |
24-Aug-2024 | gcdcomd 11929 | The operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
21-Aug-2024 | dvds2addd 11791 | Deduction form of dvds2add 11787. (Contributed by SN, 21-Aug-2024.) |
17-Aug-2024 | fprodcl2lem 11568 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
16-Aug-2024 | if0ab 13840 |
Expression of a conditional class as a class abstraction when the False
alternative is the empty class: in that case, the conditional class is
the extension, in the True alternative, of the condition.
Remark: a consequence which could be formalized is the inclusion and therefore, using elpwg 3574, , from which fmelpw1o 13841 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.) |
16-Aug-2024 | fprodunsn 11567 | Multiply in an additional term in a finite product. See also fprodsplitsn 11596 which is the same but with a hypothesis in place of the distinct variable condition between and . (Contributed by Jim Kingdon, 16-Aug-2024.) |
15-Aug-2024 | bj-charfundcALT 13844 | Alternate proof of bj-charfundc 13843. It was expected to be much shorter since it uses bj-charfun 13842 for the main part of the proof and the rest is basic computations, but these turn out to be lengthy, maybe because of the limited library of available lemmas. (Contributed by BJ, 15-Aug-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
DECID | ||
15-Aug-2024 | bj-charfun 13842 | Properties of the characteristic function on the class of the class . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | fmelpw1o 13841 |
With a formula
one can associate an element of ,
which
can therefore be thought of as the set of "truth values" (but
recall that
there are no other genuine truth values than and , by
nndc 846, which translate to and respectively by iftrue 3531
and iffalse 3534, giving pwtrufal 14030).
As proved in if0ab 13840, the associated element of is the extension, in , of the formula . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | cnstab 8564 | Equality of complex numbers is stable. Stability here means as defined at df-stab 826. This theorem for real numbers is Proposition 5.2 of [BauerHanson], p. 27. (Contributed by Jim Kingdon, 1-Aug-2023.) (Proof shortened by BJ, 15-Aug-2024.) |
STAB | ||
15-Aug-2024 | subap0d 8563 | Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) (Proof shortened by BJ, 15-Aug-2024.) |
# # | ||
15-Aug-2024 | ifexd 4469 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwun 4468 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwund 4467 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwung 4466 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifidss 3541 | A conditional class whose two alternatives are equal is included in that alternative. With excluded middle, we can prove it is equal to it. (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifssun 3540 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
12-Aug-2024 | exmidontriimlem2 7199 | Lemma for exmidontriim 7202. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
12-Aug-2024 | exmidontriimlem1 7198 | Lemma for exmidontriim 7202. A variation of r19.30dc 2617. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
11-Aug-2024 | nndc 846 |
Double negation of decidability of a formula. Intuitionistic logic
refutes the negation of decidability (but does not prove decidability) of
any formula.
This should not trick the reader into thinking that EXMID is provable in intuitionistic logic. Indeed, if we could quantify over formula metavariables, then generalizing nnexmid 845 over would give " DECID ", but EXMID is "DECID ", so proving EXMID would amount to proving " DECID ", which is not implied by the above theorem. Indeed, the converse of nnal 1642 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of , like we do in our definition of EXMID (df-exmid 4181): then, we can prove DECID but we cannot prove DECID because the converse of nnral 2460 does not hold. Actually, EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying EXMID and noncontradiction holds (pm3.24 688). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of EXMID. (Revised by BJ, 11-Aug-2024.) |
DECID | ||
10-Aug-2024 | exmidontriim 7202 | Excluded middle implies ordinal trichotomy. Lemma 10.4.1 of [HoTT], p. (varies). The proof follows the proof from the HoTT book fairly closely. (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | exmidontriimlem4 7201 | Lemma for exmidontriim 7202. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | exmidontriimlem3 7200 | Lemma for exmidontriim 7202. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | nnnninf2 7103 | Canonical embedding of into ℕ∞. (Contributed by BJ, 10-Aug-2024.) |
ℕ∞ | ||
10-Aug-2024 | infnninf 7100 | The point at infinity in ℕ∞ is the constant sequence equal to . Note that with our encoding of functions, that constant function can also be expressed as , as fconstmpt 4658 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
ℕ∞ | ||
9-Aug-2024 | ss1o0el1o 6890 | Reformulation of ss1o0el1 4183 using instead of . (Contributed by BJ, 9-Aug-2024.) |
9-Aug-2024 | pw1dc0el 6889 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
EXMID DECID | ||
9-Aug-2024 | ss1o0el1 4183 | A subclass of contains the empty set if and only if it equals . (Contributed by BJ and Jim Kingdon, 9-Aug-2024.) |
8-Aug-2024 | pw1dc1 6891 | If, in the set of truth values (the powerset of 1o), equality to 1o is decidable, then excluded middle holds (and conversely). (Contributed by BJ and Jim Kingdon, 8-Aug-2024.) |
EXMID DECID | ||
7-Aug-2024 | pw1fin 6888 | Excluded middle is equivalent to the power set of being finite. (Contributed by SN and Jim Kingdon, 7-Aug-2024.) |
EXMID | ||
7-Aug-2024 | elomssom 4589 | A natural number ordinal is, as a set, included in the set of natural number ordinals. (Contributed by NM, 21-Jun-1998.) Extract this result from the previous proof of elnn 4590. (Revised by BJ, 7-Aug-2024.) |
6-Aug-2024 | bj-charfunbi 13846 |
In an ambient set , if
membership in is
stable, then it is
decidable if and only if has a characteristic function.
This characterization can be applied to singletons when the set has stable equality, which is the case as soon as it has a tight apartness relation. (Contributed by BJ, 6-Aug-2024.) |
STAB DECID | ||
6-Aug-2024 | bj-charfunr 13845 |
If a class has a
"weak" characteristic function on a class ,
then negated membership in is decidable (in other words,
membership in
is testable) in .
The hypothesis imposes that be a set. As usual, it could be formulated as to deal with general classes, but that extra generality would not make the theorem much more useful. The theorem would still hold if the codomain of were any class with testable equality to the point where is sent. (Contributed by BJ, 6-Aug-2024.) |
DECID | ||
6-Aug-2024 | bj-charfundc 13843 | Properties of the characteristic function on the class of the class , provided membership in is decidable in . (Contributed by BJ, 6-Aug-2024.) |
DECID | ||
6-Aug-2024 | prodssdc 11552 | Change the index set to a subset in an upper integer product. (Contributed by Scott Fenton, 11-Dec-2017.) (Revised by Jim Kingdon, 6-Aug-2024.) |
# DECID DECID | ||
5-Aug-2024 | fnmptd 13839 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | funmptd 13838 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5235, then prove funmptd 13838 from it, and then prove funmpt 5236 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | bj-dcfal 13790 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-dctru 13788 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-stfal 13777 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | bj-sttru 13775 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | prod1dc 11549 | Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | 2ssom 6503 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
2-Aug-2024 | onntri52 7221 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri24 7219 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri45 7218 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri51 7217 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri13 7215 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri35 7214 |
Double negated ordinal trichotomy.
There are five equivalent statements: (1) , (2) , (3) , (4) , and (5) EXMID. That these are all equivalent is expressed by (1) implies (3) (onntri13 7215), (3) implies (5) (onntri35 7214), (5) implies (1) (onntri51 7217), (2) implies (4) (onntri24 7219), (4) implies (5) (onntri45 7218), and (5) implies (2) (onntri52 7221). Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7216 and exmidontri2or 7220, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7222 and (4) by onntri2or 7223. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
1-Aug-2024 | nnral 2460 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1642. (Contributed by Jim Kingdon, 1-Aug-2024.) |
31-Jul-2024 | 3nsssucpw1 7213 | Negated excluded middle implies that is not a subset of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
31-Jul-2024 | sucpw1nss3 7212 | Negated excluded middle implies that the successor of the power set of is not a subset of . (Contributed by James E. Hanson and Jim Kingdon, 31-Jul-2024.) |
EXMID | ||
30-Jul-2024 | 3nelsucpw1 7211 | Three is not an element of the successor of the power set of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | sucpw1nel3 7210 | The successor of the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | sucpw1ne3 7209 | Negated excluded middle implies that the successor of the power set of is not three . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
30-Jul-2024 | pw1nel3 7208 | Negated excluded middle implies that the power set of is not an element of . (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
EXMID | ||
30-Jul-2024 | pw1ne3 7207 | The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne1 7206 | The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne0 7205 | The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.) |
29-Jul-2024 | grpcld 12721 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
29-Jul-2024 | pw1on 7203 | The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.) |
28-Jul-2024 | exmidpweq 6887 | Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.) |
EXMID | ||
27-Jul-2024 | dcapnconstALT 14093 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 14092 by means of dceqnconst 14091. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
DECID # | ||
27-Jul-2024 | reap0 14090 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
DECID # | ||
26-Jul-2024 | nconstwlpolemgt0 14095 | Lemma for nconstwlpo 14097. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
26-Jul-2024 | nconstwlpolem0 14094 | Lemma for nconstwlpo 14097. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
24-Jul-2024 | tridceq 14088 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 14075 and redcwlpo 14087). Thus, this is an analytic analogue to lpowlpo 7144. (Contributed by Jim Kingdon, 24-Jul-2024.) |
DECID | ||
24-Jul-2024 | iswomni0 14083 | Weak omniscience stated in terms of equality with . Like iswomninn 14082 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.) |
WOmni DECID | ||
24-Jul-2024 | lpowlpo 7144 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7143. There is an analogue in terms of analytic omniscience principles at tridceq 14088. (Contributed by Jim Kingdon, 24-Jul-2024.) |
Omni WOmni | ||
23-Jul-2024 | nconstwlpolem 14096 | Lemma for nconstwlpo 14097. (Contributed by Jim Kingdon, 23-Jul-2024.) |
23-Jul-2024 | dceqnconst 14091 | Decidability of real number equality implies the existence of a certain non-constant function from real numbers to integers. Variation of Exercise 11.6(i) of [HoTT], p. (varies). See redcwlpo 14087 for more discussion of decidability of real number equality. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) (Revised by Jim Kingdon, 23-Jul-2024.) |
DECID | ||
23-Jul-2024 | redc0 14089 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
DECID DECID | ||
23-Jul-2024 | canth 5807 | No set is equinumerous to its power set (Cantor's theorem), i.e., no function can map onto its power set. Compare Theorem 6B(b) of [Enderton] p. 132. (Use nex 1493 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.) |
22-Jul-2024 | nconstwlpo 14097 | Existence of a certain non-constant function from reals to integers implies WOmni (the Weak Limited Principle of Omniscience or WLPO). Based on Exercise 11.6(ii) of [HoTT], p. (varies). (Contributed by BJ and Jim Kingdon, 22-Jul-2024.) |
WOmni | ||
15-Jul-2024 | fprodseq 11546 | The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) (Revised by Jim Kingdon, 15-Jul-2024.) |
14-Jul-2024 | rexbid2 2475 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
14-Jul-2024 | ralbid2 2474 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
12-Jul-2024 | 2irrexpqap 13690 | There exist real numbers and which are irrational (in the sense of being apart from any rational number) such that is rational. Statement in the Metamath book, section 1.1.5, footnote 27 on page 17, and the "constructive proof" for theorem 1.2 of [Bauer], p. 483. This is a constructive proof because it is based on two explicitly named irrational numbers and logb , see sqrt2irrap 12134, 2logb9irrap 13689 and sqrt2cxp2logb9e3 13687. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.) |
# # | ||
12-Jul-2024 | 2logb9irrap 13689 | Example for logbgcd1irrap 13682. The logarithm of nine to base two is irrational (in the sense of being apart from any rational number). (Contributed by Jim Kingdon, 12-Jul-2024.) |
logb # | ||
11-Jul-2024 | logbgcd1irraplemexp 13680 | Lemma for logbgcd1irrap 13682. Apartness of and . (Contributed by Jim Kingdon, 11-Jul-2024.) |
# | ||
11-Jul-2024 | reapef 13493 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) |
# # | ||
10-Jul-2024 | apcxp2 13652 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) |
# # # | ||
9-Jul-2024 | logbgcd1irraplemap 13681 | Lemma for logbgcd1irrap 13682. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) |
logb # | ||
9-Jul-2024 | apexp1 10652 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) |
# # | ||
5-Jul-2024 | logrpap0 13592 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) |
# # | ||
3-Jul-2024 | rplogbval 13657 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the argument of the logarithm function here. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by Jim Kingdon, 3-Jul-2024.) |
# logb | ||
3-Jul-2024 | logrpap0d 13593 | Deduction form of logrpap0 13592. (Contributed by Jim Kingdon, 3-Jul-2024.) |
# # | ||
3-Jul-2024 | logrpap0b 13591 | The logarithm is apart from 0 if and only if its argument is apart from 1. (Contributed by Jim Kingdon, 3-Jul-2024.) |
# # | ||
28-Jun-2024 | 2o01f 14029 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
28-Jun-2024 | 012of 14028 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
27-Jun-2024 | iooreen 14067 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
27-Jun-2024 | iooref1o 14066 | A one-to-one mapping from the real numbers onto the open unit interval. (Contributed by Jim Kingdon, 27-Jun-2024.) |
25-Jun-2024 | neapmkvlem 14098 | Lemma for neapmkv 14099. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
# | ||
25-Jun-2024 | ismkvnn 14085 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov | ||
25-Jun-2024 | ismkvnnlem 14084 | Lemma for ismkvnn 14085. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
frec Markov | ||
25-Jun-2024 | enmkvlem 7137 | Lemma for enmkv 7138. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov Markov | ||
24-Jun-2024 | neapmkv 14099 | If negated equality for real numbers implies apartness, Markov's Principle follows. Exercise 11.10 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 24-Jun-2024.) |
# Markov | ||
24-Jun-2024 | dcapnconst 14092 |
Decidability of real number apartness implies the existence of a certain
non-constant function from real numbers to integers. Variation of
Exercise 11.6(i) of [HoTT], p. (varies).
See trilpo 14075 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 14091 and in fact this theorem can be proved using dceqnconst 14091 as shown at dcapnconstALT 14093. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
DECID # | ||
24-Jun-2024 | enmkv 7138 | Being Markov is invariant with respect to equinumerosity. For example, this means that we can express the Markov's Principle as either Markov or Markov. The former is a better match to conventional notation in the sense that df2o3 6409 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 24-Jun-2024.) |
Markov Markov | ||
21-Jun-2024 | redcwlpolemeq1 14086 | Lemma for redcwlpo 14087. A biconditionalized version of trilpolemeq1 14072. (Contributed by Jim Kingdon, 21-Jun-2024.) |
20-Jun-2024 | redcwlpo 14087 |
Decidability of real number equality implies the Weak Limited Principle
of Omniscience (WLPO). We expect that we'd need some form of countable
choice to prove the converse.
Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence is all ones or it is not. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. This real number will equal one if and only if the sequence is all ones (redcwlpolemeq1 14086). Therefore decidability of real number equality would imply decidability of whether the sequence is all ones. Because of this theorem, decidability of real number equality is sometimes called "analytic WLPO". WLPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qdceq 10203 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
DECID WOmni | ||
20-Jun-2024 | iswomninn 14082 | Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7142 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni DECID | ||
20-Jun-2024 | iswomninnlem 14081 | Lemma for iswomnimap 7142. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
frec WOmni DECID | ||
20-Jun-2024 | enwomni 7146 | Weak omniscience is invariant with respect to equinumerosity. For example, this means that we can express the Weak Limited Principle of Omniscience as either WOmni or WOmni. The former is a better match to conventional notation in the sense that df2o3 6409 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
20-Jun-2024 | enwomnilem 7145 | Lemma for enwomni 7146. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
19-Jun-2024 | rpabscxpbnd 13653 | Bound on the absolute value of a complex power. (Contributed by Mario Carneiro, 15-Sep-2014.) (Revised by Jim Kingdon, 19-Jun-2024.) |
16-Jun-2024 | rpcxpsqrt 13636 | The exponential function with exponent exactly matches the square root function, and thus serves as a suitable generalization to other -th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 16-Jun-2024.) |
13-Jun-2024 | rpcxpadd 13620 | Sum of exponents law for complex exponentiation. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 13-Jun-2024.) |
12-Jun-2024 | cxpap0 13619 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
# | ||
12-Jun-2024 | rpcncxpcl 13617 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | rpcxp0 13613 | Value of the complex power function when the second argument is zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | cxpexpnn 13611 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | cxpexprp 13610 | Relate the complex power function to the integer power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | rpcxpef 13609 | Value of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | df-rpcxp 13574 | Define the power function on complex numbers. Because df-relog 13573 is only defined on positive reals, this definition only allows for a base which is a positive real. (Contributed by Jim Kingdon, 12-Jun-2024.) |
10-Jun-2024 | trirec0xor 14077 |
Version of trirec0 14076 with exclusive-or.
The definition of a discrete field is sometimes stated in terms of exclusive-or but as proved here, this is equivalent to inclusive-or because the two disjuncts cannot be simultaneously true. (Contributed by Jim Kingdon, 10-Jun-2024.) |
10-Jun-2024 | trirec0 14076 |
Every real number having a reciprocal or equaling zero is equivalent to
real number trichotomy.
This is the key part of the definition of what is known as a discrete field, so "the real numbers are a discrete field" can be taken as an equivalent way to state real trichotomy (see further discussion at trilpo 14075). (Contributed by Jim Kingdon, 10-Jun-2024.) |
9-Jun-2024 | omniwomnimkv 7143 | A set is omniscient if and only if it is weakly omniscient and Markov. The case says that LPO WLPO MP which is a remark following Definition 2.5 of [Pierik], p. 9. (Contributed by Jim Kingdon, 9-Jun-2024.) |
Omni WOmni Markov | ||
9-Jun-2024 | iswomnimap 7142 | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
9-Jun-2024 | iswomni 7141 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
9-Jun-2024 | df-womni 7140 |
A weakly omniscient set is one where we can decide whether a predicate
(here represented by a function ) holds (is equal to ) for
all elements or not. Generalization of definition 2.4 of [Pierik],
p. 9.
In particular, WOmni is known as the Weak Limited Principle of Omniscience (WLPO). The term WLPO is common in the literature; there appears to be no widespread term for what we are calling a weakly omniscient set. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
1-Jun-2024 | grpmndd 12720 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
29-May-2024 | pw1nct 14036 | A condition which ensures that the powerset of a singleton is not countable. The antecedent here can be referred to as the uniformity principle. Based on Mastodon posts by Andrej Bauer and Rahul Chhabra. (Contributed by Jim Kingdon, 29-May-2024.) |
⊔ | ||
28-May-2024 | sssneq 14035 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
26-May-2024 | elpwi2 4144 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
24-May-2024 | dvmptcjx 13480 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) |
23-May-2024 | cbvralfw 2687 | Rule used to change bound variables, using implicit substitution. Version of cbvralf 2689 with a disjoint variable condition. Although we don't do so yet, we expect this disjoint variable condition will allow us to remove reliance on ax-i12 1500 and ax-bndl 1502 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by Gino Giotto, 23-May-2024.) |
22-May-2024 | efltlemlt 13489 | Lemma for eflt 13490. The converse of efltim 11661 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) |
21-May-2024 | eflt 13490 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.) |
19-May-2024 | apdifflemr 14079 | Lemma for apdiff 14080. (Contributed by Jim Kingdon, 19-May-2024.) |
# # # | ||
18-May-2024 | apdifflemf 14078 | Lemma for apdiff 14080. Being apart from the point halfway between and suffices for to be a different distance from and from . (Contributed by Jim Kingdon, 18-May-2024.) |
# # | ||
17-May-2024 | apdiff 14080 | The irrationals (reals apart from any rational) are exactly those reals that are a different distance from every rational. (Contributed by Jim Kingdon, 17-May-2024.) |
# # | ||
15-May-2024 | reeff1oleme 13487 | Lemma for reeff1o 13488. (Contributed by Jim Kingdon, 15-May-2024.) |
14-May-2024 | df-relog 13573 | Define the natural logarithm function. Defining the logarithm on complex numbers is similar to square root - there are ways to define it but they tend to make use of excluded middle. Therefore, we merely define logarithms on positive reals. See http://en.wikipedia.org/wiki/Natural_logarithm and https://en.wikipedia.org/wiki/Complex_logarithm. (Contributed by Jim Kingdon, 14-May-2024.) |
12-May-2024 | dvdstrd 11792 | The divides relation is transitive, a deduction version of dvdstr 11790. (Contributed by metakunt, 12-May-2024.) |
7-May-2024 | ioocosf1o 13569 | The cosine function is a bijection when restricted to its principal domain. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Jim Kingdon, 7-May-2024.) |
7-May-2024 | cos0pilt1 13567 | Cosine is between minus one and one on the open interval between zero and . (Contributed by Jim Kingdon, 7-May-2024.) |
6-May-2024 | cos11 13568 | Cosine is one-to-one over the closed interval from to . (Contributed by Paul Chapman, 16-Mar-2008.) (Revised by Jim Kingdon, 6-May-2024.) |
5-May-2024 | omiunct 12399 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12395 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
CCHOICE ⊔ ⊔ | ||
5-May-2024 | ctiunctal 12396 | Variation of ctiunct 12395 which allows to be present in . (Contributed by Jim Kingdon, 5-May-2024.) |
⊔ ⊔ ⊔ | ||
3-May-2024 | cc4n 7233 | Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7232, the hypotheses only require an A(n) for each value of , not a single set which suffices for every . (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
3-May-2024 | cc4f 7231 | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 3-May-2024.) |
CCHOICE | ||
1-May-2024 | cc4 7232 | Countable choice by showing the existence of a function which can choose a value at each index such that holds. (Contributed by Mario Carneiro, 7-Apr-2013.) (Revised by Jim Kingdon, 1-May-2024.) |
CCHOICE | ||
29-Apr-2024 | cc3 7230 | Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.) |
CCHOICE | ||
27-Apr-2024 | cc2 7229 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
27-Apr-2024 | cc2lem 7228 | Lemma for cc2 7229. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
27-Apr-2024 | cc1 7227 | Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
19-Apr-2024 | omctfn 12398 | Using countable choice to find a sequence of enumerations for a collection of countable sets. Lemma 8.1.27 of [AczelRathjen], p. 77. (Contributed by Jim Kingdon, 19-Apr-2024.) |
CCHOICE ⊔ ⊔ | ||
13-Apr-2024 | prodmodclem2 11540 | Lemma for prodmodc 11541. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) |
♯ DECID # | ||
11-Apr-2024 | prodmodclem2a 11539 | Lemma for prodmodc 11541. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
♯ ♯ DECID ♯ | ||
11-Apr-2024 | prodmodclem3 11538 | Lemma for prodmodc 11541. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
♯ ♯ | ||
10-Apr-2024 | jcnd 647 | Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.) |
4-Apr-2024 | prodrbdclem 11534 | Lemma for prodrbdc 11537. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) |
DECID | ||
24-Mar-2024 | prodfdivap 11510 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
24-Mar-2024 | prodfrecap 11509 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
23-Mar-2024 | prodfap0 11508 | The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.) |
# # | ||
22-Mar-2024 | prod3fmul 11504 | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.) |
21-Mar-2024 | df-proddc 11514 | Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sumdc 11317 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a nonzero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 21-Mar-2024.) |
DECID # | ||
19-Mar-2024 | cos02pilt1 13566 | Cosine is less than one between zero and . (Contributed by Jim Kingdon, 19-Mar-2024.) |
19-Mar-2024 | cosq34lt1 13565 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) |
14-Mar-2024 | coseq0q4123 13549 | Location of the zeroes of cosine in . (Contributed by Jim Kingdon, 14-Mar-2024.) |
14-Mar-2024 | cosq23lt0 13548 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) |
9-Mar-2024 | pilem3 13498 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) |
9-Mar-2024 | exmidonfin 7171 | If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 6850 and nnon 4594. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
9-Mar-2024 | exmidonfinlem 7170 | Lemma for exmidonfin 7171. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
8-Mar-2024 | sin0pilem2 13497 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
8-Mar-2024 | sin0pilem1 13496 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
7-Mar-2024 | cosz12 13495 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) |
6-Mar-2024 | cos12dec 11730 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
2-Mar-2024 | plusffvalg 12616 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.) |
25-Feb-2024 | insubm 12703 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
SubMnd SubMnd SubMnd | ||
25-Feb-2024 | mul2lt0pn 9721 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | mul2lt0np 9720 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | lt0ap0 8567 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# | ||
25-Feb-2024 | negap0d 8550 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# # | ||
24-Feb-2024 | lt0ap0d 8568 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) |
# | ||
20-Feb-2024 | ivthdec 13416 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) |
20-Feb-2024 | ivthinclemex 13414 | Lemma for ivthinc 13415. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) |
19-Feb-2024 | ivthinclemuopn 13410 | Lemma for ivthinc 13415. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) |
19-Feb-2024 | dedekindicc 13405 | A Dedekind cut identifies a unique real number. Similar to df-inp 7428 except that 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, 19-Feb-2024.) |
19-Feb-2024 | grpsubfvalg 12748 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) |
18-Feb-2024 | ivthinclemloc 13413 | Lemma for ivthinc 13415. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemdisj 13412 | Lemma for ivthinc 13415. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemur 13411 | Lemma for ivthinc 13415. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlr 13409 | Lemma for ivthinc 13415. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemum 13407 | Lemma for ivthinc 13415. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlm 13406 | Lemma for ivthinc 13415. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
17-Feb-2024 | 0subm 12702 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
SubMnd | ||
17-Feb-2024 | mndissubm 12697 | If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. (Contributed by AV, 17-Feb-2024.) |
SubMnd | ||
17-Feb-2024 | mgmsscl 12615 | If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.) |
Mgm Mgm | ||
15-Feb-2024 | dedekindicclemeu 13403 | Lemma for dedekindicc 13405. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlu 13402 | Lemma for dedekindicc 13405. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlub 13401 | Lemma for dedekindicc 13405. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemloc 13400 | Lemma for dedekindicc 13405. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemub 13399 | Lemma for dedekindicc 13405. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemuub 13398 | Lemma for dedekindicc 13405. 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 13397 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7992 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 13396 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7992 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
6-Feb-2024 | ivthinclemlopn 13408 | Lemma for ivthinc 13415. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) |
5-Feb-2024 | ivthinc 13415 | The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.) |
2-Feb-2024 | dedekindeulemuub 13389 | Lemma for dedekindeu 13395. 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 13394 | Lemma for dedekindeu 13395. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlu 13393 | Lemma for dedekindeu 13395. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlub 13392 | Lemma for dedekindeu 13395. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemloc 13391 | Lemma for dedekindeu 13395. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemub 13390 | Lemma for dedekindeu 13395. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
30-Jan-2024 | axsuploc 7992 | 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 7895 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
30-Jan-2024 | iotam 5190 | Representation of "the unique element such that " with a class expression which is inhabited (that means that "the unique element such that " exists). (Contributed by AV, 30-Jan-2024.) |
29-Jan-2024 | sgrpidmndm 12656 | A semigroup with an identity element which is inhabited is a monoid. Of course there could be monoids with the empty set as identity element, but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.) |
Smgrp | ||
24-Jan-2024 | axpre-suploclemres 7863 | Lemma for axpre-suploc 7864. 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 7771. (Contributed by Jim Kingdon, 24-Jan-2024.) |
23-Jan-2024 | ax-pre-suploc 7895 |
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 7894 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7894. (Contributed by Jim Kingdon, 23-Jan-2024.) |
23-Jan-2024 | axpre-suploc 7864 |
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 7895. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
22-Jan-2024 | suplocsr 7771 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
21-Jan-2024 | bj-el2oss1o 13809 | Shorter proof of el2oss1o 6422 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
21-Jan-2024 | ltm1sr 7739 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
20-Jan-2024 | mndinvmod 12678 | Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.) |
19-Jan-2024 | suplocsrlempr 7769 | Lemma for suplocsr 7771. The set has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
18-Jan-2024 | suplocsrlemb 7768 | Lemma for suplocsr 7771. The set is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
16-Jan-2024 | suplocsrlem 7770 | Lemma for suplocsr 7771. The set has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
14-Jan-2024 | suplocexprlemlub 7686 | Lemma for suplocexpr 7687. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
14-Jan-2024 | suplocexprlemub 7685 | Lemma for suplocexpr 7687. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
10-Jan-2024 | nfcsbw 3085 | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3086 with a disjoint variable condition. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | nfsbcdw 3083 | Version of nfsbcd 2974 with a disjoint variable condition. (Contributed by NM, 23-Nov-2005.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvcsbw 3053 | Version of cbvcsb 3054 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvsbcw 2982 | Version of cbvsbc 2983 with a disjoint variable condition. (Contributed by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvrex2vw 2708 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2710 with a disjoint variable condition, which does not require ax-13 2143. (Contributed by FL, 2-Jul-2012.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvral2vw 2707 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2709 with a disjoint variable condition, which does not require ax-13 2143. (Contributed by NM, 10-Aug-2004.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvralw 2691 | Rule used to change bound variables, using implicit substitution. Version of cbvral 2692 with a disjoint variable condition. Although we don't do so yet, we expect this disjoint variable condition will allow us to remove reliance on ax-i12 1500 and ax-bndl 1502 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbvrexfw 2688 | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2690 with a disjoint variable condition, which does not require ax-13 2143. (Contributed by FL, 27-Apr-2008.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | nfralw 2507 | Bound-variable hypothesis builder for restricted quantification. See nfralya 2510 for a version with and distinct instead of and . (Contributed by NM, 1-Sep-1999.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | nfraldw 2502 | Not-free for restricted universal quantification where and are distinct. See nfraldya 2505 for a version with and distinct instead. (Contributed by NM, 15-Feb-2013.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | nfabdw 2331 | Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2332 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by Gino Giotto, 10-Jan-2024.) |
10-Jan-2024 | cbv2w 1743 | Rule used to change bound variables, using implicit substitution. Version of cbv2 1742 with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) (Revised by Gino Giotto, 10-Jan-2024.) |
9-Jan-2024 | suplocexprlemloc 7683 | Lemma for suplocexpr 7687. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemdisj 7682 | Lemma for suplocexpr 7687. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemru 7681 | Lemma for suplocexpr 7687. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemrl 7679 | Lemma for suplocexpr 7687. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlem2b 7676 | Lemma for suplocexpr 7687. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
9-Jan-2024 | suplocexprlemell 7675 | Lemma for suplocexpr 7687. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
7-Jan-2024 | suplocexpr 7687 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemex 7684 | Lemma for suplocexpr 7687. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemmu 7680 | Lemma for suplocexpr 7687. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemml 7678 | Lemma for suplocexpr 7687. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
7-Jan-2024 | suplocexprlemss 7677 | Lemma for suplocexpr 7687. is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.) |
5-Jan-2024 | dedekindicclemicc 13404 | Lemma for dedekindicc 13405. Same as dedekindicc 13405, except that we merely show to be an element of . Later we will strengthen that to . (Contributed by Jim Kingdon, 5-Jan-2024.) |
5-Jan-2024 | dedekindeu 13395 | A Dedekind cut identifies a unique real number. Similar to df-inp 7428 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 13479 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
31-Dec-2023 | dvmptnegcn 13478 | 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 13477 | 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 4039 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
30-Dec-2023 | dvmptccn 13473 | 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 13472 | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
29-Dec-2023 | mndbn0 12667 | The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 12666). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
26-Dec-2023 | lidrididd 12636 | If there is a left and right identity element for any binary operation (group operation) , the left identity element (and therefore also the right identity element according to lidrideqd 12635) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.) |
26-Dec-2023 | lidrideqd 12635 | If there is a left and right identity element for any binary operation (group operation) , both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.) |
25-Dec-2023 | ctfoex 7095 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
⊔ | ||
23-Dec-2023 | enct 12388 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | enctlem 12387 | Lemma for enct 12388. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ ⊔ | ||
23-Dec-2023 | omct 7094 | is countable. (Contributed by Jim Kingdon, 23-Dec-2023.) |
⊔ | ||
21-Dec-2023 | dvcoapbr 13465 | 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 8566 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
19-Dec-2023 | aprcl 8565 | Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.) |
# | ||
18-Dec-2023 | limccoap 13441 | 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 10942 | Complex apartness in terms of real and imaginary parts. See also apreim 8522 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
# # # | ||
14-Dec-2023 | cnopnap 13388 | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
# | ||
14-Dec-2023 | cnovex 12990 | 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 13332 | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
# | ||
12-Dec-2023 | cnopncntop 13331 | 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 13330 | 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 13785 | Clavius law for stable formulas. See pm2.18dc 850. (Contributed by BJ, 4-Dec-2023.) |
STAB | ||
4-Dec-2023 | bj-nnclavius 13772 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
2-Dec-2023 | dvmulxx 13462 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 13460. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.) |
1-Dec-2023 | dvmulxxbr 13460 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 13462. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.) |
29-Nov-2023 | subctctexmid 14034 | 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 7131 | 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 14033 | 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 7226 | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
CCHOICE | ||
27-Nov-2023 | df-cc 7225 | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7183 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
CCHOICE | ||
26-Nov-2023 | offeq 6074 | 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 13461 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 13459. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
25-Nov-2023 | dvaddxxbr 13459 | 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 843 | Decidability of the negation of a proposition is equivalent to decidability of its double negation. See also dcn 837. The relation between dcn 837 and dcnn 843 is analogous to that between notnot 624 and notnotnot 629 (and directly stems from it). Using the notion of "testable proposition" (proposition whose negation is decidable), dcnn 843 means that a proposition is testable if and only if its negation is testable, and dcn 837 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 13796 | 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 13792 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 13779. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-dcstab 13791 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
DECID STAB | ||
24-Nov-2023 | bj-fadc 13789 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-trdc 13787 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
DECID | ||
24-Nov-2023 | bj-stal 13784 | The universal quantification of a stable formula is stable. See bj-stim 13781 for implication, stabnot 828 for negation, and bj-stan 13782 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-stand 13783 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 13782. Its proof is shorter (when counting all steps, including syntactic steps), so one could prove it first and then bj-stan 13782 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stan 13782 | The conjunction of two stable formulas is stable. See bj-stim 13781 for implication, stabnot 828 for negation, and bj-stal 13784 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB STAB | ||
24-Nov-2023 | bj-stim 13781 | A conjunction with a stable consequent is stable. See stabnot 828 for negation , bj-stan 13782 for conjunction , and bj-stal 13784 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
STAB STAB | ||
24-Nov-2023 | bj-nnbist 13779 | 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 13792). (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-fast 13776 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-trst 13774 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
STAB | ||
24-Nov-2023 | bj-nnan 13771 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | bj-nnim 13770 | 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 13768 | As far as implying a negated formula is concerned, a formula is equivalent to its double negation. (Contributed by BJ, 24-Nov-2023.) |
24-Nov-2023 | nnal 1642 | The double negation of a universal quantification implies the universal quantification of the double negation. (Contributed by BJ, 24-Nov-2023.) |
22-Nov-2023 | ofvalg 6070 | 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 7186 | The axiom of choice implies excluded middle. See acexmid 5852 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 7185 | Lemma for exmidac 7186. 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 4186 | A convenience theorem for proving that something implies EXMID. Think of this as an alternative to using a proposition, as in proofs like undifexmid 4179 or ordtriexmid 4505. In this context can be thought of as "x is true". (Contributed by Jim Kingdon, 21-Nov-2023.) |
DECID EXMID | ||
20-Nov-2023 | acfun 7184 | 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 848 |
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 | stdcn 842 | 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 837. (Contributed by BJ, 18-Nov-2023.) |
STAB DECID DECID | ||
17-Nov-2023 | cnplimclemr 13432 | Lemma for cnplimccntop 13433. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾t lim | ||
17-Nov-2023 | cnplimclemle 13431 | Lemma for cnplimccntop 13433. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
↾t lim # | ||
14-Nov-2023 | limccnp2cntop 13440 | 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 11187 | The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.) |
9-Nov-2023 | limccnp2lem 13439 | Lemma for limccnp2cntop 13440. This is most of the result, expressed in epsilon-delta form, with a large number of hypotheses so that lengthy expressions do not need to be repeated. (Contributed by Jim Kingdon, 9-Nov-2023.) |
↾t lim lim # # # | ||
4-Nov-2023 | ellimc3apf 13423 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.) |
lim # | ||
3-Nov-2023 | limcmpted 13426 | Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.) |
lim # | ||
1-Nov-2023 | unct 12397 | The union of two countable sets is countable. Corollary 8.1.20 of [AczelRathjen], p. 75. (Contributed by Jim Kingdon, 1-Nov-2023.) |
⊔ ⊔ ⊔ | ||
31-Oct-2023 | ctiunct 12395 |
A sequence of enumerations gives an enumeration of the union. We refer
to "sequence of enumerations" rather than "countably many
countable
sets" because the hypothesis provides more than countability for
each
: it refers to together with the
which enumerates it. Theorem 8.1.19 of [AczelRathjen], p. 74.
For "countably many countable sets" the key hypothesis would be ⊔ . This is almost omiunct 12399 (which uses countable choice) although that is for a countably infinite collection not any countable collection. Compare with the case of two sets instead of countably many, as seen at unct 12397, which says that the union of two countable sets is countable . The proof proceeds by mapping a natural number to a pair of natural numbers (by xpomen 12350) and using the first number to map to an element of and the second number to map to an element of B(x) . In this way we are able to map to every element of . Although it would be possible to work directly with countability expressed as ⊔ , we instead use functions from subsets of the natural numbers via ctssdccl 7088 and ctssdc 7090. (Contributed by Jim Kingdon, 31-Oct-2023.) |
⊔ ⊔ ⊔ | ||
30-Oct-2023 | ctssdccl 7088 | A mapping from a decidable subset of the natural numbers onto a countable set. This is similar to one direction of ctssdc 7090 but expressed in terms of classes rather than . (Contributed by Jim Kingdon, 30-Oct-2023.) |
⊔ inl inl DECID | ||
28-Oct-2023 | ctiunctlemfo 12394 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemf 12393 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemudc 12392 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID DECID | ||
28-Oct-2023 | ctiunctlemuom 12391 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemu2nd 12390 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | ctiunctlemu1st 12389 | Lemma for ctiunct 12395. (Contributed by Jim Kingdon, 28-Oct-2023.) |
DECID DECID | ||
28-Oct-2023 | pm2.521gdc 863 | A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107, under a decidability condition. (Contributed by BJ, 28-Oct-2023.) |
DECID | ||
28-Oct-2023 | stdcndc 840 | A formula is decidable if and only if its negation is decidable and it is stable (that is, it is testable and stable). (Contributed by David A. Wheeler, 13-Aug-2018.) (Proof shortened by BJ, 28-Oct-2023.) |
STAB DECID DECID | ||
28-Oct-2023 | conax1k 649 | Weakening of conax1 648. General instance of pm2.51 650 and of pm2.52 651. (Contributed by BJ, 28-Oct-2023.) |
28-Oct-2023 | conax1 648 | Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.) |
25-Oct-2023 | divcnap 13349 | Complex number division is a continuous function, when the second argument is apart from zero. (Contributed by Mario Carneiro, 12-Aug-2014.) (Revised by Jim Kingdon, 25-Oct-2023.) |
↾t # # | ||
23-Oct-2023 | cnm 7794 | A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.) |
23-Oct-2023 | oprssdmm 6150 | Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.) |
22-Oct-2023 | addcncntoplem 13345 | Lemma for addcncntop 13346, subcncntop 13347, and mulcncntop 13348. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
22-Oct-2023 | txmetcnp 13312 | Continuity of a binary operation on metric spaces. (Contributed by Mario Carneiro, 2-Sep-2015.) (Revised by Jim Kingdon, 22-Oct-2023.) |
22-Oct-2023 | xmetxpbl 13302 | The maximum metric (Chebyshev distance) on the product of two sets, expressed in terms of balls centered on a point with radius . (Contributed by Jim Kingdon, 22-Oct-2023.) |
15-Oct-2023 | xmettxlem 13303 | Lemma for xmettx 13304. (Contributed by Jim Kingdon, 15-Oct-2023.) |
11-Oct-2023 | xmettx 13304 | The maximum metric (Chebyshev distance) on the product of two sets, expressed as a binary topological product. (Contributed by Jim Kingdon, 11-Oct-2023.) |
11-Oct-2023 | xmetxp 13301 | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
29-Sep-2023 | syl2anc2 410 | Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.) |
12-Sep-2023 | pwntru 4185 | A slight strengthening of pwtrufal 14030. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) |
11-Sep-2023 | pwtrufal 14030 | A subset of the singleton cannot be anything other than or . Removing the double negation would change the meaning, as seen at exmid01 4184. If we view a subset of a singleton as a truth value (as seen in theorems like exmidexmid 4182), then this theorem states there are no truth values other than true and false, as described in section 1.1 of [Bauer], p. 481. (Contributed by Mario Carneiro and Jim Kingdon, 11-Sep-2023.) |
9-Sep-2023 | mathbox 13767 |
(This theorem is a dummy placeholder for these guidelines. The label
of this theorem, "mathbox", is hard-coded into the Metamath
program to
identify the start of the mathbox section for web page generation.)
A "mathbox" is a user-contributed section that is maintained by its contributor independently from the main part of iset.mm. For contributors: By making a contribution, you agree to release it into the public domain, according to the statement at the beginning of iset.mm. Guidelines: Mathboxes in iset.mm follow the same practices as in set.mm, so refer to the mathbox guidelines there for more details. (Contributed by NM, 20-Feb-2007.) (Revised by the Metamath team, 9-Sep-2023.) (New usage is discouraged.) |
6-Sep-2023 | djuexb 7021 | The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023.) |
⊔ | ||
3-Sep-2023 | pwf1oexmid 14032 | An exercise related to copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
EXMID | ||
3-Sep-2023 | pwle2 14031 | An exercise related to copies of a singleton and the power set of a singleton (where the latter can also be thought of as representing truth values). Posed as an exercise by Martin Escardo online. (Contributed by Jim Kingdon, 3-Sep-2023.) |
30-Aug-2023 | isomninn 14063 | Omniscience stated in terms of natural numbers. Similar to isomnimap 7113 but it will sometimes be more convenient to use and rather than and . (Contributed by Jim Kingdon, 30-Aug-2023.) |
Omni | ||
30-Aug-2023 | isomninnlem 14062 | Lemma for isomninn 14063. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
frec Omni | ||
28-Aug-2023 | trilpolemisumle 14070 | Lemma for trilpo 14075. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
25-Aug-2023 | cvgcmp2n 14065 | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
25-Aug-2023 | cvgcmp2nlemabs 14064 | Lemma for cvgcmp2n 14065. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting as the sum of and a term which gets smaller as gets large. (Contributed by Jim Kingdon, 25-Aug-2023.) |
24-Aug-2023 | trilpolemclim 14068 | Lemma for trilpo 14075. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
23-Aug-2023 | trilpo 14075 |
Real number trichotomy implies the Limited Principle of Omniscience
(LPO). We expect that we'd need some form of countable choice to prove
the converse.
Here's the outline of the proof. Given an infinite sequence F of zeroes and ones, we need to show the sequence contains a zero or it is all ones. Construct a real number A whose representation in base two consists of a zero, a decimal point, and then the numbers of the sequence. Compare it with one using trichotomy. The three cases from trichotomy are trilpolemlt1 14073 (which means the sequence contains a zero), trilpolemeq1 14072 (which means the sequence is all ones), and trilpolemgt1 14071 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 14061) or that the real numbers are a discrete field (see trirec0 14076). LPO is known to not be provable in IZF (and most constructive foundations), so this theorem establishes that we will be unable to prove an analogue to qtri3or 10199 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.) |
Omni | ||
23-Aug-2023 | trilpolemres 14074 | Lemma for trilpo 14075. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemlt1 14073 | Lemma for trilpo 14075. The case. We can use the distance between and one (that is, ) to find a position in the sequence where terms after that point will not add up to as much as . By finomni 7116 we know the terms up to either contain a zero or are all one. But if they are all one that contradicts the way we constructed , so we know that the sequence contains a zero. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemeq1 14072 | Lemma for trilpo 14075. The case. This is proved by noting that if any is zero, then the infinite sum is less than one based on the term which is zero. We are using the fact that the sequence is decidable (in the sense that each element is either zero or one). (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemgt1 14071 | Lemma for trilpo 14075. The case. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | trilpolemcl 14069 | Lemma for trilpo 14075. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
23-Aug-2023 | triap 14061 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
DECID # | ||
19-Aug-2023 | djuenun 7189 | Disjoint union is equinumerous to union for disjoint sets. (Contributed by Mario Carneiro, 29-Apr-2015.) (Revised by Jim Kingdon, 19-Aug-2023.) |
⊔ | ||
16-Aug-2023 | ctssdclemr 7089 | Lemma for ctssdc 7090. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
⊔ DECID | ||
16-Aug-2023 | ctssdclemn0 7087 | Lemma for ctssdc 7090. The case. (Contributed by Jim Kingdon, 16-Aug-2023.) |
DECID ⊔ | ||
15-Aug-2023 | ctssexmid 7126 | The decidability condition in ctssdc 7090 is needed. More specifically, ctssdc 7090 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
⊔ Omni | ||
15-Aug-2023 | ctssdc 7090 | A set is countable iff there is a surjection from a decidable subset of the natural numbers onto it. The decidability condition is needed as shown at ctssexmid 7126. (Contributed by Jim Kingdon, 15-Aug-2023.) |
DECID ⊔ | ||
14-Aug-2023 | mpoexw 6192 | Weak version of mpoex 6193 that holds without ax-coll 4104. If the domain and codomain of an operation given by maps-to notation are sets, the operation is a set. (Contributed by Rohan Ridenour, 14-Aug-2023.) |
13-Aug-2023 | grpinvfvalg 12745 | The inverse function of a group. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Revised by Rohan Ridenour, 13-Aug-2023.) |
13-Aug-2023 | ltntri 8047 | Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, . Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.) |
13-Aug-2023 | mptexw 6092 | Weak version of mptex 5722 that holds without ax-coll 4104. If the domain and codomain of a function given by maps-to notation are sets, the function is a set. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
13-Aug-2023 | funexw 6091 | Weak version of funex 5719 that holds without ax-coll 4104. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
11-Aug-2023 | qnnen 12386 | The rational numbers are countably infinite. Corollary 8.1.23 of [AczelRathjen], p. 75. This is Metamath 100 proof #3. (Contributed by Jim Kingdon, 11-Aug-2023.) |
10-Aug-2023 | ctinfomlemom 12382 | Lemma for ctinfom 12383. Converting between and . (Contributed by Jim Kingdon, 10-Aug-2023.) |
frec | ||
9-Aug-2023 | difinfsnlem 7076 | Lemma for difinfsn 7077. The case where we need to swap and inr in building the mapping . (Contributed by Jim Kingdon, 9-Aug-2023.) |
DECID ⊔ inr inl inr inl | ||
8-Aug-2023 | difinfinf 7078 | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
8-Aug-2023 | difinfsn 7077 | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
DECID | ||
7-Aug-2023 | ctinf 12385 | A set is countably infinite if and only if it has decidable equality, is countable, and is infinite. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
7-Aug-2023 | inffinp1 12384 | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
7-Aug-2023 | ctinfom 12383 | A condition for a set being countably infinite. Restates ennnfone 12380 in terms of and function image. Like ennnfone 12380 the condition can be summarized as being countable, infinite, and having decidable equality. (Contributed by Jim Kingdon, 7-Aug-2023.) |
DECID | ||
6-Aug-2023 | rerestcntop 13344 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
↾t ↾t | ||
6-Aug-2023 | tgioo2cntop 13343 | The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
↾t | ||
4-Aug-2023 | nninffeq 14053 | Equality of two functions on ℕ∞ which agree at every integer and at the point at infinity. From an online post by Martin Escardo. Remark: the last two hypotheses can be grouped into one, . (Contributed by Jim Kingdon, 4-Aug-2023.) |
ℕ∞ ℕ∞ | ||
3-Aug-2023 | txvalex 13048 | Existence of the binary topological product. If and are known to be topologies, see txtop 13054. (Contributed by Jim Kingdon, 3-Aug-2023.) |
3-Aug-2023 | hashfingrpnn 12739 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
♯ | ||
3-Aug-2023 | hashfinmndnn 12668 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
♯ | ||
3-Aug-2023 | dvdsgcdidd 11949 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | gcdmultipled 11948 | The greatest common divisor of a nonnegative integer and a multiple of it is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | fihashelne0d 10732 | A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
♯ | ||
3-Aug-2023 | phpeqd 6910 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6843 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | enpr2d 6795 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | elrnmpt2d 4866 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | elrnmptdv 4865 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | rspcime 2841 | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
3-Aug-2023 | neqcomd 2175 | Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
2-Aug-2023 | dvid 13456 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
2-Aug-2023 | dvconst 13455 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
2-Aug-2023 | dvidlemap 13454 | Lemma for dvid 13456 and dvconst 13455. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
# | ||
2-Aug-2023 | diveqap1bd 8753 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8622. Converse of diveqap1d 8715. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.) |
# | ||
31-Jul-2023 | mul0inf 11204 | Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11026 and mulap0bd 8575 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.) |
inf | ||
31-Jul-2023 | mul0eqap 8588 | If two numbers are apart from each other and their product is zero, one of them must be zero. (Contributed by Jim Kingdon, 31-Jul-2023.) |
# | ||
31-Jul-2023 | apcon4bid 8543 | Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.) |
# # | ||
30-Jul-2023 | uzennn 10392 | An upper integer set is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 30-Jul-2023.) |
30-Jul-2023 | djuen 7188 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ ⊔ | ||
30-Jul-2023 | endjudisj 7187 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
⊔ | ||
30-Jul-2023 | eninr 7075 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inr | ||
30-Jul-2023 | eninl 7074 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
inl | ||
29-Jul-2023 | exmidunben 12381 | If any unbounded set of positive integers is equinumerous to , then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.) |
Omni EXMID | ||
29-Jul-2023 | exmidsssnc 4189 | Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4184 but lets you choose any set as the element of the singleton rather than just . It is similar to exmidsssn 4188 but for a particular set rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.) |
EXMID | ||
28-Jul-2023 | dvfcnpm 13453 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.) |
28-Jul-2023 | dvfpm 13452 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.) |
23-Jul-2023 | ennnfonelemhdmp1 12364 | Lemma for ennnfone 12380. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
23-Jul-2023 | ennnfonelemp1 12361 | Lemma for ennnfone 12380. Value of at a successor. (Contributed by Jim Kingdon, 23-Jul-2023.) |
DECID frec | ||
22-Jul-2023 | nntr2 6482 | Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.) |
22-Jul-2023 | nnsssuc 6481 | A natural number is a subset of another natural number if and only if it belongs to its successor. (Contributed by Jim Kingdon, 22-Jul-2023.) |
21-Jul-2023 | ennnfoneleminc 12366 | Lemma for ennnfone 12380. We only add elements to as the index increases. (Contributed by Jim Kingdon, 21-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemg 12358 | Lemma for ennnfone 12380. Closure for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemjn 12357 | Lemma for ennnfone 12380. Non-initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | ennnfonelemj0 12356 | Lemma for ennnfone 12380. Initial state for . (Contributed by Jim Kingdon, 20-Jul-2023.) |
DECID frec | ||
20-Jul-2023 | seqp1cd 10422 | Value of the sequence builder function at a successor. A version of seq3p1 10418 which provides two classes and for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 20-Jul-2023.) |
20-Jul-2023 | seqovcd 10419 | A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10420 and seq1cd 10421 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.) |
19-Jul-2023 | ennnfonelemhom 12370 | Lemma for ennnfone 12380. The sequences in increase in length without bound if you go out far enough. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemex 12369 | Lemma for ennnfone 12380. Extending the sequence to include an additional element. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemkh 12367 | Lemma for ennnfone 12380. Because we add zero or one entries for each new index, the length of each sequence is no greater than its index. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelemom 12363 | Lemma for ennnfone 12380. yields finite sequences. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | ennnfonelem1 12362 | Lemma for ennnfone 12380. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
DECID frec | ||
19-Jul-2023 | seq1cd 10421 | Initial value of the recursive sequence builder. A version of seq3-1 10416 which provides two classes and for the terms and the value being accumulated, respectively. (Contributed by Jim Kingdon, 19-Jul-2023.) |
17-Jul-2023 | ennnfonelemhf1o 12368 | Lemma for ennnfone 12380. Each of the functions in is one to one and onto an image of . (Contributed by Jim Kingdon, 17-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemen 12376 | Lemma for ennnfone 12380. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemdm 12375 | Lemma for ennnfone 12380. The function is defined everywhere. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemrn 12374 | Lemma for ennnfone 12380. is onto . (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemf1 12373 | Lemma for ennnfone 12380. is one-to-one. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemfun 12372 | Lemma for ennnfone 12380. is a function. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
16-Jul-2023 | ennnfonelemrnh 12371 | Lemma for ennnfone 12380. A consequence of ennnfonelemss 12365. (Contributed by Jim Kingdon, 16-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelemss 12365 | Lemma for ennnfone 12380. We only add elements to as the index increases. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelem0 12360 | Lemma for ennnfone 12380. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID frec | ||
15-Jul-2023 | ennnfonelemk 12355 | Lemma for ennnfone 12380. (Contributed by Jim Kingdon, 15-Jul-2023.) |
15-Jul-2023 | ennnfonelemdc 12354 | Lemma for ennnfone 12380. A direct consequence of fidcenumlemrk 6931. (Contributed by Jim Kingdon, 15-Jul-2023.) |
DECID DECID | ||
14-Jul-2023 | djur 7046 | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) |
⊔ inl inr | ||
13-Jul-2023 | sbthomlem 14057 | Lemma for sbthom 14058. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) |
Omni ⊔ | ||
12-Jul-2023 | caseinr 7069 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) |
case inr | ||
12-Jul-2023 | inl11 7042 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) |
inl inl | ||
11-Jul-2023 | djudomr 7197 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
11-Jul-2023 | djudoml 7196 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) |
⊔ | ||
11-Jul-2023 | omp1eomlem 7071 | Lemma for omp1eom 7072. (Contributed by Jim Kingdon, 11-Jul-2023.) |
inr inl case ⊔ | ||
11-Jul-2023 | xp01disjl 6413 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) |
10-Jul-2023 | sbthom 14058 | Schroeder-Bernstein is not possible even for . We know by exmidsbth 14056 that full Schroeder-Bernstein will not be provable but what about the case where one of the sets is ? That case plus the Limited Principle of Omniscience (LPO) implies excluded middle, so we will not be able to prove it. (Contributed by Mario Carneiro and Jim Kingdon, 10-Jul-2023.) |
Omni EXMID | ||
10-Jul-2023 | endjusym 7073 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ ⊔ | ||
10-Jul-2023 | omp1eom 7072 | Adding one to . (Contributed by Jim Kingdon, 10-Jul-2023.) |
⊔ | ||
9-Jul-2023 | refeq 14060 | Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.) |
9-Jul-2023 | seqvalcd 10415 | Value of the sequence builder function. Similar to seq3val 10414 but the classes (type of each term) and (type of the value we are accumulating) do not need to be the same. (Contributed by Jim Kingdon, 9-Jul-2023.) |
frec | ||
9-Jul-2023 | djuun 7044 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr ⊔ | ||
9-Jul-2023 | djuin 7041 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) |
inl inr | ||
8-Jul-2023 | limcimo 13428 | Conditions which ensure there is at most one limit value of at . (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 8-Jul-2023.) |
↾t # lim | ||
8-Jul-2023 | ennnfonelemh 12359 | Lemma for ennnfone 12380. (Contributed by Jim Kingdon, 8-Jul-2023.) |
DECID frec | ||
7-Jul-2023 | seqf2 10420 | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 7-Jul-2023.) |
3-Jul-2023 | limcimolemlt 13427 | Lemma for limcimo 13428. (Contributed by Jim Kingdon, 3-Jul-2023.) |
↾t # lim lim # # | ||
28-Jun-2023 | dvfgg 13451 | Explicitly write out the functionality condition on derivative for and . (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jun-2023.) |
28-Jun-2023 | dvbsssg 13449 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.) |
27-Jun-2023 | dvbssntrcntop 13447 | The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t | ||
27-Jun-2023 | eldvap 13445 | The differentiable predicate. A function is differentiable at with derivative iff is defined in a neighborhood of and the difference quotient has limit at . (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t # lim | ||
27-Jun-2023 | dvfvalap 13444 | Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
↾t # lim | ||
27-Jun-2023 | dvlemap 13443 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) |
# | ||
25-Jun-2023 | reldvg 13442 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.) |
25-Jun-2023 | df-dvap 13420 | Define the derivative operator. This acts on functions to produce a function that is defined where the original function is differentiable, with value the derivative of the function at these points. The set here is the ambient topological space under which we are evaluating the continuity of the difference quotient. Although the definition is valid for any subset of and is well-behaved when contains no isolated points, we will restrict our attention to the cases or for the majority of the development, these corresponding respectively to real and complex differentiation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.) |
↾t # lim | ||
18-Jun-2023 | limccnpcntop 13438 | If the limit of at is and is continuous at , then the limit of at is . (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 18-Jun-2023.) |
↾t lim lim | ||
18-Jun-2023 | r19.30dc 2617 | Restricted quantifier version of 19.30dc 1620. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) |
DECID | ||
17-Jun-2023 | r19.28v 2598 | Restricted quantifier version of one direction of 19.28 1556. (The other direction holds when is inhabited, see r19.28mv 3507.) (Contributed by NM, 2-Apr-2004.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
17-Jun-2023 | r19.27v 2597 | Restricted quantitifer version of one direction of 19.27 1554. (The other direction holds when is inhabited, see r19.27mv 3511.) (Contributed by NM, 3-Jun-2004.) (Proof shortened by Andrew Salmon, 30-May-2011.) (Proof shortened by Wolf Lammen, 17-Jun-2023.) |
16-Jun-2023 | cnlimcim 13434 | If is a continuous function, the limit of the function at each point equals the value of the function. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 16-Jun-2023.) |
lim | ||
16-Jun-2023 | cncfcn1cntop 13375 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.) |
14-Jun-2023 | cnplimcim 13430 | If a function is continuous at , its limit at equals the value of the function there. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 14-Jun-2023.) |
↾t lim | ||
14-Jun-2023 | metcnpd 13314 | Two ways to say a mapping from metric to metric is continuous at point . (Contributed by Jim Kingdon, 14-Jun-2023.) |
6-Jun-2023 | cntoptop 13327 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
6-Jun-2023 | cntoptopon 13326 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) |
TopOn | ||
3-Jun-2023 | limcdifap 13425 | It suffices to consider functions which are not defined at to define the limit of a function. In particular, the value of the original function at does not affect the limit of . (Contributed by Mario Carneiro, 25-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # lim | ||
3-Jun-2023 | ellimc3ap 13424 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # | ||
3-Jun-2023 | df-limced 13419 | Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.) |
lim # | ||
30-May-2023 | modprm1div 12201 | A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.) |
30-May-2023 | modm1div 11762 | An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.) |
30-May-2023 | eluz4nn 9527 | An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.) |
30-May-2023 | eluz4eluz2 9526 | An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.) |
29-May-2023 | mulcncflem 13384 | Lemma for mulcncf 13385. (Contributed by Jim Kingdon, 29-May-2023.) |
26-May-2023 | cdivcncfap 13381 | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.) |
# # | ||
26-May-2023 | reccn2ap 11276 | The reciprocal function is continuous. The class is just for convenience in writing the proof and typically would be passed in as an instance of eqid 2170. (Contributed by Mario Carneiro, 9-Feb-2014.) Using apart, infimum of pair. (Revised by Jim Kingdon, 26-May-2023.) |
inf # # | ||
23-May-2023 | iooretopg 13322 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.) |
23-May-2023 | minclpr 11200 | The minimum of two real numbers is one of those numbers if and only if dichotomy ( ) holds. For example, this can be combined with zletric 9256 if one is dealing with integers, but real number dichotomy in general does not follow from our axioms. (Contributed by Jim Kingdon, 23-May-2023.) |
inf | ||
22-May-2023 | qtopbasss 13315 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.) |
inf | ||
22-May-2023 | iooinsup 11240 | Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.) |
inf | ||
21-May-2023 | df-sumdc 11317 | Define the sum of a series with an index set of integers . The variable is normally a free variable in , i.e., can be thought of as . This definition is the result of a collection of discussions over the most general definition for a sum that does not need the index set to have a specified ordering. This definition is in two parts, one for finite sums and one for subsets of the upper integers. When summing over a subset of the upper integers, we extend the index set to the upper integers by adding zero outside the domain, and then sum the set in order, setting the result to the limit of the partial sums, if it exists. This means that conditionally convergent sums can be evaluated meaningfully. For finite sums, we are explicitly order-independent, by picking any bijection to a 1-based finite sequence and summing in the induced order. In both cases we have an expression so that we only need to be defined where . In the infinite case, we also require that the indexing set be a decidable subset of an upperset of integers (that is, membership of integers in it is decidable). These two methods of summation produce the same result on their common region of definition (i.e., finite sets of integers). Examples: means , and means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 11485). (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 21-May-2023.) |
DECID | ||
19-May-2023 | bdmopn 13298 | The standard bounded metric corresponding to generates the same topology as . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | bdbl 13297 | The standard bounded metric corresponding to generates the same balls as for radii less than . (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | bdmet 13296 | The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | xrminltinf 11235 | Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.) |
inf | ||
19-May-2023 | clel5 2867 | Alternate definition of class membership: a class is an element of another class iff there is an element of equal to . (Contributed by AV, 13-Nov-2020.) (Revised by Steven Nguyen, 19-May-2023.) |
18-May-2023 | xrminrecl 11236 | The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.) |
inf inf | ||
18-May-2023 | ralnex2 2609 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.) |
17-May-2023 | bdtrilem 11202 | Lemma for bdtri 11203. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.) |
15-May-2023 | xrbdtri 11239 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) |
inf inf inf | ||
15-May-2023 | bdtri 11203 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) |
inf inf inf | ||
15-May-2023 | minabs 11199 | The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.) |
inf | ||
11-May-2023 | xrmaxadd 11224 | Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.) |
11-May-2023 | xrmaxaddlem 11223 | Lemma for xrmaxadd 11224. The case where is real. (Contributed by Jim Kingdon, 11-May-2023.) |
10-May-2023 | xrminadd 11238 | Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.) |
inf inf | ||
10-May-2023 | xrmaxlesup 11222 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 10-May-2023.) |
10-May-2023 | xrltmaxsup 11220 | The maximum as a least upper bound. (Contributed by Jim Kingdon, 10-May-2023.) |
9-May-2023 | bdxmet 13295 | The standard bounded metric is an extended metric given an extended metric and a positive extended real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
inf | ||
9-May-2023 | bdmetval 13294 | Value of the standard bounded metric. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 9-May-2023.) |
inf inf | ||
7-May-2023 | setsmstsetg 13275 | The topology of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015.) (Revised by Jim Kingdon, 7-May-2023.) |
sSet TopSet TopSet | ||
6-May-2023 | dsslid 12578 | Slot property of . (Contributed by Jim Kingdon, 6-May-2023.) |
Slot | ||
5-May-2023 | mopnrel 13235 | The class of open sets of a metric space is a relation. (Contributed by Jim Kingdon, 5-May-2023.) |
5-May-2023 | fsumsersdc 11358 | Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013.) (Revised by Jim Kingdon, 5-May-2023.) |
DECID | ||
4-May-2023 | blex 13181 | A ball is a set. (Contributed by Jim Kingdon, 4-May-2023.) |
4-May-2023 | summodc 11346 | A sum has at most one limit. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
♯ ♯ DECID | ||
4-May-2023 | summodclem2 11345 | Lemma for summodc 11346. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
♯ DECID | ||
4-May-2023 | xrminrpcl 11237 | The minimum of two positive reals is a positive real. (Contributed by Jim Kingdon, 4-May-2023.) |
inf | ||
4-May-2023 | xrlemininf 11234 | Two ways of saying a number is less than or equal to the minimum of two others. (Contributed by Mario Carneiro, 18-Jun-2014.) (Revised by Jim Kingdon, 4-May-2023.) |
inf | ||
3-May-2023 | xrltmininf 11233 | Two ways of saying an extended real is less than the minimum of two others. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmineqinf 11232 | The minimum of two extended reals is equal to the second if the first is bigger. (Contributed by Mario Carneiro, 25-Mar-2015.) (Revised by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmin2inf 11231 | The minimum of two extended reals is less than or equal to the second. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmin1inf 11230 | The minimum of two extended reals is less than or equal to the first. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
3-May-2023 | xrmincl 11229 | The minumum of two extended reals is an extended real. (Contributed by Jim Kingdon, 3-May-2023.) |
inf | ||
2-May-2023 | xrminmax 11228 | Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 2-May-2023.) |
inf | ||
2-May-2023 | xrnegcon1d 11227 | Contraposition law for extended real unary minus. (Contributed by Jim Kingdon, 2-May-2023.) |
2-May-2023 | infxrnegsupex 11226 | The infimum of a set of extended reals is the negative of the supremum of the negatives of its elements. (Contributed by Jim Kingdon, 2-May-2023.) |
inf | ||
2-May-2023 | xrnegiso 11225 | Negation is an order anti-isomorphism of the extended reals, which is its own inverse. (Contributed by Jim Kingdon, 2-May-2023.) |
30-Apr-2023 | xrmaxltsup 11221 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmaxrecl 11218 | The maximum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmax2sup 11217 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.) |
30-Apr-2023 | xrmax1sup 11216 | An extended real is less than or equal to the maximum of it and another. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 30-Apr-2023.) |
29-Apr-2023 | xrmaxcl 11215 | The maximum of two extended reals is an extended real. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemval 11213 | Lemma for xrmaxif 11214. Value of the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemcom 11212 | Lemma for xrmaxif 11214. Commutativity of an expression which we will later show to be the supremum. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | xrmaxiflemcl 11208 | Lemma for xrmaxif 11214. Closure. (Contributed by Jim Kingdon, 29-Apr-2023.) |
29-Apr-2023 | sbco2v 1941 | Version of sbco2 1958 with disjoint variable conditions. (Contributed by Wolf Lammen, 29-Apr-2023.) |
28-Apr-2023 | xrmaxiflemlub 11211 | Lemma for xrmaxif 11214. A least upper bound for . (Contributed by Jim Kingdon, 28-Apr-2023.) |
26-Apr-2023 | xrmaxif 11214 | Maximum of two extended reals in terms of expressions. (Contributed by Jim Kingdon, 26-Apr-2023.) |
26-Apr-2023 | xrmaxiflemab 11210 | Lemma for xrmaxif 11214. A variation of xrmaxleim 11207- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 26-Apr-2023.) |
26-Apr-2023 | xrmaxifle 11209 | An upper bound for in the extended reals. (Contributed by Jim Kingdon, 26-Apr-2023.) |
25-Apr-2023 | xrmaxleim 11207 | Value of maximum when we know which extended real is larger. (Contributed by Jim Kingdon, 25-Apr-2023.) |
25-Apr-2023 | rpmincl 11201 | The minumum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 25-Apr-2023.) |
inf | ||
25-Apr-2023 | mincl 11194 | The minumum of two real numbers is a real number. (Contributed by Jim Kingdon, 25-Apr-2023.) |
inf | ||
24-Apr-2023 | psmetrel 13116 | The class of pseudometrics is a relation. (Contributed by Jim Kingdon, 24-Apr-2023.) |
PsMet | ||
23-Apr-2023 | bcval5 10697 | Write out the top and bottom parts of the binomial coefficient explicitly. In this form, it is valid even for , although it is no longer valid for nonpositive . (Contributed by Mario Carneiro, 22-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | ser3le 10474 | Comparison of partial sums of two infinite series of reals. (Contributed by NM, 27-Dec-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3z 10467 | If the operation has an absorbing element (a.k.a. zero element), then any sequence containing a evaluates to . (Contributed by Mario Carneiro, 27-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3caopr 10439 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 23-Apr-2023.) |
23-Apr-2023 | seq3caopr2 10438 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Mario Carneiro, 30-May-2014.) (Revised by Jim Kingdon, 23-Apr-2023.) |
22-Apr-2023 | ser3sub 10462 | The difference of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
22-Apr-2023 | seq3caopr3 10437 | Lemma for seq3caopr2 10438. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by Jim Kingdon, 22-Apr-2023.) |
..^ | ||
22-Apr-2023 | ser3mono 10434 | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 22-Apr-2023.) |
21-Apr-2023 | metrtri 13171 | Reverse triangle inequality for the distance function of a metric space. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 21-Apr-2023.) |
21-Apr-2023 | sqxpeq0 5034 | A Cartesian square is empty iff its member is empty. (Contributed by Jim Kingdon, 21-Apr-2023.) |
20-Apr-2023 | xmetrel 13137 | The class of extended metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.) |
20-Apr-2023 | metrel 13136 | The class of metrics is a relation. (Contributed by Jim Kingdon, 20-Apr-2023.) |
19-Apr-2023 | psmetge0 13125 | The distance function of a pseudometric space is nonnegative. (Contributed by Thierry Arnoux, 7-Feb-2018.) (Revised by Jim Kingdon, 19-Apr-2023.) |
PsMet | ||
18-Apr-2023 | xleaddadd 9844 | Cancelling a factor of two in (expressed as addition rather than as a factor to avoid extended real multiplication). (Contributed by Jim Kingdon, 18-Apr-2023.) |
17-Apr-2023 | xposdif 9839 | Extended real version of posdif 8374. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.) |
17-Apr-2023 | nmnfgt 9775 | An extended real is greater than minus infinite iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.) |
17-Apr-2023 | npnflt 9772 | An extended real is less than plus infinity iff they are not equal. (Contributed by Jim Kingdon, 17-Apr-2023.) |
16-Apr-2023 | xltadd1 9833 | Extended real version of ltadd1 8348. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.) |
13-Apr-2023 | xrmnfdc 9800 | An extended real is or is not minus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.) |
DECID | ||
13-Apr-2023 | xrpnfdc 9799 | An extended real is or is not plus infinity. (Contributed by Jim Kingdon, 13-Apr-2023.) |
DECID | ||
11-Apr-2023 | dmxpid 4832 | The domain of a square Cartesian product. (Contributed by NM, 28-Jul-1995.) (Revised by Jim Kingdon, 11-Apr-2023.) |
9-Apr-2023 | isumz 11352 | Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID | ||
9-Apr-2023 | summodclem2a 11344 | Lemma for summodc 11346. (Contributed by Mario Carneiro, 3-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID ♯ ♯ | ||
9-Apr-2023 | summodclem3 11343 | Lemma for summodc 11346. (Contributed by Mario Carneiro, 29-Mar-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
9-Apr-2023 | sumrbdc 11342 | Rebase the starting point of a sum. (Contributed by Mario Carneiro, 14-Jul-2013.) (Revised by Jim Kingdon, 9-Apr-2023.) |
DECID DECID | ||
9-Apr-2023 | seq3coll 10777 | The function contains a sparse set of nonzero values to be summed. The function is an order isomorphism from the set of nonzero values of to a 1-based finite sequence, and collects these nonzero values together. Under these conditions, the sum over the values in yields the same result as the sum over the original set . (Contributed by Mario Carneiro, 2-Apr-2014.) (Revised by Jim Kingdon, 9-Apr-2023.) |
♯ ♯ ♯ ♯ | ||
8-Apr-2023 | zsumdc 11347 | Series sum with index set a subset of the upper integers. (Contributed by Mario Carneiro, 13-Jun-2019.) (Revised by Jim Kingdon, 8-Apr-2023.) |
DECID | ||
8-Apr-2023 | sumrbdclem 11340 | Lemma for sumrbdc 11342. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 8-Apr-2023.) |
DECID | ||
8-Apr-2023 | isermulc2 11303 | Multiplication of an infinite series by a constant. (Contributed by Paul Chapman, 14-Nov-2007.) (Revised by Jim Kingdon, 8-Apr-2023.) |
8-Apr-2023 | seq3id 10464 | Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for ) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 8-Apr-2023.) |
8-Apr-2023 | seq3id3 10463 | A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a -idempotent sums (or "'s") to that element. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Jim Kingdon, 8-Apr-2023.) |
7-Apr-2023 | seq3shft2 10429 | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
7-Apr-2023 | seq3feq 10428 | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) (Revised by Jim Kingdon, 7-Apr-2023.) |
7-Apr-2023 | r19.2m 3501 | Theorem 19.2 of [Margaris] p. 89 with restricted quantifiers (compare 19.2 1631). The restricted version is valid only when the domain of quantification is inhabited. (Contributed by Jim Kingdon, 5-Aug-2018.) (Revised by Jim Kingdon, 7-Apr-2023.) |
6-Apr-2023 | lmtopcnp 13044 | The image of a convergent sequence under a continuous map is convergent to the image of the original point. (Contributed by Mario Carneiro, 3-May-2014.) (Revised by Jim Kingdon, 6-Apr-2023.) |
6-Apr-2023 | cnptoprest2 13034 | Equivalence of point-continuity in the parent topology and point-continuity in a subspace. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 6-Apr-2023.) |
↾t | ||
5-Apr-2023 | cnptoprest 13033 | Equivalence of continuity at a point and continuity of the restricted function at a point. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 5-Apr-2023.) |
↾t | ||
4-Apr-2023 | exmidmp 7133 | Excluded middle implies Markov's Principle (MP). (Contributed by Jim Kingdon, 4-Apr-2023.) |
EXMID Markov | ||
2-Apr-2023 | sup3exmid 8873 | If any inhabited set of real numbers bounded from above has a supremum, excluded middle follows. (Contributed by Jim Kingdon, 2-Apr-2023.) |
DECID | ||
31-Mar-2023 | cnptopresti 13032 | One direction of cnptoprest 13033 under the weaker condition that the point is in the subset rather than the interior of the subset. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 31-Mar-2023.) |
TopOn ↾t | ||
30-Mar-2023 | cncnp2m 13025 | A continuous function is continuous at all points. Theorem 7.2(g) of [Munkres] p. 107. (Contributed by Raph Levien, 20-Nov-2006.) (Revised by Jim Kingdon, 30-Mar-2023.) |
29-Mar-2023 | exmidlpo 7119 | Excluded middle implies the Limited Principle of Omniscience (LPO). (Contributed by Jim Kingdon, 29-Mar-2023.) |
EXMID Omni | ||
28-Mar-2023 | icnpimaex 13005 | Property of a function continuous at a point. (Contributed by FL, 31-Dec-2006.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn TopOn | ||
28-Mar-2023 | cnpf2 13001 | A continuous function at point is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn TopOn | ||
28-Mar-2023 | cnprcl2k 13000 | Reverse closure for a function continuous at a point. (Contributed by Mario Carneiro, 21-Aug-2015.) (Revised by Jim Kingdon, 28-Mar-2023.) |
TopOn | ||
27-Mar-2023 | mptrcl 5578 | Reverse closure for a mapping: If the function value of a mapping has a member, the argument belongs to the base class of the mapping. (Contributed by AV, 4-Apr-2020.) (Revised by Jim Kingdon, 27-Mar-2023.) |
25-Mar-2023 | lmreltop 12987 | The topological space convergence relation is a relation. (Contributed by Jim Kingdon, 25-Mar-2023.) |
25-Mar-2023 | fodjumkv 7136 | A condition which ensures that a nonempty set is inhabited. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ | ||
25-Mar-2023 | fodjumkvlemres 7135 | Lemma for fodjumkv 7136. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 25-Mar-2023.) |
Markov ⊔ inl | ||
25-Mar-2023 | fodju0 7123 | Lemma for fodjuomni 7125 and fodjumkv 7136. A condition which shows that is empty. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
25-Mar-2023 | fodjum 7122 | Lemma for fodjuomni 7125 and fodjumkv 7136. A condition which shows that is inhabited. (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
25-Mar-2023 | fodjuf 7121 | Lemma for fodjuomni 7125 and fodjumkv 7136. Domain and range of . (Contributed by Jim Kingdon, 27-Jul-2022.) (Revised by Jim Kingdon, 25-Mar-2023.) |
⊔ inl | ||
23-Mar-2023 | restrcl 12961 | Reverse closure for the subspace topology. (Contributed by Mario Carneiro, 19-Mar-2015.) (Proof shortened by Jim Kingdon, 23-Mar-2023.) |
↾t | ||
22-Mar-2023 | neipsm 12948 | A neighborhood of a set is a neighborhood of every point in the set. Proposition 1 of [BourbakiTop1] p. I.2. (Contributed by FL, 16-Nov-2006.) (Revised by Jim Kingdon, 22-Mar-2023.) |
19-Mar-2023 | mkvprop 7134 | Markov's Principle expressed in terms of propositions (or more precisely, the case is Markov's Principle). (Contributed by Jim Kingdon, 19-Mar-2023.) |
Markov DECID | ||
18-Mar-2023 | omnimkv 7132 | An omniscient set is Markov. In particular, the case where is means that the Limited Principle of Omniscience (LPO) implies Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.) |
Omni Markov | ||
18-Mar-2023 | ismkvmap 7130 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
18-Mar-2023 | ismkv 7129 | The predicate of being Markov. (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
18-Mar-2023 | df-markov 7128 |
A Markov set is one where if a predicate (here represented by a function
) on that set
does not hold (where hold means is equal to )
for all elements, then there exists an element where it fails (is equal
to ). Generalization of definition 2.5 of [Pierik], p. 9.
In particular, Markov is known as Markov's Principle (MP). (Contributed by Jim Kingdon, 18-Mar-2023.) |
Markov | ||
17-Mar-2023 | finct 7093 | A finite set is countable. (Contributed by Jim Kingdon, 17-Mar-2023.) |
⊔ | ||
16-Mar-2023 | ctmlemr 7085 | Lemma for ctm 7086. One of the directions of the biconditional. (Contributed by Jim Kingdon, 16-Mar-2023.) |
⊔ | ||
15-Mar-2023 | caseinl 7068 | Applying the "case" construction to a left injection. (Contributed by Jim Kingdon, 15-Mar-2023.) |
case inl | ||
13-Mar-2023 | enumct 7092 | A finitely enumerable set is countable. Lemma 8.1.14 of [AczelRathjen], p. 73 (except that our definition of countable does not require the set to be inhabited). "Finitely enumerable" is defined as per Definition 8.1.4 of [AczelRathjen], p. 71 and "countable" is defined as ⊔ per [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | enumctlemm 7091 | Lemma for enumct 7092. The case where is greater than zero. (Contributed by Jim Kingdon, 13-Mar-2023.) |
13-Mar-2023 | ctm 7086 | Two equivalent definitions of countable for an inhabited set. Remark of [BauerSwan], p. 14:3. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | 0ct 7084 | The empty set is countable. Remark of [BauerSwan], p. 14:3 which also has the definition of countable used here. (Contributed by Jim Kingdon, 13-Mar-2023.) |
⊔ | ||
13-Mar-2023 | ctex 6731 | A class dominated by is a set. See also ctfoex 7095 which says that a countable class is a set. (Contributed by Thierry Arnoux, 29-Dec-2016.) (Proof shortened by Jim Kingdon, 13-Mar-2023.) |
12-Mar-2023 | cls0 12927 | The closure of the empty set. (Contributed by NM, 2-Oct-2007.) (Proof shortened by Jim Kingdon, 12-Mar-2023.) |
12-Mar-2023 | algrp1 12000 | The value of the algorithm iterator at . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
12-Mar-2023 | ialgr0 11998 | The value of the algorithm iterator at is the initial state . (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
11-Mar-2023 | ntreq0 12926 | Two ways to say that a subset has an empty interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.) |
11-Mar-2023 | clstop 12921 | The closure of a topology's underlying set is the entire set. (Contributed by NM, 5-Oct-2007.) (Proof shortened by Jim Kingdon, 11-Mar-2023.) |
11-Mar-2023 | ntrss 12913 | Subset relationship for interior. (Contributed by NM, 3-Oct-2007.) (Revised by Jim Kingdon, 11-Mar-2023.) |
10-Mar-2023 | iuncld 12909 | A finite indexed union of closed sets is closed. (Contributed by Mario Carneiro, 19-Sep-2015.) (Revised by Jim Kingdon, 10-Mar-2023.) |
5-Mar-2023 | 2basgeng 12876 | Conditions that determine the equality of two generated topologies. (Contributed by NM, 8-May-2007.) (Revised by Jim Kingdon, 5-Mar-2023.) |
5-Mar-2023 | exmidsssn 4188 | Excluded middle is equivalent to the biconditionalized version of sssnr 3740 for sets. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
5-Mar-2023 | exmidn0m 4187 | Excluded middle is equivalent to any set being empty or inhabited. (Contributed by Jim Kingdon, 5-Mar-2023.) |
EXMID | ||
4-Mar-2023 | eltg3 12851 | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Jim Kingdon, 4-Mar-2023.) |
4-Mar-2023 | tgvalex 12844 | The topology generated by a basis is a set. (Contributed by Jim Kingdon, 4-Mar-2023.) |
4-Mar-2023 | biadanii 608 | Inference associated with biadani 607. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.) |
4-Mar-2023 | biadani 607 | An implication implies to the equivalence of some implied equivalence and some other equivalence involving a conjunction. (Contributed by BJ, 4-Mar-2023.) |
16-Feb-2023 | ixp0 6709 | The infinite Cartesian product of a family with an empty member is empty. (Contributed by NM, 1-Oct-2006.) (Revised by Jim Kingdon, 16-Feb-2023.) |
16-Feb-2023 | ixpm 6708 | If an infinite Cartesian product of a family is inhabited, every is inhabited. (Contributed by Mario Carneiro, 22-Jun-2016.) (Revised by Jim Kingdon, 16-Feb-2023.) |
16-Feb-2023 | exmidundifim 4193 | Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4192 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.) |
EXMID | ||
15-Feb-2023 | ixpintm 6703 | The intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | ixpiinm 6702 | The indexed intersection of a collection of infinite Cartesian products. (Contributed by Mario Carneiro, 6-Feb-2015.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | ixpexgg 6700 | The existence of an infinite Cartesian product. is normally a free-variable parameter in . Remark in Enderton p. 54. (Contributed by NM, 28-Sep-2006.) (Revised by Jim Kingdon, 15-Feb-2023.) |
15-Feb-2023 | nfixpxy 6695 | Bound-variable hypothesis builder for indexed Cartesian product. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by Jim Kingdon, 15-Feb-2023.) |
13-Feb-2023 | topnpropgd 12593 | The topology extractor function depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Jim Kingdon, 13-Feb-2023.) |
TopSet TopSet | ||
12-Feb-2023 | slotex 12443 | Existence of slot value. A corollary of slotslfn 12442. (Contributed by Jim Kingdon, 12-Feb-2023.) |
Slot | ||
11-Feb-2023 | topnvalg 12591 | Value of the topology extractor function. (Contributed by Mario Carneiro, 13-Aug-2015.) (Revised by Jim Kingdon, 11-Feb-2023.) |
TopSet ↾t | ||
10-Feb-2023 | slotslfn 12442 | A slot is a function on sets, treated as structures. (Contributed by Mario Carneiro, 22-Sep-2015.) (Revised by Jim Kingdon, 10-Feb-2023.) |
Slot | ||
9-Feb-2023 | pleslid 12575 | Slot property of . (Contributed by Jim Kingdon, 9-Feb-2023.) |
Slot | ||
9-Feb-2023 | topgrptsetd 12572 | The topology of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet TopSet | ||
9-Feb-2023 | topgrpplusgd 12571 | The additive operation of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet | ||
9-Feb-2023 | topgrpbasd 12570 | The base set of a constructed topological group. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet | ||
9-Feb-2023 | topgrpstrd 12569 | A constructed topological group is a structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 9-Feb-2023.) |
TopSet Struct | ||
9-Feb-2023 | tsetslid 12568 | Slot property of TopSet. (Contributed by Jim Kingdon, 9-Feb-2023.) |
TopSet Slot TopSet TopSet | ||
8-Feb-2023 | ipsipd 12565 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar | ||
8-Feb-2023 | ipsvscad 12564 | The scalar product operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar | ||
8-Feb-2023 | ipsscad 12563 | The set of scalars of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 8-Feb-2023.) |
Scalar Scalar | ||
7-Feb-2023 | ipsmulrd 12562 | The multiplicative operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsaddgd 12561 | The additive operation of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsbased 12560 | The base set of a constructed inner product space. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
7-Feb-2023 | ipsstrd 12559 | A constructed inner product space is a structure. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar Struct | ||
7-Feb-2023 | ipslid 12558 | Slot property of . (Contributed by Jim Kingdon, 7-Feb-2023.) |
Slot | ||
7-Feb-2023 | lmodvscad 12555 | The scalar product operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 7-Feb-2023.) |
Scalar | ||
6-Feb-2023 | lmodscad 12554 | The set of scalars of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar Scalar | ||
6-Feb-2023 | lmodplusgd 12553 | The additive operation of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar | ||
6-Feb-2023 | lmodbased 12552 | The base set of a constructed left vector space. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 6-Feb-2023.) |
Scalar | ||
5-Feb-2023 | lmodstrd 12551 | A constructed left module or left vector space is a structure. (Contributed by Mario Carneiro, 1-Oct-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
Scalar Struct | ||
5-Feb-2023 | vscaslid 12550 | Slot property of . (Contributed by Jim Kingdon, 5-Feb-2023.) |
Slot | ||
5-Feb-2023 | scaslid 12547 | Slot property of Scalar. (Contributed by Jim Kingdon, 5-Feb-2023.) |
Scalar Slot Scalar Scalar | ||
5-Feb-2023 | srngplusgd 12542 | The addition operation of a constructed star ring. (Contributed by Mario Carneiro, 20-Jun-2015.) (Revised by Jim Kingdon, 5-Feb-2023.) |
5-Feb-2023 | srngbased 12541 | The base set of a constructed star ring. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
5-Feb-2023 | srngstrd 12540 | A constructed star ring is a structure. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Jim Kingdon, 5-Feb-2023.) |
Struct | ||
5-Feb-2023 | opelstrsl 12514 | The slot of a structure which contains an ordered pair for that slot. (Contributed by Jim Kingdon, 5-Feb-2023.) |
Slot Struct | ||
4-Feb-2023 | starvslid 12539 | Slot property of . (Contributed by Jim Kingdon, 4-Feb-2023.) |
Slot | ||
3-Feb-2023 | rngbaseg 12534 | The base set of a constructed ring. (Contributed by Mario Carneiro, 2-Oct-2013.) (Revised by Jim Kingdon, 3-Feb-2023.) |
3-Feb-2023 | rngstrg 12533 | A constructed ring is a structure. (Contributed by Mario Carneiro, 28-Sep-2013.) (Revised by Jim Kingdon, 3-Feb-2023.) |
Struct | ||
3-Feb-2023 | mulrslid 12530 | Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.) |
Slot | ||
3-Feb-2023 | plusgslid 12513 | Slot property of . (Contributed by Jim Kingdon, 3-Feb-2023.) |
Slot | ||
2-Feb-2023 | 2strop1g 12523 | The other slot of a constructed two-slot structure. Version of 2stropg 12520 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
Slot | ||
2-Feb-2023 | 2strbas1g 12522 | The base set of a constructed two-slot structure. Version of 2strbasg 12519 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
2-Feb-2023 | 2strstr1g 12521 | A constructed two-slot structure. Version of 2strstrg 12518 not depending on the hard-coded index value of the base set. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 2-Feb-2023.) |
Struct | ||
31-Jan-2023 | baseslid 12472 | The base set extractor is a slot. (Contributed by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strsl0 12464 | All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strslss 12463 | Propagate component extraction to a structure from a subset structure . (Contributed by Mario Carneiro, 11-Oct-2013.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
31-Jan-2023 | strslssd 12462 | Deduction version of strslss 12463. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 31-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfv3 12461 | Variant on strslfv 12460 for large structures. (Contributed by Mario Carneiro, 10-Jan-2017.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Struct Slot | ||
30-Jan-2023 | strslfv 12460 | Extract a structure component (such as the base set) from a structure with a component extractor (such as the base set extractor df-base 12422). By virtue of ndxslid 12441, this can be done without having to refer to the hard-coded numeric index of . (Contributed by Mario Carneiro, 6-Oct-2013.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Struct Slot | ||
30-Jan-2023 | strslfv2 12459 | A variation on strslfv 12460 to avoid asserting that itself is a function, which involves sethood of all the ordered pair components of . (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfv2d 12458 | Deduction version of strslfv 12460. (Contributed by Mario Carneiro, 30-Apr-2015.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strslfvd 12457 | Deduction version of strslfv 12460. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot | ||
30-Jan-2023 | strsetsid 12449 | Value of the structure replacement function. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 30-Jan-2023.) |
Slot Struct sSet | ||
30-Jan-2023 | funresdfunsndc 6485 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in the function itself, where equality is decidable. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon, 30-Jan-2023.) |
DECID | ||
29-Jan-2023 | ndxslid 12441 | A structure component extractor is defined by its own index. That the index is a natural number will also be needed in quite a few contexts so it is included in the conclusion of this theorem which can be used as a hypothesis of theorems like strslfv 12460. (Contributed by Jim Kingdon, 29-Jan-2023.) |
Slot Slot | ||
29-Jan-2023 | fnsnsplitdc 6484 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 29-Jan-2023.) |
DECID | ||
28-Jan-2023 | 2stropg 12520 | The other slot of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot | ||
28-Jan-2023 | 2strbasg 12519 | The base set of a constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot | ||
28-Jan-2023 | 2strstrg 12518 | A constructed two-slot structure. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Slot Struct | ||
28-Jan-2023 | 1strstrg 12516 | A constructed one-slot structure. (Contributed by AV, 27-Mar-2020.) (Revised by Jim Kingdon, 28-Jan-2023.) |
Struct | ||
27-Jan-2023 | strle2g 12509 | Make a structure from a pair. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct | ||
27-Jan-2023 | strle1g 12508 | Make a structure from a singleton. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct | ||
27-Jan-2023 | strleund 12506 | Combine two structures into one. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 27-Jan-2023.) |
Struct Struct Struct | ||
26-Jan-2023 | ressid2 12477 | General behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 26-Jan-2023.) |
↾s | ||
24-Jan-2023 | setsslnid 12467 | Value of the structure replacement function at an untouched index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
Slot sSet | ||
24-Jan-2023 | setsslid 12466 | Value of the structure replacement function at a replaced index. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2023.) |
Slot sSet | ||
22-Jan-2023 | setsabsd 12455 | Replacing the same components twice yields the same as the second setting only. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet sSet sSet | ||
22-Jan-2023 | setsresg 12454 | The structure replacement function does not affect the value of away from . (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
22-Jan-2023 | setsex 12448 | Applying the structure replacement function yields a set. (Contributed by Jim Kingdon, 22-Jan-2023.) |
sSet | ||
22-Jan-2023 | 2zsupmax 11189 | Two ways to express the maximum of two integers. Because order of integers is decidable, we have more flexibility than for real numbers. (Contributed by Jim Kingdon, 22-Jan-2023.) |
22-Jan-2023 | elpwpwel 4460 | A class belongs to a double power class if and only if its union belongs to the power class. (Contributed by BJ, 22-Jan-2023.) |
21-Jan-2023 | funresdfunsnss 5699 | Restricting a function to a domain without one element of the domain of the function, and adding a pair of this element and the function value of the element results in a subset of the function itself. (Contributed by AV, 2-Dec-2018.) (Revised by Jim Kingdon, 21-Jan-2023.) |
20-Jan-2023 | setsvala 12447 | Value of the structure replacement function. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 20-Jan-2023.) |
sSet | ||
20-Jan-2023 | fnsnsplitss 5695 | Split a function into a single point and all the rest. (Contributed by Stefan O'Rear, 27-Feb-2015.) (Revised by Jim Kingdon, 20-Jan-2023.) |
19-Jan-2023 | strfvssn 12438 | A structure component extractor produces a value which is contained in a set dependent on , but not . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
19-Jan-2023 | strnfvn 12437 |
Value of a structure component extractor . Normally, is a
defined constant symbol such as (df-base 12422) and is a
fixed integer such as . is a
structure, i.e. a specific
member of a class of structures.
Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strslfv 12460. (Contributed by NM, 9-Sep-2011.) (Revised by Jim Kingdon, 19-Jan-2023.) (New usage is discouraged.) |
Slot | ||
19-Jan-2023 | strnfvnd 12436 | Deduction version of strnfvn 12437. (Contributed by Mario Carneiro, 15-Nov-2014.) (Revised by Jim Kingdon, 19-Jan-2023.) |
Slot | ||
18-Jan-2023 | isstructr 12431 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstructim 12430 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstruct2r 12427 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | isstruct2im 12426 | The property of being a structure with components in . (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 18-Jan-2023.) |
Struct | ||
18-Jan-2023 | sbiev 1785 | Conversion of implicit substitution to explicit substitution. Version of sbie 1784 with a disjoint variable condition. (Contributed by Wolf Lammen, 18-Jan-2023.) |
16-Jan-2023 | toponsspwpwg 12814 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) (Revised by Jim Kingdon, 16-Jan-2023.) |
TopOn | ||
14-Jan-2023 | istopfin 12792 | Express the predicate " is a topology" using nonempty finite intersections instead of binary intersections as in istopg 12791. It is not clear we can prove the converse without adding additional conditions. (Contributed by NM, 19-Jul-2006.) (Revised by Jim Kingdon, 14-Jan-2023.) |
14-Jan-2023 | fiintim 6906 |
If a class is closed under pairwise intersections, then it is closed
under nonempty finite intersections. The converse would appear to
require an additional condition, such as and not being
equal, or
having decidable equality.
This theorem is applicable to a topology, which (among other axioms) is closed under finite intersections. Some texts use a pairwise intersection and some texts use a finite intersection, but most topology texts assume excluded middle (in which case the two intersection properties would be equivalent). (Contributed by NM, 22-Sep-2002.) (Revised by Jim Kingdon, 14-Jan-2023.) |
9-Jan-2023 | divccncfap 13371 | Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Jim Kingdon, 9-Jan-2023.) |
# | ||
7-Jan-2023 | eap1 11748 | is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
7-Jan-2023 | eap0 11746 | is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
7-Jan-2023 | egt2lt3 11742 | Euler's constant = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.) |
6-Jan-2023 | eirr 11741 | is not rational. In the absence of excluded middle, we can distinguish between this and saying that is irrational in the sense of being apart from any rational number, which is eirrap 11740. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
6-Jan-2023 | eirrap 11740 | is irrational. That is, for any rational number, is apart from it. In the absence of excluded middle, we can distinguish between this and saying that is not rational, which is eirr 11741. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
6-Jan-2023 | btwnapz 9342 | A number between an integer and its successor is apart from any integer. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
6-Jan-2023 | apmul2 8706 | Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# # # | ||
1-Jan-2023 | nnap0i 8909 | A positive integer is apart from zero (inference version). (Contributed by Jim Kingdon, 1-Jan-2023.) |
# | ||
31-Dec-2022 | 2logb9irrALT 13686 | Alternate proof of 2logb9irr 13683: The logarithm of nine to base two is not rational. (Contributed by AV, 31-Dec-2022.) (Proof modification is discouraged.) (New usage is discouraged.) |
logb | ||
31-Dec-2022 | 2logb3irr 13685 | Example for logbprmirr 13684. The logarithm of three to base two is not rational. (Contributed by AV, 31-Dec-2022.) |
logb | ||
31-Dec-2022 | logbprmirr 13684 | The logarithm of a prime to a different prime base is not rational. For example, logb (see 2logb3irr 13685). (Contributed by AV, 31-Dec-2022.) |
logb | ||
30-Dec-2022 | elpqb 9608 | A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.) |
29-Dec-2022 | sqrt2cxp2logb9e3 13687 | The square root of two to the power of the logarithm of nine to base two is three. and logb are not rational (see sqrt2irr0 12118 resp. 2logb9irr 13683), satisfying the statement in 2irrexpq 13688. (Contributed by AV, 29-Dec-2022.) |
logb | ||
29-Dec-2022 | 2logb9irr 13683 | Example for logbgcd1irr 13679. The logarithm of nine to base two is not rational. Also see 2logb9irrap 13689 which says that it is irrational (in the sense of being apart from any rational number). (Contributed by AV, 29-Dec-2022.) |
logb | ||
29-Dec-2022 | logbgcd1irrap 13682 | The logarithm of an integer greater than 1 to an integer base greater than 1 is irrational (in the sense of being apart from any rational number) if the argument and the base are relatively prime. For example, logb # where is rational. (Contributed by AV, 29-Dec-2022.) |
logb # | ||
29-Dec-2022 | logbgcd1irr 13679 | The logarithm of an integer greater than 1 to an integer base greater than 1 is not rational if the argument and the base are relatively prime. For example, logb . (Contributed by AV, 29-Dec-2022.) |
logb | ||
29-Dec-2022 | logbgt0b 13678 | The logarithm of a positive real number to a real base greater than 1 is positive iff the number is greater than 1. (Contributed by AV, 29-Dec-2022.) |
logb | ||
29-Dec-2022 | cxpcom 13651 | Commutative law for real exponentiation. (Contributed by AV, 29-Dec-2022.) |
29-Dec-2022 | elpq 9607 | A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.) |
26-Dec-2022 | apdivmuld 8730 | Relationship between division and multiplication. (Contributed by Jim Kingdon, 26-Dec-2022.) |
# # # | ||
25-Dec-2022 | tanaddaplem 11701 | A useful intermediate step in tanaddap 11702 when showing that the addition of tangents is well-defined. (Contributed by Mario Carneiro, 4-Apr-2015.) (Revised by Jim Kingdon, 25-Dec-2022.) |
# # # # | ||
25-Dec-2022 | subap0 8562 | Two numbers being apart is equivalent to their difference being apart from zero. (Contributed by Jim Kingdon, 25-Dec-2022.) |
# # | ||
23-Dec-2022 | 2irrexpq 13688 |
There exist real numbers and which
are not rational such
that is
rational. Statement in the Metamath book, section
1.1.5, footnote 27 on page 17, and the "constructive proof"
for theorem
1.2 of [Bauer], p. 483. This is a
constructive proof because it is
based on two explicitly named non-rational numbers and
logb , see sqrt2irr0 12118, 2logb9irr 13683 and
sqrt2cxp2logb9e3 13687. Therefore, this proof is acceptable/usable
in
intuitionistic logic.
For a theorem which is the same but proves that and are irrational (in the sense of being apart from any rational number), see 2irrexpqap 13690. (Contributed by AV, 23-Dec-2022.) |
23-Dec-2022 | rpcxpsqrtth 13644 | Square root theorem over the complex numbers for the complex power function. Compare with resqrtth 10995. (Contributed by AV, 23-Dec-2022.) |
23-Dec-2022 | sqrt2irr0 12118 | The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.) |
22-Dec-2022 | tanval3ap 11677 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
22-Dec-2022 | tanval2ap 11676 | Express the tangent function directly in terms of . (Contributed by Mario Carneiro, 25-Feb-2015.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
22-Dec-2022 | tanclapd 11675 | Closure of the tangent function. (Contributed by Mario Carneiro, 29-May-2016.) (Revised by Jim Kingdon, 22-Dec-2022.) |
# | ||
21-Dec-2022 | tanclap 11672 | The closure of the tangent function with a complex argument. (Contributed by David A. Wheeler, 15-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
# | ||
21-Dec-2022 | tanvalap 11671 | Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Jim Kingdon, 21-Dec-2022.) |
# | ||
20-Dec-2022 | reef11 11662 | The exponential function on real numbers is one-to-one. (Contributed by NM, 21-Aug-2008.) (Revised by Jim Kingdon, 20-Dec-2022.) |
20-Dec-2022 | efltim 11661 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 20-Dec-2022.) |
20-Dec-2022 | eqord1 8402 | A strictly increasing real function on a subset of is one-to-one. (Contributed by Mario Carneiro, 14-Jun-2014.) (Revised by Jim Kingdon, 20-Dec-2022.) |
14-Dec-2022 | iserabs 11438 | Generalized triangle inequality: the absolute value of an infinite sum is less than or equal to the sum of absolute values. (Contributed by Paul Chapman, 10-Sep-2007.) (Revised by Jim Kingdon, 14-Dec-2022.) |
12-Dec-2022 | efap0 11640 | The exponential of a complex number is apart from zero. (Contributed by Jim Kingdon, 12-Dec-2022.) |
# | ||
8-Dec-2022 | efcllem 11622 | Lemma for efcl 11627. The series that defines the exponential function converges. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | efcllemp 11621 | Lemma for efcl 11627. The series that defines the exponential function converges. The ratio test cvgratgt0 11496 is used to show convergence. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | eftvalcn 11620 | The value of a term in the series expansion of the exponential function. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 8-Dec-2022.) |
8-Dec-2022 | mertensabs 11500 | Mertens' theorem. If is an absolutely convergent series and is convergent, then (and this latter series is convergent). This latter sum is commonly known as the Cauchy product of the sequences. The proof follows the outline at http://en.wikipedia.org/wiki/Cauchy_product#Proof_of_Mertens.27_theorem. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 8-Dec-2022.) |
3-Dec-2022 | mertenslemub 11497 | Lemma for mertensabs 11500. An upper bound for . (Contributed by Jim Kingdon, 3-Dec-2022.) |
2-Dec-2022 | mertenslemi1 11498 | Lemma for mertensabs 11500. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
2-Dec-2022 | fsum3cvg3 11359 | A finite sum is convergent. (Contributed by Mario Carneiro, 24-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
DECID | ||
2-Dec-2022 | fsum3cvg2 11357 | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.) |
DECID | ||
24-Nov-2022 | cvgratnnlembern 11486 | Lemma for cvgratnn 11494. Upper bound for a geometric progression of positive ratio less than one. (Contributed by Jim Kingdon, 24-Nov-2022.) |
23-Nov-2022 | cvgratnnlemfm 11492 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 23-Nov-2022.) |
23-Nov-2022 | cvgratnnlemsumlt 11491 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 23-Nov-2022.) |
21-Nov-2022 | cvgratnnlemrate 11493 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemabsle 11490 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 21-Nov-2022.) |
21-Nov-2022 | cvgratnnlemseq 11489 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 21-Nov-2022.) |
15-Nov-2022 | cvgratnnlemmn 11488 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 15-Nov-2022.) |
15-Nov-2022 | cvgratnnlemnexp 11487 | Lemma for cvgratnn 11494. (Contributed by Jim Kingdon, 15-Nov-2022.) |
12-Nov-2022 | cvgratnn 11494 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. Although this theorem is similar to cvgratz 11495 and cvgratgt0 11496, the decision to index starting at one is not merely cosmetic, as proving convergence using climcvg1n 11313 is sensitive to how a sequence is indexed. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 12-Nov-2022.) |
12-Nov-2022 | fsum3cvg 11341 | The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 12-Nov-2022.) |
DECID | ||
12-Nov-2022 | seq3id2 10465 | The last few partial sums of a sequence that ends with all zeroes (or any element which is a right-identity for ) are all the same. (Contributed by Mario Carneiro, 13-Jul-2013.) (Revised by Jim Kingdon, 12-Nov-2022.) |
11-Nov-2022 | cvgratgt0 11496 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms beyond some index , then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
11-Nov-2022 | cvgratz 11495 | Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.) |
4-Nov-2022 | seq3val 10414 | Value of the sequence builder function. This helps expand the definition although there should be little need for it once we have proved seqf 10417, seq3-1 10416 and seq3p1 10418, as further development can be done in terms of those. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
4-Nov-2022 | df-seqfrec 10402 |
Define a general-purpose operation that builds a recursive sequence
(i.e., a function on an upper integer set such as or )
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 seqf 10417, seq3-1 10416 and
seq3p1 10418. 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. means "the sum of F(n) from n = M to infinity is 2". Since limits are unique (climuni 11256), by climdm 11258 the "sum of F(n) from n = 1 to infinity" can be expressed as (provided the sequence converges) and evaluates to 2 in this example. 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 NM, 18-Apr-2005.) (Revised by Jim Kingdon, 4-Nov-2022.) |
frec | ||
3-Nov-2022 | seq3f1o 10460 | Rearrange a sum via an arbitrary bijection on . (Contributed by Mario Carneiro, 27-Feb-2014.) (Revised by Jim Kingdon, 3-Nov-2022.) |
3-Nov-2022 | seq3m1 10424 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 3-Nov-2022.) |
29-Oct-2022 | absgtap 11473 | Greater-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | absltap 11472 | Less-than of absolute value implies apartness. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
29-Oct-2022 | 1ap2 9085 | 1 is apart from 2. (Contributed by Jim Kingdon, 29-Oct-2022.) |
# | ||
28-Oct-2022 | expcnv 11467 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 28-Oct-2022.) |
28-Oct-2022 | expcnvre 11466 | A sequence of powers of a nonnegative real number less than one converges to zero. (Contributed by Jim Kingdon, 28-Oct-2022.) |
27-Oct-2022 | ennnfone 12380 | A condition for a set being countably infinite. Corollary 8.1.13 of [AczelRathjen], p. 73. Roughly speaking, the condition says that is countable (that's the part, as seen in theorems like ctm 7086), infinite (that's the part about being able to find an element of distinct from any mapping of a natural number via ), and has decidable equality. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemim 12379 | Lemma for ennnfone 12380. The trivial direction. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemr 12378 | Lemma for ennnfone 12380. The interesting direction, expressed in deduction form. (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID | ||
27-Oct-2022 | ennnfonelemnn0 12377 | Lemma for ennnfone 12380. A version of ennnfonelemen 12376 expressed in terms of instead of . (Contributed by Jim Kingdon, 27-Oct-2022.) |
DECID frec | ||
24-Oct-2022 | pwm1geoserap1 11471 | The n-th power of a number decreased by 1 expressed by the finite geometric series ... . (Contributed by AV, 14-Aug-2021.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geoserap 11470 | The value of the finite geometric series ... . This is Metamath 100 proof #66. (Contributed by NM, 12-May-2006.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# | ||
24-Oct-2022 | geosergap 11469 | The value of the finite geometric series ... . (Contributed by Mario Carneiro, 2-May-2016.) (Revised by Jim Kingdon, 24-Oct-2022.) |
# ..^ | ||
23-Oct-2022 | expcnvap0 11465 | A sequence of powers of a complex number with absolute value smaller than 1 converges to zero. (Contributed by NM, 8-May-2006.) (Revised by Jim Kingdon, 23-Oct-2022.) |
# | ||
22-Oct-2022 | divcnv 11460 | The sequence of reciprocals of positive integers, multiplied by the factor , converges to zero. (Contributed by NM, 6-Feb-2008.) (Revised by Jim Kingdon, 22-Oct-2022.) |
22-Oct-2022 | impcomd 253 | Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.) |
21-Oct-2022 | isumsplit 11454 | Split off the first terms of an infinite sum. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 21-Oct-2022.) |
21-Oct-2022 | seq3split 10435 | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) (Revised by Jim Kingdon, 21-Oct-2022.) |
20-Oct-2022 | fidcenumlemrk 6931 | Lemma for fidcenum 6933. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
20-Oct-2022 | fidcenumlemrks 6930 | Lemma for fidcenum 6933. Induction step for fidcenumlemrk 6931. (Contributed by Jim Kingdon, 20-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenum 6933 | A set is finite if and only if it has decidable equality and is finitely enumerable. Proposition 8.1.11 of [AczelRathjen], p. 72. The definition of "finitely enumerable" as is Definition 8.1.4 of [AczelRathjen], p. 71. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemr 6932 | Lemma for fidcenum 6933. Reverse direction (put into deduction form). (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
19-Oct-2022 | fidcenumlemim 6929 | Lemma for fidcenum 6933. Forward direction. (Contributed by Jim Kingdon, 19-Oct-2022.) |
DECID | ||
17-Oct-2022 | iser3shft 11309 | Index shift of the limit of an infinite series. (Contributed by Mario Carneiro, 6-Sep-2013.) (Revised by Jim Kingdon, 17-Oct-2022.) |
17-Oct-2022 | seq3shft 10802 | Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 17-Oct-2022.) |
16-Oct-2022 | resqrexlemf1 10972 | Lemma for resqrex 10990. 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.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemf 10971 | Lemma for resqrex 10990. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlemp1rp 10970 | Lemma for resqrex 10990. Applying the recursion rule yields a positive real (expressed in a way that will help apply seqf 10417 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
16-Oct-2022 | resqrexlem1arp 10969 | Lemma for resqrex 10990. is a positive real (expressed in a way that will help apply seqf 10417 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) (Revised by Jim Kingdon, 16-Oct-2022.) |
15-Oct-2022 | inffz 14101 | The infimum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
inf | ||
15-Oct-2022 | supfz 14100 | The supremum of a finite sequence of integers. (Contributed by Scott Fenton, 8-Aug-2013.) (Revised by Jim Kingdon, 15-Oct-2022.) |
12-Oct-2022 | fsumlessfi 11423 | A shorter sum of nonnegative terms is no greater than a longer one. (Contributed by NM, 26-Dec-2005.) (Revised by Jim Kingdon, 12-Oct-2022.) |
12-Oct-2022 | modfsummodlemstep 11420 | Induction step for modfsummod 11421. (Contributed by Alexander van der Vekens, 1-Sep-2018.) (Revised by Jim Kingdon, 12-Oct-2022.) |
10-Oct-2022 | fsum3 11350 | The value of a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | fsumgcl 11349 | Closure for a function used to describe a sum over a nonempty finite set. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3distr 10469 | The distributive property for series. (Contributed by Jim Kingdon, 10-Oct-2022.) |
10-Oct-2022 | seq3homo 10466 | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 10-Oct-2022.) |
8-Oct-2022 | fsum2dlemstep 11397 | Lemma for fsum2d 11398- induction step. (Contributed by Mario Carneiro, 23-Apr-2014.) (Revised by Jim Kingdon, 8-Oct-2022.) |
7-Oct-2022 | iunfidisj 6923 | The finite union of disjoint finite sets is finite. Note that depends on , i.e. can be thought of as . (Contributed by NM, 23-Mar-2006.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
7-Oct-2022 | disjnims 3981 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by Jim Kingdon, 7-Oct-2022.) |
Disj | ||
6-Oct-2022 | disjnim 3980 | If a collection for is disjoint, then pairs are disjoint. (Contributed by Mario Carneiro, 26-Mar-2015.) (Revised by Jim Kingdon, 6-Oct-2022.) |
Disj | ||
5-Oct-2022 | dcun 3525 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) |
DECID DECID DECID | ||
4-Oct-2022 | ser3add 10461 | The sum of two infinite series. (Contributed by NM, 17-Mar-2005.) (Revised by Jim Kingdon, 4-Oct-2022.) |
3-Oct-2022 | seq3-1 10416 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 3-Oct-2022.) |
3-Oct-2022 | brrelex12i 4653 | Two classes that are related by a binary relation are sets. (An artifact of our ordered pair definition.) (Contributed by BJ, 3-Oct-2022.) |
1-Oct-2022 | fsum3ser 11360 | A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 11375 and fsump1 11383, which should make our notation clear and from which, along with closure fsumcl 11363, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) |
1-Oct-2022 | tpfidisj 6905 | A triple is finite if it consists of three unequal sets. (Contributed by Jim Kingdon, 1-Oct-2022.) |
30-Sep-2022 | exdistrv 1903 | Distribute a pair of existential quantifiers (over disjoint variables) over a conjunction. Combination of 19.41v 1895 and 19.42v 1899. For a version with fewer disjoint variable conditions but requiring more axioms, see eeanv 1925. (Contributed by BJ, 30-Sep-2022.) |
28-Sep-2022 | seq3clss 10423 | Closure property of the recursive sequence builder. (Contributed by Jim Kingdon, 28-Sep-2022.) |
27-Sep-2022 | zmaxcl 11188 | The maximum of two integers is an integer. (Contributed by Jim Kingdon, 27-Sep-2022.) |
24-Sep-2022 | isumss2 11356 | Change the index set of a sum by adding zeroes. The nonzero elements are in the contained set and the added zeroes compose the rest of the containing set which needs to be summable. (Contributed by Mario Carneiro, 15-Jul-2013.) (Revised by Jim Kingdon, 24-Sep-2022.) |
DECID DECID | ||
24-Sep-2022 | preimaf1ofi 6928 | The preimage of a finite set under a one-to-one, onto function is finite. (Contributed by Jim Kingdon, 24-Sep-2022.) |
24-Sep-2022 | ifmdc 3565 | If a conditional class is inhabited, then the condition is decidable. This shows that conditionals are not very useful unless one can prove the condition decidable. (Contributed by BJ, 24-Sep-2022.) |
DECID | ||
24-Sep-2022 | bianassc 467 | An inference to merge two lists of conjuncts. (Contributed by Peter Mazsa, 24-Sep-2022.) |
24-Sep-2022 | mpbiran2d 440 | Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.) |
24-Sep-2022 | anim1ci 339 | Introduce conjunct to both sides of an implication. (Contributed by Peter Mazsa, 24-Sep-2022.) |
23-Sep-2022 | fisumss 11355 | Change the index set to a subset in a finite sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 23-Sep-2022.) |
DECID | ||
21-Sep-2022 | isumss 11354 | Change the index set to a subset in an upper integer sum. (Contributed by Mario Carneiro, 21-Apr-2014.) (Revised by Jim Kingdon, 21-Sep-2022.) |
DECID DECID | ||
21-Sep-2022 | pw1dom2 7204 | The power set of dominates . Also see pwpw0ss 3791 which is similar. (Contributed by Jim Kingdon, 21-Sep-2022.) |
18-Sep-2022 | sumfct 11337 | A lemma to facilitate conversions from the function form to the class-variable form of a sum. (Contributed by Mario Carneiro, 12-Aug-2013.) (Revised by Jim Kingdon, 18-Sep-2022.) |
18-Sep-2022 | syl21anbrc 1177 | Syllogism inference. (Contributed by Peter Mazsa, 18-Sep-2022.) |
18-Sep-2022 | an21 468 | Swap two conjuncts. (Contributed by Peter Mazsa, 18-Sep-2022.) |
16-Sep-2022 | fser0const 10472 | Simplifying an expression which turns out just to be a constant zero sequence. (Contributed by Jim Kingdon, 16-Sep-2022.) |
8-Sep-2022 | zfz1isolemiso 10774 | Lemma for zfz1iso 10776. Adding one element to the order isomorphism. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ ♯ ♯ | ||
8-Sep-2022 | zfz1isolemsplit 10773 | Lemma for zfz1iso 10776. Removing one element from an integer range. (Contributed by Jim Kingdon, 8-Sep-2022.) |
♯ ♯ ♯ | ||
7-Sep-2022 | zfz1isolem1 10775 | Lemma for zfz1iso 10776. Existence of an order isomorphism given the existence of shorter isomorphisms. (Contributed by Jim Kingdon, 7-Sep-2022.) |
♯ ♯ | ||
6-Sep-2022 | fimaxq 10762 | A finite set of rational numbers has a maximum. (Contributed by Jim Kingdon, 6-Sep-2022.) |
5-Sep-2022 | fimax2gtri 6879 | A finite set has a maximum under a trichotomous order. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | fimax2gtrilemstep 6878 | Lemma for fimax2gtri 6879. The induction step. (Contributed by Jim Kingdon, 5-Sep-2022.) |
5-Sep-2022 | tridc 6877 | A trichotomous order is decidable. (Contributed by Jim Kingdon, 5-Sep-2022.) |
DECID | ||
3-Sep-2022 | zfz1iso 10776 | A finite set of integers has an order isomorphism to a one-based finite sequence. (Contributed by Jim Kingdon, 3-Sep-2022.) |
♯ | ||
2-Sep-2022 | rspceeqv 2852 | Restricted existential specialization in an equality, using implicit substitution. (Contributed by BJ, 2-Sep-2022.) |
1-Sep-2022 | ssidd 3168 | Weakening of ssid 3167. (Contributed by BJ, 1-Sep-2022.) |
31-Aug-2022 | fveqeq2 5505 | Equality deduction for function value. (Contributed by BJ, 31-Aug-2022.) |
30-Aug-2022 | iseqf1olemfvp 10453 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 30-Aug-2022.) |
30-Aug-2022 | fveqeq2d 5504 | Equality deduction for function value. (Contributed by BJ, 30-Aug-2022.) |
29-Aug-2022 | seq3f1olemqsumkj 10454 | Lemma for seq3f1o 10460. gives the same sum as in the range . (Contributed by Jim Kingdon, 29-Aug-2022.) |
..^ | ||
29-Aug-2022 | iseqf1olemqpcl 10452 | Lemma for seq3f1o 10460. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
29-Aug-2022 | iseqf1olemjpcl 10451 | Lemma for seq3f1o 10460. A closure lemma involving and . (Contributed by Jim Kingdon, 29-Aug-2022.) |
28-Aug-2022 | iseqf1olemqval 10443 | Lemma for seq3f1o 10460. Value of the function . (Contributed by Jim Kingdon, 28-Aug-2022.) |
27-Aug-2022 | iseqf1olemmo 10448 | Lemma for seq3f1o 10460. Showing that is one-to-one. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnanb 10446 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemab 10445 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemnab 10444 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
27-Aug-2022 | iseqf1olemqcl 10442 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 27-Aug-2022.) |
26-Aug-2022 | iseqf1olemqf 10447 | Lemma for seq3f1o 10460. Domain and codomain of . (Contributed by Jim Kingdon, 26-Aug-2022.) |
25-Aug-2022 | fzodcel 10108 | Decidability of membership in a half-open integer interval. (Contributed by Jim Kingdon, 25-Aug-2022.) |
DECID ..^ | ||
24-Aug-2022 | rspceaimv 2842 | Restricted existential specialization of a universally quantified implication. (Contributed by BJ, 24-Aug-2022.) |
22-Aug-2022 | seq3f1olemqsumk 10455 | Lemma for seq3f1o 10460. gives the same sum as in the range . (Contributed by Jim Kingdon, 22-Aug-2022.) |
..^ | ||
21-Aug-2022 | seq3f1olemqsum 10456 | Lemma for seq3f1o 10460. gives the same sum as . (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemqk 10450 | Lemma for seq3f1o 10460. is constant for one more position than is. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemqf1o 10449 | Lemma for seq3f1o 10460. is a permutation of . is formed from the constant portion of , followed by the single element (at position ), followed by the rest of J (with the deleted and the elements before moved one position later to fill the gap). (Contributed by Jim Kingdon, 21-Aug-2022.) |
21-Aug-2022 | iseqf1olemklt 10441 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | iseqf1olemkle 10440 | Lemma for seq3f1o 10460. (Contributed by Jim Kingdon, 21-Aug-2022.) |
..^ | ||
21-Aug-2022 | fssdm 5362 | Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, semi-deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | fssdmd 5361 | Expressing that a class is a subclass of the domain of a function expressed in maps-to notation, deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | eqelssd 3166 | Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | reximssdv 2574 | Derivation of a restricted existential quantification over a subset (the second hypothesis implies ), deduction form. (Contributed by AV, 21-Aug-2022.) |
21-Aug-2022 | animpimp2impd 554 | Deduction deriving nested implications from conjunctions. (Contributed by AV, 21-Aug-2022.) |
20-Aug-2022 | brimralrspcev 4048 | Restricted existential specialization with a restricted universal quantifier over an implication with a relation in the antecedent, closed form. (Contributed by AV, 20-Aug-2022.) |
20-Aug-2022 | brralrspcev 4047 | Restricted existential specialization with a restricted universal quantifier over a relation, closed form. (Contributed by AV, 20-Aug-2022.) |
19-Aug-2022 | seq3f1olemstep 10457 | Lemma for seq3f1o 10460. Given a permutation which is constant up to a point, supply a new one which is constant for one more position. (Contributed by Jim Kingdon, 19-Aug-2022.) |
..^ | ||
18-Aug-2022 | seq3f1olemp 10458 | Lemma for seq3f1o 10460. Existence of a constant permutation of which leads to the same sum as the permutation itself. (Contributed by Jim Kingdon, 18-Aug-2022.) |
17-Aug-2022 | seq3f1oleml 10459 | Lemma for seq3f1o 10460. This is more or less the result, but stated in terms of and without . and may differ in terms of what happens to terms after . The terms after don't matter for the value at but we need some definition given the way our theorems concerning work. (Contributed by Jim Kingdon, 17-Aug-2022.) |
17-Aug-2022 | imbrov2fvoveq 5878 | Equality theorem for nested function and operation value in an implication for a binary relation. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 17-Aug-2022.) |
16-Aug-2022 | fmpttd 5651 | Version of fmptd 5650 with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021.) (Proof shortened by BJ, 16-Aug-2022.) |
15-Aug-2022 | nnf1o 11339 | Lemma for sum and product theorems. (Contributed by Jim Kingdon, 15-Aug-2022.) |
14-Aug-2022 | 2fveq3 5501 | Equality theorem for nested function values. (Contributed by AV, 14-Aug-2022.) |
13-Aug-2022 | exmidsbth 14056 |
The Schroeder-Bernstein Theorem is equivalent to excluded middle. This
is Metamath 100 proof #25. The forward direction (isbth 6944) is the
proof of the Schroeder-Bernstein Theorem from the Metamath Proof
Explorer database (in which excluded middle holds), but adapted to use
EXMID as an antecedent rather than being unconditionally
true, as in
the non-intuitionistic proof at
https://us.metamath.org/mpeuni/sbth.html 6944.
The reverse direction (exmidsbthr 14055) is the one which establishes that Schroeder-Bernstein implies excluded middle. This resolves the question of whether we will be able to prove Schroeder-Bernstein from our axioms in the negative. (Contributed by Jim Kingdon, 13-Aug-2022.) |
EXMID | ||
13-Aug-2022 | fv0p1e1 8993 | Function value at with replaced by . Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
13-Aug-2022 | ovanraleqv 5877 | Equality theorem for a conjunction with an operation values within a restricted universal quantification. Technical theorem to be used to reduce the size of a significant number of proofs. (Contributed by AV, 13-Aug-2022.) |
12-Aug-2022 | stbid 827 | The equivalent of a stable proposition is stable. (Contributed by Jim Kingdon, 12-Aug-2022.) |
STAB STAB | ||
11-Aug-2022 | exmidsbthr 14055 | The Schroeder-Bernstein Theorem implies excluded middle. Theorem 1 of [PradicBrown2022], p. 1. (Contributed by Jim Kingdon, 11-Aug-2022.) |
EXMID | ||
11-Aug-2022 | exmidsbthrlem 14054 | Lemma for exmidsbthr 14055. (Contributed by Jim Kingdon, 11-Aug-2022.) |
ℕ∞ EXMID | ||
10-Aug-2022 | nninfomni 14052 | ℕ∞ is omniscient. Corollary 3.7 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ Omni | ||
10-Aug-2022 | nninfomnilem 14051 | Lemma for nninfomni 14052. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ ℕ∞ Omni | ||
10-Aug-2022 | nninfex 7098 | ℕ∞ is a set. (Contributed by Jim Kingdon, 10-Aug-2022.) |
ℕ∞ | ||
10-Aug-2022 | vpwex 4165 | Power set axiom: the powerclass of a set is a set. Axiom 4 of [TakeutiZaring] p. 17. (Contributed by NM, 30-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) Revised to prove pwexg 4166 from vpwex 4165. (Revised by BJ, 10-Aug-2022.) |
9-Aug-2022 | nninfsel 14050 | is a selection function for ℕ∞. Theorem 3.6 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemeqinf 14049 | Lemma for nninfsel 14050. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemqall 14048 | Lemma for nninfsel 14050. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
9-Aug-2022 | nninfsellemeq 14047 | Lemma for nninfsel 14050. (Contributed by Jim Kingdon, 9-Aug-2022.) |
ℕ∞ ℕ∞ | ||
8-Aug-2022 | nninfsellemcl 14044 | Lemma for nninfself 14046. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ | ||
8-Aug-2022 | nninfsellemdc 14043 | Lemma for nninfself 14046. Showing that the selection function is well defined. (Contributed by Jim Kingdon, 8-Aug-2022.) |
ℕ∞ DECID | ||
8-Aug-2022 | ss1oel2o 14026 | Any subset of ordinal one being an element of ordinal two is equivalent to excluded middle. A variation of exmid01 4184 which more directly illustrates the contrast with el2oss1o 6422. (Contributed by Jim Kingdon, 8-Aug-2022.) |
EXMID | ||
8-Aug-2022 | el2oss1o 6422 | Being an element of ordinal two implies being a subset of ordinal one. The converse is equivalent to excluded middle by ss1oel2o 14026. (Contributed by Jim Kingdon, 8-Aug-2022.) |
7-Aug-2022 | nnti 14027 | Ordering on a natural number generates a tight apartness. (Contributed by Jim Kingdon, 7-Aug-2022.) |
6-Aug-2022 | nninfself 14046 | Domain and range of the selection function for ℕ∞. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
6-Aug-2022 | nninfsellemsuc 14045 | Lemma for nninfself 14046. (Contributed by Jim Kingdon, 6-Aug-2022.) |
ℕ∞ | ||
4-Aug-2022 | nnnninfeq2 7105 | Mapping of a natural number to an element of ℕ∞. Similar to nnnninfeq 7104 but if we have information about a single digit, that gives information about all previous digits. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
4-Aug-2022 | nnnninfeq 7104 | Mapping of a natural number to an element of ℕ∞. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
4-Aug-2022 | nninff 7099 | An element of ℕ∞ is a sequence of zeroes and ones. (Contributed by Jim Kingdon, 4-Aug-2022.) |
ℕ∞ | ||
1-Aug-2022 | nninfall 14042 | Given a decidable predicate on ℕ∞, showing it holds for natural numbers and the point at infinity suffices to show it holds everywhere. The sense in which is a decidable predicate is that it assigns a value of either or (which can be thought of as false and true) to every element of ℕ∞. Lemma 3.5 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
1-Aug-2022 | nninfalllem1 14041 | Lemma for nninfall 14042. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
1-Aug-2022 | peano3nninf 14040 | The successor function on ℕ∞ is never zero. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 1-Aug-2022.) |
ℕ∞ ℕ∞ | ||
31-Jul-2022 | peano4nninf 14039 | The successor function on ℕ∞ is one to one. Half of Lemma 3.4 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 31-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
31-Jul-2022 | 1lt2o 6421 | Ordinal one is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | 0lt2o 6420 | Ordinal zero is less than ordinal two. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | nnpredcl 4607 | The predecessor of a natural number is a natural number. This theorem is most interesting when the natural number is a successor (as seen in theorems like onsucuni2 4548) but also holds when it is by uni0 3823. (Contributed by Jim Kingdon, 31-Jul-2022.) |
31-Jul-2022 | nnsucpred 4601 | The successor of the precedessor of a nonzero natural number. (Contributed by Jim Kingdon, 31-Jul-2022.) |
30-Jul-2022 | nnsf 14038 | Domain and range of . Part of Definition 3.3 of [PradicBrown2022], p. 5. (Contributed by Jim Kingdon, 30-Jul-2022.) |
ℕ∞ ℕ∞ℕ∞ | ||
29-Jul-2022 | fodjuomnilemres 7124 | Lemma for fodjuomni 7125. The final result with expressed as a local definition. (Contributed by Jim Kingdon, 29-Jul-2022.) |
Omni ⊔ inl | ||
28-Jul-2022 | eqifdc 3560 | Expansion of an equality with a conditional operator. (Contributed by Jim Kingdon, 28-Jul-2022.) |
DECID | ||
27-Jul-2022 | fodjuomni 7125 | A condition which ensures is either inhabited or empty. Lemma 3.2 of [PradicBrown2022], p. 4. (Contributed by Jim Kingdon, 27-Jul-2022.) |
Omni ⊔ | ||
27-Jul-2022 | fodjuomnilemdc 7120 | Lemma for fodjuomni 7125. Decidability of a condition we use in various lemmas. (Contributed by Jim Kingdon, 27-Jul-2022.) |
⊔ DECID inl | ||
25-Jul-2022 | djudom 7070 | Dominance law for disjoint union. (Contributed by Jim Kingdon, 25-Jul-2022.) |
⊔ ⊔ | ||
23-Jul-2022 | fvoveq1 5876 | Equality theorem for nested function and operation value. Closed form of fvoveq1d 5875. (Contributed by AV, 23-Jul-2022.) |
23-Jul-2022 | fvoveq1d 5875 | Equality deduction for nested function and operation value. (Contributed by AV, 23-Jul-2022.) |
17-Jul-2022 | inftonninf 10397 | The mapping of into ℕ∞ is the sequence of all ones. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
17-Jul-2022 | 1tonninf 10396 | The mapping of one into ℕ∞ is a sequence which is a one followed by zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
17-Jul-2022 | 0tonninf 10395 | The mapping of zero into ℕ∞ is the sequence of all zeroes. (Contributed by Jim Kingdon, 17-Jul-2022.) |
frec | ||
16-Jul-2022 | fxnn0nninf 10394 | A function from NN0* into ℕ∞. (Contributed by Jim Kingdon, 16-Jul-2022.) TODO: use infnninf 7100 instead of infnninfOLD 7101. More generally, this theorem and most theorems in this section could use an extended defined by frec and as in nnnninf2 7103. |
frec NN0*ℕ∞ |
Copyright terms: Public domain | W3C HTML validation [external] |