| 
       | 
    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 | ||
| 28-Oct-2025 | nn0maxcl 11390 | The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.) | 
| 28-Oct-2025 | qdcle 10336 | 
Rational  | 
| 17-Oct-2025 | plycoeid3 14993 | 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 6991 | 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 6989 | 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 3560 | 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 12407 | A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.) | 
| 6-Oct-2025 | dvconstss 14934 | Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.) | 
| 6-Oct-2025 | dcfrompeirce 1460 | 
The decidability of a proposition  | 
| 6-Oct-2025 | dcfromcon 1459 | 
The decidability of a proposition  | 
| 6-Oct-2025 | dcfromnotnotr 1458 | 
The decidability of a proposition  | 
| 3-Oct-2025 | dvidre 14933 | Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.) | 
| 3-Oct-2025 | dvconstre 14932 | Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.) | 
| 3-Oct-2025 | dvidsslem 14929 | 
Lemma for dvconstss 14934.  Analogue of dvidlemap 14927 where  | 
| 3-Oct-2025 | dvidrelem 14928 | Lemma for dvidre 14933 and dvconstre 14932. Analogue of dvidlemap 14927 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.) | 
| 28-Sep-2025 | metuex 14111 | Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.) | 
| 28-Sep-2025 | cndsex 14109 | The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.) | 
| 25-Sep-2025 | cntopex 14110 | The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.) | 
| 24-Sep-2025 | mopnset 14108 | 
Getting a set by applying  | 
| 24-Sep-2025 | blfn 14107 | The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.) | 
| 22-Sep-2025 | plycjlemc 14996 | Lemma for plycj 14997. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.) | 
| 20-Sep-2025 | plycolemc 14994 | 
Lemma for plyco 14995.  The result expressed as a sum, with a
degree and
         coefficients for  | 
| 16-Sep-2025 | lgsquadlemofi 15317 | 
Lemma for lgsquad 15321.  There are finitely many members of  | 
| 16-Sep-2025 | lgsquadlemsfi 15316 | 
Lemma for lgsquad 15321.  | 
| 16-Sep-2025 | opabfi 6999 | 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 6195 | 
Principle of unique choice.  This is also called non-choice.  The name
       choice results in its similarity to something like acfun 7274 (with the key
       difference being the change of  | 
| 11-Sep-2025 | expghmap 14163 | 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 14145 | The invertible complex numbers are exactly those apart from zero. This is recapb 8698 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.) | 
| 9-Sep-2025 | gsumfzfsumlemm 14143 | Lemma for gsumfzfsum 14144. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.) | 
| 9-Sep-2025 | gsumfzfsumlem0 14142 | Lemma for gsumfzfsum 14144. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.) | 
| 9-Sep-2025 | gsumfzmhm2 13474 | 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 13473 | 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 12100 | 5 does not divide 6. (Contributed by AV, 8-Sep-2025.) | 
| 8-Sep-2025 | 5ndvds3 12099 | 5 does not divide 3. (Contributed by AV, 8-Sep-2025.) | 
| 6-Sep-2025 | gsumfzconst 13471 | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.) | 
| 31-Aug-2025 | gsumfzmptfidmadd 13469 | 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 13468 | 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 10566 | 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 10613 | 
Rearrange a sum via an arbitrary bijection on  | 
| 25-Aug-2025 | irrmulap 9722 | 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 9721. (Contributed by Jim Kingdon, 25-Aug-2025.) | 
| 19-Aug-2025 | seqp1g 10558 | 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 10555 | 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 10942 | A zero-based sequence is a word. In iswrdinn0 10940 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 13131 | 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 10940 | 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 13127 | 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 13034 | 
An expression for  | 
| 13-Aug-2025 | znidom 14213 | 
The ℤ/nℤ structure is an integral domain when  | 
| 12-Aug-2025 | rrgmex 13817 | A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.) | 
| 10-Aug-2025 | gausslemma2dlem1cl 15300 | 
Lemma for gausslemma2dlem1 15302.  Closure of the body of the
definition
         of  | 
| 9-Aug-2025 | gausslemma2dlem1f1o 15301 | Lemma for gausslemma2dlem1 15302. (Contributed by Jim Kingdon, 9-Aug-2025.) | 
| 7-Aug-2025 | qdclt 10335 | 
Rational  | 
| 22-Jul-2025 | ivthdich 14889 | 
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 14879 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 14888 | 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 14887 | Lemma for ivthdich 14889. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.) | 
| 22-Jul-2025 | hovergt0 14886 | The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.) | 
| 22-Jul-2025 | hoverlt1 14885 | The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.) | 
| 21-Jul-2025 | hoverb 14884 | A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) | 
| 21-Jul-2025 | hovera 14883 | A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) | 
| 21-Jul-2025 | rexeqtrrdv 2704 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) | 
| 21-Jul-2025 | raleqtrrdv 2703 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) | 
| 21-Jul-2025 | rexeqtrdv 2702 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) | 
| 21-Jul-2025 | raleqtrdv 2701 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) | 
| 20-Jul-2025 | hovercncf 14882 | 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 14852 | The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.) | 
| 18-Jul-2025 | maxcncf 14851 | The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.) | 
| 14-Jul-2025 | xnn0nnen 10529 | 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 7189 | 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 12207 | Lemma for nninfct 12208. (Contributed by Jim Kingdon, 10-Jul-2025.) | 
| 8-Jul-2025 | nnnninfen 15665 | 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 12208 | The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.) | 
| 8-Jul-2025 | nninfinf 10535 | ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.) | 
| 7-Jul-2025 | ivthreinc 14881 | 
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 14879).
       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 13031 | Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.) | 
| 28-Jun-2025 | iotaexel 5882 | 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 12930 | 
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 13741 | The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13742. (Contributed by SN, 20-Jun-2025.) | 
| 16-Jun-2025 | fnpsr 14221 | The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.) | 
| 14-Jun-2025 | basm 12739 | A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) | 
| 14-Jun-2025 | elfvm 5591 | If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) | 
| 6-Jun-2025 | pcxqcl 12481 | The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.) | 
| 5-Jun-2025 | xqltnle 10357 | 
"Less than" expressed in terms of "less than or equal to",
for extended
     numbers which are rational or  | 
| 5-Jun-2025 | ceqsexv2d 2803 | 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 12568 | Exercise which may help in understanding the proof of 4sqlemsdc 12569. (Contributed by Jim Kingdon, 30-May-2025.) | 
| 27-May-2025 | iotaexab 5237 | 
Existence of the  | 
| 25-May-2025 | 4sqlemsdc 12569 | 
Lemma for 4sq 12579.  The property of being the sum of four
squares is
         decidable.
 
         The proof involves showing that (for a particular   | 
| 25-May-2025 | 4sqexercise1 12567 | Exercise which may help in understanding the proof of 4sqlemsdc 12569. (Contributed by Jim Kingdon, 25-May-2025.) | 
| 24-May-2025 | 4sqleminfi 12566 | 
Lemma for 4sq 12579.  | 
| 24-May-2025 | 4sqlemffi 12565 | 
Lemma for 4sq 12579.  | 
| 24-May-2025 | 4sqlemafi 12564 | 
Lemma for 4sq 12579.  | 
| 24-May-2025 | infidc 7000 | 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 14177 | 
Set existence for  | 
| 16-May-2025 | rhmex 13713 | Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.) | 
| 15-May-2025 | ghmex 13385 | The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) | 
| 15-May-2025 | mhmex 13094 | The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) | 
| 14-May-2025 | idomcringd 13834 | 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 13824 | 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 13510 | 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 12749. (Contributed by Jim Kingdon, 5-May-2025.) | 
| 5-May-2025 | ablressid 13465 | 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 12749. (Contributed by Jim Kingdon, 5-May-2025.) | 
| 30-Apr-2025 | dvply2g 15002 | 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 14016 | Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.) | 
| 29-Apr-2025 | ressbasid 12748 | The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.) | 
| 28-Apr-2025 | lssmex 13911 | 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 14120 | 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 14118 | 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 14029 | Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.) | 
| 27-Apr-2025 | lssex 13910 | Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.) | 
| 25-Apr-2025 | rspex 14030 | Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.) | 
| 25-Apr-2025 | lspex 13951 | Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.) | 
| 25-Apr-2025 | eqgex 13351 | The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.) | 
| 25-Apr-2025 | qusex 12968 | Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.) | 
| 23-Apr-2025 | 1dom1el 15637 | 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 13253 | Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.) | 
| 20-Apr-2025 | elovmpod 6121 | Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6122 in deduction form. (Revised by AV, 20-Apr-2025.) | 
| 18-Apr-2025 | fsumdvdsmul 15227 | 
Product of two divisor sums.  (This is also the main part of the proof
       that " | 
| 18-Apr-2025 | mpodvdsmulf1o 15226 | 
If  | 
| 18-Apr-2025 | df2idl2 14065 | 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 14057 | 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 14044 | 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 14031 | 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 13985 | 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 14002 | Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.) | 
| 14-Apr-2025 | grpmgmd 13158 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) | 
| 12-Apr-2025 | psraddcl 14232 | 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 15703 | Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.) | 
| 4-Apr-2025 | ghmf1 13403 | 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 14089 | 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 14124 | 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 14113. (Revised by GG, 31-Mar-2025.) | 
| 31-Mar-2025 | cnfldle 14123 | 
The ordering of the field of complex numbers.  Note that this is not
       actually an ordering on  | 
| 31-Mar-2025 | cnfldtset 14122 | 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 14119 | The multiplication operation of the field of complex numbers. Version of cnfldmul 14120 using maps-to notation, which does not require ax-mulf 8002. (Contributed by GG, 31-Mar-2025.) | 
| 31-Mar-2025 | mpocnfldadd 14117 | The addition operation of the field of complex numbers. Version of cnfldadd 14118 using maps-to notation, which does not require ax-addf 8001. (Contributed by GG, 31-Mar-2025.) | 
| 31-Mar-2025 | df-cnfld 14113 | 
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 14115, cnfldadd 14118, cnfldmul 14120, cnfldcj 14121, cnfldtset 14122, cnfldle 14123, cnfldds 14124, and cnfldbas 14116. 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 14080 | 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 13835 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) | 
| 22-Mar-2025 | idomdomd 13833 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) | 
| 21-Mar-2025 | df2idl2rng 14064 | 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 14038 | 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 14037 | 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 12909 | Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.) | 
| 20-Mar-2025 | homslid 12907 | 
Slot property of  | 
| 19-Mar-2025 | ptex 12935 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) | 
| 18-Mar-2025 | prdsex 12940 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) | 
| 16-Mar-2025 | plycn 14998 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8002. (Revised by GG, 16-Mar-2025.) | 
| 16-Mar-2025 | expcn 14805 | 
The power function on complex numbers, for fixed exponent  | 
| 16-Mar-2025 | mpomulcn 14802 | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) | 
| 16-Mar-2025 | mpomulf 8016 | Multiplication is an operation on complex numbers. Version of ax-mulf 8002 using maps-to notation, proved from the axioms of set theory and ax-mulcl 7977. (Contributed by GG, 16-Mar-2025.) | 
| 13-Mar-2025 | 2idlss 14070 | 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 12948 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) | 
| 11-Mar-2025 | rng2idlsubgsubrng 14076 | 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 14073 | 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 14054 | 
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 14053 | 
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 14052 | 
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 12949 | Value of an image structure. The is a lemma for the theorems imasbas 12950, imasplusg 12951, and imasmulr 12952 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 14063 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) | 
| 9-Mar-2025 | 2idllidld 14062 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) | 
| 9-Mar-2025 | quseccl 13363 | 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 6028 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.) | 
| 8-Mar-2025 | subgex 13306 | The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.) | 
| 7-Mar-2025 | ringrzd 13602 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) | 
| 7-Mar-2025 | ringlzd 13601 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) | 
| 7-Mar-2025 | qusecsub 13461 | 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 13360 | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) | 
| 28-Feb-2025 | qusmulrng 14088 | Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14089. Similar to qusmul2 14085. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.) | 
| 28-Feb-2025 | ringressid 13619 | 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 12749. (Contributed by Jim Kingdon, 28-Feb-2025.) | 
| 28-Feb-2025 | grpressid 13193 | 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 12749. (Contributed by Jim Kingdon, 28-Feb-2025.) | 
| 27-Feb-2025 | imasringf1 13621 | The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.) | 
| 26-Feb-2025 | strext 12783 | 
Extending the upper range of a structure.  This works because when we
       say that a structure has components in  | 
| 25-Feb-2025 | subrngringnsg 13761 | A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.) | 
| 25-Feb-2025 | rngansg 13506 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) | 
| 25-Feb-2025 | ecqusaddd 13368 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) | 
| 24-Feb-2025 | ecqusaddcl 13369 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) | 
| 24-Feb-2025 | quseccl0g 13361 | 
Closure of the quotient map for a quotient group.  (Contributed by Mario
       Carneiro, 18-Sep-2015.)  Generalization of quseccl 13363 for arbitrary sets
        | 
| 23-Feb-2025 | ltlenmkv 15714 | 
If  | 
| 23-Feb-2025 | neap0mkv 15713 | 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 14081 | 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 14083 analog). (Contributed by AV, 23-Feb-2025.) | 
| 23-Feb-2025 | 2idlcpblrng 14079 | 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 13752 | 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 13751 | A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) | 
| 23-Feb-2025 | lringring 13750 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) | 
| 23-Feb-2025 | lringnzr 13749 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) | 
| 23-Feb-2025 | islring 13748 | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) | 
| 23-Feb-2025 | df-lring 13747 | 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 13745 | 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 13739 | 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 13514 | The quotient structure of a non-unital ring is a non-unital ring (qusring2 13622 analog). (Contributed by AV, 23-Feb-2025.) | 
| 23-Feb-2025 | rngsubdir 13508 | Ring multiplication distributes over subtraction. (subdir 8412 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 13613. (Revised by AV, 23-Feb-2025.) | 
| 23-Feb-2025 | rngsubdi 13507 | Ring multiplication distributes over subtraction. (subdi 8411 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 13612. (Revised by AV, 23-Feb-2025.) | 
| 22-Feb-2025 | imasrngf1 13513 | 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 13512 | The image structure of a non-unital ring is a non-unital ring (imasring 13620 analog). (Contributed by AV, 22-Feb-2025.) | 
| 22-Feb-2025 | rngmgpf 13493 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 13567 analog). (Contributed by AV, 22-Feb-2025.) | 
| 22-Feb-2025 | imasabl 13466 | The image structure of an abelian group is an abelian group (imasgrp 13241 analog). (Contributed by AV, 22-Feb-2025.) | 
| 21-Feb-2025 | dftap2 7318 | Tight apartness with the apartness properties from df-pap 7315 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.) | 
| 20-Feb-2025 | rng2idlsubg0 14078 | 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 14077 | 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 14075 | 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 14074 | 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 14072 | 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 14071 | The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.) | 
| 20-Feb-2025 | 2idlelb 14061 | Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) | 
| 20-Feb-2025 | aprap 13842 | The relation given by df-apr 13837 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.) | 
| 20-Feb-2025 | setscomd 12719 | Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.) | 
| 20-Feb-2025 | ifnebibdc 3604 | The converse of ifbi 3581 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) | 
| 20-Feb-2025 | ifnefals 3603 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) | 
| 20-Feb-2025 | ifnetruedc 3602 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) | 
| 18-Feb-2025 | rnglidlmcl 14036 | 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 13841 | The apartness relation given by df-apr 13837 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.) | 
| 17-Feb-2025 | aprsym 13840 | The apartness relation given by df-apr 13837 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.) | 
| 17-Feb-2025 | aprval 13838 | Expand Definition df-apr 13837. (Contributed by Jim Kingdon, 17-Feb-2025.) | 
| 17-Feb-2025 | subrngpropd 13772 | 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 13505 | Double negation of a product in a non-unital ring (mul2neg 8424 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 13611. (Revised by AV, 17-Feb-2025.) | 
| 17-Feb-2025 | rngmneg2 13504 | Negation of a product in a non-unital ring (mulneg2 8422 analog). In contrast to ringmneg2 13610, 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 13503 | Negation of a product in a non-unital ring (mulneg1 8421 analog). In contrast to ringmneg1 13609, 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 13839 | The apartness relation given by df-apr 13837 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.) | 
| 16-Feb-2025 | rngrz 13502 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 13600. (Revised by AV, 16-Feb-2025.) | 
| 16-Feb-2025 | rng0cl 13499 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) | 
| 16-Feb-2025 | rngacl 13498 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) | 
| 16-Feb-2025 | rnggrp 13494 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) | 
| 16-Feb-2025 | aptap 8677 | Complex apartness (as defined at df-ap 8609) is a tight apartness (as defined at df-tap 7317). (Contributed by Jim Kingdon, 16-Feb-2025.) | 
| 15-Feb-2025 | subsubrng2 13771 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | subsubrng 13770 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | subrngin 13769 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | subrngintm 13768 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | opprsubrngg 13767 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | issubrng2 13766 | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | opprrngbg 13634 | A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 13633. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | opprrng 13633 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | rngpropd 13511 | 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 13056 | 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 13052 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) | 
| 15-Feb-2025 | tapeq2 7320 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.) | 
| 14-Feb-2025 | subrngmcl 13765 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 13789. (Revised by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngacl 13764 | A subring is closed under addition. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrng0 13763 | A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngbas 13762 | Base set of a subring structure. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngsubg 13760 | A subring is a subgroup. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngrcl 13759 | Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngrng 13758 | A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngid 13757 | Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | subrngss 13756 | A subring is a subset. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | issubrng 13755 | The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | df-subrng 13754 | 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 13509 | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | rngdi 13496 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) | 
| 14-Feb-2025 | exmidmotap 7328 | 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 7327 | 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 7315 | 
Apartness predicate.  A relation  | 
| 13-Feb-2025 | 2idl1 14069 | Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.) | 
| 13-Feb-2025 | 2idl0 14068 | Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.) | 
| 13-Feb-2025 | ridl1 14067 | Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.) | 
| 13-Feb-2025 | ridl0 14066 | Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.) | 
| 13-Feb-2025 | isridl 14060 | 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 13837 | The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 13842. (Contributed by Jim Kingdon, 13-Feb-2025.) | 
| 13-Feb-2025 | rngass 13495 | 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 13055 | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) | 
| 8-Feb-2025 | 2oneel 7323 | 
 | 
| 8-Feb-2025 | tapeq1 7319 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.) | 
| 7-Feb-2025 | resrhm2b 13805 | Restriction of the codomain of a (ring) homomorphism. resghm2b 13392 analog. (Contributed by SN, 7-Feb-2025.) | 
| 6-Feb-2025 | zzlesq 10800 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) | 
| 6-Feb-2025 | 2omotap 7326 | 
If there is at most one tight apartness on  | 
| 6-Feb-2025 | 2omotaplemst 7325 | Lemma for 2omotap 7326. (Contributed by Jim Kingdon, 6-Feb-2025.) | 
| 6-Feb-2025 | 2omotaplemap 7324 | Lemma for 2omotap 7326. (Contributed by Jim Kingdon, 6-Feb-2025.) | 
| 6-Feb-2025 | 2onetap 7322 | 
Negated equality is a tight apartness on  | 
| 5-Feb-2025 | netap 7321 | Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.) | 
| 5-Feb-2025 | df-tap 7317 | 
Tight apartness predicate.  A relation  | 
| 1-Feb-2025 | mulgnn0cld 13273 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13268. (Contributed by SN, 1-Feb-2025.) | 
| 31-Jan-2025 | 0subg 13329 | 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 13188 | The right inverse of a group element. Deduction associated with grprinv 13183. (Contributed by SN, 29-Jan-2025.) | 
| 29-Jan-2025 | grplinvd 13187 | The left inverse of a group element. Deduction associated with grplinv 13182. (Contributed by SN, 29-Jan-2025.) | 
| 29-Jan-2025 | grpinvcld 13181 | A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.) | 
| 29-Jan-2025 | grpridd 13166 | The identity element of a group is a right identity. Deduction associated with grprid 13164. (Contributed by SN, 29-Jan-2025.) | 
| 29-Jan-2025 | grplidd 13165 | The identity element of a group is a left identity. Deduction associated with grplid 13163. (Contributed by SN, 29-Jan-2025.) | 
| 29-Jan-2025 | grpassd 13144 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) | 
| 28-Jan-2025 | dvdsrex 13654 | Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.) | 
| 24-Jan-2025 | reldvdsrsrg 13648 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.) | 
| 18-Jan-2025 | rerecapb 8870 | 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 8698 | 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 12750 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.) | 
| 17-Jan-2025 | strressid 12749 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.) | 
| 16-Jan-2025 | ressex 12743 | Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) | 
| 16-Jan-2025 | ressvalsets 12742 | Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) | 
| 12-Jan-2025 | isrim 13725 | 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 13727 | A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) | 
| 10-Jan-2025 | isrim0 13717 | 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 13629 | 
Existence of the opposite ring.  If you know that  | 
| 10-Jan-2025 | mgpex 13481 | 
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 3757 | The singleton of an element of a class is a subset of the class (inference form of snssg 3756). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.) | 
| 1-Jan-2025 | snssg 3756 | 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 3755 | Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.) | 
| 9-Dec-2024 | nninfwlpoim 7244 | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) | 
| 8-Dec-2024 | nninfwlpoimlemdc 7243 | Lemma for nninfwlpoim 7244. (Contributed by Jim Kingdon, 8-Dec-2024.) | 
| 8-Dec-2024 | nninfwlpoimlemginf 7242 | Lemma for nninfwlpoim 7244. (Contributed by Jim Kingdon, 8-Dec-2024.) | 
| 8-Dec-2024 | nninfwlpoimlemg 7241 | Lemma for nninfwlpoim 7244. (Contributed by Jim Kingdon, 8-Dec-2024.) | 
| 7-Dec-2024 | nninfwlpor 7240 | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) | 
| 7-Dec-2024 | nninfwlporlem 7239 | Lemma for nninfwlpor 7240. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) | 
| 6-Dec-2024 | nninfwlporlemd 7238 | 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 7245 | 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 7237 | 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.) | 
| 28-Nov-2024 | basmexd 12738 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) | 
| 22-Nov-2024 | eliotaeu 5247 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) | 
| 22-Nov-2024 | eliota 5246 | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) | 
| 18-Nov-2024 | basmex 12737 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) | 
| 14-Nov-2024 | dcand 934 | 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 13999 | 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 13998 | 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 12852 | The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.) | 
| 11-Nov-2024 | bj-con1st 15397 | Contraposition when the antecedent is a negated stable proposition. See con1dc 857. (Contributed by BJ, 11-Nov-2024.) | 
| 11-Nov-2024 | slotsdifdsndx 12898 | The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.) | 
| 11-Nov-2024 | slotsdifplendx 12887 | 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 12871 | 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 6137 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) | 
| 11-Nov-2024 | const 853 | Contraposition when the antecedent is a negated stable proposition. See comment of condc 854. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.) | 
| 10-Nov-2024 | slotsdifunifndx 12905 | 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 12745 | 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 13632 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) | 
| 6-Nov-2024 | opprbasg 13631 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) | 
| 6-Nov-2024 | opprsllem 13630 | Lemma for opprbasg 13631 and oppraddg 13632. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) | 
| 4-Nov-2024 | lgsfvalg 15246 | 
Value of the function  | 
| 3-Nov-2024 | znmul 14198 | 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 14197 | 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 14196 | 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 14195 | Lemma for znbas 14200. (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 14187 | 
Ring operation of a  | 
| 3-Nov-2024 | zlmplusgg 14186 | 
Group operation of a  | 
| 3-Nov-2024 | zlmbasg 14185 | 
Base set of a  | 
| 3-Nov-2024 | zlmlemg 14184 | Lemma for zlmbasg 14185 and zlmplusgg 14186. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) | 
| 2-Nov-2024 | zlmsca 14188 | 
Scalar ring of a  | 
| 1-Nov-2024 | plendxnvscandx 12886 | 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 12885 | 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 12884 | 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 10742 | 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 12895 | 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 12870 | 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 12868 | 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 12867 | 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 12866 | 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 | plendxnbasendx 12882 | 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 12881 | 
The index value of the  | 
| 30-Oct-2024 | plendxnn 12880 | 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 14004 | 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 14001 | 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 13997 | 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 13996 | 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 13995 | 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 13994 | Lemma for srabaseg 13995 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 12897 | 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 12896 | 
The slots Scalar,  | 
| 29-Oct-2024 | slotstnscsi 12872 | 
The slots Scalar,  | 
| 29-Oct-2024 | ipndxnmulrndx 12851 | 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 12850 | 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 12838 | 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 12833 | 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 10922 | 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 10921 | A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.) | 
| 29-Oct-2024 | fiubm 10920 | Lemma for fiubz 10921 and fiubnn 10922. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.) | 
| 28-Oct-2024 | unifndxntsetndx 12904 | 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 12902 | 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 12901 | 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 12893 | 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 12892 | 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 12891 | 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 15389 | 
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 15636 for the version not using the definition of
stability.
     (Contributed by BJ, 9-Oct-2019.)  Prove it in  | 
| 27-Oct-2024 | bj-imnimnn 15384 | 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 15383 as its last step. (Contributed by BJ, 27-Oct-2024.) | 
| 25-Oct-2024 | nnwosdc 12206 | 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 12203 | 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 12204 | 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 15636 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 851, 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 12903 | 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 12849 | 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 12831 | 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 12309 | 
Lemma for isprm5 12310.  The interesting direction (showing that
one only
       needs to check prime divisors up to the square root of  | 
| 19-Oct-2024 | resseqnbasd 12751 | 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 13907 | 
The right module  | 
| 18-Oct-2024 | mgpress 13487 | 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 12894 | 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 12883 | 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 12869 | 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 12839 | 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 12837 | 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 12836 | 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 12832 | 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 12821 | 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 12820 | 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 12819 | 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 12791 | 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 12789 | 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 9686 | 
Membership of an integer in  | 
| 14-Oct-2024 | 2zinfmin 11408 | 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 11407 | 
Equivalence of  | 
| 13-Oct-2024 | pcxnn0cl 12479 | Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.) | 
| 13-Oct-2024 | xnn0letri 9878 | Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) | 
| 13-Oct-2024 | xnn0dcle 9877 | 
Decidability of  | 
| 9-Oct-2024 | nn0leexp2 10802 | Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.) | 
| 8-Oct-2024 | pclemdc 12457 | Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.) | 
| 8-Oct-2024 | elnn0dc 9685 | 
Membership of an integer in  | 
| 7-Oct-2024 | pclemub 12456 | 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 12455 | 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 10801 | Special case of ltexp2 15177 which we use here because we haven't yet defined df-rpcxp 15095 which is used in the current proof of ltexp2 15177. (Contributed by Jim Kingdon, 7-Oct-2024.) | 
| 6-Oct-2024 | suprzcl2dc 10329 | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 8000.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) | 
| 5-Oct-2024 | zsupssdc 10328 | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 8000.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) | 
| 5-Oct-2024 | suprzubdc 10326 | 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 7100 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) | 
| 30-Sep-2024 | unbendc 12671 | 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 12298 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) | 
| 30-Sep-2024 | dcfi 7047 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) | 
| 29-Sep-2024 | ssnnct 12664 | 
A decidable subset of  | 
| 29-Sep-2024 | ssnnctlemct 12663 | Lemma for ssnnct 12664. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) | 
| 28-Sep-2024 | nninfdcex 10327 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) | 
| 27-Sep-2024 | infregelbex 9672 | 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 12667 | 
Lemma for nninfdc 12670.  Each element of the sequence  | 
| 26-Sep-2024 | nnminle 12202 | 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 12201. (Contributed by Jim Kingdon, 26-Sep-2024.) | 
| 25-Sep-2024 | nninfdclemcl 12665 | Lemma for nninfdc 12670. (Contributed by Jim Kingdon, 25-Sep-2024.) | 
| 24-Sep-2024 | nninfdclemlt 12668 | Lemma for nninfdc 12670. The function from nninfdclemf 12666 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) | 
| 23-Sep-2024 | nninfdc 12670 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) | 
| 23-Sep-2024 | nninfdclemf1 12669 | Lemma for nninfdc 12670. The function from nninfdclemf 12666 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) | 
| 23-Sep-2024 | nninfdclemf 12666 | 
Lemma for nninfdc 12670.  A function from the natural numbers into
          | 
| 23-Sep-2024 | nnmindc 12201 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) | 
| 19-Sep-2024 | ssomct 12662 | 
A decidable subset of  | 
| 14-Sep-2024 | nnpredlt 4660 | The predecessor (see nnpredcl 4659) of a nonzero natural number is less than (see df-iord 4401) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) | 
| 13-Sep-2024 | nninfisollemeq 7198 | 
Lemma for nninfisol 7199.  The case where  | 
| 13-Sep-2024 | nninfisollemne 7197 | 
Lemma for nninfisol 7199.  A case where  | 
| 13-Sep-2024 | nninfisollem0 7196 | 
Lemma for nninfisol 7199.  The case where  | 
| 12-Sep-2024 | nninfisol 7199 | 
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  | 
| 8-Sep-2024 | relopabv 4790 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4792. (Contributed by SN, 8-Sep-2024.) | 
| 7-Sep-2024 | eulerthlemfi 12396 | 
Lemma for eulerth 12401.  The set  | 
| 7-Sep-2024 | modqexp 10758 | 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 12399 | 
Lemma for eulerth 12401.  A permutation of  | 
| 2-Sep-2024 | eulerthlemth 12400 | Lemma for eulerth 12401. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) | 
| 2-Sep-2024 | eulerthlema 12398 | Lemma for eulerth 12401. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) | 
| 2-Sep-2024 | eulerthlemrprm 12397 | 
Lemma for eulerth 12401.  | 
| 1-Sep-2024 | qusmul2 14085 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) | 
| 30-Aug-2024 | fprodap0f 11801 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 11786 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 11794 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) | 
| 26-Aug-2024 | exmidontri2or 7310 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) | 
| 26-Aug-2024 | exmidontri 7306 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) | 
| 26-Aug-2024 | ontri2orexmidim 4608 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4607. (Contributed by Jim Kingdon, 26-Aug-2024.) | 
| 26-Aug-2024 | ontriexmidim 4558 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4557. (Contributed by Jim Kingdon, 26-Aug-2024.) | 
| 25-Aug-2024 | onntri2or 7313 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) | 
| 25-Aug-2024 | onntri3or 7312 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) | 
| 25-Aug-2024 | csbcow 3095 | Composition law for chained substitutions into a class. Version of csbco 3094 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 2735 | Version of cbvreuv 2731 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | cbvrexvw 2734 | Version of cbvrexv 2730 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | cbvralvw 2733 | Version of cbvralv 2729 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | cbvabw 2319 | Version of cbvab 2320 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | nfsbv 1966 | 
If  | 
| 25-Aug-2024 | cbvexvw 1935 | Change bound variable. See cbvexv 1933 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1462. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | cbvalvw 1934 | Change bound variable. See cbvalv 1932 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1462. (Revised by GG, 25-Aug-2024.) | 
| 25-Aug-2024 | nfal 1590 | 
If  | 
| 24-Aug-2024 | gcdcomd 12141 | 
The  | 
| 21-Aug-2024 | dvds2addd 11994 | Deduction form of dvds2add 11990. (Contributed by SN, 21-Aug-2024.) | 
| 17-Aug-2024 | fprodcl2lem 11770 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) | 
| 16-Aug-2024 | if0ab 15451 | 
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 11769 | 
Multiply in an additional term in a finite product.  See also
       fprodsplitsn 11798 which is the same but with a  | 
| 15-Aug-2024 | bj-charfundcALT 15455 | Alternate proof of bj-charfundc 15454. It was expected to be much shorter since it uses bj-charfun 15453 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 15453 | 
Properties of the characteristic function on the class  | 
| 15-Aug-2024 | fmelpw1o 15452 | 
With a formula  
     As proved in if0ab 15451, the associated element of   | 
| 15-Aug-2024 | cnstab 8672 | 
Equality of complex numbers is stable.  Stability here means
      | 
| 15-Aug-2024 | subap0d 8671 | 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 4519 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) | 
| 15-Aug-2024 | ifelpwun 4518 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) | 
| 15-Aug-2024 | ifelpwund 4517 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) | 
| 15-Aug-2024 | ifelpwung 4516 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) | 
| 15-Aug-2024 | ifidss 3576 | 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 3575 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) | 
| 12-Aug-2024 | exmidontriimlem2 7289 | Lemma for exmidontriim 7292. (Contributed by Jim Kingdon, 12-Aug-2024.) | 
| 12-Aug-2024 | exmidontriimlem1 7288 | Lemma for exmidontriim 7292. A variation of r19.30dc 2644. (Contributed by Jim Kingdon, 12-Aug-2024.) | 
| 11-Aug-2024 | nndc 852 | 
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 7292 | 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 7291 | 
Lemma for exmidontriim 7292.  The induction step for the induction on
        | 
| 10-Aug-2024 | exmidontriimlem3 7290 | 
Lemma for exmidontriim 7292.  What we get to do based on induction on
both
        | 
| 10-Aug-2024 | nnnninf2 7193 | 
Canonical embedding of  | 
| 10-Aug-2024 | infnninf 7190 | 
The point at infinity in ℕ∞ is the constant sequence
equal to
        | 
| 9-Aug-2024 | ss1o0el1o 6974 | 
Reformulation of ss1o0el1 4230 using  | 
| 9-Aug-2024 | pw1dc0el 6972 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) | 
| 9-Aug-2024 | ss1o0el1 4230 | 
A subclass of  | 
| 8-Aug-2024 | pw1dc1 6975 | 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 6971 | 
Excluded middle is equivalent to the power set of  | 
| 7-Aug-2024 | elomssom 4641 | 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 4642. (Revised by BJ, 7-Aug-2024.) | 
| 6-Aug-2024 | bj-charfunbi 15457 | 
In an ambient set  
       This characterization can be applied to singletons when the set   | 
| 6-Aug-2024 | bj-charfunr 15456 | 
If a class  
       The hypothesis imposes that  
       The theorem would still hold if the codomain of   | 
| 6-Aug-2024 | bj-charfundc 15454 | 
Properties of the characteristic function on the class  | 
| 6-Aug-2024 | prodssdc 11754 | 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 15450 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) | 
| 5-Aug-2024 | funmptd 15449 | 
The maps-to notation defines a function (deduction form).
 Note: one should similarly prove a deduction form of funopab4 5295, then prove funmptd 15449 from it, and then prove funmpt 5296 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.)  | 
| 5-Aug-2024 | bj-dcfal 15401 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | 
| 5-Aug-2024 | bj-dctru 15399 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) | 
| 5-Aug-2024 | bj-stfal 15388 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) | 
| 5-Aug-2024 | bj-sttru 15386 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) | 
| 5-Aug-2024 | prod1dc 11751 | 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 6582 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) | 
| 2-Aug-2024 | onntri52 7311 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) | 
| 2-Aug-2024 | onntri24 7309 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) | 
| 2-Aug-2024 | onntri45 7308 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) | 
| 2-Aug-2024 | onntri51 7307 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) | 
| 2-Aug-2024 | onntri13 7305 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) | 
| 2-Aug-2024 | onntri35 7304 | 
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 2487 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1663. (Contributed by Jim Kingdon, 1-Aug-2024.) | 
| 31-Jul-2024 | 3nsssucpw1 7303 | 
Negated excluded middle implies that  | 
| 31-Jul-2024 | sucpw1nss3 7302 | 
Negated excluded middle implies that the successor of the power set of
      | 
| 30-Jul-2024 | psrbagf 14224 | 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 7301 | 
Three is not an element of the successor of the power set of  | 
| 30-Jul-2024 | sucpw1nel3 7300 | 
The successor of the power set of  | 
| 30-Jul-2024 | sucpw1ne3 7299 | 
Negated excluded middle implies that the successor of the power set of
      | 
| 30-Jul-2024 | pw1nel3 7298 | 
Negated excluded middle implies that the power set of  | 
| 30-Jul-2024 | pw1ne3 7297 | 
The power set of  | 
| 30-Jul-2024 | pw1ne1 7296 | 
The power set of  | 
| 30-Jul-2024 | pw1ne0 7295 | 
The power set of  | 
| 29-Jul-2024 | grpcld 13146 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) | 
| 29-Jul-2024 | pw1on 7293 | 
The power set of  | 
| 28-Jul-2024 | exmidpweq 6970 | 
Excluded middle is equivalent to the power set of  | 
| 27-Jul-2024 | dcapnconstALT 15706 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 15705 by means of dceqnconst 15704. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) | 
| 27-Jul-2024 | reap0 15702 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) | 
| 26-Jul-2024 | nconstwlpolemgt0 15708 | Lemma for nconstwlpo 15710. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) | 
| 26-Jul-2024 | nconstwlpolem0 15707 | Lemma for nconstwlpo 15710. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) | 
| 24-Jul-2024 | tridceq 15700 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 15687 and redcwlpo 15699). Thus, this is an analytic analogue to lpowlpo 7234. (Contributed by Jim Kingdon, 24-Jul-2024.) | 
| 24-Jul-2024 | iswomni0 15695 | 
Weak omniscience stated in terms of equality with  | 
| 24-Jul-2024 | lpowlpo 7234 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7233. There is an analogue in terms of analytic omniscience principles at tridceq 15700. (Contributed by Jim Kingdon, 24-Jul-2024.) | 
| 23-Jul-2024 | nconstwlpolem 15709 | Lemma for nconstwlpo 15710. (Contributed by Jim Kingdon, 23-Jul-2024.) | 
| 23-Jul-2024 | dceqnconst 15704 | 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 15699 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 15701 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) | 
| 23-Jul-2024 | canth 5875 | 
No set  | 
| 22-Jul-2024 | nconstwlpo 15710 | 
Existence of a certain non-constant function from reals to integers
       implies  | 
| 15-Jul-2024 | fprodseq 11748 | 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 2502 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) | 
| 14-Jul-2024 | ralbid2 2501 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) | 
| 12-Jul-2024 | 2irrexpqap 15214 | 
There exist real numbers  | 
| 12-Jul-2024 | 2logb9irrap 15213 | Example for logbgcd1irrap 15206. 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 12975 | 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 12974 | 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 12973 | Lemma for ercpbl 12974. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) | 
| 12-Jul-2024 | divsfvalg 12972 | Value of the function in qusval 12966. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) | 
| 12-Jul-2024 | divsfval 12971 | Value of the function in qusval 12966. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) | 
| 11-Jul-2024 | logbgcd1irraplemexp 15204 | 
Lemma for logbgcd1irrap 15206.  Apartness of  | 
| 11-Jul-2024 | reapef 15014 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) | 
| 10-Jul-2024 | apcxp2 15175 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) | 
| 9-Jul-2024 | logbgcd1irraplemap 15205 | Lemma for logbgcd1irrap 15206. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) | 
| 9-Jul-2024 | apexp1 10810 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) | 
| 5-Jul-2024 | logrpap0 15113 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) | 
| 3-Jul-2024 | rplogbval 15181 | 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 15114 | Deduction form of logrpap0 15113. (Contributed by Jim Kingdon, 3-Jul-2024.) | 
| 3-Jul-2024 | logrpap0b 15112 | 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 15641 | 
Mapping zero and one between  | 
| 28-Jun-2024 | 012of 15640 | 
Mapping zero and one between  | 
| 27-Jun-2024 | iooreen 15679 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) | 
| 27-Jun-2024 | iooref1o 15678 | 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 15711 | Lemma for neapmkv 15712. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) | 
| 25-Jun-2024 | ismkvnn 15697 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) | 
| 25-Jun-2024 | ismkvnnlem 15696 | Lemma for ismkvnn 15697. 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 7227 | Lemma for enmkv 7228. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) | 
| 24-Jun-2024 | neapmkv 15712 | 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 15705 | 
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 15687 for more
       discussion of decidability of real number apartness.
 This is a weaker form of dceqnconst 15704 and in fact this theorem can be proved using dceqnconst 15704 as shown at dcapnconstALT 15706. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.)  | 
| 24-Jun-2024 | enmkv 7228 | 
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 15698 | Lemma for redcwlpo 15699. A biconditionalized version of trilpolemeq1 15684. (Contributed by Jim Kingdon, 21-Jun-2024.) | 
| 20-Jun-2024 | redcwlpo 15699 | 
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 15698). 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 10334 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.)  | 
| 20-Jun-2024 | iswomninn 15694 | 
Weak omniscience stated in terms of natural numbers.  Similar to
       iswomnimap 7232 but it will sometimes be more convenient to
use  | 
| 20-Jun-2024 | iswomninnlem 15693 | Lemma for iswomnimap 7232. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) | 
| 20-Jun-2024 | enwomni 7236 | 
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 7235 | Lemma for enwomni 7236. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) | 
| 19-Jun-2024 | rpabscxpbnd 15176 | 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 15158 | 
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 15141 | 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 15140 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) | 
| 12-Jun-2024 | rpcncxpcl 15138 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) | 
| 12-Jun-2024 | rpcxp0 15134 | 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 15132 | 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 15131 | 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 15130 | 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 15095 | Define the power function on complex numbers. Because df-relog 15094 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 15689 | 
Version of trirec0 15688 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 15688 | 
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 15687). (Contributed by Jim Kingdon, 10-Jun-2024.)  | 
| 9-Jun-2024 | omniwomnimkv 7233 | 
A set is omniscient if and only if it is weakly omniscient and Markov.
       The case  | 
| 9-Jun-2024 | iswomnimap 7232 | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) | 
| 9-Jun-2024 | iswomni 7231 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) | 
| 9-Jun-2024 | df-womni 7230 | 
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 13591 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) | 
| 1-Jun-2024 | ringabld 13590 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) | 
| 1-Jun-2024 | cmnmndd 13438 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) | 
| 1-Jun-2024 | ablcmnd 13422 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) | 
| 1-Jun-2024 | grpmndd 13145 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) | 
| 29-May-2024 | pw1nct 15647 | 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 15646 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) | 
| 26-May-2024 | elpwi2 4191 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) | 
| 24-May-2024 | dvmptcjx 14960 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) | 
| 23-May-2024 | cbvralfw 2719 | Rule used to change bound variables, using implicit substitution. Version of cbvralf 2721 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 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.) | 
| 22-May-2024 | efltlemlt 15010 | Lemma for eflt 15011. The converse of efltim 11863 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) | 
| 21-May-2024 | eflt 15011 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.) | 
| 19-May-2024 | apdifflemr 15691 | Lemma for apdiff 15692. (Contributed by Jim Kingdon, 19-May-2024.) | 
| 18-May-2024 | apdifflemf 15690 | 
Lemma for apdiff 15692.  Being apart from the point halfway between
 | 
| 17-May-2024 | apdiff 15692 | 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 13853 | A left module is a group. (Contributed by SN, 16-May-2024.) | 
| 16-May-2024 | crnggrpd 13566 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) | 
| 16-May-2024 | crngringd 13565 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) | 
| 16-May-2024 | ringgrpd 13561 | A ring is a group. (Contributed by SN, 16-May-2024.) | 
| 15-May-2024 | reeff1oleme 15008 | Lemma for reeff1o 15009. (Contributed by Jim Kingdon, 15-May-2024.) | 
| 14-May-2024 | df-relog 15094 | 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 6059 | Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.) | 
| 12-May-2024 | dvdstrd 11995 | The divides relation is transitive, a deduction version of dvdstr 11993. (Contributed by metakunt, 12-May-2024.) | 
| 7-May-2024 | ioocosf1o 15090 | 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 15088 | 
Cosine is between minus one and one on the open interval between zero and
      | 
| 6-May-2024 | cos11 15089 | 
Cosine is one-to-one over the closed interval from  | 
| 5-May-2024 | omiunct 12661 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 12657 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) | 
| 5-May-2024 | ctiunctal 12658 | 
Variation of ctiunct 12657 which allows  | 
| 3-May-2024 | cc4n 7338 | 
Countable choice with a simpler restriction on how every set in the
       countable collection needs to be inhabited.  That is, compared with
       cc4 7337, the hypotheses only require an A(n) for each
value of  | 
| 3-May-2024 | cc4f 7336 | 
Countable choice by showing the existence of a function  | 
| 1-May-2024 | cc4 7337 | 
Countable choice by showing the existence of a function  | 
| 29-Apr-2024 | cc3 7335 | 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 7334 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) | 
| 27-Apr-2024 | cc2lem 7333 | Lemma for cc2 7334. (Contributed by Jim Kingdon, 27-Apr-2024.) | 
| 27-Apr-2024 | cc1 7332 | 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 13988 | 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 12660 | 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 11742 | Lemma for prodmodc 11743. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) | 
| 11-Apr-2024 | prodmodclem2a 11741 | Lemma for prodmodc 11743. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) | 
| 11-Apr-2024 | prodmodclem3 11740 | Lemma for prodmodc 11743. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) | 
| 10-Apr-2024 | jcnd 653 | 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 11736 | Lemma for prodrbdc 11739. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) | 
| 24-Mar-2024 | prodfdivap 11712 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) | 
| 24-Mar-2024 | prodfrecap 11711 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) | 
| 23-Mar-2024 | prodfap0 11710 | 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 11706 | 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 11716 | 
Define the product of a series with an index set of integers  | 
| 19-Mar-2024 | cos02pilt1 15087 | 
Cosine is less than one between zero and  | 
| 19-Mar-2024 | cosq34lt1 15086 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) | 
| 14-Mar-2024 | coseq0q4123 15070 | 
Location of the zeroes of cosine in
      | 
| 14-Mar-2024 | cosq23lt0 15069 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) | 
| 9-Mar-2024 | pilem3 15019 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) | 
| 9-Mar-2024 | exmidonfin 7261 | 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 6933 and nnon 4646. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) | 
| 9-Mar-2024 | exmidonfinlem 7260 | Lemma for exmidonfin 7261. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) | 
| 8-Mar-2024 | sin0pilem2 15018 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) | 
| 8-Mar-2024 | sin0pilem1 15017 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) | 
| 7-Mar-2024 | cosz12 15016 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) | 
| 6-Mar-2024 | cos12dec 11933 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) | 
| 2-Mar-2024 | scaffvalg 13862 | 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 13689 | 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 13005 | 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 13117 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) | 
| 25-Feb-2024 | mul2lt0pn 9839 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) | 
| 25-Feb-2024 | mul2lt0np 9838 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) | 
| 25-Feb-2024 | lt0ap0 8675 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) | 
| 25-Feb-2024 | negap0d 8658 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) | 
| 24-Feb-2024 | lt0ap0d 8676 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) | 
| 20-Feb-2024 | ivthdec 14880 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) | 
| 20-Feb-2024 | ivthinclemex 14878 | Lemma for ivthinc 14879. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) | 
| 19-Feb-2024 | ivthinclemuopn 14874 | Lemma for ivthinc 14879. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) | 
| 19-Feb-2024 | dedekindicc 14869 | A Dedekind cut identifies a unique real number. Similar to df-inp 7533 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 13177 | 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 14877 | Lemma for ivthinc 14879. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 18-Feb-2024 | ivthinclemdisj 14876 | Lemma for ivthinc 14879. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 18-Feb-2024 | ivthinclemur 14875 | Lemma for ivthinc 14879. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 18-Feb-2024 | ivthinclemlr 14873 | Lemma for ivthinc 14879. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 18-Feb-2024 | ivthinclemum 14871 | Lemma for ivthinc 14879. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 18-Feb-2024 | ivthinclemlm 14870 | Lemma for ivthinc 14879. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) | 
| 17-Feb-2024 | 0subm 13116 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) | 
| 17-Feb-2024 | mndissubm 13107 | 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 13004 | 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 14867 | Lemma for dedekindicc 14869. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) | 
| 15-Feb-2024 | dedekindicclemlu 14866 | Lemma for dedekindicc 14869. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) | 
| 15-Feb-2024 | dedekindicclemlub 14865 | Lemma for dedekindicc 14869. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) | 
| 15-Feb-2024 | dedekindicclemloc 14864 | Lemma for dedekindicc 14869. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) | 
| 15-Feb-2024 | dedekindicclemub 14863 | Lemma for dedekindicc 14869. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) | 
| 15-Feb-2024 | dedekindicclemuub 14862 | Lemma for dedekindicc 14869. 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 14861 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8099 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 14860 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8099 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 1946 | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 1944 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 1945 | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 1943 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 14872 | Lemma for ivthinc 14879. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) | 
| 5-Feb-2024 | ivthinc 14879 | 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 14853 | Lemma for dedekindeu 14859. 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 14858 | Lemma for dedekindeu 14859. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) | 
| 31-Jan-2024 | dedekindeulemlu 14857 | Lemma for dedekindeu 14859. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) | 
| 31-Jan-2024 | dedekindeulemlub 14856 | Lemma for dedekindeu 14859. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) | 
| 31-Jan-2024 | dedekindeulemloc 14855 | Lemma for dedekindeu 14859. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) | 
| 31-Jan-2024 | dedekindeulemub 14854 | Lemma for dedekindeu 14859. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) | 
| 30-Jan-2024 | axsuploc 8099 | 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 8000 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) | 
| 30-Jan-2024 | iotam 5250 | 
Representation of "the unique element such that  | 
| 29-Jan-2024 | sgrpidmndm 13061 | 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 6124 | 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 4291 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 4290 with a disjoint variable condition. (Contributed by NM, 14-Apr-1995.) (Revised by GG, 26-Jan-2024.) | 
| 24-Jan-2024 | axpre-suploclemres 7968 | 
Lemma for axpre-suploc 7969.  The result.  The proof just needs to define
        | 
| 23-Jan-2024 | ax-pre-suploc 8000 | 
An inhabited, bounded-above, located set of reals has a supremum.
 
       Locatedness here means that given  Although this and ax-caucvg 7999 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7999. (Contributed by Jim Kingdon, 23-Jan-2024.)  | 
| 23-Jan-2024 | axpre-suploc 7969 | 
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 8000. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)  | 
| 22-Jan-2024 | suplocsr 7876 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) | 
| 21-Jan-2024 | bj-el2oss1o 15420 | Shorter proof of el2oss1o 6501 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) | 
| 21-Jan-2024 | ltm1sr 7844 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) | 
| 20-Jan-2024 | mndinvmod 13086 | Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.) | 
| 19-Jan-2024 | suplocsrlempr 7874 | 
Lemma for suplocsr 7876.  The set  | 
| 18-Jan-2024 | suplocsrlemb 7873 | 
Lemma for suplocsr 7876.  The set  | 
| 16-Jan-2024 | suplocsrlem 7875 | 
Lemma for suplocsr 7876.  The set  | 
| 15-Jan-2024 | eqg0el 13359 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) | 
| 14-Jan-2024 | suplocexprlemlub 7791 | Lemma for suplocexpr 7792. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) | 
| 14-Jan-2024 | suplocexprlemub 7790 | Lemma for suplocexpr 7792. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) | 
| 10-Jan-2024 | nfcsbw 3121 | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3122 with a disjoint variable condition. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | nfsbcw 3119 | Bound-variable hypothesis builder for class substitution. Version of nfsbc 3010 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 3118 | Version of nfsbcd 3009 with a disjoint variable condition. (Contributed by NM, 23-Nov-2005.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvcsbw 3088 | Version of cbvcsb 3089 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvsbcw 3017 | Version of cbvsbc 3018 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvrex2vw 2741 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2743 with a disjoint variable condition, which does not require ax-13 2169. (Contributed by FL, 2-Jul-2012.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvral2vw 2740 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2742 with a disjoint variable condition, which does not require ax-13 2169. (Contributed by NM, 10-Aug-2004.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvrexw 2724 | Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2720 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 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvralw 2723 | Rule used to change bound variables, using implicit substitution. Version of cbvral 2725 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 1521 and ax-bndl 1523 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvrexfw 2720 | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2722 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 1521 and ax-bndl 1523 in the proof. (Contributed by FL, 27-Apr-2008.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | nfralw 2534 | 
Bound-variable hypothesis builder for restricted quantification.  See
       nfralya 2537 for a version with  | 
| 10-Jan-2024 | nfraldw 2529 | 
Not-free for restricted universal quantification where  | 
| 10-Jan-2024 | nfabdw 2358 | Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2359 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by GG, 10-Jan-2024.) | 
| 10-Jan-2024 | cbvex2vw 1948 | 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 1947 | 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 1764 | Rule used to change bound variables, using implicit substitution. Version of cbv2 1763 with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) (Revised by GG, 10-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlemloc 7788 | Lemma for suplocexpr 7792. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlemdisj 7787 | Lemma for suplocexpr 7792. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlemru 7786 | Lemma for suplocexpr 7792. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlemrl 7784 | Lemma for suplocexpr 7792. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlem2b 7781 | Lemma for suplocexpr 7792. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 9-Jan-2024 | suplocexprlemell 7780 | Lemma for suplocexpr 7792. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) | 
| 7-Jan-2024 | suplocexpr 7792 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) | 
| 7-Jan-2024 | suplocexprlemex 7789 | Lemma for suplocexpr 7792. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) | 
| 7-Jan-2024 | suplocexprlemmu 7785 | Lemma for suplocexpr 7792. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) | 
| 7-Jan-2024 | suplocexprlemml 7783 | Lemma for suplocexpr 7792. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) | 
| 7-Jan-2024 | suplocexprlemss 7782 | 
Lemma for suplocexpr 7792.  | 
| 5-Jan-2024 | dedekindicclemicc 14868 | 
Lemma for dedekindicc 14869.  Same as dedekindicc 14869, except that we
         merely show  | 
| 5-Jan-2024 | dedekindeu 14859 | A Dedekind cut identifies a unique real number. Similar to df-inp 7533 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.) | 
| 31-Dec-2023 | dvmptsubcn 14959 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) | 
| 31-Dec-2023 | dvmptnegcn 14958 | 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 14957 | 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 13439 | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6117. (Contributed by AV, 31-Dec-2023.) | 
| 31-Dec-2023 | brm 4083 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) | 
| 30-Dec-2023 | dvmptccn 14951 | 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 14950 | 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 10975 | 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 13072 | The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 13071). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) | 
| 28-Dec-2023 | mulgnn0gsum 13258 | 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 13257 | Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.) | 
| 26-Dec-2023 | gsumfzreidx 13467 | 
Re-index a finite group sum using a bijection.  Corresponds to the first
       equation in [Lang] p. 5 with  | 
| 26-Dec-2023 | gsumsplit1r 13041 | 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 13025 | 
If there is a left and right identity element for any binary operation
       (group operation)  | 
| 26-Dec-2023 | lidrideqd 13024 | 
If there is a left and right identity element for any binary operation
       (group operation)  | 
| 25-Dec-2023 | ctfoex 7184 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) | 
| 23-Dec-2023 | enct 12650 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) | 
| 23-Dec-2023 | enctlem 12649 | Lemma for enct 12650. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) | 
| 23-Dec-2023 | omct 7183 | 
 | 
| 21-Dec-2023 | dvcoapbr 14943 | 
The chain rule for derivatives at a point.  The
          | 
| 19-Dec-2023 | apsscn 8674 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) | 
| 19-Dec-2023 | aprcl 8673 | Reverse closure for apartness. (Contributed by Jim Kingdon, 19-Dec-2023.) | 
| 18-Dec-2023 | limccoap 14914 | 
Composition of two limits.  This theorem is only usable in the case
       where  | 
| 16-Dec-2023 | cnreim 11143 | Complex apartness in terms of real and imaginary parts. See also apreim 8630 which is similar but with different notation. (Contributed by Jim Kingdon, 16-Dec-2023.) | 
| 14-Dec-2023 | cnopnap 14847 | The complex numbers apart from a given complex number form an open set. (Contributed by Jim Kingdon, 14-Dec-2023.) | 
| 14-Dec-2023 | cnovex 14432 | 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 14782 | The real numbers apart from a given real number form an open set. (Contributed by Jim Kingdon, 13-Dec-2023.) | 
| 12-Dec-2023 | cnopncntop 14780 | 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 14778 | 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 15396 | Clavius law for stable formulas. See pm2.18dc 856. (Contributed by BJ, 4-Dec-2023.) | 
| 4-Dec-2023 | bj-nnclavius 15383 | Clavius law with doubly negated consequent. (Contributed by BJ, 4-Dec-2023.) | 
| 2-Dec-2023 | dvmulxx 14940 | The product rule for derivatives at a point. For the (more general) relation version, see dvmulxxbr 14938. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 2-Dec-2023.) | 
| 1-Dec-2023 | dvmulxxbr 14938 | The product rule for derivatives at a point. For the (simpler but more limited) function version, see dvmulxx 14940. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 1-Dec-2023.) | 
| 29-Nov-2023 | subctctexmid 15645 | 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 7221 | 
The predicate of being Markov stated in terms of double negation and
       comparison with  | 
| 28-Nov-2023 | ccfunen 7331 | Existence of a choice function for a countably infinite set. (Contributed by Jim Kingdon, 28-Nov-2023.) | 
| 28-Nov-2023 | exmid1stab 4241 | 
If every proposition is stable, excluded middle follows.  We are
       thinking of  | 
| 27-Nov-2023 | df-cc 7330 | The expression CCHOICE will be used as a readable shorthand for any form of countable choice, analogous to df-ac 7273 for full choice. (Contributed by Jim Kingdon, 27-Nov-2023.) | 
| 26-Nov-2023 | offeq 6149 | 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 14939 | The sum rule for derivatives at a point. For the (more general) relation version, see dvaddxxbr 14937. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Jim Kingdon, 25-Nov-2023.) | 
| 25-Nov-2023 | dvaddxxbr 14937 | 
The sum rule for derivatives at a point.  That is, if the derivative
         of  | 
| 25-Nov-2023 | dcnn 849 | Decidability of the negation of a proposition is equivalent to decidability of its double negation. See also dcn 843. The relation between dcn 843 and dcnn 849 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 849 means that a proposition is testable if and only if its negation is testable, and dcn 843 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 15407 | 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 15403 | If a formula is not refutable, then it is decidable if and only if it is provable. See also comment of bj-nnbist 15390. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-dcstab 15402 | A decidable formula is stable. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | 
| 24-Nov-2023 | bj-fadc 15400 | A refutable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-trdc 15398 | A provable formula is decidable. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-stal 15395 | The universal quantification of a stable formula is stable. See bj-stim 15392 for implication, stabnot 834 for negation, and bj-stan 15393 for conjunction. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-stand 15394 | The conjunction of two stable formulas is stable. Deduction form of bj-stan 15393. Its proof is shorter (when counting all steps, including syntactic steps), so one could prove it first and then bj-stan 15393 from it, the usual way. (Contributed by BJ, 24-Nov-2023.) (Proof modification is discouraged.) | 
| 24-Nov-2023 | bj-stan 15393 | The conjunction of two stable formulas is stable. See bj-stim 15392 for implication, stabnot 834 for negation, and bj-stal 15395 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-stim 15392 | A conjunction with a stable consequent is stable. See stabnot 834 for negation , bj-stan 15393 for conjunction , and bj-stal 15395 for universal quantification. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-nnbist 15390 | 
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 15387 | A refutable formula is stable. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-trst 15385 | A provable formula is stable. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-nnan 15382 | The double negation of a conjunction implies the conjunction of the double negations. (Contributed by BJ, 24-Nov-2023.) | 
| 24-Nov-2023 | bj-nnim 15381 | 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 15379 | 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 1663 | 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 6145 | 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 7276 | The axiom of choice implies excluded middle. See acexmid 5921 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 7275 | Lemma for exmidac 7276. The result, with a few hypotheses to break out commonly used expressions. (Contributed by Jim Kingdon, 21-Nov-2023.) | 
| 21-Nov-2023 | exmid1dc 4233 | 
A convenience theorem for proving that something implies EXMID.
       Think of this as an alternative to using a proposition, as in proofs
       like undifexmid 4226 or ordtriexmid 4557.  In this context  | 
| 20-Nov-2023 | acfun 7274 | 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 13808 | The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.) | 
| 18-Nov-2023 | condc 854 | 
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 848 | 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 843. (Contributed by BJ, 18-Nov-2023.) | 
| 17-Nov-2023 | cnplimclemr 14905 | Lemma for cnplimccntop 14906. The reverse direction. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) | 
| 17-Nov-2023 | cnplimclemle 14904 | Lemma for cnplimccntop 14906. Satisfying the epsilon condition for continuity. (Contributed by Mario Carneiro and Jim Kingdon, 17-Nov-2023.) | 
| 14-Nov-2023 | limccnp2cntop 14913 | 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 11388 | The maximum of two positive real numbers is a positive real number. (Contributed by Jim Kingdon, 10-Nov-2023.) | 
| 9-Nov-2023 | limccnp2lem 14912 | Lemma for limccnp2cntop 14913. 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 14896 | 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 14899 | 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 12659 | 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 12657 | 
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 12659, 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 12612) and using the first number to map to an
element
        (Contributed by Jim Kingdon, 31-Oct-2023.)  | 
| 30-Oct-2023 | ctssdccl 7177 | 
A mapping from a decidable subset of the natural numbers onto a
       countable set.  This is similar to one direction of ctssdc 7179 but
       expressed in terms of classes rather than  | 
| 28-Oct-2023 | ctiunctlemfo 12656 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | ctiunctlemf 12655 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | ctiunctlemudc 12654 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | ctiunctlemuom 12653 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | ctiunctlemu2nd 12652 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | ctiunctlemu1st 12651 | Lemma for ctiunct 12657. (Contributed by Jim Kingdon, 28-Oct-2023.) | 
| 28-Oct-2023 | pm2.521gdc 869 | 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 846 | 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 655 | Weakening of conax1 654. General instance of pm2.51 656 and of pm2.52 657. (Contributed by BJ, 28-Oct-2023.) | 
| 28-Oct-2023 | conax1 654 | Contrapositive of ax-1 6. (Contributed by BJ, 28-Oct-2023.) | 
| 25-Oct-2023 | divcnap 14801 | 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 7899 | 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 6229 | Domain of closure of an operation. (Contributed by Jim Kingdon, 23-Oct-2023.) | 
| 22-Oct-2023 | addcncntoplem 14797 | Lemma for addcncntop 14798, subcncntop 14799, and mulcncntop 14800. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Jim Kingdon, 22-Oct-2023.) | 
| 22-Oct-2023 | txmetcnp 14754 | 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 14744 | 
The maximum metric (Chebyshev distance) on the product of two sets,
         expressed in terms of balls centered on a point  | 
| 15-Oct-2023 | xmettxlem 14745 | Lemma for xmettx 14746. (Contributed by Jim Kingdon, 15-Oct-2023.) | 
| 11-Oct-2023 | xmettx 14746 | 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 14743 | The maximum metric (Chebyshev distance) on the product of two sets. (Contributed by Jim Kingdon, 11-Oct-2023.) | 
| 7-Oct-2023 | df-iress 12686 | 
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 12983 | Biconditional version of fnpr2o 12982. (Contributed by Jim Kingdon, 27-Sep-2023.) | 
| 25-Sep-2023 | xpsval 12995 | 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 12985 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) | 
| 25-Sep-2023 | fvpr0o 12984 | The value of a function with a domain of (at most) two elements. (Contributed by Jim Kingdon, 25-Sep-2023.) | 
| 25-Sep-2023 | fnpr2o 12982 | 
Function with a domain of  | 
| 25-Sep-2023 | df-xps 12947 | Define a binary product on structures. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revised by Jim Kingdon, 25-Sep-2023.) | 
| 12-Sep-2023 | pwntru 4232 | A slight strengthening of pwtrufal 15642. (Contributed by Mario Carneiro and Jim Kingdon, 12-Sep-2023.) | 
| 11-Sep-2023 | pwtrufal 15642 | 
A subset of the singleton  | 
| 9-Sep-2023 | mathbox 15378 | 
(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 7110 | 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 15644 | 
An exercise related to  | 
| 3-Sep-2023 | pwle2 15643 | 
An exercise related to  | 
| 30-Aug-2023 | isomninn 15675 | 
Omniscience stated in terms of natural numbers.  Similar to isomnimap 7203
       but it will sometimes be more convenient to use  | 
| 30-Aug-2023 | isomninnlem 15674 | Lemma for isomninn 15675. The result, with a hypothesis to provide a convenient notation. (Contributed by Jim Kingdon, 30-Aug-2023.) | 
| 28-Aug-2023 | trilpolemisumle 15682 | Lemma for trilpo 15687. An upper bound for the sum of the digits beyond a certain point. (Contributed by Jim Kingdon, 28-Aug-2023.) | 
| 25-Aug-2023 | cvgcmp2n 15677 | A comparison test for convergence of a real infinite series. (Contributed by Jim Kingdon, 25-Aug-2023.) | 
| 25-Aug-2023 | cvgcmp2nlemabs 15676 | 
Lemma for cvgcmp2n 15677.  The partial sums get closer to each other
as
         we go further out.  The proof proceeds by rewriting
          | 
| 24-Aug-2023 | trilpolemclim 15680 | Lemma for trilpo 15687. Convergence of the series. (Contributed by Jim Kingdon, 24-Aug-2023.) | 
| 23-Aug-2023 | trilpo 15687 | 
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 15685 (which means the sequence contains a zero), trilpolemeq1 15684 (which means the sequence is all ones), and trilpolemgt1 15683 (which is not possible). Equivalent ways to state real number trichotomy (sometimes called "analytic LPO") include decidability of real number apartness (see triap 15673) or that the real numbers are a discrete field (see trirec0 15688). 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 10330 for real numbers. (Contributed by Jim Kingdon, 23-Aug-2023.)  | 
| 23-Aug-2023 | trilpolemres 15686 | Lemma for trilpo 15687. The result. (Contributed by Jim Kingdon, 23-Aug-2023.) | 
| 23-Aug-2023 | trilpolemlt1 15685 | 
Lemma for trilpo 15687.  The  | 
| 23-Aug-2023 | trilpolemeq1 15684 | 
Lemma for trilpo 15687.  The  | 
| 23-Aug-2023 | trilpolemgt1 15683 | 
Lemma for trilpo 15687.  The  | 
| 23-Aug-2023 | trilpolemcl 15681 | Lemma for trilpo 15687. The sum exists. (Contributed by Jim Kingdon, 23-Aug-2023.) | 
| 23-Aug-2023 | triap 15673 | Two ways of stating real number trichotomy. (Contributed by Jim Kingdon, 23-Aug-2023.) | 
| 19-Aug-2023 | djuenun 7279 | 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 7178 | Lemma for ctssdc 7179. Showing that our usual definition of countable implies the alternate one. (Contributed by Jim Kingdon, 16-Aug-2023.) | 
| 16-Aug-2023 | ctssdclemn0 7176 | 
Lemma for ctssdc 7179.  The  | 
| 15-Aug-2023 | ctssexmid 7216 | The decidability condition in ctssdc 7179 is needed. More specifically, ctssdc 7179 minus that condition, plus the Limited Principle of Omniscience (LPO), implies excluded middle. (Contributed by Jim Kingdon, 15-Aug-2023.) | 
| 15-Aug-2023 | ctssdc 7179 | 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 7216. (Contributed by Jim Kingdon, 15-Aug-2023.) | 
| 14-Aug-2023 | mpoexw 6271 | Weak version of mpoex 6272 that holds without ax-coll 4148. 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 13174 | 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 8154 | 
Negative trichotomy property for real numbers.  It is well known that we
     cannot prove real number trichotomy,  | 
| 13-Aug-2023 | mptexw 6170 | Weak version of mptex 5788 that holds without ax-coll 4148. 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 6169 | Weak version of funex 5785 that holds without ax-coll 4148. If the domain and codomain of a function exist, so does the function. (Contributed by Rohan Ridenour, 13-Aug-2023.) | 
| 11-Aug-2023 | qnnen 12648 | 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 12644 | 
Lemma for ctinfom 12645.  Converting between  | 
| 9-Aug-2023 | difinfsnlem 7165 | 
Lemma for difinfsn 7166.  The case where we need to swap  | 
| 8-Aug-2023 | difinfinf 7167 | 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 7166 | 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 12647 | 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 12646 | An infinite set contains an element not contained in a given finite subset. (Contributed by Jim Kingdon, 7-Aug-2023.) | 
| 7-Aug-2023 | ctinfom 12645 | 
A condition for a set being countably infinite.  Restates ennnfone 12642 in
       terms of  | 
| 6-Aug-2023 | rerestcntop 14794 | 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 14793 | 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 15664 | 
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 14490 | 
Existence of the binary topological product.  If  | 
| 3-Aug-2023 | ablgrpd 13420 | An Abelian group is a group, deduction form of ablgrp 13419. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | 1nsgtrivd 13349 | A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | triv1nsgd 13348 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | trivnsgd 13347 | The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | 0idnsgd 13346 | The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | trivsubgsnd 13331 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | trivsubgd 13330 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | mulgcld 13274 | Deduction associated with mulgcl 13269. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | hashfingrpnn 13168 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | hashfinmndnn 13073 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | dvdsgcdidd 12161 | 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 12160 | 
The greatest common divisor of a nonnegative integer  | 
| 3-Aug-2023 | fihashelne0d 10889 | A finite set with an element has nonzero size. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | phpeqd 6996 | Corollary of the Pigeonhole Principle using equality. Strengthening of phpm 6926 expressed without negation. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | enpr2d 6876 | A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | elrnmpt2d 4921 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | elrnmptdv 4920 | Elementhood in the range of a function in maps-to notation, deduction form. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | rspcime 2875 | Prove a restricted existential. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 3-Aug-2023 | neqcomd 2201 | Commute an inequality. (Contributed by Rohan Ridenour, 3-Aug-2023.) | 
| 2-Aug-2023 | dvid 14931 | Derivative of the identity function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) | 
| 2-Aug-2023 | dvconst 14930 | Derivative of a constant function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) | 
| 2-Aug-2023 | dvidlemap 14927 | Lemma for dvid 14931 and dvconst 14930. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 2-Aug-2023.) | 
| 2-Aug-2023 | diveqap1bd 8863 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveqap1 8732. Converse of diveqap1d 8825. (Contributed by David Moews, 28-Feb-2017.) (Revised by Jim Kingdon, 2-Aug-2023.) | 
| 31-Jul-2023 | mul0inf 11406 | Equality of a product with zero. A bit of a curiosity, in the sense that theorems like abs00ap 11227 and mulap0bd 8684 may better express the ideas behind it. (Contributed by Jim Kingdon, 31-Jul-2023.) | 
| 31-Jul-2023 | mul0eqap 8697 | 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 8651 | Contrapositive law deduction for apartness. (Contributed by Jim Kingdon, 31-Jul-2023.) | 
| 30-Jul-2023 | uzennn 10528 | An upper integer set is equinumerous to the set of natural numbers. (Contributed by Jim Kingdon, 30-Jul-2023.) | 
| 30-Jul-2023 | djuen 7278 | Disjoint unions of equinumerous sets are equinumerous. (Contributed by Jim Kingdon, 30-Jul-2023.) | 
| 30-Jul-2023 | endjudisj 7277 | Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by Jim Kingdon, 30-Jul-2023.) | 
| 30-Jul-2023 | eninr 7164 | Equinumerosity of a set and its image under right injection. (Contributed by Jim Kingdon, 30-Jul-2023.) | 
| 30-Jul-2023 | eninl 7163 | Equinumerosity of a set and its image under left injection. (Contributed by Jim Kingdon, 30-Jul-2023.) | 
| 29-Jul-2023 | exmidunben 12643 | 
If any unbounded set of positive integers is equinumerous to  | 
| 29-Jul-2023 | exmidsssnc 4236 | 
Excluded middle in terms of subsets of a singleton.  This is similar to
       exmid01 4231 but lets you choose any set as the element of
the singleton
       rather than just  | 
| 28-Jul-2023 | dvfcnpm 14926 | The derivative is a function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Jim Kingdon, 28-Jul-2023.) | 
| 28-Jul-2023 | dvfpm 14925 | The derivative is a function. (Contributed by Mario Carneiro, 8-Aug-2014.) (Revised by Jim Kingdon, 28-Jul-2023.) | 
| 24-Jul-2023 | sraring 14005 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) | 
| 23-Jul-2023 | ennnfonelemhdmp1 12626 | Lemma for ennnfone 12642. 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 12623 | 
Lemma for ennnfone 12642.  Value of  | 
| 22-Jul-2023 | nntr2 6561 | Transitive law for natural numbers. (Contributed by Jim Kingdon, 22-Jul-2023.) | 
| 22-Jul-2023 | nnsssuc 6560 | 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 4789 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopabi 4791. (Contributed by BJ, 22-Jul-2023.) | 
| 21-Jul-2023 | ennnfoneleminc 12628 | 
Lemma for ennnfone 12642.  We only add elements to  | 
| 20-Jul-2023 | ennnfonelemg 12620 | 
Lemma for ennnfone 12642.  Closure for  | 
| 20-Jul-2023 | ennnfonelemjn 12619 | 
Lemma for ennnfone 12642.  Non-initial state for  | 
| 20-Jul-2023 | ennnfonelemj0 12618 | 
Lemma for ennnfone 12642.  Initial state for  | 
| 20-Jul-2023 | seqp1cd 10562 | 
Value of the sequence builder function at a successor.  A version of
       seq3p1 10557 which provides two classes  | 
| 20-Jul-2023 | seqovcd 10559 | A closure law for the recursive sequence builder. This is a lemma for theorems such as seqf2 10560 and seq1cd 10561 and is unlikely to be needed once such theorems are proved. (Contributed by Jim Kingdon, 20-Jul-2023.) | 
| 19-Jul-2023 | ennnfonelemhom 12632 | 
Lemma for ennnfone 12642.  The sequences in  | 
| 19-Jul-2023 | ennnfonelemex 12631 | 
Lemma for ennnfone 12642.  Extending the sequence  | 
| 19-Jul-2023 | ennnfonelemkh 12629 | Lemma for ennnfone 12642. 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 12625 | 
Lemma for ennnfone 12642.  | 
| 19-Jul-2023 | ennnfonelem1 12624 | Lemma for ennnfone 12642. Second value. (Contributed by Jim Kingdon, 19-Jul-2023.) | 
| 19-Jul-2023 | seq1cd 10561 | 
Initial value of the recursive sequence builder.  A version of seq3-1 10554
       which provides two classes  | 
| 17-Jul-2023 | ennnfonelemhf1o 12630 | 
Lemma for ennnfone 12642.  Each of the functions in  | 
| 16-Jul-2023 | ennnfonelemen 12638 | Lemma for ennnfone 12642. The result. (Contributed by Jim Kingdon, 16-Jul-2023.) | 
| 16-Jul-2023 | ennnfonelemdm 12637 | 
Lemma for ennnfone 12642.  The function  | 
| 16-Jul-2023 | ennnfonelemrn 12636 | 
Lemma for ennnfone 12642.  | 
| 16-Jul-2023 | ennnfonelemf1 12635 | 
Lemma for ennnfone 12642.  | 
| 16-Jul-2023 | ennnfonelemfun 12634 | 
Lemma for ennnfone 12642.  | 
| 16-Jul-2023 | ennnfonelemrnh 12633 | Lemma for ennnfone 12642. A consequence of ennnfonelemss 12627. (Contributed by Jim Kingdon, 16-Jul-2023.) | 
| 15-Jul-2023 | ennnfonelemss 12627 | 
Lemma for ennnfone 12642.  We only add elements to  | 
| 15-Jul-2023 | ennnfonelem0 12622 | Lemma for ennnfone 12642. Initial value. (Contributed by Jim Kingdon, 15-Jul-2023.) | 
| 15-Jul-2023 | ennnfonelemk 12617 | Lemma for ennnfone 12642. (Contributed by Jim Kingdon, 15-Jul-2023.) | 
| 15-Jul-2023 | ennnfonelemdc 12616 | Lemma for ennnfone 12642. A direct consequence of fidcenumlemrk 7020. (Contributed by Jim Kingdon, 15-Jul-2023.) | 
| 14-Jul-2023 | djur 7135 | A member of a disjoint union can be mapped from one of the classes which produced it. (Contributed by Jim Kingdon, 23-Jun-2022.) Upgrade implication to biconditional and shorten proof. (Revised by BJ, 14-Jul-2023.) | 
| 13-Jul-2023 | sbthomlem 15669 | Lemma for sbthom 15670. (Contributed by Mario Carneiro and Jim Kingdon, 13-Jul-2023.) | 
| 12-Jul-2023 | caseinr 7158 | Applying the "case" construction to a right injection. (Contributed by Jim Kingdon, 12-Jul-2023.) | 
| 12-Jul-2023 | inl11 7131 | Left injection is one-to-one. (Contributed by Jim Kingdon, 12-Jul-2023.) | 
| 11-Jul-2023 | djudomr 7287 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) | 
| 11-Jul-2023 | djudoml 7286 | A set is dominated by its disjoint union with another. (Contributed by Jim Kingdon, 11-Jul-2023.) | 
| 11-Jul-2023 | omp1eomlem 7160 | Lemma for omp1eom 7161. (Contributed by Jim Kingdon, 11-Jul-2023.) | 
| 11-Jul-2023 | xp01disjl 6492 | Cartesian products with the singletons of ordinals 0 and 1 are disjoint. (Contributed by Jim Kingdon, 11-Jul-2023.) | 
| 10-Jul-2023 | sbthom 15670 | 
Schroeder-Bernstein is not possible even for  | 
| 10-Jul-2023 | endjusym 7162 | Reversing right and left operands of a disjoint union produces an equinumerous result. (Contributed by Jim Kingdon, 10-Jul-2023.) | 
| 10-Jul-2023 | omp1eom 7161 | 
Adding one to  | 
| 9-Jul-2023 | refeq 15672 | Equality of two real functions which agree at negative numbers, positive numbers, and zero. This holds even without real trichotomy. From an online post by Martin Escardo. (Contributed by Jim Kingdon, 9-Jul-2023.) | 
| 9-Jul-2023 | seqvalcd 10553 | 
Value of the sequence builder function.  Similar to seq3val 10552 but the
       classes  | 
| 9-Jul-2023 | djuun 7133 | The disjoint union of two classes is the union of the images of those two classes under right and left injection. (Contributed by Jim Kingdon, 22-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) | 
| 9-Jul-2023 | djuin 7130 | The images of any classes under right and left injection produce disjoint sets. (Contributed by Jim Kingdon, 21-Jun-2022.) (Proof shortened by BJ, 9-Jul-2023.) | 
| 8-Jul-2023 | limcimo 14901 | 
Conditions which ensure there is at most one limit value of  | 
| 8-Jul-2023 | ennnfonelemh 12621 | Lemma for ennnfone 12642. (Contributed by Jim Kingdon, 8-Jul-2023.) | 
| 7-Jul-2023 | seqf2 10560 | Range of the recursive sequence builder. (Contributed by Mario Carneiro, 24-Jun-2013.) (Revised by Jim Kingdon, 7-Jul-2023.) | 
| 6-Jul-2023 | sbbidv 1899 | 
Deduction substituting both sides of a biconditional, with  | 
| 3-Jul-2023 | limcimolemlt 14900 | Lemma for limcimo 14901. (Contributed by Jim Kingdon, 3-Jul-2023.) | 
| 28-Jun-2023 | dvfgg 14924 | 
Explicitly write out the functionality condition on derivative for
        | 
| 28-Jun-2023 | dvbsssg 14922 | The set of differentiable points is a subset of the ambient topology. (Contributed by Mario Carneiro, 18-Mar-2015.) (Revised by Jim Kingdon, 28-Jun-2023.) | 
| 27-Jun-2023 | dvbssntrcntop 14920 | The set of differentiable points is a subset of the interior of the domain of the function. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) | 
| 27-Jun-2023 | eldvap 14918 | 
The differentiable predicate.  A function  | 
| 27-Jun-2023 | dvfvalap 14917 | Value and set bounds on the derivative operator. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) | 
| 27-Jun-2023 | dvlemap 14916 | Closure for a difference quotient. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 27-Jun-2023.) | 
| 25-Jun-2023 | reldvg 14915 | The derivative function is a relation. (Contributed by Mario Carneiro, 7-Aug-2014.) (Revised by Jim Kingdon, 25-Jun-2023.) | 
| 25-Jun-2023 | df-dvap 14893 | 
Define the derivative operator.  This acts on functions to produce a
       function that is defined where the original function is differentiable,
       with value the derivative of the function at these points.  The set
        | 
| 18-Jun-2023 | limccnpcntop 14911 | 
If the limit of  | 
| 18-Jun-2023 | r19.30dc 2644 | Restricted quantifier version of 19.30dc 1641. (Contributed by Scott Fenton, 25-Feb-2011.) (Proof shortened by Wolf Lammen, 18-Jun-2023.) | 
| 17-Jun-2023 | r19.28v 2625 | 
Restricted quantifier version of one direction of 19.28 1577.  (The other
       direction holds when  | 
| 17-Jun-2023 | r19.27v 2624 | 
Restricted quantitifer version of one direction of 19.27 1575.  (The other
       direction holds when  | 
| 16-Jun-2023 | cnlimcim 14907 | 
If  | 
| 16-Jun-2023 | cncfcn1cntop 14830 | Relate complex function continuity to topological continuity. (Contributed by Paul Chapman, 28-Nov-2007.) (Revised by Mario Carneiro, 7-Sep-2015.) (Revised by Jim Kingdon, 16-Jun-2023.) | 
| 14-Jun-2023 | cnplimcim 14903 | 
If a function is continuous at  | 
| 14-Jun-2023 | metcnpd 14756 | 
Two ways to say a mapping from metric  | 
| 6-Jun-2023 | cntoptop 14769 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) | 
| 6-Jun-2023 | cntoptopon 14768 | The topology of the complex numbers is a topology. (Contributed by Jim Kingdon, 6-Jun-2023.) | 
| 3-Jun-2023 | limcdifap 14898 | 
It suffices to consider functions which are not defined at  | 
| 3-Jun-2023 | ellimc3ap 14897 | Write the epsilon-delta definition of a limit. (Contributed by Mario Carneiro, 28-Dec-2016.) Use apartness. (Revised by Jim Kingdon, 3-Jun-2023.) | 
| 3-Jun-2023 | df-limced 14892 | Define the set of limits of a complex function at a point. Under normal circumstances, this will be a singleton or empty, depending on whether the limit exists. (Contributed by Mario Carneiro, 24-Dec-2016.) (Revised by Jim Kingdon, 3-Jun-2023.) | 
| 30-May-2023 | modprm1div 12416 | A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.) | 
| 30-May-2023 | modm1div 11965 | An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.) | 
| 30-May-2023 | eluz4nn 9642 | An integer greater than or equal to 4 is a positive integer. (Contributed by AV, 30-May-2023.) | 
| 30-May-2023 | eluz4eluz2 9641 | An integer greater than or equal to 4 is an integer greater than or equal to 2. (Contributed by AV, 30-May-2023.) | 
| 29-May-2023 | mulcncflem 14843 | Lemma for mulcncf 14844. (Contributed by Jim Kingdon, 29-May-2023.) | 
| 26-May-2023 | cdivcncfap 14840 | Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016.) (Revised by Jim Kingdon, 26-May-2023.) | 
| 26-May-2023 | reccn2ap 11478 | 
The reciprocal function is continuous.  The class  | 
| 23-May-2023 | iooretopg 14764 | Open intervals are open sets of the standard topology on the reals . (Contributed by FL, 18-Jun-2007.) (Revised by Jim Kingdon, 23-May-2023.) | 
| 23-May-2023 | minclpr 11402 | 
The minimum of two real numbers is one of those numbers if and only if
     dichotomy ( | 
| 22-May-2023 | qtopbasss 14757 | The set of open intervals with endpoints in a subset forms a basis for a topology. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Jim Kingdon, 22-May-2023.) | 
| 22-May-2023 | iooinsup 11442 | Intersection of two open intervals of extended reals. (Contributed by NM, 7-Feb-2007.) (Revised by Jim Kingdon, 22-May-2023.) | 
| 21-May-2023 | df-sumdc 11519 | 
Define the sum of a series with an index set of integers  | 
| 19-May-2023 | bdmopn 14740 | 
The standard bounded metric corresponding to  | 
| 19-May-2023 | bdbl 14739 | 
The standard bounded metric corresponding to  | 
| 19-May-2023 | bdmet 14738 | The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015.) (Revised by Jim Kingdon, 19-May-2023.) | 
| 19-May-2023 | xrminltinf 11437 | Two ways of saying an extended real is greater than the minimum of two others. (Contributed by Jim Kingdon, 19-May-2023.) | 
| 19-May-2023 | clel5 2901 | 
Alternate definition of class membership: a class  | 
| 18-May-2023 | xrminrecl 11438 | The minimum of two real numbers is the same when taken as extended reals or as reals. (Contributed by Jim Kingdon, 18-May-2023.) | 
| 18-May-2023 | ralnex2 2636 | Relationship between two restricted universal and existential quantifiers. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 18-May-2023.) | 
| 17-May-2023 | bdtrilem 11404 | Lemma for bdtri 11405. (Contributed by Steven Nguyen and Jim Kingdon, 17-May-2023.) | 
| 15-May-2023 | xrbdtri 11441 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) | 
| 15-May-2023 | bdtri 11405 | Triangle inequality for bounded values. (Contributed by Jim Kingdon, 15-May-2023.) | 
| 15-May-2023 | minabs 11401 | The minimum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 15-May-2023.) | 
| 13-May-2023 | kerf1ghm 13404 | 
A group homomorphism  | 
| 13-May-2023 | f1ghm0to0 13402 | 
If a group homomorphism  | 
| 11-May-2023 | xrmaxadd 11426 | Distributing addition over maximum. (Contributed by Jim Kingdon, 11-May-2023.) | 
| 11-May-2023 | xrmaxaddlem 11425 | 
Lemma for xrmaxadd 11426.  The case where  | 
| 10-May-2023 | xrminadd 11440 | Distributing addition over minimum. (Contributed by Jim Kingdon, 10-May-2023.) | 
| Copyright terms: Public domain | W3C HTML validation [external] |