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 | ||
1-Oct-2024 | infex2g 6979 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
inf | ||
30-Sep-2024 | unbendc 12227 | 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 12011 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
DECID | ||
30-Sep-2024 | dcfi 6926 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
DECID DECID | ||
29-Sep-2024 | ssnnct 12218 | A decidable subset of is countable. (Contributed by Jim Kingdon, 29-Sep-2024.) |
DECID ⊔ | ||
29-Sep-2024 | ssnnctlemct 12217 | Lemma for ssnnct 12218. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
frec DECID ⊔ | ||
28-Sep-2024 | nninfdcex 11843 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
DECID | ||
27-Sep-2024 | infregelbex 9510 | 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 12223 | Lemma for nninfdc 12226. Each element of the sequence is greater than the previous element. (Contributed by Jim Kingdon, 26-Sep-2024.) |
DECID inf | ||
26-Sep-2024 | nnminle 12220 | 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 12219. (Contributed by Jim Kingdon, 26-Sep-2024.) |
DECID inf | ||
25-Sep-2024 | nninfdclemcl 12221 | Lemma for nninfdc 12226. (Contributed by Jim Kingdon, 25-Sep-2024.) |
DECID inf | ||
24-Sep-2024 | nninfdclemlt 12224 | Lemma for nninfdc 12226. The function from nninfdclemf 12222 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nninfdc 12226 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID | ||
23-Sep-2024 | nninfdclemf1 12225 | Lemma for nninfdc 12226. The function from nninfdclemf 12222 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nninfdclemf 12222 | Lemma for nninfdc 12226. A function from the natural numbers into . (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
23-Sep-2024 | nnmindc 12219 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
DECID inf | ||
19-Sep-2024 | ssomct 12216 | A decidable subset of is countable. (Contributed by Jim Kingdon, 19-Sep-2024.) |
DECID ⊔ | ||
14-Sep-2024 | nnpredlt 4584 | The predecessor (see nnpredcl 4583) of a nonzero natural number is less than (see df-iord 4327) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
13-Sep-2024 | nninfisollemeq 7076 | Lemma for nninfisol 7077. The case where is a successor and and are equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
13-Sep-2024 | nninfisollemne 7075 | Lemma for nninfisol 7077. A case where is a successor and and are not equal. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
13-Sep-2024 | nninfisollem0 7074 | Lemma for nninfisol 7077. The case where is zero. (Contributed by Jim Kingdon, 13-Sep-2024.) |
ℕ_{∞} DECID | ||
12-Sep-2024 | nninfisol 7077 | 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 12107 | Lemma for eulerth 12112. The set is finite. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 7-Sep-2024.) |
..^ | ||
7-Sep-2024 | modqexp 10548 | 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 12110 | Lemma for eulerth 12112. A permutation of . (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 5-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemth 12111 | Lemma for eulerth 12112. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlema 12109 | Lemma for eulerth 12112. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
2-Sep-2024 | eulerthlemrprm 12108 | Lemma for eulerth 12112. and are relatively prime. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
..^ | ||
30-Aug-2024 | fprodap0f 11537 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 11522 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 11530 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
# | ||
26-Aug-2024 | exmidontri2or 7179 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | exmidontri 7175 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
EXMID | ||
26-Aug-2024 | ontri2orexmidim 4532 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4531. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
26-Aug-2024 | ontriexmidim 4482 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4481. (Contributed by Jim Kingdon, 26-Aug-2024.) |
DECID | ||
25-Aug-2024 | onntri2or 7182 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | onntri3or 7181 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
EXMID | ||
25-Aug-2024 | csbcow 3042 | Composition law for chained substitutions into a class. Version of csbco 3041 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 2686 | Version of cbvreuv 2682 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 2685 | Version of cbvrexv 2681 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 2684 | Version of cbvralv 2680 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 2280 | Version of cbvab 2281 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 1927 | If is not free in , it is not free in when is distinct from and . Version of nfsb 1926 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 1900 | Change bound variable. See cbvexv 1898 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | cbvalvw 1899 | Change bound variable. See cbvalv 1897 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1428. (Revised by Gino Giotto, 25-Aug-2024.) |
25-Aug-2024 | nfal 1556 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1490. (Revised by Gino Giotto, 25-Aug-2024.) |
24-Aug-2024 | gcdcomd 11862 | The operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
17-Aug-2024 | fprodcl2lem 11506 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
16-Aug-2024 | if0ab 13422 |
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 3551, , from which fmelpw1o 13423 could be derived, yielding an alternative proof. (Contributed by BJ, 16-Aug-2024.) |
16-Aug-2024 | fprodunsn 11505 | Multiply in an additional term in a finite product. See also fprodsplitsn 11534 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 13426 | Alternate proof of bj-charfundc 13425. It was expected to be much shorter since it uses bj-charfun 13424 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 13424 | Properties of the characteristic function on the class of the class . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | fmelpw1o 13423 |
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 837, which translate to and respectively by iftrue 3510
and iffalse 3513, giving pwtrufal 13611).
As proved in if0ab 13422, the associated element of is the extension, in , of the formula . (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | cnstab 8521 | Equality of complex numbers is stable. Stability here means as defined at df-stab 817. 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 8520 | 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 4445 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwun 4444 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwund 4443 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifelpwung 4442 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
15-Aug-2024 | ifidss 3520 | 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 3519 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
12-Aug-2024 | exmidontriimlem2 7158 | Lemma for exmidontriim 7161. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
12-Aug-2024 | exmidontriimlem1 7157 | Lemma for exmidontriim 7161. A variation of r19.30dc 2604. (Contributed by Jim Kingdon, 12-Aug-2024.) |
EXMID | ||
11-Aug-2024 | nndc 837 |
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 836 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 1629 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 4157): then, we can prove DECID but we cannot prove DECID because the converse of nnral 2447 does not hold. Actually, EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying EXMID and noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.) Add explanation on non-provability of EXMID. (Revised by BJ, 11-Aug-2024.) |
DECID | ||
10-Aug-2024 | exmidontriim 7161 | 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 7160 | Lemma for exmidontriim 7161. The induction step for the induction on . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | exmidontriimlem3 7159 | Lemma for exmidontriim 7161. What we get to do based on induction on both and . (Contributed by Jim Kingdon, 10-Aug-2024.) |
EXMID | ||
10-Aug-2024 | nnnninf2 7071 | Canonical embedding of into ℕ_{∞}. (Contributed by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
10-Aug-2024 | infnninf 7068 | 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 4634 shows. (Contributed by Jim Kingdon, 14-Jul-2022.) Use maps-to notation. (Revised by BJ, 10-Aug-2024.) |
ℕ_{∞} | ||
9-Aug-2024 | ss1o0el1o 6858 | Reformulation of ss1o0el1 4159 using instead of . (Contributed by BJ, 9-Aug-2024.) |
9-Aug-2024 | pw1dc0el 6857 | 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 4159 | 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 6859 | 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 6856 | 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 4565 | 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 4566. (Revised by BJ, 7-Aug-2024.) |
6-Aug-2024 | bj-charfunbi 13428 |
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 13427 |
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 13425 | 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 11490 | 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 13421 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | funmptd 13420 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5208, then prove funmptd 13420 from it, and then prove funmpt 5209 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | 2ssom 13419 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
5-Aug-2024 | bj-dcfal 13369 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-dctru 13367 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
DECID | ||
5-Aug-2024 | bj-stfal 13359 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | bj-sttru 13357 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
STAB | ||
5-Aug-2024 | prod1dc 11487 | 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 | ||
2-Aug-2024 | onntri52 7180 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri24 7178 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri45 7177 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri51 7176 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
2-Aug-2024 | onntri13 7174 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
2-Aug-2024 | onntri35 7173 |
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 7174), (3) implies (5) (onntri35 7173), (5) implies (1) (onntri51 7176), (2) implies (4) (onntri24 7178), (4) implies (5) (onntri45 7177), and (5) implies (2) (onntri52 7180). Another way of stating this is that EXMID is equivalent to trichotomy, either the or the form, as shown in exmidontri 7175 and exmidontri2or 7179, respectively. Thus EXMID is equivalent to (1) or (2). In addition, EXMID is equivalent to (3) by onntri3or 7181 and (4) by onntri2or 7182. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
EXMID | ||
1-Aug-2024 | nnral 2447 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1629. (Contributed by Jim Kingdon, 1-Aug-2024.) |
31-Jul-2024 | 3nsssucpw1 7172 | 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 7171 | 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 7170 | 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 7169 | 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 7168 | 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 7167 | 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 7166 | The power set of is not three. (Contributed by James E. Hanson and Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne1 7165 | The power set of is not one. (Contributed by Jim Kingdon, 30-Jul-2024.) |
30-Jul-2024 | pw1ne0 7164 | The power set of is not zero. (Contributed by Jim Kingdon, 30-Jul-2024.) |
29-Jul-2024 | pw1on 7162 | The power set of is an ordinal. (Contributed by Jim Kingdon, 29-Jul-2024.) |
28-Jul-2024 | exmidpweq 6855 | Excluded middle is equivalent to the power set of being . (Contributed by Jim Kingdon, 28-Jul-2024.) |
EXMID | ||
27-Jul-2024 | dcapnconstALT 13674 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 13673 by means of dceqnconst 13672. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
DECID # | ||
27-Jul-2024 | reap0 13671 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
DECID # | ||
26-Jul-2024 | nconstwlpolemgt0 13676 | Lemma for nconstwlpo 13678. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
26-Jul-2024 | nconstwlpolem0 13675 | Lemma for nconstwlpo 13678. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
24-Jul-2024 | tridceq 13669 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 13656 and redcwlpo 13668). Thus, this is an analytic analogue to lpowlpo 7112. (Contributed by Jim Kingdon, 24-Jul-2024.) |
DECID | ||
24-Jul-2024 | iswomni0 13664 | Weak omniscience stated in terms of equality with . Like iswomninn 13663 but with zero in place of one. (Contributed by Jim Kingdon, 24-Jul-2024.) |
WOmni DECID | ||
24-Jul-2024 | lpowlpo 7112 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7111. There is an analogue in terms of analytic omniscience principles at tridceq 13669. (Contributed by Jim Kingdon, 24-Jul-2024.) |
Omni WOmni | ||
23-Jul-2024 | nconstwlpolem 13677 | Lemma for nconstwlpo 13678. (Contributed by Jim Kingdon, 23-Jul-2024.) |
23-Jul-2024 | dceqnconst 13672 | 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 13668 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 13670 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
DECID DECID | ||
23-Jul-2024 | canth 5779 | 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 1480 if you want the form .) (Contributed by NM, 7-Aug-1994.) (Revised by Noah R Kingdon, 23-Jul-2024.) |
22-Jul-2024 | nconstwlpo 13678 | 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 11484 | 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 2462 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
14-Jul-2024 | ralbid2 2461 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
12-Jul-2024 | 2irrexpqap 13337 | 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 log_{b} , see sqrt2irrap 12059, 2logb9irrap 13336 and sqrt2cxp2logb9e3 13334. Therefore, this proof is acceptable/usable in intuitionistic logic. (Contributed by Jim Kingdon, 12-Jul-2024.) |
# # | ||
12-Jul-2024 | 2logb9irrap 13336 | Example for logbgcd1irrap 13329. 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.) |
log_{b} # | ||
11-Jul-2024 | logbgcd1irraplemexp 13327 | Lemma for logbgcd1irrap 13329. Apartness of and . (Contributed by Jim Kingdon, 11-Jul-2024.) |
# | ||
11-Jul-2024 | reapef 13141 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) |
# # | ||
10-Jul-2024 | apcxp2 13300 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) |
# # # | ||
9-Jul-2024 | logbgcd1irraplemap 13328 | Lemma for logbgcd1irrap 13329. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) |
log_{b} # | ||
9-Jul-2024 | apexp1 10596 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) |
# # | ||
5-Jul-2024 | logrpap0 13240 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) |
# # | ||
3-Jul-2024 | rplogbval 13304 | Define the value of the log_{b} 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.) |
# log_{b} | ||
3-Jul-2024 | logrpap0d 13241 | Deduction form of logrpap0 13240. (Contributed by Jim Kingdon, 3-Jul-2024.) |
# # | ||
3-Jul-2024 | logrpap0b 13239 | 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 13610 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
28-Jun-2024 | 012of 13609 | Mapping zero and one between and style integers. (Contributed by Jim Kingdon, 28-Jun-2024.) |
frec | ||
27-Jun-2024 | iooreen 13648 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
27-Jun-2024 | iooref1o 13647 | 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 13679 | Lemma for neapmkv 13680. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
# | ||
25-Jun-2024 | ismkvnn 13666 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov | ||
25-Jun-2024 | ismkvnnlem 13665 | Lemma for ismkvnn 13666. 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 7105 | Lemma for enmkv 7106. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
Markov Markov | ||
24-Jun-2024 | neapmkv 13680 | 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 13673 |
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 13656 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 13672 and in fact this theorem can be proved using dceqnconst 13672 as shown at dcapnconstALT 13674. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
DECID # | ||
24-Jun-2024 | enmkv 7106 | 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 6378 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 24-Jun-2024.) |
Markov Markov | ||
21-Jun-2024 | redcwlpolemeq1 13667 | Lemma for redcwlpo 13668. A biconditionalized version of trilpolemeq1 13653. (Contributed by Jim Kingdon, 21-Jun-2024.) |
20-Jun-2024 | redcwlpo 13668 |
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 13667). 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 10150 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
DECID WOmni | ||
20-Jun-2024 | iswomninn 13663 | Weak omniscience stated in terms of natural numbers. Similar to iswomnimap 7110 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 13662 | Lemma for iswomnimap 7110. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
frec WOmni DECID | ||
20-Jun-2024 | enwomni 7114 | 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 6378 says that whereas the corresponding relationship does not exist between and . (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
20-Jun-2024 | enwomnilem 7113 | Lemma for enwomni 7114. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
WOmni WOmni | ||
19-Jun-2024 | rpabscxpbnd 13301 | 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 13284 | 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 13268 | 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 13267 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
# | ||
12-Jun-2024 | rpcncxpcl 13265 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) |
12-Jun-2024 | rpcxp0 13261 | 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 13259 | 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 13258 | 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 13257 | 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 13222 | Define the power function on complex numbers. Because df-relog 13221 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 13658 |
Version of trirec0 13657 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 13657 |
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 13656). (Contributed by Jim Kingdon, 10-Jun-2024.) |
9-Jun-2024 | omniwomnimkv 7111 | 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 7110 | 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 7109 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
WOmni DECID | ||
9-Jun-2024 | df-womni 7108 |
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 | ||
29-May-2024 | pw1nct 13617 | 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 13616 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
26-May-2024 | elpwi2 4120 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
24-May-2024 | dvmptcjx 13128 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) |
22-May-2024 | efltlemlt 13137 | Lemma for eflt 13138. The converse of efltim 11599 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) |
21-May-2024 | eflt 13138 | 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 13660 | Lemma for apdiff 13661. (Contributed by Jim Kingdon, 19-May-2024.) |
# # # | ||
18-May-2024 | apdifflemf 13659 | Lemma for apdiff 13661. 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 13661 | 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 13135 | Lemma for reeff1o 13136. (Contributed by Jim Kingdon, 15-May-2024.) |
14-May-2024 | df-relog 13221 | 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.) |
7-May-2024 | ioocosf1o 13217 | 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 13215 | 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 13216 | 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 12215 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12211 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
CCHOICE ⊔ ⊔ | ||
5-May-2024 | ctiunctal 12212 | Variation of ctiunct 12211 which allows to be present in . (Contributed by Jim Kingdon, 5-May-2024.) |
⊔ ⊔ ⊔ | ||
3-May-2024 | cc4n 7192 | Countable choice with a simpler restriction on how every set in the countable collection needs to be inhabited. That is, compared with cc4 7191, 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 7190 | 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 7191 | 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 7189 | 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 7188 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
27-Apr-2024 | cc2lem 7187 | Lemma for cc2 7188. (Contributed by Jim Kingdon, 27-Apr-2024.) |
CCHOICE | ||
27-Apr-2024 | cc1 7186 | 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 12214 | 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 11478 | Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) |
♯ DECID # | ||
11-Apr-2024 | prodmodclem2a 11477 | Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
♯ ♯ DECID ♯ | ||
11-Apr-2024 | prodmodclem3 11476 | Lemma for prodmodc 11479. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
♯ ♯ | ||
10-Apr-2024 | jcnd 642 | 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 11472 | Lemma for prodrbdc 11475. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) |
DECID | ||
24-Mar-2024 | prodfdivap 11448 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
24-Mar-2024 | prodfrecap 11447 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
# | ||
23-Mar-2024 | prodfap0 11446 | 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 11442 | 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 11452 | Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sumdc 11255 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 13214 | Cosine is less than one between zero and . (Contributed by Jim Kingdon, 19-Mar-2024.) |
19-Mar-2024 | cosq34lt1 13213 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) |
14-Mar-2024 | coseq0q4123 13197 | Location of the zeroes of cosine in . (Contributed by Jim Kingdon, 14-Mar-2024.) |
14-Mar-2024 | cosq23lt0 13196 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) |
9-Mar-2024 | pilem3 13146 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) |
9-Mar-2024 | exmidonfin 7130 | 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 6818 and nnon 4570. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
EXMID | ||
9-Mar-2024 | exmidonfinlem 7129 | Lemma for exmidonfin 7130. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
DECID | ||
8-Mar-2024 | sin0pilem2 13145 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
8-Mar-2024 | sin0pilem1 13144 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
7-Mar-2024 | cosz12 13143 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) |
6-Mar-2024 | cos12dec 11668 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
25-Feb-2024 | mul2lt0pn 9672 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | mul2lt0np 9671 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
25-Feb-2024 | lt0ap0 8524 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# | ||
25-Feb-2024 | negap0d 8507 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
# # | ||
24-Feb-2024 | lt0ap0d 8525 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) |
# | ||
20-Feb-2024 | ivthdec 13064 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) |
20-Feb-2024 | ivthinclemex 13062 | Lemma for ivthinc 13063. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) |
19-Feb-2024 | ivthinclemuopn 13058 | Lemma for ivthinc 13063. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) |
19-Feb-2024 | dedekindicc 13053 | A Dedekind cut identifies a unique real number. Similar to df-inp 7387 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.) |
18-Feb-2024 | ivthinclemloc 13061 | Lemma for ivthinc 13063. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemdisj 13060 | Lemma for ivthinc 13063. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemur 13059 | Lemma for ivthinc 13063. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlr 13057 | Lemma for ivthinc 13063. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemum 13055 | Lemma for ivthinc 13063. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
18-Feb-2024 | ivthinclemlm 13054 | Lemma for ivthinc 13063. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
15-Feb-2024 | dedekindicclemeu 13051 | Lemma for dedekindicc 13053. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlu 13050 | Lemma for dedekindicc 13053. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemlub 13049 | Lemma for dedekindicc 13053. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemloc 13048 | Lemma for dedekindicc 13053. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemub 13047 | Lemma for dedekindicc 13053. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
15-Feb-2024 | dedekindicclemuub 13046 | Lemma for dedekindicc 13053. 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 13045 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7951 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 13044 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 7951 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 13056 | Lemma for ivthinc 13063. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) |
5-Feb-2024 | ivthinc 13063 | 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 13037 | Lemma for dedekindeu 13043. 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 13042 | Lemma for dedekindeu 13043. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
31-Jan-2024 | dedekindeulemlu 13041 | Lemma for dedekindeu 13043. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |