|
|
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: |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 31-Dec-2025 | pw0ss 15723 | There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.) |
| 31-Dec-2025 | df-ushgrm 15710 |
Define the class of all undirected simple hypergraphs. An undirected
simple hypergraph is a special (non-simple, multiple, multi-) hypergraph
for which the edge function |
| 29-Dec-2025 | df-uhgrm 15709 |
Define the class of all undirected hypergraphs. An undirected
hypergraph consists of a set |
| 29-Dec-2025 | iedgex 15662 | Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | vtxex 15661 | Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | snmb 3755 | A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.) |
| 27-Dec-2025 | lswex 11052 | Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11049 or lswcl 11051 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.) |
| 23-Dec-2025 | fzowrddc 11108 | Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.) |
| 19-Dec-2025 | ccatclab 11058 | The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.) |
| 18-Dec-2025 | lswwrd 11047 | Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.) |
| 14-Dec-2025 | 2strstrndx 12994 | A constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 14-Dec-2025.) |
| 12-Dec-2025 | funiedgdm2vald 15675 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 12-Dec-2025.) |
| 11-Dec-2025 | funvtxdm2vald 15674 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 11-Dec-2025 | funiedgdm2domval 15673 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 11-Dec-2025 | funvtxdm2domval 15672 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 4-Dec-2025 | hash2en 10995 | Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.) |
| 30-Nov-2025 | nninfnfiinf 16034 | An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.) |
| 27-Nov-2025 | psrelbasfi 14482 | Simpler form of psrelbas 14481 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.) |
| 26-Nov-2025 | mplsubgfileminv 14506 | Lemma for mplsubgfi 14507. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 26-Nov-2025 | mplsubgfilemcl 14505 | Lemma for mplsubgfi 14507. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 25-Nov-2025 | nninfinfwlpo 7289 | The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7242). (Contributed by Jim Kingdon, 25-Nov-2025.) |
| 23-Nov-2025 | psrbagfi 14479 | A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.) |
| 22-Nov-2025 | df-acnm 7294 |
Define a local and length-limited version of the axiom of choice. The
definition of the predicate |
| 21-Nov-2025 | mplsubgfilemm 14504 | Lemma for mplsubgfi 14507. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.) |
| 14-Nov-2025 | 2omapen 16007 |
Equinumerosity of |
| 12-Nov-2025 | 2omap 16006 |
Mapping between |
| 11-Nov-2025 | domomsubct 16012 |
A set dominated by |
| 10-Nov-2025 | prdsbaslemss 13150 | Lemma for prdsbas 13152 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.) |
| 5-Nov-2025 | fnmpl 14499 | mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.) |
| 4-Nov-2025 | mplelbascoe 14498 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 4-Nov-2025 | mplbascoe 14497 | Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 4-Nov-2025 | mplvalcoe 14496 | Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 1-Nov-2025 | ficardon 7303 | The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.) |
| 31-Oct-2025 | bitsdc 12302 | Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.) |
| 28-Oct-2025 | nn0maxcl 11580 | The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.) |
| 28-Oct-2025 | qdcle 10396 |
Rational |
| 17-Oct-2025 | plycoeid3 15273 | Reconstruct a polynomial as an explicit sum of the coefficient function up to an index no smaller than the degree of the polynomial. (Contributed by Jim Kingdon, 17-Oct-2025.) |
| 13-Oct-2025 | tpfidceq 7034 | A triple is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.) |
| 13-Oct-2025 | prfidceq 7032 | A pair is finite if it consists of elements of a class with decidable equality. (Contributed by Jim Kingdon, 13-Oct-2025.) |
| 13-Oct-2025 | dcun 3571 | The union of two decidable classes is decidable. (Contributed by Jim Kingdon, 5-Oct-2022.) (Revised by Jim Kingdon, 13-Oct-2025.) |
| 9-Oct-2025 | dvdsfi 12605 | A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.) |
| 7-Oct-2025 | df-mplcoe 14470 |
Define the subalgebra of the power series algebra generated by the
variables; this is the polynomial algebra (the set of power series with
finite degree).
The index set (which has an element for each variable) is |
| 6-Oct-2025 | dvconstss 15214 | Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.) |
| 6-Oct-2025 | dcfrompeirce 1470 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromcon 1469 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromnotnotr 1468 |
The decidability of a proposition |
| 3-Oct-2025 | dvidre 15213 | Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvconstre 15212 | Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvidsslem 15209 |
Lemma for dvconstss 15214. Analogue of dvidlemap 15207 where |
| 3-Oct-2025 | dvidrelem 15208 | Lemma for dvidre 15213 and dvconstre 15212. Analogue of dvidlemap 15207 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 28-Sep-2025 | metuex 14361 | Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 28-Sep-2025 | cndsex 14359 | The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 25-Sep-2025 | cntopex 14360 | The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.) |
| 24-Sep-2025 | mopnset 14358 |
Getting a set by applying |
| 24-Sep-2025 | blfn 14357 | The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.) |
| 23-Sep-2025 | elfzoext 10328 | Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020.) (Proof shortened by AV, 23-Sep-2025.) |
| 22-Sep-2025 | plycjlemc 15276 | Lemma for plycj 15277. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.) |
| 20-Sep-2025 | plycolemc 15274 |
Lemma for plyco 15275. The result expressed as a sum, with a
degree and
coefficients for |
| 18-Sep-2025 | elfzoextl 10327 | Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025.) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025.) |
| 16-Sep-2025 | lgsquadlemofi 15597 |
Lemma for lgsquad 15601. There are finitely many members of |
| 16-Sep-2025 | lgsquadlemsfi 15596 |
Lemma for lgsquad 15601. |
| 16-Sep-2025 | opabfi 7042 | Finiteness of an ordered pair abstraction which is a decidable subset of finite sets. (Contributed by Jim Kingdon, 16-Sep-2025.) |
| 13-Sep-2025 | uchoice 6230 |
Principle of unique choice. This is also called non-choice. The name
choice results in its similarity to something like acfun 7326 (with the key
difference being the change of |
| 11-Sep-2025 | expghmap 14413 | Exponentiation is a group homomorphism from addition to multiplication. (Contributed by Mario Carneiro, 18-Jun-2015.) (Revised by AV, 10-Jun-2019.) (Revised by Jim Kingdon, 11-Sep-2025.) |
| 11-Sep-2025 | cnfldui 14395 | The invertible complex numbers are exactly those apart from zero. This is recapb 8751 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.) |
| 9-Sep-2025 | gsumfzfsumlemm 14393 | Lemma for gsumfzfsum 14394. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.) |
| 9-Sep-2025 | gsumfzfsumlem0 14392 | Lemma for gsumfzfsum 14394. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.) |
| 9-Sep-2025 | gsumfzmhm2 13724 | Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.) |
| 8-Sep-2025 | gsumfzmhm 13723 | Apply a monoid homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 8-Sep-2025.) |
| 8-Sep-2025 | 5ndvds6 12290 | 5 does not divide 6. (Contributed by AV, 8-Sep-2025.) |
| 8-Sep-2025 | 5ndvds3 12289 | 5 does not divide 3. (Contributed by AV, 8-Sep-2025.) |
| 6-Sep-2025 | gsumfzconst 13721 | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.) |
| 31-Aug-2025 | gsumfzmptfidmadd 13719 | The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.) |
| 30-Aug-2025 | gsumfzsubmcl 13718 | Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 30-Aug-2025.) |
| 30-Aug-2025 | seqm1g 10626 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 30-Aug-2025.) |
| 29-Aug-2025 | seqf1og 10673 |
Rearrange a sum via an arbitrary bijection on |
| 25-Aug-2025 | irrmulap 9776 | The product of an irrational with a nonzero rational is irrational. By irrational we mean apart from any rational number. For a similar theorem with not rational in place of irrational, see irrmul 9775. (Contributed by Jim Kingdon, 25-Aug-2025.) |
| 19-Aug-2025 | seqp1g 10618 | Value of the sequence builder function at a successor. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.) |
| 19-Aug-2025 | seq1g 10615 | Value of the sequence builder function at its initial value. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 19-Aug-2025.) |
| 18-Aug-2025 | iswrdiz 11008 | A zero-based sequence is a word. In iswrdinn0 11006 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.) |
| 16-Aug-2025 | gsumfzcl 13375 | Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.) |
| 16-Aug-2025 | iswrdinn0 11006 | A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.) |
| 15-Aug-2025 | gsumfzz 13371 | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.) |
| 14-Aug-2025 | gsumfzval 13267 |
An expression for |
| 13-Aug-2025 | znidom 14463 |
The ℤ/nℤ structure is an integral domain when |
| 12-Aug-2025 | rrgmex 14067 | A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.) |
| 10-Aug-2025 | gausslemma2dlem1cl 15580 |
Lemma for gausslemma2dlem1 15582. Closure of the body of the
definition
of |
| 9-Aug-2025 | gausslemma2dlem1f1o 15581 | Lemma for gausslemma2dlem1 15582. (Contributed by Jim Kingdon, 9-Aug-2025.) |
| 7-Aug-2025 | qdclt 10395 |
Rational |
| 22-Jul-2025 | ivthdich 15169 |
The intermediate value theorem implies real number dichotomy. Because
real number dichotomy (also known as analytic LLPO) is a constructive
taboo, this means we will be unable to prove the intermediate value
theorem as stated here (although versions with additional conditions,
such as ivthinc 15159 for strictly monotonic functions, can be
proved).
The proof is via a function which we call the hover function and which
is also described in Section 5.1 of [Bauer], p. 493. Consider any real
number |
| 22-Jul-2025 | dich0 15168 | Real number dichotomy stated in terms of two real numbers or a real number and zero. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | ivthdichlem 15167 | Lemma for ivthdich 15169. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hovergt0 15166 | The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hoverlt1 15165 | The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 21-Jul-2025 | hoverb 15164 | A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | hovera 15163 | A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrrdv 2714 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrrdv 2713 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrdv 2712 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrdv 2711 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 20-Jul-2025 | hovercncf 15162 | The hover function is continuous. By hover function, we mean a a function which starts out as a line of slope one, is constant at zero from zero to one, and then resumes as a slope of one. (Contributed by Jim Kingdon, 20-Jul-2025.) |
| 19-Jul-2025 | mincncf 15132 | The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.) |
| 18-Jul-2025 | maxcncf 15131 | The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.) |
| 14-Jul-2025 | xnn0nnen 10589 | The set of extended nonnegative integers is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 14-Jul-2025.) |
| 12-Jul-2025 | nninfninc 7232 | All values beyond a zero in an ℕ∞ sequence are zero. This is another way of stating that elements of ℕ∞ are nonincreasing. (Contributed by Jim Kingdon, 12-Jul-2025.) |
| 10-Jul-2025 | nninfctlemfo 12405 | Lemma for nninfct 12406. (Contributed by Jim Kingdon, 10-Jul-2025.) |
| 8-Jul-2025 | nnnninfen 16032 | Equinumerosity of the natural numbers and ℕ∞ is equivalent to the Limited Principle of Omniscience (LPO). Remark in Section 1.1 of [Pradic2025], p. 2. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 8-Jul-2025 | nninfct 12406 | The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 8-Jul-2025 | nninfinf 10595 | ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 7-Jul-2025 | ivthreinc 15161 |
Restating the intermediate value theorem. Given a hypothesis stating
the intermediate value theorem (in a strong form which is not provable
given our axioms alone), provide a conclusion similar to the theorem as
stated in the Metamath Proof Explorer (which is also similar to how we
state the theorem for a strictly monotonic function at ivthinc 15159).
Being able to have a hypothesis stating the intermediate value theorem
will be helpful when it comes time to show that it implies a
constructive taboo. This version of the theorem requires that the
function |
| 28-Jun-2025 | fngsum 13264 | Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.) |
| 28-Jun-2025 | iotaexel 5911 | Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.) |
| 27-Jun-2025 | df-igsum 13135 |
Define a finite group sum (also called "iterated sum") of a
structure.
Given
1. If
2. If 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.) |
| 20-Jun-2025 | opprnzrbg 13991 | The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13992. (Contributed by SN, 20-Jun-2025.) |
| 16-Jun-2025 | fnpsr 14473 | The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.) |
| 14-Jun-2025 | basm 12937 | A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 14-Jun-2025 | elfvm 5616 | If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 6-Jun-2025 | pcxqcl 12679 | The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.) |
| 5-Jun-2025 | xqltnle 10417 |
"Less than" expressed in terms of "less than or equal to",
for extended
numbers which are rational or |
| 5-Jun-2025 | ceqsexv2d 2813 | Elimination of an existential quantifier, using implicit substitution. (Contributed by Thierry Arnoux, 10-Sep-2016.) Shorten, reduce dv conditions. (Revised by Wolf Lammen, 5-Jun-2025.) (Proof shortened by SN, 5-Jun-2025.) |
| 30-May-2025 | 4sqexercise2 12766 | Exercise which may help in understanding the proof of 4sqlemsdc 12767. (Contributed by Jim Kingdon, 30-May-2025.) |
| 27-May-2025 | iotaexab 5255 |
Existence of the |
| 25-May-2025 | 4sqlemsdc 12767 |
Lemma for 4sq 12777. The property of being the sum of four
squares is
decidable.
The proof involves showing that (for a particular |
| 25-May-2025 | 4sqexercise1 12765 | Exercise which may help in understanding the proof of 4sqlemsdc 12767. (Contributed by Jim Kingdon, 25-May-2025.) |
| 24-May-2025 | 4sqleminfi 12764 |
Lemma for 4sq 12777. |
| 24-May-2025 | 4sqlemffi 12763 |
Lemma for 4sq 12777. |
| 24-May-2025 | 4sqlemafi 12762 |
Lemma for 4sq 12777. |
| 24-May-2025 | infidc 7043 | The intersection of two sets is finite if one of them is and the other is decidable. (Contributed by Jim Kingdon, 24-May-2025.) |
| 19-May-2025 | zrhex 14427 |
Set existence for |
| 16-May-2025 | rhmex 13963 | Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.) |
| 15-May-2025 | ghmex 13635 | The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 15-May-2025 | mhmex 13338 | The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 14-May-2025 | idomcringd 14084 | An integral domain is a commutative ring with unity. (Contributed by Thierry Arnoux, 4-May-2025.) (Proof shortened by SN, 14-May-2025.) |
| 6-May-2025 | rrgnz 14074 | In a nonzero ring, the zero is a left zero divisor (that is, not a left-regular element). (Contributed by Thierry Arnoux, 6-May-2025.) |
| 5-May-2025 | rngressid 13760 | A non-unital ring restricted to its base set is a non-unital ring. It will usually be the original non-unital ring exactly, of course, but to show that needs additional conditions such as those in strressid 12947. (Contributed by Jim Kingdon, 5-May-2025.) |
| 5-May-2025 | ablressid 13715 | A commutative group restricted to its base set is a commutative group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12947. (Contributed by Jim Kingdon, 5-May-2025.) |
| 30-Apr-2025 | dvply2g 15282 | The derivative of a polynomial with coefficients in a subring is a polynomial with coefficients in the same ring. (Contributed by Mario Carneiro, 1-Jan-2017.) (Revised by GG, 30-Apr-2025.) |
| 29-Apr-2025 | rlmscabas 14266 | Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 29-Apr-2025 | ressbasid 12946 | The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 28-Apr-2025 | lssmex 14161 | If a linear subspace is inhabited, the class it is built from is a set. (Contributed by Jim Kingdon, 28-Apr-2025.) |
| 27-Apr-2025 | cnfldmul 14370 | The multiplication operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.) |
| 27-Apr-2025 | cnfldadd 14368 | The addition operation of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 27-Apr-2025.) |
| 27-Apr-2025 | lidlex 14279 | Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 27-Apr-2025 | lssex 14160 | Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 25-Apr-2025 | rspex 14280 | Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | lspex 14201 | Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | eqgex 13601 | The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | qusex 13201 | Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 23-Apr-2025 | 1dom1el 16001 | If a set is dominated by one, then any two of its elements are equal. (Contributed by Jim Kingdon, 23-Apr-2025.) |
| 22-Apr-2025 | mulgex 13503 | Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.) |
| 20-Apr-2025 | elovmpod 6151 | Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6152 in deduction form. (Revised by AV, 20-Apr-2025.) |
| 18-Apr-2025 | fsumdvdsmul 15507 |
Product of two divisor sums. (This is also the main part of the proof
that " |
| 18-Apr-2025 | mpodvdsmulf1o 15506 |
If |
| 18-Apr-2025 | df2idl2 14315 | Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.) |
| 18-Apr-2025 | 2idlmex 14307 | Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.) |
| 18-Apr-2025 | dflidl2 14294 | Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.) |
| 18-Apr-2025 | lidlmex 14281 | Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.) |
| 18-Apr-2025 | lsslsp 14235 | Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.) |
| 16-Apr-2025 | sraex 14252 | Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.) |
| 14-Apr-2025 | grpmgmd 13402 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) |
| 12-Apr-2025 | psraddcl 14486 | Closure of the power series addition operation. (Contributed by Mario Carneiro, 28-Dec-2014.) Generalize to magmas. (Revised by SN, 12-Apr-2025.) |
| 10-Apr-2025 | cndcap 16072 | Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.) |
| 4-Apr-2025 | ghmf1 13653 | Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 4-Apr-2025.) |
| 3-Apr-2025 | quscrng 14339 | The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.) |
| 31-Mar-2025 | cnfldds 14374 | The metric of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) Revise df-cnfld 14363. (Revised by GG, 31-Mar-2025.) |
| 31-Mar-2025 | cnfldle 14373 |
The ordering of the field of complex numbers. Note that this is not
actually an ordering on |
| 31-Mar-2025 | cnfldtset 14372 | The topology component of the field of complex numbers. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Mario Carneiro, 6-Oct-2015.) (Revised by Thierry Arnoux, 17-Dec-2017.) (Revised by GG, 31-Mar-2025.) |
| 31-Mar-2025 | mpocnfldmul 14369 | The multiplication operation of the field of complex numbers. Version of cnfldmul 14370 using maps-to notation, which does not require ax-mulf 8055. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | mpocnfldadd 14367 | The addition operation of the field of complex numbers. Version of cnfldadd 14368 using maps-to notation, which does not require ax-addf 8054. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | df-cnfld 14363 |
The field of complex numbers. Other number fields and rings can be
constructed by applying the ↾s restriction operator.
The contract of this set is defined entirely by cnfldex 14365, cnfldadd 14368, cnfldmul 14370, cnfldcj 14371, cnfldtset 14372, cnfldle 14373, cnfldds 14374, and cnfldbas 14366. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) Use maps-to notation for addition and multiplication. (Revised by GG, 31-Mar-2025.) (New usage is discouraged.) |
| 31-Mar-2025 | 2idlcpbl 14330 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.) |
| 22-Mar-2025 | idomringd 14085 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 22-Mar-2025 | idomdomd 14083 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 21-Mar-2025 | df2idl2rng 14314 | Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.) |
| 21-Mar-2025 | isridlrng 14288 | A right ideal is a left ideal of the opposite non-unital ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.) |
| 21-Mar-2025 | dflidl2rng 14287 | Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.) |
| 20-Mar-2025 | ccoslid 13114 | Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.) |
| 20-Mar-2025 | homslid 13111 |
Slot property of |
| 19-Mar-2025 | ptex 13140 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) |
| 18-Mar-2025 | prdsex 13145 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) |
| 16-Mar-2025 | plycn 15278 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8055. (Revised by GG, 16-Mar-2025.) |
| 16-Mar-2025 | expcn 15085 |
The power function on complex numbers, for fixed exponent |
| 16-Mar-2025 | mpomulcn 15082 | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| 16-Mar-2025 | mpomulf 8069 | Multiplication is an operation on complex numbers. Version of ax-mulf 8055 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8030. (Contributed by GG, 16-Mar-2025.) |
| 13-Mar-2025 | 2idlss 14320 | A two-sided ideal is a subset of the base set. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.) |
| 13-Mar-2025 | imasex 13181 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) |
| 11-Mar-2025 | rng2idlsubgsubrng 14326 | A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.) |
| 11-Mar-2025 | rng2idlsubrng 14323 | A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.) |
| 11-Mar-2025 | rnglidlrng 14304 |
A (left) ideal of a non-unital ring is a non-unital ring. (Contributed
by AV, 17-Feb-2020.) Generalization for non-unital rings. The
assumption |
| 11-Mar-2025 | rnglidlmsgrp 14303 |
The multiplicative group of a (left) ideal of a non-unital ring is a
semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for
non-unital rings. The assumption |
| 11-Mar-2025 | rnglidlmmgm 14302 |
The multiplicative group of a (left) ideal of a non-unital ring is a
magma. (Contributed by AV, 17-Feb-2020.) Generalization for
non-unital rings. The assumption |
| 11-Mar-2025 | imasival 13182 | Value of an image structure. The is a lemma for the theorems imasbas 13183, imasplusg 13184, and imasmulr 13185 and should not be needed once they are proved. (Contributed by Mario Carneiro, 23-Feb-2015.) (Revised by Jim Kingdon, 11-Mar-2025.) (New usage is discouraged.) |
| 9-Mar-2025 | 2idlridld 14313 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | 2idllidld 14312 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | quseccl 13613 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.) |
| 9-Mar-2025 | fovcl 6058 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.) |
| 8-Mar-2025 | subgex 13556 | The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.) |
| 7-Mar-2025 | ringrzd 13852 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | ringlzd 13851 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | qusecsub 13711 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
| 1-Mar-2025 | quselbasg 13610 | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
| 28-Feb-2025 | qusmulrng 14338 | Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14339. Similar to qusmul2 14335. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.) |
| 28-Feb-2025 | ringressid 13869 | A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 12947. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 28-Feb-2025 | grpressid 13437 | A group restricted to its base set is a group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12947. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 27-Feb-2025 | imasringf1 13871 | The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.) |
| 26-Feb-2025 | strext 12981 |
Extending the upper range of a structure. This works because when we
say that a structure has components in |
| 25-Feb-2025 | subrngringnsg 14011 | A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | rngansg 13756 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | ecqusaddd 13618 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) |
| 24-Feb-2025 | ecqusaddcl 13619 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) |
| 24-Feb-2025 | quseccl0g 13611 |
Closure of the quotient map for a quotient group. (Contributed by Mario
Carneiro, 18-Sep-2015.) Generalization of quseccl 13613 for arbitrary sets
|
| 23-Feb-2025 | ltlenmkv 16083 |
If |
| 23-Feb-2025 | neap0mkv 16082 | The analytic Markov principle can be expressed either with two arbitrary real numbers, or one arbitrary number and zero. (Contributed by Jim Kingdon, 23-Feb-2025.) |
| 23-Feb-2025 | qus2idrng 14331 | The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14333 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | 2idlcpblrng 14329 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | lringuplu 14002 | If the sum of two elements of a local ring is invertible, then at least one of the summands must be invertible. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringnz 14001 | A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringring 14000 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringnzr 13999 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | islring 13998 | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | df-lring 13997 | A local ring is a nonzero ring where for any two elements summing to one, at least one is invertible. Any field is a local ring; the ring of integers is an example of a ring which is not a local ring. (Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | 01eq0ring 13995 | If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by SN, 23-Feb-2025.) |
| 23-Feb-2025 | nzrring 13989 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.) |
| 23-Feb-2025 | qusrng 13764 | The quotient structure of a non-unital ring is a non-unital ring (qusring2 13872 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdir 13758 | Ring multiplication distributes over subtraction. (subdir 8465 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 13863. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdi 13757 | Ring multiplication distributes over subtraction. (subdi 8464 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 13862. (Revised by AV, 23-Feb-2025.) |
| 22-Feb-2025 | imasrngf1 13763 | The image of a non-unital ring under an injection is a non-unital ring. (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | imasrng 13762 | The image structure of a non-unital ring is a non-unital ring (imasring 13870 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | rngmgpf 13743 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 13817 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | imasabl 13716 | The image structure of an abelian group is an abelian group (imasgrp 13491 analog). (Contributed by AV, 22-Feb-2025.) |
| 21-Feb-2025 | prdssgrpd 13291 | The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | prdsplusgsgrpcl 13290 | Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | dftap2 7370 | Tight apartness with the apartness properties from df-pap 7367 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.) |
| 20-Feb-2025 | rng2idlsubg0 14328 | The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | rng2idlsubgnsg 14327 | A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | rng2idl0 14325 | The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | rng2idlnsg 14324 | A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | 2idlelbas 14322 | The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | 2idlbas 14321 | The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | 2idlelb 14311 | Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) |
| 20-Feb-2025 | aprap 14092 | The relation given by df-apr 14087 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | setscomd 12917 | Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | ifnebibdc 3616 | The converse of ifbi 3592 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnefals 3615 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnetruedc 3614 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 18-Feb-2025 | rnglidlmcl 14286 | A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven. (Contributed by AV, 18-Feb-2025.) |
| 17-Feb-2025 | aprcotr 14091 | The apartness relation given by df-apr 14087 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprsym 14090 | The apartness relation given by df-apr 14087 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprval 14088 | Expand Definition df-apr 14087. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | subrngpropd 14022 | If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.) |
| 17-Feb-2025 | rngm2neg 13755 | Double negation of a product in a non-unital ring (mul2neg 8477 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 13861. (Revised by AV, 17-Feb-2025.) |
| 17-Feb-2025 | rngmneg2 13754 | Negation of a product in a non-unital ring (mulneg2 8475 analog). In contrast to ringmneg2 13860, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
| 17-Feb-2025 | rngmneg1 13753 | Negation of a product in a non-unital ring (mulneg1 8474 analog). In contrast to ringmneg1 13859, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
| 16-Feb-2025 | aprirr 14089 | The apartness relation given by df-apr 14087 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 16-Feb-2025 | rngrz 13752 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 13850. (Revised by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rng0cl 13749 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rngacl 13748 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rnggrp 13744 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | aptap 8730 | Complex apartness (as defined at df-ap 8662) is a tight apartness (as defined at df-tap 7369). (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 15-Feb-2025 | subsubrng2 14021 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subsubrng 14020 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngin 14019 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngintm 14018 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprsubrngg 14017 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | issubrng2 14016 | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrngbg 13884 | A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 13883. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrng 13883 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | rngpropd 13761 | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | sgrppropd 13289 | If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | sgrpcl 13285 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | tapeq2 7372 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.) |
| 14-Feb-2025 | subrngmcl 14015 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14039. (Revised by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngacl 14014 | A subring is closed under addition. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrng0 14013 | A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngbas 14012 | Base set of a subring structure. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngsubg 14010 | A subring is a subgroup. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrcl 14009 | Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrng 14008 | A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngid 14007 | Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngss 14006 | A subring is a subset. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | issubrng 14005 | The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | df-subrng 14004 | Define a subring of a non-unital ring as a set of elements that is a non-unital ring in its own right. In this section, a subring of a non-unital ring is simply called "subring", unless it causes any ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | isrngd 13759 | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | rngdi 13746 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | exmidmotap 7380 | The proposition that every class has at most one tight apartness is equivalent to excluded middle. (Contributed by Jim Kingdon, 14-Feb-2025.) |
| 14-Feb-2025 | exmidapne 7379 | Excluded middle implies there is only one tight apartness on any class, namely negated equality. (Contributed by Jim Kingdon, 14-Feb-2025.) |
| 14-Feb-2025 | df-pap 7367 |
Apartness predicate. A relation |
| 13-Feb-2025 | 2idl1 14319 | Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | 2idl0 14318 | Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl1 14317 | Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl0 14316 | Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | isridl 14310 | A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | df-apr 14087 | The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14092. (Contributed by Jim Kingdon, 13-Feb-2025.) |
| 13-Feb-2025 | rngass 13745 | Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.) |
| 13-Feb-2025 | issgrpd 13288 | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) |
| 8-Feb-2025 | 2oneel 7375 |
|
| 8-Feb-2025 | tapeq1 7371 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.) |
| 7-Feb-2025 | psrgrp 14491 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.) |
| 7-Feb-2025 | resrhm2b 14055 | Restriction of the codomain of a (ring) homomorphism. resghm2b 13642 analog. (Contributed by SN, 7-Feb-2025.) |
| 6-Feb-2025 | zzlesq 10860 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotap 7378 |
If there is at most one tight apartness on |
| 6-Feb-2025 | 2omotaplemst 7377 | Lemma for 2omotap 7378. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotaplemap 7376 | Lemma for 2omotap 7378. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2onetap 7374 |
Negated equality is a tight apartness on |
| 5-Feb-2025 | netap 7373 | Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.) |
| 5-Feb-2025 | df-tap 7369 |
Tight apartness predicate. A relation |
| 1-Feb-2025 | mulgnn0cld 13523 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13518. (Contributed by SN, 1-Feb-2025.) |
| 31-Jan-2025 | 0subg 13579 | The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.) |
| 29-Jan-2025 | grprinvd 13432 | The right inverse of a group element. Deduction associated with grprinv 13427. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplinvd 13431 | The left inverse of a group element. Deduction associated with grplinv 13426. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpinvcld 13425 | A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpridd 13410 | The identity element of a group is a right identity. Deduction associated with grprid 13408. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplidd 13409 | The identity element of a group is a left identity. Deduction associated with grplid 13407. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpassd 13388 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
| 28-Jan-2025 | dvdsrex 13904 | Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.) |
| 24-Jan-2025 | reldvdsrsrg 13898 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.) |
| 18-Jan-2025 | rerecapb 8923 | A real number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 18-Jan-2025.) |
| 18-Jan-2025 | recapb 8751 | A complex number has a multiplicative inverse if and only if it is apart from zero. Theorem 11.2.4 of [HoTT], p. (varies), generalized from real to complex numbers. (Contributed by Jim Kingdon, 18-Jan-2025.) |
| 17-Jan-2025 | ressval3d 12948 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 17-Jan-2025 | strressid 12947 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 16-Jan-2025 | ressex 12941 | Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 16-Jan-2025 | ressvalsets 12940 | Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 12-Jan-2025 | isrim 13975 | An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.) |
| 10-Jan-2025 | rimrhm 13977 | A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
| 10-Jan-2025 | isrim0 13967 | A ring isomorphism is a homomorphism whose converse is also a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 10-Jan-2025.) |
| 10-Jan-2025 | opprex 13879 |
Existence of the opposite ring. If you know that |
| 10-Jan-2025 | mgpex 13731 |
Existence of the multiplication group. If |
| 5-Jan-2025 | imbibi 252 | The antecedent of one side of a biconditional can be moved out of the biconditional to become the antecedent of the remaining biconditional. (Contributed by BJ, 1-Jan-2025.) (Proof shortened by Wolf Lammen, 5-Jan-2025.) |
| 1-Jan-2025 | snss 3770 | The singleton of an element of a class is a subset of the class (inference form of snssg 3769). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.) |
| 1-Jan-2025 | snssg 3769 | The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.) |
| 1-Jan-2025 | snssb 3768 | Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.) |
| 30-Dec-2024 | rex2dom 6917 | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
| 23-Dec-2024 | en2prd 6916 | Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
| 9-Dec-2024 | nninfwlpoim 7288 | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
| 8-Dec-2024 | nninfinfwlpolem 7287 | Lemma for nninfinfwlpo 7289. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemdc 7286 | Lemma for nninfwlpoim 7288. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemginf 7285 | Lemma for nninfwlpoim 7288. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemg 7284 | Lemma for nninfwlpoim 7288. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 7-Dec-2024 | nninfwlpor 7283 | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | nninfwlporlem 7282 | Lemma for nninfwlpor 7283. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | domssr 6876 |
If |
| 7-Dec-2024 | f1dom4g 6851 | The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 6856 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 7-Dec-2024 | f1oen4g 6850 | The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 6855 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 6-Dec-2024 | nninfwlporlemd 7281 | 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 7290 | Decidability of equality for ℕ∞ is equivalent to the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 3-Dec-2024.) |
| 3-Dec-2024 | nninfdcinf 7280 | 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.) |
| 29-Nov-2024 | brdom2g 6843 | Dominance relation. This variation of brdomg 6844 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 6844. (Revised by BTernaryTau, 29-Nov-2024.) |
| 28-Nov-2024 | basmexd 12936 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
| 22-Nov-2024 | eliotaeu 5265 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 22-Nov-2024 | eliota 5264 | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 18-Nov-2024 | basmex 12935 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
| 14-Nov-2024 | dcand 935 | A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) (Revised by BJ, 14-Nov-2024.) |
| 12-Nov-2024 | sravscag 14249 | The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.) |
| 12-Nov-2024 | srascag 14248 | The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.) |
| 12-Nov-2024 | slotsdifipndx 13051 | The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.) |
| 11-Nov-2024 | bj-con1st 15761 | Contraposition when the antecedent is a negated stable proposition. See con1dc 858. (Contributed by BJ, 11-Nov-2024.) |
| 11-Nov-2024 | slotsdifdsndx 13101 | The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | plendxnocndx 13090 | The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | basendxnocndx 13089 | The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | slotsdifplendx 13086 | The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | tsetndxnstarvndx 13070 | The slot for the topology is not the slot for the involution in an extensible structure. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | ofeqd 6167 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) |
| 11-Nov-2024 | const 854 | Contraposition when the antecedent is a negated stable proposition. See comment of condc 855. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.) |
| 10-Nov-2024 | slotsdifunifndx 13108 | The index of the slot for the uniform set is not the index of other slots. (Contributed by AV, 10-Nov-2024.) |
| 7-Nov-2024 | ressbasd 12943 | Base set of a structure restriction. (Contributed by Stefan O'Rear, 26-Nov-2014.) (Proof shortened by AV, 7-Nov-2024.) |
| 6-Nov-2024 | oppraddg 13882 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprbasg 13881 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprsllem 13880 | Lemma for opprbasg 13881 and oppraddg 13882. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
| 4-Nov-2024 | lgsfvalg 15526 |
Value of the function |
| 3-Nov-2024 | znmul 14448 | The multiplicative structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| 3-Nov-2024 | znadd 14447 | The additive structure of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| 3-Nov-2024 | znbas2 14446 | The base set of ℤ/nℤ is the same as the quotient ring it is based on. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 3-Nov-2024.) |
| 3-Nov-2024 | znbaslemnn 14445 | Lemma for znbas 14450. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 14-Aug-2015.) (Revised by AV, 13-Jun-2019.) (Revised by AV, 9-Sep-2021.) (Revised by AV, 3-Nov-2024.) |
| 3-Nov-2024 | zlmmulrg 14437 |
Ring operation of a |
| 3-Nov-2024 | zlmplusgg 14436 |
Group operation of a |
| 3-Nov-2024 | zlmbasg 14435 |
Base set of a |
| 3-Nov-2024 | zlmlemg 14434 | Lemma for zlmbasg 14435 and zlmplusgg 14436. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| 2-Nov-2024 | zlmsca 14438 |
Scalar ring of a |
| 1-Nov-2024 | plendxnvscandx 13085 | The slot for the "less than or equal to" ordering is not the slot for the scalar product in an extensible structure. (Contributed by AV, 1-Nov-2024.) |
| 1-Nov-2024 | plendxnscandx 13084 | The slot for the "less than or equal to" ordering is not the slot for the scalar in an extensible structure. (Contributed by AV, 1-Nov-2024.) |
| 1-Nov-2024 | plendxnmulrndx 13083 | The slot for the "less than or equal to" ordering is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 1-Nov-2024.) |
| 1-Nov-2024 | qsqeqor 10802 | The squares of two rational numbers are equal iff one number equals the other or its negative. (Contributed by Jim Kingdon, 1-Nov-2024.) |
| 31-Oct-2024 | dsndxnmulrndx 13098 | The slot for the distance function is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
| 31-Oct-2024 | tsetndxnmulrndx 13069 | The slot for the topology is not the slot for the ring multiplication operation in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
| 31-Oct-2024 | tsetndxnbasendx 13067 | The slot for the topology is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 31-Oct-2024.) |
| 31-Oct-2024 | basendxlttsetndx 13066 | The index of the slot for the base set is less then the index of the slot for the topology in an extensible structure. (Contributed by AV, 31-Oct-2024.) |
| 31-Oct-2024 | tsetndxnn 13065 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.) |
| 30-Oct-2024 | basendxltedgfndx 15653 |
The index value of the |
| 30-Oct-2024 | plendxnbasendx 13081 | The slot for the order is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 30-Oct-2024.) |
| 30-Oct-2024 | basendxltplendx 13080 |
The index value of the |
| 30-Oct-2024 | plendxnn 13079 | The index value of the order slot is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 30-Oct-2024.) |
| 29-Oct-2024 | sradsg 14254 | Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | sratsetg 14251 | Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | sramulrg 14247 | Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | sraaddgg 14246 | Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | srabaseg 14245 | Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | sralemg 14244 | Lemma for srabaseg 14245 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.) |
| 29-Oct-2024 | dsndxntsetndx 13100 | The slot for the distance function is not the slot for the topology in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| 29-Oct-2024 | slotsdnscsi 13099 |
The slots Scalar, |
| 29-Oct-2024 | slotstnscsi 13071 |
The slots Scalar, |
| 29-Oct-2024 | ipndxnmulrndx 13050 | The slot for the inner product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| 29-Oct-2024 | ipndxnplusgndx 13049 | The slot for the inner product is not the slot for the group operation in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| 29-Oct-2024 | vscandxnmulrndx 13037 | The slot for the scalar product is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| 29-Oct-2024 | scandxnmulrndx 13032 | The slot for the scalar field is not the slot for the ring (multiplication) operation in an extensible structure. (Contributed by AV, 29-Oct-2024.) |
| 29-Oct-2024 | fiubnn 10982 | 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 10981 | A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 29-Oct-2024 | fiubm 10980 | Lemma for fiubz 10981 and fiubnn 10982. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 28-Oct-2024 | edgfndxid 15652 | The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.) |
| 28-Oct-2024 | unifndxntsetndx 13107 | The slot for the uniform set is not the slot for the topology in an extensible structure. (Contributed by AV, 28-Oct-2024.) |
| 28-Oct-2024 | basendxltunifndx 13105 | The index of the slot for the base set is less then the index of the slot for the uniform set in an extensible structure. (Contributed by AV, 28-Oct-2024.) |
| 28-Oct-2024 | unifndxnn 13104 | The index of the slot for the uniform set in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.) |
| 28-Oct-2024 | dsndxnbasendx 13096 | The slot for the distance is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) (Proof shortened by AV, 28-Oct-2024.) |
| 28-Oct-2024 | basendxltdsndx 13095 | The index of the slot for the base set is less then the index of the slot for the distance in an extensible structure. (Contributed by AV, 28-Oct-2024.) |
| 28-Oct-2024 | dsndxnn 13094 | The index of the slot for the distance in an extensible structure is a positive integer. (Contributed by AV, 28-Oct-2024.) |
| 27-Oct-2024 | bj-nnst 15753 |
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 16000 for the version not using the definition of
stability.
(Contributed by BJ, 9-Oct-2019.) Prove it in |
| 27-Oct-2024 | bj-imnimnn 15748 | 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 15747 as its last step. (Contributed by BJ, 27-Oct-2024.) |
| 25-Oct-2024 | nnwosdc 12404 | 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.) |
| 23-Oct-2024 | nnwodc 12401 | 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.) |
| 22-Oct-2024 | uzwodc 12402 | 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.) |
| 21-Oct-2024 | nnnotnotr 16000 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 852, it can be proved with reference only to implication and negation (that is, without use of disjunction). (Contributed by Jim Kingdon, 21-Oct-2024.) |
| 21-Oct-2024 | unifndxnbasendx 13106 | The slot for the uniform set is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
| 21-Oct-2024 | ipndxnbasendx 13048 | The slot for the inner product is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
| 21-Oct-2024 | scandxnbasendx 13030 | The slot for the scalar is not the slot for the base set in an extensible structure. (Contributed by AV, 21-Oct-2024.) |
| 20-Oct-2024 | isprm5lem 12507 |
Lemma for isprm5 12508. The interesting direction (showing that
one only
needs to check prime divisors up to the square root of |
| 19-Oct-2024 | resseqnbasd 12949 | The components of an extensible structure except the base set remain unchanged on a structure restriction. (Contributed by Mario Carneiro, 26-Nov-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Revised by AV, 19-Oct-2024.) |
| 18-Oct-2024 | rmodislmod 14157 |
The right module |
| 18-Oct-2024 | mgpress 13737 | Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.) |
| 18-Oct-2024 | dsndxnplusgndx 13097 | The slot for the distance function is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | plendxnplusgndx 13082 | The slot for the "less than or equal to" ordering is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | tsetndxnplusgndx 13068 | The slot for the topology is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | vscandxnscandx 13038 | The slot for the scalar product is not the slot for the scalar field in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | vscandxnplusgndx 13036 | The slot for the scalar product is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | vscandxnbasendx 13035 | The slot for the scalar product is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | scandxnplusgndx 13031 | The slot for the scalar field is not the slot for the group operation in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | starvndxnmulrndx 13020 | The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | starvndxnplusgndx 13019 | The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 18-Oct-2024 | starvndxnbasendx 13018 | The slot for the involution function is not the slot for the base set in an extensible structure. (Contributed by AV, 18-Oct-2024.) |
| 17-Oct-2024 | basendxltplusgndx 12989 | The index of the slot for the base set is less then the index of the slot for the group operation in an extensible structure. (Contributed by AV, 17-Oct-2024.) |
| 17-Oct-2024 | plusgndxnn 12987 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 17-Oct-2024.) |
| 17-Oct-2024 | elnndc 9740 |
Membership of an integer in |
| 14-Oct-2024 | 2zinfmin 11598 | 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.) |
| 14-Oct-2024 | mingeb 11597 |
Equivalence of |
| 13-Oct-2024 | edgfndxnn 15651 | The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.) |
| 13-Oct-2024 | edgfndx 15650 | Index value of the df-edgf 15648 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.) |
| 13-Oct-2024 | prdsvallem 13148 | Lemma for prdsval 13149. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 13149, dependency on df-hom 12977 removed. (Revised by AV, 13-Oct-2024.) |
| 13-Oct-2024 | pcxnn0cl 12677 | Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0letri 9932 | Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0dcle 9931 |
Decidability of |
| 9-Oct-2024 | nn0leexp2 10862 | Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.) |
| 8-Oct-2024 | pclemdc 12655 | Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.) |
| 8-Oct-2024 | elnn0dc 9739 |
Membership of an integer in |
| 7-Oct-2024 | pclemub 12654 | 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 12653 | 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 10861 | Special case of ltexp2 15457 which we use here because we haven't yet defined df-rpcxp 15375 which is used in the current proof of ltexp2 15457. (Contributed by Jim Kingdon, 7-Oct-2024.) |
| 6-Oct-2024 | suprzcl2dc 10389 | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 8053.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) |
| 5-Oct-2024 | zsupssdc 10388 | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 8053.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
| 5-Oct-2024 | suprzubdc 10386 | 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.) |
| 1-Oct-2024 | infex2g 7143 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
| 30-Sep-2024 | unbendc 12869 | An unbounded decidable set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | prmdc 12496 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | dcfi 7090 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 29-Sep-2024 | ssnnct 12862 |
A decidable subset of |
| 29-Sep-2024 | ssnnctlemct 12861 | Lemma for ssnnct 12862. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
| 28-Sep-2024 | nninfdcex 10387 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
| 27-Sep-2024 | infregelbex 9726 | 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.) |
| 26-Sep-2024 | nninfdclemp1 12865 |
Lemma for nninfdc 12868. Each element of the sequence |
| 26-Sep-2024 | nnminle 12400 | 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 12399. (Contributed by Jim Kingdon, 26-Sep-2024.) |
| 25-Sep-2024 | nninfdclemcl 12863 | Lemma for nninfdc 12868. (Contributed by Jim Kingdon, 25-Sep-2024.) |
| 24-Sep-2024 | nninfdclemlt 12866 | Lemma for nninfdc 12868. The function from nninfdclemf 12864 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
| 23-Sep-2024 | nninfdc 12868 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf1 12867 | Lemma for nninfdc 12868. The function from nninfdclemf 12864 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf 12864 |
Lemma for nninfdc 12868. A function from the natural numbers into
|
| 23-Sep-2024 | nnmindc 12399 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | breng 6841 | Equinumerosity relation. This variation of bren 6842 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 6842. (Revised by BTernaryTau, 23-Sep-2024.) |
| 19-Sep-2024 | ssomct 12860 |
A decidable subset of |
| 14-Sep-2024 | nnpredlt 4676 | The predecessor (see nnpredcl 4675) of a nonzero natural number is less than (see df-iord 4417) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
| 13-Sep-2024 | nninfisollemeq 7241 |
Lemma for nninfisol 7242. The case where |
| 13-Sep-2024 | nninfisollemne 7240 |
Lemma for nninfisol 7242. A case where |
| 13-Sep-2024 | nninfisollem0 7239 |
Lemma for nninfisol 7242. The case where |
| 12-Sep-2024 | nninfisol 7242 |
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 By contrast, the point at infinity being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO) (nninfinfwlpo 7289). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
| 8-Sep-2024 | relopabv 4806 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4808. (Contributed by SN, 8-Sep-2024.) |
| 7-Sep-2024 | eulerthlemfi 12594 |
Lemma for eulerth 12599. The set |
| 7-Sep-2024 | modqexp 10818 | 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 12597 |
Lemma for eulerth 12599. A permutation of |
| 2-Sep-2024 | eulerthlemth 12598 | Lemma for eulerth 12599. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlema 12596 | Lemma for eulerth 12599. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlemrprm 12595 |
Lemma for eulerth 12599. |
| 1-Sep-2024 | qusmul2 14335 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
| 30-Aug-2024 | fprodap0f 11991 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 11976 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 11984 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
| 26-Aug-2024 | exmidontri2or 7362 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | exmidontri 7358 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontri2orexmidim 4624 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4623. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontriexmidim 4574 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4573. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 25-Aug-2024 | onntri2or 7365 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | onntri3or 7364 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | csbcow 3105 | Composition law for chained substitutions into a class. Version of csbco 3104 with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 10-Nov-2005.) (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvreuvw 2745 | Version of cbvreuv 2741 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvrexvw 2744 | Version of cbvrexv 2740 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvralvw 2743 | Version of cbvralv 2739 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvabw 2329 | Version of cbvab 2330 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfsbv 1976 |
If |
| 25-Aug-2024 | cbvexvw 1945 | Change bound variable. See cbvexv 1943 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1472. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvalvw 1944 | Change bound variable. See cbvalv 1942 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1472. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfal 1600 |
If |
| 24-Aug-2024 | gcdcomd 12339 |
The |
| 21-Aug-2024 | dvds2addd 12184 | Deduction form of dvds2add 12180. (Contributed by SN, 21-Aug-2024.) |
| 18-Aug-2024 | prdsmulr 13154 | Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsplusg 13153 | Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsbas 13152 | Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdssca 13151 | Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsval 13149 | Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | df-prds 13143 | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 17-Aug-2024 | fprodcl2lem 11960 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
| 16-Aug-2024 | if0ab 15815 |
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
|
| 16-Aug-2024 | fprodunsn 11959 |
Multiply in an additional term in a finite product. See also
fprodsplitsn 11988 which is the same but with a |
| 15-Aug-2024 | bj-charfundcALT 15819 | Alternate proof of bj-charfundc 15818. It was expected to be much shorter since it uses bj-charfun 15817 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.) |
| 15-Aug-2024 | bj-charfun 15817 |
Properties of the characteristic function on the class |
| 15-Aug-2024 | fmelpw1o 15816 |
With a formula
As proved in if0ab 15815, the associated element of |
| 15-Aug-2024 | cnstab 8725 |
Equality of complex numbers is stable. Stability here means
|
| 15-Aug-2024 | subap0d 8724 | 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 4535 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwun 4534 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwund 4533 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwung 4532 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifidss 3587 | 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 3586 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem2 7341 | Lemma for exmidontriim 7344. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem1 7340 | Lemma for exmidontriim 7344. A variation of r19.30dc 2654. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 11-Aug-2024 | nndc 853 |
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
Actually, |
| 10-Aug-2024 | exmidontriim 7344 | 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.) |
| 10-Aug-2024 | exmidontriimlem4 7343 |
Lemma for exmidontriim 7344. The induction step for the induction on
|
| 10-Aug-2024 | exmidontriimlem3 7342 |
Lemma for exmidontriim 7344. What we get to do based on induction on
both
|
| 10-Aug-2024 | nnnninf2 7236 |
Canonical embedding of |
| 10-Aug-2024 | infnninf 7233 |
The point at infinity in ℕ∞ is the constant sequence
equal to
|
| 9-Aug-2024 | ss1o0el1o 7017 |
Reformulation of ss1o0el1 4245 using |
| 9-Aug-2024 | pw1dc0el 7015 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
| 9-Aug-2024 | ss1o0el1 4245 |
A subclass of |
| 8-Aug-2024 | pw1dc1 7018 | 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.) |
| 7-Aug-2024 | pw1fin 7014 |
Excluded middle is equivalent to the power set of |
| 7-Aug-2024 | elomssom 4657 | 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 4658. (Revised by BJ, 7-Aug-2024.) |
| 6-Aug-2024 | bj-charfunbi 15821 |
In an ambient set
This characterization can be applied to singletons when the set |
| 6-Aug-2024 | bj-charfunr 15820 |
If a class
The hypothesis imposes that
The theorem would still hold if the codomain of |
| 6-Aug-2024 | bj-charfundc 15818 |
Properties of the characteristic function on the class |
| 6-Aug-2024 | prodssdc 11944 | 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.) |
| 5-Aug-2024 | fnmptd 15814 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | funmptd 15813 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5313, then prove funmptd 15813 from it, and then prove funmpt 5314 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dcfal 15765 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dctru 15763 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-stfal 15752 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-sttru 15750 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | prod1dc 11941 | Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) (Revised by Jim Kingdon, 5-Aug-2024.) |
| 5-Aug-2024 | 2ssom 6617 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
| 2-Aug-2024 | onntri52 7363 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri24 7361 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri45 7360 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri51 7359 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri13 7357 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri35 7356 |
Double negated ordinal trichotomy.
There are five equivalent statements: (1)
Another way of stating this is that EXMID is equivalent
to
trichotomy, either the (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 1-Aug-2024 | nnral 2497 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1673. (Contributed by Jim Kingdon, 1-Aug-2024.) |
| 31-Jul-2024 | 3nsssucpw1 7355 |
Negated excluded middle implies that |
| 31-Jul-2024 | sucpw1nss3 7354 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | psrbagf 14476 | A finite bag is a function. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 30-Jul-2024.) |
| 30-Jul-2024 | 3nelsucpw1 7353 |
Three is not an element of the successor of the power set of |
| 30-Jul-2024 | sucpw1nel3 7352 |
The successor of the power set of |
| 30-Jul-2024 | sucpw1ne3 7351 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | pw1nel3 7350 |
Negated excluded middle implies that the power set of |
| 30-Jul-2024 | pw1ne3 7349 |
The power set of |
| 30-Jul-2024 | pw1ne1 7348 |
The power set of |
| 30-Jul-2024 | pw1ne0 7347 |
The power set of |
| 29-Jul-2024 | grpcld 13390 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
| 29-Jul-2024 | pw1on 7345 |
The power set of |
| 28-Jul-2024 | exmidpweq 7013 |
Excluded middle is equivalent to the power set of |
| 27-Jul-2024 | dcapnconstALT 16075 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 16074 by means of dceqnconst 16073. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| 27-Jul-2024 | reap0 16071 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolemgt0 16077 | Lemma for nconstwlpo 16079. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolem0 16076 | Lemma for nconstwlpo 16079. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 24-Jul-2024 | tridceq 16069 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 16056 and redcwlpo 16068). Thus, this is an analytic analogue to lpowlpo 7277. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 24-Jul-2024 | iswomni0 16064 |
Weak omniscience stated in terms of equality with |
| 24-Jul-2024 | lpowlpo 7277 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7276. There is an analogue in terms of analytic omniscience principles at tridceq 16069. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 23-Jul-2024 | nconstwlpolem 16078 | Lemma for nconstwlpo 16079. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | dceqnconst 16073 | 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 16068 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.) |
| 23-Jul-2024 | redc0 16070 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | canth 5904 |
No set |
| 22-Jul-2024 | nconstwlpo 16079 |
Existence of a certain non-constant function from reals to integers
implies |
| 15-Jul-2024 | fprodseq 11938 | 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 2512 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 14-Jul-2024 | ralbid2 2511 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 12-Jul-2024 | 2irrexpqap 15494 |
There exist real numbers |
| 12-Jul-2024 | 2logb9irrap 15493 | Example for logbgcd1irrap 15486. 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.) |
| 12-Jul-2024 | erlecpbl 13208 | Translate the relation compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | ercpbl 13207 | Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | ercpbllemg 13206 | Lemma for ercpbl 13207. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfvalg 13205 | Value of the function in qusval 13199. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfval 13204 | Value of the function in qusval 13199. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 11-Jul-2024 | logbgcd1irraplemexp 15484 |
Lemma for logbgcd1irrap 15486. Apartness of |
| 11-Jul-2024 | reapef 15294 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) |
| 10-Jul-2024 | apcxp2 15455 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) |
| 9-Jul-2024 | logbgcd1irraplemap 15485 | Lemma for logbgcd1irrap 15486. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 9-Jul-2024 | apexp1 10870 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 5-Jul-2024 | logrpap0 15393 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) |
| 3-Jul-2024 | rplogbval 15461 | 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.) |
| 3-Jul-2024 | logrpap0d 15394 | Deduction form of logrpap0 15393. (Contributed by Jim Kingdon, 3-Jul-2024.) |
| 3-Jul-2024 | logrpap0b 15392 | 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 16005 |
Mapping zero and one between |
| 28-Jun-2024 | 012of 16004 |
Mapping zero and one between |
| 27-Jun-2024 | iooreen 16048 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
| 27-Jun-2024 | iooref1o 16047 | 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 16080 | Lemma for neapmkv 16081. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnn 16066 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnnlem 16065 | Lemma for ismkvnn 16066. The result, with a hypothesis to give a name to an expression for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | enmkvlem 7270 | Lemma for enmkv 7271. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 24-Jun-2024 | neapmkv 16081 | 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.) |
| 24-Jun-2024 | dcapnconst 16074 |
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 16056 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 16073 and in fact this theorem can be proved using dceqnconst 16073 as shown at dcapnconstALT 16075. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
| 24-Jun-2024 | enmkv 7271 |
Being Markov is invariant with respect to equinumerosity. For example,
this means that we can express the Markov's Principle as either
|
| 21-Jun-2024 | redcwlpolemeq1 16067 | Lemma for redcwlpo 16068. A biconditionalized version of trilpolemeq1 16053. (Contributed by Jim Kingdon, 21-Jun-2024.) |
| 20-Jun-2024 | redcwlpo 16068 |
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 16067). 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 10394 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | iswomninn 16063 |
Weak omniscience stated in terms of natural numbers. Similar to
iswomnimap 7275 but it will sometimes be more convenient to
use |
| 20-Jun-2024 | iswomninnlem 16062 | Lemma for iswomnimap 7275. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | enwomni 7279 |
Weak omniscience is invariant with respect to equinumerosity. For
example, this means that we can express the Weak Limited Principle of
Omniscience as either |
| 20-Jun-2024 | enwomnilem 7278 | Lemma for enwomni 7279. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 19-Jun-2024 | rpabscxpbnd 15456 | 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 15438 |
The exponential function with exponent |
| 16-Jun-2024 | biadanid 614 | Deduction associated with biadani 612. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| 13-Jun-2024 | rpcxpadd 15421 | 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 15420 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcncxpcl 15418 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcxp0 15414 | 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 15412 | 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 15411 | 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 15410 | 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 15375 | Define the power function on complex numbers. Because df-relog 15374 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 16058 |
Version of trirec0 16057 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 16057 |
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 16056). (Contributed by Jim Kingdon, 10-Jun-2024.) |
| 9-Jun-2024 | omniwomnimkv 7276 |
A set is omniscient if and only if it is weakly omniscient and Markov.
The case |
| 9-Jun-2024 | iswomnimap 7275 | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | iswomni 7274 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | df-womni 7273 |
A weakly omniscient set is one where we can decide whether a predicate
(here represented by a function
In particular, 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.) |
| 1-Jun-2024 | ringcmnd 13841 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ringabld 13840 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | cmnmndd 13688 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ablcmnd 13672 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | grpmndd 13389 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | fndmi 5379 | The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.) |
| 29-May-2024 | pw1nct 16014 | 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 16013 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
| 26-May-2024 | elpwi2 4206 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
| 25-May-2024 | mplnegfi 14511 | The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.) |
| 24-May-2024 | dvmptcjx 15240 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) |
| 23-May-2024 | cbvralfw 2729 | Rule used to change bound variables, using implicit substitution. Version of cbvralf 2731 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 1531 and ax-bndl 1533 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.) |
| 22-May-2024 | efltlemlt 15290 | Lemma for eflt 15291. The converse of efltim 12053 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) |
| 21-May-2024 | eflt 15291 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.) |
| 20-May-2024 | nsyl5 651 | A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.) |
| 19-May-2024 | apdifflemr 16060 | Lemma for apdiff 16061. (Contributed by Jim Kingdon, 19-May-2024.) |
| 18-May-2024 | apdifflemf 16059 |
Lemma for apdiff 16061. Being apart from the point halfway between
|
| 17-May-2024 | apdiff 16061 | 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.) |
| 16-May-2024 | lmodgrpd 14103 | A left module is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crnggrpd 13816 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crngringd 13815 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | ringgrpd 13811 | A ring is a group. (Contributed by SN, 16-May-2024.) |
| 15-May-2024 | reeff1oleme 15288 | Lemma for reeff1o 15289. (Contributed by Jim Kingdon, 15-May-2024.) |
| 14-May-2024 | df-relog 15374 | 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.) |
| 14-May-2024 | fvmpopr2d 6089 | Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.) |
| 12-May-2024 | dvdstrd 12185 | The divides relation is transitive, a deduction version of dvdstr 12183. (Contributed by metakunt, 12-May-2024.) |
| 7-May-2024 | ioocosf1o 15370 | 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 15368 |
Cosine is between minus one and one on the open interval between zero and
|
| 6-May-2024 | cos11 15369 |
Cosine is one-to-one over the closed interval from |
| 5-May-2024 | omiunct 12859 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12855 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
| 5-May-2024 | ctiunctal 12856 |
Variation of ctiunct 12855 which allows |
| 3-May-2024 | cc4n 7390 |
Countable choice with a simpler restriction on how every set in the
countable collection needs to be inhabited. That is, compared with
cc4 7389, the hypotheses only require an A(n) for each
value of |
| 3-May-2024 | cc4f 7388 |
Countable choice by showing the existence of a function |
| 1-May-2024 | cc4 7389 |
Countable choice by showing the existence of a function |
| 29-Apr-2024 | cc3 7387 | Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.) |
| 27-Apr-2024 | cc2 7386 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc2lem 7385 | Lemma for cc2 7386. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc1 7384 | Countable choice in terms of a choice function on a countably infinite set of inhabited sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 24-Apr-2024 | lsppropd 14238 | If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.) |
| 19-Apr-2024 | omctfn 12858 | 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.) |
| 13-Apr-2024 | prodmodclem2 11932 | Lemma for prodmodc 11933. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) |
| 11-Apr-2024 | prodmodclem2a 11931 | Lemma for prodmodc 11933. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
| 11-Apr-2024 | prodmodclem3 11930 | Lemma for prodmodc 11933. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
| 10-Apr-2024 | jcnd 654 | 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 11926 | Lemma for prodrbdc 11929. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) |
| 24-Mar-2024 | prodfdivap 11902 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
| 24-Mar-2024 | prodfrecap 11901 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
| 23-Mar-2024 | prodfap0 11900 | 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 11896 | 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 11906 |
Define the product of a series with an index set of integers |
| 19-Mar-2024 | cos02pilt1 15367 |
Cosine is less than one between zero and |
| 19-Mar-2024 | cosq34lt1 15366 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) |
| 14-Mar-2024 | coseq0q4123 15350 |
Location of the zeroes of cosine in
|
| 14-Mar-2024 | cosq23lt0 15349 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) |
| 9-Mar-2024 | pilem3 15299 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) |
| 9-Mar-2024 | exmidonfin 7309 | 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 6976 and nnon 4662. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
| 9-Mar-2024 | exmidonfinlem 7308 | Lemma for exmidonfin 7309. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
| 8-Mar-2024 | sin0pilem2 15298 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
| 8-Mar-2024 | sin0pilem1 15297 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
| 7-Mar-2024 | cosz12 15296 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) |
| 6-Mar-2024 | cos12dec 12123 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
| 2-Mar-2024 | scaffvalg 14112 | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
| 2-Mar-2024 | dvrfvald 13939 | Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 2-Mar-2024.) |
| 2-Mar-2024 | plusffvalg 13238 | 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 13361 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
| 25-Feb-2024 | mul2lt0pn 9893 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | mul2lt0np 9892 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | lt0ap0 8728 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | negap0d 8711 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 24-Feb-2024 | lt0ap0d 8729 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) |
| 20-Feb-2024 | ivthdec 15160 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) |
| 20-Feb-2024 | ivthinclemex 15158 | Lemma for ivthinc 15159. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) |
| 19-Feb-2024 | ivthinclemuopn 15154 | Lemma for ivthinc 15159. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) |
| 19-Feb-2024 | dedekindicc 15149 | A Dedekind cut identifies a unique real number. Similar to df-inp 7586 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 13421 | 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 15157 | Lemma for ivthinc 15159. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemdisj 15156 | Lemma for ivthinc 15159. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemur 15155 | Lemma for ivthinc 15159. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemlr 15153 | Lemma for ivthinc 15159. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemum 15151 | Lemma for ivthinc 15159. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemlm 15150 | Lemma for ivthinc 15159. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 17-Feb-2024 | 0subm 13360 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
| 17-Feb-2024 | mndissubm 13351 | 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.) |
| 17-Feb-2024 | mgmsscl 13237 | 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.) |
| 15-Feb-2024 | dedekindicclemeu 15147 | Lemma for dedekindicc 15149. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemlu 15146 | Lemma for dedekindicc 15149. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemlub 15145 | Lemma for dedekindicc 15149. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemloc 15144 | Lemma for dedekindicc 15149. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemub 15143 | Lemma for dedekindicc 15149. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemuub 15142 | Lemma for dedekindicc 15149. 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 15141 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8152 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 15140 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8152 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
| 10-Feb-2024 | cbvexdvaw 1956 | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 1954 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.) |
| 10-Feb-2024 | cbvaldvaw 1955 | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 1953 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.) |
| 6-Feb-2024 | ivthinclemlopn 15152 | Lemma for ivthinc 15159. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) |
| 5-Feb-2024 | ivthinc 15159 | 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 15133 | Lemma for dedekindeu 15139. 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 15138 | Lemma for dedekindeu 15139. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemlu 15137 | Lemma for dedekindeu 15139. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemlub 15136 | Lemma for dedekindeu 15139. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemloc 15135 | Lemma for dedekindeu 15139. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemub 15134 | Lemma for dedekindeu 15139. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 30-Jan-2024 | axsuploc 8152 | 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 8053 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
| 30-Jan-2024 | iotam 5268 |
Representation of "the unique element such that |
| 29-Jan-2024 | sgrpidmndm 13296 | 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.) |
| 26-Jan-2024 | elovmporab1w 6154 | Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by GG, 26-Jan-2024.) |
| 26-Jan-2024 | opabidw 4307 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 4306 with a disjoint variable condition. (Contributed by NM, 14-Apr-1995.) (Revised by GG, 26-Jan-2024.) |
| 26-Jan-2024 | invdisjrab 4041 |
The restricted class abstractions |
| 24-Jan-2024 | axpre-suploclemres 8021 |
Lemma for axpre-suploc 8022. The result. The proof just needs to define
|
| 23-Jan-2024 | ax-pre-suploc 8053 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given Although this and ax-caucvg 8052 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8052. (Contributed by Jim Kingdon, 23-Jan-2024.) |
| 23-Jan-2024 | axpre-suploc 8022 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8053. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
| 22-Jan-2024 | suplocsr 7929 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
| 21-Jan-2024 | bj-el2oss1o 15784 | Shorter proof of el2oss1o 6536 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| 21-Jan-2024 | ltm1sr 7897 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
| 20-Jan-2024 | mndinvmod 13321 | Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.) |
| 20-Jan-2024 | ccats1val1g 11099 | Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by JJ, 20-Jan-2024.) |
| 19-Jan-2024 | suplocsrlempr 7927 |
Lemma for suplocsr 7929. The set |
| 18-Jan-2024 | ccatval1 11061 | Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.) |
| 18-Jan-2024 | ccat0 11060 | The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.) |
| 18-Jan-2024 | suplocsrlemb 7926 |
Lemma for suplocsr 7929. The set |
| 16-Jan-2024 | suplocsrlem 7928 |
Lemma for suplocsr 7929. The set |
| 15-Jan-2024 | eqg0el 13609 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| 14-Jan-2024 | suplocexprlemlub 7844 | Lemma for suplocexpr 7845. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
| 14-Jan-2024 | suplocexprlemub 7843 | Lemma for suplocexpr 7845. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
| 10-Jan-2024 | nfcsbw 3131 | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3132 with a disjoint variable condition. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfsbcw 3129 | Bound-variable hypothesis builder for class substitution. Version of nfsbc 3020 with a disjoint variable condition, which in the future may make it possible to reduce axiom usage. (Contributed by NM, 7-Sep-2014.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfsbcdw 3128 | Version of nfsbcd 3019 with a disjoint variable condition. (Contributed by NM, 23-Nov-2005.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvcsbw 3098 | Version of cbvcsb 3099 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvsbcw 3027 | Version of cbvsbc 3028 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrex2vw 2751 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2753 with a disjoint variable condition, which does not require ax-13 2179. (Contributed by FL, 2-Jul-2012.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvral2vw 2750 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2752 with a disjoint variable condition, which does not require ax-13 2179. (Contributed by NM, 10-Aug-2004.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrexw 2734 | Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2730 with more disjoint variable conditions. Although we don't do so yet, we expect the disjoint variable conditions will allow us to remove reliance on ax-i12 1531 and ax-bndl 1533 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvralw 2733 | Rule used to change bound variables, using implicit substitution. Version of cbvral 2735 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 1531 and ax-bndl 1533 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrexfw 2730 | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2732 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 1531 and ax-bndl 1533 in the proof. (Contributed by FL, 27-Apr-2008.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfralw 2544 |
Bound-variable hypothesis builder for restricted quantification. See
nfralya 2547 for a version with |
| 10-Jan-2024 | nfraldw 2539 |
Not-free for restricted universal quantification where |
| 10-Jan-2024 | nfabdw 2368 | Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2369 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvex2vw 1958 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbval2vw 1957 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbv2w 1774 | Rule used to change bound variables, using implicit substitution. Version of cbv2 1773 with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) (Revised by GG, 10-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemloc 7841 | Lemma for suplocexpr 7845. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemdisj 7840 | Lemma for suplocexpr 7845. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemru 7839 | Lemma for suplocexpr 7845. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemrl 7837 | Lemma for suplocexpr 7845. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlem2b 7834 | Lemma for suplocexpr 7845. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemell 7833 | Lemma for suplocexpr 7845. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 7-Jan-2024 | suplocexpr 7845 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemex 7842 | Lemma for suplocexpr 7845. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemmu 7838 | Lemma for suplocexpr 7845. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemml 7836 | Lemma for suplocexpr 7845. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemss 7835 |
Lemma for suplocexpr 7845. |
| 5-Jan-2024 | dedekindicclemicc 15148 |
Lemma for dedekindicc 15149. Same as dedekindicc 15149, except that we
merely show |
| 5-Jan-2024 | dedekindeu 15139 | A Dedekind cut identifies a unique real number. Similar to df-inp 7586 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.) |
| 1-Jan-2024 | ccatlen 11059 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
| 31-Dec-2023 | dvmptsubcn 15239 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
| 31-Dec-2023 | dvmptnegcn 15238 | 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 15237 | 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 | rinvmod 13689 | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6147. (Contributed by AV, 31-Dec-2023.) |
| 31-Dec-2023 | brm 4098 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
| 30-Dec-2023 | dvmptccn 15231 | 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 15230 | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
| 30-Dec-2023 | eqwrd 11041 | Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.) |
| 29-Dec-2023 | mndbn0 13307 | The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 13306). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
| 28-Dec-2023 | mulgnn0gsum 13508 | Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.) |
| 28-Dec-2023 | mulgnngsum 13507 | Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.) |
| 26-Dec-2023 | gsumfzreidx 13717 |
Re-index a finite group sum using a bijection. Corresponds to the first
equation in [Lang] p. 5 with |
| 26-Dec-2023 | gsumsplit1r 13274 | Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.) |
| 26-Dec-2023 | lidrididd 13258 |
If there is a left and right identity element for any binary operation
(group operation) |
| 26-Dec-2023 | lidrideqd 13257 |
If there is a left and right identity element for any binary operation
(group operation) |
| 25-Dec-2023 | ctfoex 7227 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
| 23-Dec-2023 | enct 12848 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
| 23-Dec-2023 | enctlem 12847 | Lemma for enct 12848. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
| 23-Dec-2023 | omct 7226 |
|
| 21-Dec-2023 | dvcoapbr 15223 |
The chain rule for derivatives at a point. The
|
| 19-Dec-2023 | apsscn 8727 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) |
| 19-Dec-2023 | aprcl 8726 | Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.) |
| 18-Dec-2023 | limccoap 15194 |
Composition of two limits. This theorem is only usable in the case
where |
| 16-Dec-2023 | cnreim 11333 | Complex apartness in terms of real and imaginary parts. See also apreim 8683 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) |
| 14-Dec-2023 | cnopnap 15127 | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) |
| 14-Dec-2023 | cnovex 14712 | 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 15062 | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) |
| 12-Dec-2023 | cnopncntop 15060 | 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 15058 | 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 15760 | Clavius law for stable formulas. See pm2.18dc 857. (Contributed by BJ, 4-Dec-2023.) |
| 4-Dec-2023 | bj-nnclavius 15747 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) |
| 2-Dec-2023 | dvmulxx 15220 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 15218. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.) |
| 1-Dec-2023 | dvmulxxbr 15218 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 15220. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.) |
| 29-Nov-2023 | subctctexmid 16011 | 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.) |
| 29-Nov-2023 | ismkvnex 7264 |
The predicate of being Markov stated in terms of double negation and
comparison with |
| 28-Nov-2023 | ccfunen 7383 | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) |
| 28-Nov-2023 | exmid1stab 4256 |
If every proposition is stable, excluded middle follows. We are
thinking of |
| 27-Nov-2023 | df-cc 7382 | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7325 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) |
| 26-Nov-2023 | offeq 6179 | 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 15219 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 15217. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) |
| 25-Nov-2023 | dvaddxxbr 15217 |
The sum rule for derivatives at a point. That is, if the derivative
of |
| 25-Nov-2023 | dcnn 850 | Decidability of the negation of a proposition is equivalent to decidability of its double negation. See also dcn 844. The relation between dcn 844 and dcnn 850 is analogous to that between notnot 630 and notnotnot 635 (and directly stems from it). Using the notion of "testable proposition" (proposition whose negation is decidable), dcnn 850 means that a proposition is testable if and only if its negation is testable, and dcn 844 means that decidability implies testability. (Contributed by David A. Wheeler, 6-Dec-2018.) (Proof shortened by BJ, 25-Nov-2023.) |
| 24-Nov-2023 | bj-dcst 15771 | Stability of a proposition is decidable if and only if that proposition is stable. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-nnbidc 15767 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 15754. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-dcstab 15766 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
| 24-Nov-2023 | bj-fadc 15764 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-trdc 15762 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-stal 15759 | The universal quantification of a stable formula is stable. See bj-stim 15756 for implication, stabnot 835 for negation, and bj-stan 15757 for conjunction. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-stand 15758 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 15757. Its proof is shorter (when counting all steps, including syntactic steps), so one could prove it first and then bj-stan 15757 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) |
| 24-Nov-2023 | bj-stan 15757 | The conjunction of two stable formulas is stable. See bj-stim 15756 for implication, stabnot 835 for negation, and bj-stal 15759 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-stim 15756 | A conjunction with a stable consequent is stable. See stabnot 835 for negation , bj-stan 15757 for conjunction , and bj-stal 15759 for universal quantification. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-nnbist 15754 |
If a formula is not refutable, then it is stable if and only if it is
provable. By double-negation translation, if |
| 24-Nov-2023 | bj-fast 15751 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-trst 15749 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-nnan 15746 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) |
| 24-Nov-2023 | bj-nnim 15745 | 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 15743 | 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 1673 | 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 6175 | 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 7328 | The axiom of choice implies excluded middle. See acexmid 5950 for more discussion of this theorem and a way of stating it without using CHOICE or EXMID. (Contributed by Jim Kingdon, 21-Nov-2023.) |
| 21-Nov-2023 | exmidaclem 7327 | Lemma for exmidac 7328. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) |
| 21-Nov-2023 | exmid1dc 4248 |
A convenience theorem for proving that something implies EXMID.
Think of this as an alternative to using a proposition, as in proofs
like undifexmid 4241 or ordtriexmid 4573. In this context |
| 20-Nov-2023 | acfun 7326 | 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.) |
| 18-Nov-2023 | rnrhmsubrg 14058 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) |
| 18-Nov-2023 | condc 855 |
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.) |
| 18-Nov-2023 | stdcn 849 | 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 844. (Contributed by BJ, 18-Nov-2023.) |
| 17-Nov-2023 | cnplimclemr 15185 | Lemma for cnplimccntop 15186. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
| 17-Nov-2023 | cnplimclemle 15184 | Lemma for cnplimccntop 15186. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) |
| 14-Nov-2023 | limccnp2cntop 15193 | 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.) |
| 10-Nov-2023 | rpmaxcl 11578 | The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.) |
| 9-Nov-2023 | limccnp2lem 15192 | Lemma for limccnp2cntop 15193. 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.) |
| 4-Nov-2023 | ellimc3apf 15176 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 4-Nov-2023.) |
| 3-Nov-2023 | limcmpted 15179 | Express the limit operator for a function defined by a mapping, via epsilon-delta. (Contributed by Jim Kingdon, 3-Nov-2023.) |
| 1-Nov-2023 | unct 12857 | 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 12855 |
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
For "countably many countable sets" the key hypothesis would
be
Compare with the case of two sets instead of countably many, as seen at unct 12857, 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 12810) and using the first number to map to an
element
(Contributed by Jim Kingdon, 31-Oct-2023.) |
| 30-Oct-2023 | ctssdccl 7220 |
A mapping from a decidable subset of the natural numbers onto a
countable set. This is similar to one direction of ctssdc 7222 but
expressed in terms of classes rather than |
| 28-Oct-2023 | ctiunctlemfo 12854 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | ctiunctlemf 12853 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | ctiunctlemudc 12852 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | ctiunctlemuom 12851 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | ctiunctlemu2nd 12850 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | ctiunctlemu1st 12849 | Lemma for ctiunct 12855. (Contributed by Jim Kingdon, 28-Oct-2023.) |
| 28-Oct-2023 | pm2.521gdc 870 | A general instance of Theorem *2.521 of [WhiteheadRussell] p. 107, under a decidability condition. (Contributed by BJ, 28-Oct-2023.) |
| 28-Oct-2023 | stdcndc 847 | 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.) |
| 28-Oct-2023 | conax1k 656 | Weakening of conax1 655. General instance of pm2.51 657 and of pm2.52 658. (Contributed by BJ, 28-Oct-2023.) |
| 28-Oct-2023 | conax1 655 | Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.) |
| 25-Oct-2023 | divcnap 15081 | 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.) |
| 23-Oct-2023 | cnm 7952 | 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 6264 | Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.) |
| 22-Oct-2023 | addcncntoplem 15077 | Lemma for addcncntop 15078, subcncntop 15079, and mulcncntop 15080. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) |
| 22-Oct-2023 | txmetcnp 15034 | 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 15024 |
The maximum metric (Chebyshev distance) on the product of two sets,
expressed in terms of balls centered on a point |
| 15-Oct-2023 | xmettxlem 15025 | Lemma for xmettx 15026. (Contributed by Jim Kingdon, 15-Oct-2023.) |
| 11-Oct-2023 | xmettx 15026 | 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 15023 | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) |
| 7-Oct-2023 | df-iress 12884 |
Define a multifunction restriction operator for extensible structures,
which can be used to turn statements about rings into statements about
subrings, modules into submodules, etc. This definition knows nothing
about individual structures and merely truncates the (Credit for this operator, as well as the 2023 modification for iset.mm, goes to Mario Carneiro.) (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 7-Oct-2023.) |
| 29-Sep-2023 | syl2anc2 412 | Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.) |
| 27-Sep-2023 | fnpr2ob 13216 | Biconditional version of fnpr2o 13215. (Contributed by Jim Kingdon, 27-Sep-2023.) |
| 25-Sep-2023 | xpsval 13228 | Value of the binary structure product function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
| 25-Sep-2023 | fvpr1o 13218 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
| 25-Sep-2023 | fvpr0o 13217 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) |
| 25-Sep-2023 | fnpr2o 13215 |
Function with a domain of |
| 25-Sep-2023 | df-xps 13180 | Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) |
| 12-Sep-2023 | pwntru 4247 | A slight strengthening of pwtrufal 16008. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) |
| 11-Sep-2023 | pwtrufal 16008 |
A subset of the singleton |
| 9-Sep-2023 | mathbox 15742 |
(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 7153 | 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 16010 |
An exercise related to |
| 3-Sep-2023 | pwle2 16009 |
An exercise related to |
| 30-Aug-2023 | isomninn 16044 |
Omniscience stated in terms of natural numbers. Similar to isomnimap 7246
but it will sometimes be more convenient to use |
| 30-Aug-2023 | isomninnlem 16043 | Lemma for isomninn 16044. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) |
| 28-Aug-2023 | trilpolemisumle 16051 | Lemma for trilpo 16056. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) |
| 25-Aug-2023 | cvgcmp2n 16046 | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) |
| 25-Aug-2023 | cvgcmp2nlemabs 16045 |
Lemma for cvgcmp2n 16046. The partial sums get closer to each other
as
we go further out. The proof proceeds by rewriting
|
| 24-Aug-2023 | trilpolemclim 16049 | Lemma for trilpo 16056. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) |
| 23-Aug-2023 | trilpo 16056 |
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 16054 (which means the sequence contains a zero), trilpolemeq1 16053 (which means the sequence is all ones), and trilpolemgt1 16052 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 16042) or that the real numbers are a discrete field (see trirec0 16057). 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 10390 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.) |
| 23-Aug-2023 | trilpolemres 16055 | Lemma for trilpo 16056. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) |
| 23-Aug-2023 | trilpolemlt1 16054 |
Lemma for trilpo 16056. The |
| 23-Aug-2023 | trilpolemeq1 16053 |
Lemma for trilpo 16056. The |
| 23-Aug-2023 | trilpolemgt1 16052 |
Lemma for trilpo 16056. The |
| 23-Aug-2023 | trilpolemcl 16050 | Lemma for trilpo 16056. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) |
| 23-Aug-2023 | triap 16042 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) |
| 19-Aug-2023 | djuenun 7331 | 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 7221 | Lemma for ctssdc 7222. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) |
| 16-Aug-2023 | ctssdclemn0 7219 |
Lemma for ctssdc 7222. The |
| 15-Aug-2023 | ctssexmid 7259 | The decidability condition in ctssdc 7222 is needed. More specifically, ctssdc 7222 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) |
| 15-Aug-2023 | ctssdc 7222 | 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 7259. (Contributed by Jim Kingdon, 15-Aug-2023.) |
| 14-Aug-2023 | mpoexw 6306 | Weak version of mpoex 6307 that holds without ax-coll 4163. 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 13418 | 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 8207 |
Negative trichotomy property for real numbers. It is well known that we
cannot prove real number trichotomy, |
| 13-Aug-2023 | mptexw 6205 | Weak version of mptex 5817 that holds without ax-coll 4163. 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 6204 | Weak version of funex 5814 that holds without ax-coll 4163. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.) |
| 11-Aug-2023 | qnnen 12846 | 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 12842 |
Lemma for ctinfom 12843. Converting between |
| 9-Aug-2023 | difinfsnlem 7208 |
Lemma for difinfsn 7209. The case where we need to swap |
| 8-Aug-2023 | difinfinf 7210 | An infinite set minus a finite subset is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
| 8-Aug-2023 | difinfsn 7209 | An infinite set minus one element is infinite. We require that the set has decidable equality. (Contributed by Jim Kingdon, 8-Aug-2023.) |
| 7-Aug-2023 | ctinf 12845 | 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.) |
| 7-Aug-2023 | inffinp1 12844 | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) |
| 7-Aug-2023 | ctinfom 12843 |
A condition for a set being countably infinite. Restates ennnfone 12840 in
terms of |
| 6-Aug-2023 | rerestcntop 15074 | The subspace topology induced by a subset of the reals. (Contributed by Mario Carneiro, 13-Aug-2014.) (Revised by Jim Kingdon, 6-Aug-2023.) |
| 6-Aug-2023 | tgioo2cntop 15073 | 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.) |
| 4-Aug-2023 | nninffeq 16031 |
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,
|
| 3-Aug-2023 | txvalex 14770 |
Existence of the binary topological product. If |
| 3-Aug-2023 | ablgrpd 13670 | An Abelian group is a group, deduction form of ablgrp 13669. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | 1nsgtrivd 13599 | A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | triv1nsgd 13598 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | trivnsgd 13597 | The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | 0idnsgd 13596 | The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | trivsubgsnd 13581 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | trivsubgd 13580 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | mulgcld 13524 | Deduction associated with mulgcl 13519. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | hashfingrpnn 13412 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | hashfinmndnn 13308 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | dvdsgcdidd 12359 | 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 12358 |
The greatest common divisor of a nonnegative integer |
| 3-Aug-2023 | fihashelne0d 10949 | A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | phpeqd 7039 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6969 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | enpr2d 6918 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | elrnmpt2d 4938 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | elrnmptdv 4937 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | rspcime 2885 | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 3-Aug-2023 | neqcomd 2211 | Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| 2-Aug-2023 | dvid 15211 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
| 2-Aug-2023 | dvconst 15210 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
| 2-Aug-2023 | dvidlemap 15207 | Lemma for dvid 15211 and dvconst 15210. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) |
| 2-Aug-2023 | diveqap1bd 8916 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8785. Converse of diveqap1d 8878. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.) |
| 31-Jul-2023 | mul0inf 11596 | Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11417 and mulap0bd 8737 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.) |
| 31-Jul-2023 | mul0eqap 8750 | 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 8704 | Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.) |
| 30-Jul-2023 | uzennn 10588 | An upper integer set is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 30-Jul-2023.) |
| 30-Jul-2023 | djuen 7330 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) |
| 30-Jul-2023 | endjudisj 7329 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) |
| 30-Jul-2023 | eninr 7207 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
| 30-Jul-2023 | eninl 7206 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) |
| 29-Jul-2023 | exmidunben 12841 |
If any unbounded set of positive integers is equinumerous to |
| 29-Jul-2023 | exmidsssnc 4251 |
Excluded middle in terms of subsets of a singleton. This is similar to
exmid01 4246 but lets you choose any set as the element of
the singleton
rather than just |
| 28-Jul-2023 | dvfcnpm 15206 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.) |
| 28-Jul-2023 | dvfpm 15205 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.) |
| 24-Jul-2023 | sraring 14255 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| 23-Jul-2023 | ennnfonelemhdmp1 12824 | Lemma for ennnfone 12840. Domain at a successor where we need to add an element to the sequence. (Contributed by Jim Kingdon, 23-Jul-2023.) |
| 23-Jul-2023 | ennnfonelemp1 12821 |
Lemma for ennnfone 12840. Value of |
| 22-Jul-2023 | nntr2 6596 | Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.) |
| 22-Jul-2023 | nnsssuc 6595 | 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.) |
| 22-Jul-2023 | relopabiv 4805 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopabi 4807. (Contributed by BJ, 22-Jul-2023.) |
| 21-Jul-2023 | ennnfoneleminc 12826 |
Lemma for ennnfone 12840. We only add elements to |
| 20-Jul-2023 | ennnfonelemg 12818 |
Lemma for ennnfone 12840. Closure for |
| 20-Jul-2023 | ennnfonelemjn 12817 |
Lemma for ennnfone 12840. Non-initial state for |
| 20-Jul-2023 | ennnfonelemj0 12816 |
Lemma for ennnfone 12840. Initial state for |
| 20-Jul-2023 | seqp1cd 10622 |
Value of the sequence builder function at a successor. A version of
seq3p1 10617 which provides two classes |
| 20-Jul-2023 | seqovcd 10619 | A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10620 and seq1cd 10621 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.) |
| 19-Jul-2023 | ennnfonelemhom 12830 |
Lemma for ennnfone 12840. The sequences in |
| 19-Jul-2023 | ennnfonelemex 12829 |
Lemma for ennnfone 12840. Extending the sequence |
| 19-Jul-2023 | ennnfonelemkh 12827 | Lemma for ennnfone 12840. 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.) |
| 19-Jul-2023 | ennnfonelemom 12823 |
Lemma for ennnfone 12840. |
| 19-Jul-2023 | ennnfonelem1 12822 | Lemma for ennnfone 12840. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) |
| 19-Jul-2023 | seq1cd 10621 |
Initial value of the recursive sequence builder. A version of seq3-1 10614
which provides two classes |
| 17-Jul-2023 | ennnfonelemhf1o 12828 |
Lemma for ennnfone 12840. Each of the functions in |
| 16-Jul-2023 | ennnfonelemen 12836 | Lemma for ennnfone 12840. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) |
| 16-Jul-2023 | ennnfonelemdm 12835 |
Lemma for ennnfone 12840. The function |
| 16-Jul-2023 | ennnfonelemrn 12834 |
Lemma for ennnfone 12840. |
| 16-Jul-2023 | ennnfonelemf1 12833 |
Lemma for ennnfone 12840. |
| 16-Jul-2023 | ennnfonelemfun 12832 |
Lemma for ennnfone 12840. |
| 16-Jul-2023 | ennnfonelemrnh 12831 | Lemma for ennnfone 12840. A consequence of ennnfonelemss 12825. (Contributed by Jim Kingdon, 16-Jul-2023.) |
| 15-Jul-2023 | ennnfonelemss 12825 |
Lemma for ennnfone 12840. We only add elements to |
| 15-Jul-2023 | ennnfonelem0 12820 | Lemma for ennnfone 12840. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) |
| 15-Jul-2023 | ennnfonelemk 12815 | Lemma for ennnfone 12840. (Contributed by Jim Kingdon, 15-Jul-2023.) |
| 15-Jul-2023 | ennnfonelemdc 12814 | Lemma for ennnfone 12840. A direct consequence of fidcenumlemrk 7063. (Contributed by Jim Kingdon, 15-Jul-2023.) |
| Copyright terms: Public domain | W3C HTML validation [external] |