|
|
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 | ||
| 14-Aug-2026 | reaplog 15972 | Apartness and the real natural logarithm. (Contributed by Jim Kingdon, 14-Aug-2026.) |
| 13-Aug-2026 | efap1p 15882 | If the exponential of a number is apart from one plus that number, the number is apart from zero. To some extent can be thought of as the converse of efgt1p 12465. (Contributed by Jim Kingdon, 13-Aug-2026.) |
| 6-Aug-2026 | relndmfv 5728 | The value of a relation outside its domain is the empty set. (Contributed by Jim Kingdon, 6-Aug-2026.) |
| 1-Aug-2026 | wexmiddifxy 17058 | Being able to subtract an arbitrary finite set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 1-Aug-2026.) |
| 1-Aug-2026 | wexmiddifxylem 17057 | Lemma for wexmiddifxylem 17057. Showing weak excluded middle given a suitable finite set. (Contributed by Jim Kingdon, 1-Aug-2026.) |
| 31-Jul-2026 | rabid1o 17046 | Converting between propositions and corresponding subsets of a singleton. (Contributed by Jim Kingdon, 31-Jul-2026.) |
| 30-Jul-2026 | wexmiddc 17054 | Weak excluded middle expressed using WEXMID implies decidability of a negated proposition. (Contributed by Jim Kingdon, 30-Jul-2026.) |
| 30-Jul-2026 | df-wexmid 17053 | Weak excluded middle is the principle that any negated proposition is decidable. (Contributed by Jim Kingdon, 30-Jul-2026.) |
| 29-Jul-2026 | wexmiddiffi 17056 | Being able to subtract an arbitrary set from a finite set and get a finite set is equivalent to weak excluded middle. By adding additional conditions we can get a theorem which does not need weak excluded middle, at diffifi 7198. (Contributed by Jim Kingdon, 29-Jul-2026.) |
| 29-Jul-2026 | wexmiddiffilem 17055 | Lemma for wexmiddiffi 17056. The reverse direction, using different notation. (Contributed by Jim Kingdon, 29-Jul-2026.) |
| 24-Jul-2026 | stnot 17051 | A proposition is double negation stable if and only if it is equivalent to a negated proposition. Here by "proposition" we mean a subset of a singleton (which is a choice which allows us to quantify over them). Posed as an exercise online by Yannick Forster. (Contributed by Jim Kingdon, 24-Jul-2026.) |
| 24-Jul-2026 | slotm 13417 | A structure with an inhabited slot is inhabited. (Contributed by Jim Kingdon, 24-Jul-2026.) |
| 22-Jul-2026 | alseu-no-surprise 17191 | Demonstrate that there is never a "surprise" when using the "all some one" quantifier, that is, it is never possible for the consequent to be both always true and always false. This follows from als-no-surprise 17159 by alseuals 17177. See als-no-surprise 17159 for why ordinary "for all" with implication has no such property. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseueu 17190 |
"The |
| 22-Jul-2026 | dfalseu2 17189 |
An "all some one" statement is equivalent to its universal part
conjoined
with the claim that exactly one
The universal conjunct is what makes that work, and it cannot be dropped.
|
| 22-Jul-2026 | nfralseu 17188 | Bound-variable hypothesis builder for "all some one" restricted to a class. This is the "all some one" counterpart of nfrals 17157. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | nfalseu 17187 | Bound-variable hypothesis builder for "all some one". This is the "all some one" counterpart of nfals 17156. Unlike the set.mm version of this theorem, no disjoint variable condition is needed, because nfeu 2105 here does not require one. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | ralseubii 17186 | Congruence for "all some one" restricted to a class. This is the "all some one" counterpart of ralsbii 17154. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseubii 17185 | Congruence: equivalents may be substituted inside an "all some one". This is the "all some one" counterpart of alsbii 17153. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | ralseu2d 17184 |
Deduction rule: Given "all some one" applied to a class, you can
extract the "exactly one" part. Note that the witness must
satisfy the
antecedent |
| 22-Jul-2026 | ralseu1d 17183 | Deduction rule: Given "all some one" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseu2d 17182 | Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "exactly one" part. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseu1d 17181 | Deduction rule: Given "all some one" applied to a top-level inference, you can extract the "for all" part. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | ralseud 17180 | Introduction rule for "all some one" restricted to a class. This is the converse of ralseu1d 17183 and ralseu2d 17184 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseud 17179 | Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d 17181 and alseu2d 17182 taken together. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | ralseurals 17178 | "All some one" restricted to a class implies "all some" restricted to that class. Restricted counterpart of alseuals 17177. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | alseuals 17177 | "All some one" implies "all some": requiring exactly one witness is stronger than requiring at least one. Any consequence of an allsome statement is therefore a consequence of the corresponding "all some one" statement, which is how alseu-no-surprise 17191 is proved. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | dfralseu2 17176 | The bounded "all some one" form is the general form with the class membership folded into the antecedent. This is the "all some one" counterpart of dfrals2 17142. (Contributed by David A. Wheeler, 22-Jul-2026.) |
| 22-Jul-2026 | df-ralseu 17175 |
Define "all some one" applied to a class, which means |
| 22-Jul-2026 | df-alseu 17174 |
Define "all some one" applied to a top-level implication, which means
|
| 22-Jul-2026 | wralseu 17173 |
Extend wff definition to include "all some one" applied to a class,
which
means |
| 22-Jul-2026 | walseu 17172 |
Extend wff definition to include "all some one" applied to a
top-level
implication, which means |
| 22-Jul-2026 | mptmex 5945 | If a function given by maps-to notation is inhabited, then the class it is defined on is inhabited. (Contributed by Jim Kingdon, 22-Jul-2026.) |
| 20-Jul-2026 | 2alsraln0idm 17171 |
Nested general "all some" quantifiers with class membership as their
antecedents, for the same class |
| 20-Jul-2026 | 2alsraln0m 17170 |
Nested general "all some" quantifiers with class membership as their
antecedents: |
| 20-Jul-2026 | n0alsm 17169 |
If |
| 20-Jul-2026 | alsraln0m 17166 |
The general "all some" quantifier with class membership as its
antecedent holds if and only if |
| 20-Jul-2026 | alsralrex 17165 |
The general "all some" quantifier with class membership as its
antecedent holds if and only if |
| 20-Jul-2026 | ralsanmo 17164 |
An "all some" statement restricted to a class, conjoined with the
claim
that at most one |
| 20-Jul-2026 | alsanmo 17163 |
An "all some" statement conjoined with the claim that at most one
|
| 20-Jul-2026 | rexrals 17162 |
If a member of |
| 20-Jul-2026 | ralrals 17161 |
If the universal part of a restricted "all some" statement holds,
then the
statement reduces to the existence of a member of |
| 20-Jul-2026 | als-no-surprise 17159 |
Demonstrate that there is never a "surprise" when using the allsome
quantifier, that is, it is never possible for the consequent to be both
always true and always false. This uses the definition of df-als 17140: the
universal parts give |
| 20-Jul-2026 | ralsmd 17150 | Deduction rule: Given "all some" applied to a class, the class is inhabited. This is stronger than ralsn0d 17149, which only concludes that the class is nonempty; see n0r 3535. (Contributed by David A. Wheeler, 20-Jul-2026.) |
| 19-Jul-2026 | disjdifg 3598 | A class and its relative complement are disjoint. (Contributed by NM, 24-Mar-1998.) Generalize from disjdif 3599. (Revised by BJ, 19-Jul-2026.) |
| 19-Jul-2026 | sseq0b 3564 | The only subclass of the empty class is itself. (Contributed by NM, 7-Mar-2007.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) Strengthen sseq0 3565 to a biconditional. (Revised by BJ, 19-Jul-2026.) |
| 18-Jul-2026 | sepab 4278 | Separation Scheme (Aussonderung) in terms of a class abstraction. Prefer using the more natural statement rabexg 4279. (Contributed by NM, 8-Jun-1994.) Put in closed form. (Revised by BJ, 18-Jul-2026.) |
| 18-Jul-2026 | inssdif0im 3592 | Intersection, subclass, and difference relationship. The converse holds in classical logic but not in intuitionistic logic. (Contributed by Jim Kingdon, 3-Aug-2018.) (Proof shortened by BJ, 18-Jul-2026.) |
| 15-Jul-2026 | rexals 17168 |
If some |
| 15-Jul-2026 | ralals 17167 |
If |
| 14-Jul-2026 | uniex2 4581 |
The Axiom of Union using the standard abbreviation for union. Given any
set |
| 14-Jul-2026 | sepgi 4252 | Inference associated with sepg 4251. (Contributed by NM, 21-Jun-1993.) (Revised by BJ, 14-Jul-2026.) |
| 13-Jul-2026 | f1setfi 7317 | The set of injections between two finite sets is finite. (Contributed by Jim Kingdon, 13-Jul-2026.) |
| 13-Jul-2026 | fdcf1 7316 | It is decidable whether a function from a finite set into another finite set is one-to-one. (Contributed by Jim Kingdon, 13-Jul-2026.) |
| 12-Jul-2026 | rals-no-surprise 17160 |
Demonstrate that there is never a "surprise" when using the allsome
quantifier restricted to a class, that is, it is never possible for the
consequent to be both always true and always false of the members of |
| 12-Jul-2026 | cbvals 17158 | Rule used to change bound variables, using implicit substitution. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | nfrals 17157 | Bound-variable hypothesis builder for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | nfals 17156 | Bound-variable hypothesis builder for "all some". (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | alsbid 17155 | Deduction form of alsbii 17153. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | ralsbii 17154 | Congruence for "all some" restricted to a class. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | alsbii 17153 | Congruence: equivalents may be substituted inside an "all some". (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | ralsex 17152 |
The consequent of an "all some" restricted to a class is witnessed:
some
member of |
| 12-Jul-2026 | alsex 17151 |
The consequent of an "all some" is witnessed: if |
| 12-Jul-2026 | ralsn0d 17149 | Deduction rule: Given "all some" applied to a class, the class is not the empty set. (Contributed by David A. Wheeler, 23-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | rals2d 17148 |
Deduction rule: Given "all some" applied to a class, you can extract
the "there exists" part. Note that the witness must satisfy
the
antecedent |
| 12-Jul-2026 | rals1d 17147 | Deduction rule: Given "all some" applied to a class, you can extract the "for all" part. (Contributed by David A. Wheeler, 20-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | ralsd 17144 | Introduction rule for "all some" restricted to a class. This is the converse of rals1d 17147 and rals2d 17148 taken together. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | alsd 17143 | Introduction rule: "all some" holds if the "for all" part holds and the antecedent has a witness. This is the converse of als1d 17145 and als2d 17146 taken together, and is what lets an "all some" statement be proved rather than merely taken apart. (Contributed by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | dfrals2 17142 | The bounded "all some" form is the general form with the class membership folded into the antecedent. (Contributed by David A. Wheeler, 22-Oct-2018.) (Revised by David A. Wheeler, 12-Jul-2026.) |
| 12-Jul-2026 | df-rals 17141 |
Define "all some" applied to a class, which means
An older definition of the "all some" quantifier when scoped to
a class,
named df-alsc and now removed, instead applied a bare formula |
| 12-Jul-2026 | wrals 17139 |
Extend wff definition to include "all some" applied to a class, which
means |
| 12-Jul-2026 | wals 17138 |
Extend wff definition to include "all some" applied to a top-level
implication, which means |
| 12-Jul-2026 | vvin 3569 | Two classes are both the universal class if and only if their intersection is the universal class. Dual of un00 3567. (Contributed by BJ, 12-Jul-2026.) |
| 7-Jul-2026 | cmnsubm 14114 | A submonoid of a commutative monoid is commutative. (Contributed by Jim Kingdon, 7-Jul-2026.) |
| 29-Jun-2026 | dichmul0or 16772 | Real number dichotomy is equivalent to the zero product principle for complex numbers: if a product is zero, one of its factors must be zero. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | dichmul0orlem5 16769 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | dichmul0orlem4 16768 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | dichmul0orlem3 16767 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | dichmul0orlem2 16766 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | dichmul0orlem1 16765 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 29-Jun-2026.) |
| 29-Jun-2026 | lealltlt2 16764 |
Alternative definition for |
| 29-Jun-2026 | lealltlt1 16763 |
Alternative definition for |
| 28-Jun-2026 | dichmul0orlem7 16771 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 28-Jun-2026.) |
| 28-Jun-2026 | dichmul0orlem6 16770 | Lemma for dichmul0or 16772. (Contributed by Matthew House, 28-Jun-2026.) |
| 28-Jun-2026 | msq0 8998 | A number is zero iff its square is zero. (Contributed by Matthew House, 28-Jun-2026.) |
| 28-Jun-2026 | msqap0 8997 | A number is apart from zero iff its square is apart from zero. (Contributed by Matthew House, 28-Jun-2026.) |
| 28-Jun-2026 | letrid 8442 | Tightness of real apartness. (Contributed by Matthew House, 28-Jun-2026.) |
| 19-Jun-2026 | ringen1zr0 14624 | The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). This holds already for nonunital rings, see rngen1zr0 14263, and semirings, see srgen1zr0 14294. (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.) |
| 19-Jun-2026 | srg1zr 14293 | The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 19-Jun-2026.) |
| 18-Jun-2026 | rngen1zr0 14263 | The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 18-Jun-2026.) |
| 18-Jun-2026 | rngen1zr 14262 | The only ring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 18-Jun-2026.) |
| 18-Jun-2026 | rng1zr 14261 | The only ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.) |
| 18-Jun-2026 | rng1zrlem 14260 | Lemma for rng1zr 14261 and srg1zr 14293. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 18-Jun-2026.) |
| 17-Jun-2026 | ballotfi 13284 | Bertrand's ballot problem : the probability that A is ahead throughout the counting. The proof formalized here is a proof "by reflection", as opposed to other known proofs "by induction" or "by permutation". This is Metamath 100 proof #30. (Contributed by Thierry Arnoux, 7-Dec-2016.) (Revised by Jim Kingdon, 17-Jun-2026.) |
| 17-Jun-2026 | ballotfilembfi 13241 | The set of countings where B got the first vote is finite. (Contributed by Jim Kingdon, 17-Jun-2026.) |
| 17-Jun-2026 | ballotfilemafi 13240 | The set of countings where A got the first vote, but does not stay strictly ahead throughout, is finite. (Contributed by Jim Kingdon, 17-Jun-2026.) |
| 17-Jun-2026 | ballotfilemefi 13239 |
|
| 17-Jun-2026 | rabxmdc 3554 | Law of excluded middle given decidability, in terms of restricted class abstractions. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Jim Kingdon, 17-Jun-2026.) |
| 15-Jun-2026 | ballotfilemgun 13270 |
A property of the defined |
| 15-Jun-2026 | ballotfilemgval 13269 |
Expand the value of |
| 15-Jun-2026 | ballotfilemdifcfz 13229 | Lemma for ballotfi . The portion of a counting representing votes for B within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.) |
| 15-Jun-2026 | ballotfilemcinfz 13228 | Lemma for ballotfi . The portion of a counting representing votes for A within a specified integer range is finite. (Contributed by Jim Kingdon, 15-Jun-2026.) |
| 12-Jun-2026 | ballotfilemsle 13250 |
The infimum of the set of zeroes of |
| 12-Jun-2026 | ballotfilemscl 13249 |
The set of zeroes of |
| 12-Jun-2026 | infssfzledc 10672 | The infimum of a decidable inhabited subset of an integer range is a lower bound for that set. (Contributed by Jim Kingdon, 12-Jun-2026.) |
| 12-Jun-2026 | infssfzcldc 10671 | The infimum of a decidable inhabited subset of an integer range is a member of the set. (Contributed by Jim Kingdon, 12-Jun-2026.) |
| 10-Jun-2026 | 2t3e6 9463 | 2 times 3 equals 6. (Contributed by Umit Teoman Dogan, 10-Jun-2026.) |
| 8-Jun-2026 | ballotfilemdifcfi 13227 | Lemma for ballotfi . The portion of a counting representing votes for B up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.) |
| 8-Jun-2026 | ballotfilemcinfi 13226 | Lemma for ballotfi . The portion of a counting representing votes for A up to a specified integer is finite. (Contributed by Jim Kingdon, 8-Jun-2026.) |
| 8-Jun-2026 | zfidc 9725 | Whether an integer is an element of a finite set of integers is decidable. (Contributed by Jim Kingdon, 8-Jun-2026.) |
| 7-Jun-2026 | ballotfilemcdc 13225 |
Lemma for ballotfi . It is decidable whether a given integer is an
element of a particular element of |
| 5-Jun-2026 | hashpwfi 11271 | The number of finite subsets of a finite set is two raised to the power of the size of the set. For a similar theorem with set size expressed using equinumerosity, see 2omapfi 7320. For the number of subsets (which need not be finite) of a set, see pw1mapen 17038. (Contributed by Jim Kingdon, 5-Jun-2026.) |
| 4-Jun-2026 | ballotfilemonn 13223 | The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.) |
| 3-Jun-2026 | papeq2 7610 | Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.) |
| 3-Jun-2026 | papeq1 7609 | Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.) |
| 2-Jun-2026 | resq01 11097 | If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.) |
| 31-May-2026 | aprprop 14603 | If two structures have the same ring components (properties), df-apr 14592 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.) |
| 31-May-2026 | ringunitsap0 14596 |
The set of units of a ring. If |
| 30-May-2026 | ringunitap 14595 | Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.) |
| 29-May-2026 | drnglring 14609 | A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | isdrngtap 14608 | The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | df-drngap 14606 | Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14592 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | aprunit 14594 | The df-apr 14592 relation with zero expresses whether a ring element is a unit. That is, the difference of an element of a ring and zero is invertible iff the element is a unit. (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | tapap 7616 | A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.) |
| 28-May-2026 | aprlring 14602 | A ring is a local ring if and only if the relation given by df-apr 14592 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.) |
| 28-May-2026 | papcotr 7613 | An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.) |
| 27-May-2026 | aprnzr 14601 | If the relation given by df-apr 14592 on a ring is an apartness relation, then the ring is a nonzero ring. (Contributed by Jim Kingdon, 27-May-2026.) |
| 27-May-2026 | papsym 7612 | An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.) |
| 27-May-2026 | papirr 7611 | An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.) |
| 24-May-2026 | gsumzfi 14160 | Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.) |
| 22-May-2026 | sshashneg 11283 |
Subsets of a class of a negative size (a degenerate case). Together
with ssenneg 11282 this shows that sseqn 11281 could not be extended beyond
|
| 22-May-2026 | ssenneg 11282 |
Subsets of a class of a negative size (a degenerate case). Together
with sshashneg 11283 this shows that sseqn 11281 could not be extended beyond
|
| 22-May-2026 | sseqn 11281 |
Two ways to express the subsets of a class of a given size. It might
seem that |
| 22-May-2026 | bilanri 389 | Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.) |
| 22-May-2026 | biranri 388 | Inference adding a conjunct to the right-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.) |
| 22-May-2026 | bilani 387 | Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.) |
| 22-May-2026 | birani 386 | Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.) |
| 20-May-2026 | ballotfilemofi 13221 |
|
| 19-May-2026 | fipwfi 7321 | The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.) |
| 18-May-2026 | 2omapfi 7320 | The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11217), see hashpwfi 11271. (Contributed by Jim Kingdon, 18-May-2026.) |
| 18-May-2026 | fissfi 7263 | A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.) |
| 18-May-2026 | fresaunres1disj 5571 | From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Mario Carneiro, 16-Feb-2015.) (Revised by Jim Kingdon, 18-May-2026.) |
| 18-May-2026 | fresaunres2disj 5570 | From the union of two functions with disjoint domains, either component can be recovered by restriction. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Jim Kingdon, 18-May-2026.) |
| 15-May-2026 | fsuppcorn 7301 |
The composition of a 1-1 function with a finitely supported function is
finitely supported. The purpose of the |
| 13-May-2026 | lincmble 10408 |
A linear combination of two reals which lies in the interval between them.
Like lincmb01cmp 10407 but generalized to require merely |
| 5-May-2026 | fmelpw1o 7606 |
With a formula
As proved in if0ab 3641, the associated element of |
| 5-May-2026 | if0elpw 4295 | A conditional class with the False alternative being sent to the empty class is an element of the powerset of the class corresponding to the True alternative when that class is a set. This statement requires fewer axioms than the general case ifelpwung 4627. (Contributed by BJ, 5-May-2026.) |
| 5-May-2026 | if0ss 3642 | A conditional class with the False alternative being sent to the empty class is included in the class corresponding to the True alternative. (Contributed by BJ, 5-May-2026.) |
| 27-Apr-2026 | repiecef 17089 |
Piecewise definition on the reals yields a function. The function
agrees with |
| 27-Apr-2026 | repiecege0 17088 | Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 17089 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.) |
| 27-Apr-2026 | repiecele0 17087 | Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 17089 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.) |
| 27-Apr-2026 | repiecelem 17086 |
Lemma for repiecele0 17087, repiecege0 17088, and repiecef 17089. The function
|
| 24-Apr-2026 | qdiff 17110 | The rationals are exactly those reals for which there exist two distinct rationals that are the same distance from the original number. Similar to apdiff 17109 but by stating the result positively we can completely sidestep the issue of not equal versus apart in the statement of the result. From an online post by Ingo Blechschmidt. (Contributed by Jim Kingdon, 24-Apr-2026.) |
| 23-Apr-2026 | exmidpeirce 17050 |
Excluded middle is equivalent to Peirce's law. Read an element of
|
| 22-Apr-2026 | exmidcon 17049 |
Excluded middle is equivalent to the form of contraposition which
removes negation. Read an element of |
| 22-Apr-2026 | exmidnotnotr 17048 |
Excluded middle is equivalent to double negation elimination. Read an
element of |
| 18-Apr-2026 | hashtpglem 11300 | Lemma for hashtpg 11301. This is one of the three not-equal conclusions required for the reverse direction. (Contributed by Jim Kingdon, 18-Apr-2026.) |
| 17-Apr-2026 | hashtpgim 11299 | The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) (Revised by AV, 18-Sep-2021.) (Revised by Jim Kingdon, 17-Apr-2026.) |
| 14-Apr-2026 | depind 16762 | Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem3 16761 | Lemma for depind 16762. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem2 16760 | Lemma for depind 16762. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem1 16759 | Lemma for depind 16762. (Contributed by Matthew House, 14-Apr-2026.) |
| 11-Apr-2026 | indval0 9298 | The indicator function generator does not generate a (meaningful) indicator function for a class which is not a subset of the domain. (Contributed by AV, 11-Apr-2026.) |
| 8-Apr-2026 | gsumclfi 14161 | Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.) |
| 4-Apr-2026 | gzsumsplit0 14150 |
Splitting off the rightmost summand of a group sum (even if it is the
only summand). Similar to gzsumsplit1r 13717 except that |
| 4-Apr-2026 | fzf1o 12144 | A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.) |
| 3-Apr-2026 | gsump1 14159 | Splitting off one element from a finite group sum. This would typically used in a proof by induction. (Contributed by Jim Kingdon, 3-Apr-2026.) |
| 2-Apr-2026 | gsumsncmn 14158 | Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.) |
| 31-Mar-2026 | sspw1or2 7544 | The set of subsets of a given set with one or two elements can be expressed as elements of the power set or as inhabited elements of the power set. (Contributed by Jim Kingdon, 31-Mar-2026.) |
| 28-Mar-2026 | imaf1fi 7240 | The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.) |
| 26-Mar-2026 | gsum0cmn 14156 | An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.) |
| 26-Mar-2026 | gzsumshift 14151 | Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.) |
| 25-Mar-2026 | gzsumgsum 14157 |
On an integer range, |
| 25-Mar-2026 | gzsumgsum1 14155 |
On an integer range starting at one, |
| 24-Mar-2026 | gsumvalfi 14154 | Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.) |
| 23-Mar-2026 | df-gsumfi 14153 |
Define the finite group sum (iterated sum) over an unordered finite set.
Given For a sum indexed by consecutive integers (and thus defining an order for the sum), see df-gzsum 13615. (Contributed by Jim Kingdon, 23-Mar-2026.) |
| 20-Mar-2026 | exmidssfi 7246 | Excluded middle is equivalent to any subset of a finite set being finite. Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 20-Mar-2026.) |
| 18-Mar-2026 | umgr1een 16378 | A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.) |
| 18-Mar-2026 | upgr1een 16377 | A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16374 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.) |
| 14-Mar-2026 | trlsex 16640 | The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.) |
| 13-Mar-2026 | eupthv 16699 | The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.) |
| 13-Mar-2026 | 1hevtxdg0fi 16560 |
The vertex degree of vertex |
| 11-Mar-2026 | en1hash 11241 | A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.) |
| 4-Mar-2026 | elmpom 6474 | If a maps-to operation is inhabited, the first class it is defined with is inhabited. (Contributed by Jim Kingdon, 4-Mar-2026.) |
| 22-Feb-2026 | isclwwlkni 16660 | A word over the set of vertices representing a closed walk of a fixed length. (Contributed by Jim Kingdon, 22-Feb-2026.) |
| 21-Feb-2026 | clwwlkex 16651 | Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.) |
| 17-Feb-2026 | vtxdgfif 16546 | In a finite graph, the vertex degree function is a function from vertices to nonnegative integers. (Contributed by Jim Kingdon, 17-Feb-2026.) |
| 16-Feb-2026 | vtxlpfi 16543 | In a finite graph, the number of loops from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.) |
| 16-Feb-2026 | vtxedgfi 16542 | In a finite graph, the number of edges from a given vertex is finite. (Contributed by Jim Kingdon, 16-Feb-2026.) |
| 15-Feb-2026 | eqsndc 7210 | Decidability of equality between a finite subset of a set with decidable equality, and a singleton whose element is an element of the larger set. (Contributed by Jim Kingdon, 15-Feb-2026.) |
| 14-Feb-2026 | pw1ninf 17033 |
The powerset of |
| 14-Feb-2026 | pw1ndom3 17032 |
The powerset of |
| 14-Feb-2026 | pw1ndom3lem 17031 | Lemma for pw1ndom3 17032. (Contributed by Jim Kingdon, 14-Feb-2026.) |
| 12-Feb-2026 | pw1dceq 17047 |
The powerset of |
| 12-Feb-2026 | 3dom 17030 | A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.) |
| 11-Feb-2026 | elssdc 7209 | Membership in a finite subset of a set with decidable equality is decidable. (Contributed by Jim Kingdon, 11-Feb-2026.) |
| 10-Feb-2026 | vtxdgfifival 16544 | The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.) |
| 10-Feb-2026 | fidcen 7203 | Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.) |
| 8-Feb-2026 | wlkvtxm 16593 | A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.) |
| 7-Feb-2026 | trlsv 16637 | The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.) |
| 7-Feb-2026 | wlkex 16578 | The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.) |
| 3-Feb-2026 | dom1oi 7117 | A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.) |
| 2-Feb-2026 | edginwlkd 16608 | The value of the edge function for an index of an edge within a walk is an edge. (Contributed by AV, 2-Jan-2021.) (Revised by AV, 9-Dec-2021.) (Revised by Jim Kingdon, 2-Feb-2026.) |
| 2-Feb-2026 | wlkelvv 16602 | A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.) |
| 1-Feb-2026 | wlkcprim 16603 | A walk as class with two components. (Contributed by Alexander van der Vekens, 22-Jul-2018.) (Revised by AV, 2-Jan-2021.) (Revised by Jim Kingdon, 1-Feb-2026.) |
| 1-Feb-2026 | wlkmex 16572 | If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.) |
| 31-Jan-2026 | fvmbr 5731 | If a function value is inhabited, the argument is related to the function value. (Contributed by Jim Kingdon, 31-Jan-2026.) |
| 30-Jan-2026 | elfvfvex 5730 | If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.) |
| 30-Jan-2026 | reldmm 5000 | A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.) |
| 25-Jan-2026 | indconst1 9304 | Indicator of the whole set. (Contributed by Thierry Arnoux, 25-Jan-2026.) |
| 25-Jan-2026 | indconst0 9303 | Indicator of the empty set. (Contributed by Thierry Arnoux, 25-Jan-2026.) |
| 25-Jan-2026 | ifp2 993 | Forward direction of dfifp2dc 994. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.) |
| 25-Jan-2026 | ifpdc 992 | The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.) |
| 24-Jan-2026 | eqabcbw 2376 | Version of eqabcb 2377 using implicit substitution, which requires fewer axioms. (Contributed by TM, 24-Jan-2026.) |
| 20-Jan-2026 | cats1fvd 11540 | A symbol other than the last in a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.) |
| 20-Jan-2026 | cats1fvnd 11539 | The last symbol of a concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 20-Jan-2026.) |
| 19-Jan-2026 | cats2catd 11543 | Closure of concatenation of concatenations with singleton words. (Contributed by AV, 1-Mar-2021.) (Revised by Jim Kingdon, 19-Jan-2026.) |
| 19-Jan-2026 | cats1catd 11542 | Closure of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.) |
| 19-Jan-2026 | cats1lend 11541 | The length of concatenation with a singleton word. (Contributed by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 19-Jan-2026.) |
| 18-Jan-2026 | rexanaliim 2656 | A transformation of restricted quantifiers and logical connectives. (Contributed by NM, 4-Sep-2005.) (Revised by Jim Kingdon, 18-Jan-2026.) |
| 15-Jan-2026 | df-uspgren 16408 |
Define the class of all undirected simple pseudographs (which could have
loops). An undirected simple pseudograph is a special undirected
pseudograph or a special undirected simple hypergraph, consisting of a
set |
| 11-Jan-2026 | en2prde 7539 | A set of size two is an unordered pair of two different elements. (Contributed by Alexander van der Vekens, 8-Dec-2017.) (Revised by Jim Kingdon, 11-Jan-2026.) |
| 10-Jan-2026 | pw1mapen 17038 |
Equinumerosity of |
| 10-Jan-2026 | pw1if 7584 |
Expressing a truth value in terms of an |
| 10-Jan-2026 | pw1m 7583 | A truth value which is inhabited is equal to true. This is a variation of pwntru 4336 and pwtrufal 17039. (Contributed by Jim Kingdon, 10-Jan-2026.) |
| 10-Jan-2026 | 1ndom2 7166 | Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.) |
| 9-Jan-2026 | pw1map 17037 |
Mapping between |
| 9-Jan-2026 | iftrueb01 7582 |
Using an |
| 8-Jan-2026 | pfxclz 11453 |
Closure of the prefix extractor. This extends pfxclg 11452 from |
| 8-Jan-2026 | fnpfx 11451 | The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.) |
| 7-Jan-2026 | pr1or2 7540 | An unordered pair, with decidable equality for the specified elements, has either one or two elements. (Contributed by Jim Kingdon, 7-Jan-2026.) |
| 6-Jan-2026 | upgr1elem1 16373 | Lemma for upgr1edc 16374. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.) |
| 3-Jan-2026 | df-umgren 16347 |
Define the class of all undirected multigraphs. An (undirected)
multigraph consists of a set |
| 3-Jan-2026 | df-upgren 16346 |
Define the class of all undirected pseudographs. An (undirected)
pseudograph consists of a set |
| 3-Jan-2026 | dom1o 7116 | Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 3-Jan-2026 | en2m 7113 | A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 3-Jan-2026 | en1m 7092 | A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 31-Dec-2025 | pw0ss 16336 | There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.) |
| 31-Dec-2025 | df-ushgrm 16323 |
Define the class of all undirected simple hypergraphs. An undirected
simple hypergraph is a special (non-simple, multiple, multi-) hypergraph
for which the edge function |
| 29-Dec-2025 | df-uhgrm 16322 |
Define the class of all undirected hypergraphs. An undirected
hypergraph consists of a set |
| 29-Dec-2025 | iedgex 16272 | Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | vtxex 16271 | Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | snmb 3834 | A singleton is inhabited iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) (Revised by Jim Kingdon, 29-Dec-2025.) |
| 27-Dec-2025 | lswex 11358 | Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11355 or lswcl 11357 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.) |
| 23-Dec-2025 | fzowrddc 11421 | Decidability of whether a range of integers is a subset of a word's domain. (Contributed by Jim Kingdon, 23-Dec-2025.) |
| 19-Dec-2025 | ccatclab 11364 | The concatenation of words over two sets is a word over the union of those sets. (Contributed by Jim Kingdon, 19-Dec-2025.) |
| 18-Dec-2025 | lswwrd 11353 | Extract the last symbol of a word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Jim Kingdon, 18-Dec-2025.) |
| 14-Dec-2025 | 2strstrndx 13474 | A constructed two-slot structure not depending on the hard-coded index value of the base set. (Contributed by Mario Carneiro, 29-Aug-2015.) (Revised by Jim Kingdon, 14-Dec-2025.) |
| 12-Dec-2025 | funiedgdm2vald 16285 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 12-Dec-2025.) |
| 11-Dec-2025 | funvtxdm2vald 16284 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 22-Sep-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 11-Dec-2025 | funiedgdm2domval 16283 | The set of indexed edges of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 11-Dec-2025 | funvtxdm2domval 16282 | The set of vertices of an extensible structure with (at least) two slots. (Contributed by AV, 12-Oct-2020.) (Revised by Jim Kingdon, 11-Dec-2025.) |
| 4-Dec-2025 | hash2en 11297 | Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.) |
| 30-Nov-2025 | nninfnfiinf 17078 | An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.) |
| 30-Nov-2025 | eluz3nn 9969 | An integer greater than or equal to 3 is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) (Proof shortened by AV, 30-Nov-2025.) |
| 27-Nov-2025 | psrelbasfi 15069 | Simpler form of psrelbas 15068 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.) |
| 26-Nov-2025 | mplsubgfileminv 15093 | Lemma for mplsubgfi 15094. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 26-Nov-2025 | mplsubgfilemcl 15092 | Lemma for mplsubgfi 15094. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 25-Nov-2025 | nninfinfwlpo 7520 | The point at infinity in ℕ∞ being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO). By isolated, we mean that the equality of that point with every other element of ℕ∞ is decidable. From an online post by Martin Escardo. By contrast, elements of ℕ∞ corresponding to natural numbers are isolated (nninfisol 7473). (Contributed by Jim Kingdon, 25-Nov-2025.) |
| 23-Nov-2025 | psrbagfi 15061 | A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.) |
| 22-Nov-2025 | df-acnm 7525 |
Define a local and length-limited version of the axiom of choice. The
definition of the predicate |
| 21-Nov-2025 | mplsubgfilemm 15091 | Lemma for mplsubgfi 15094. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.) |
| 15-Nov-2025 | uzuzle35 9967 | An integer greater than or equal to 5 is an integer greater than or equal to 3. (Contributed by AV, 15-Nov-2025.) |
| 14-Nov-2025 | 2omapen 7319 |
Equinumerosity of |
| 12-Nov-2025 | 2omap 7318 |
Mapping between |
| 11-Nov-2025 | domomsubct 17043 |
A set dominated by |
| 10-Nov-2025 | prdsbaslemss 14176 | Lemma for prdsbas 14178 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.) |
| 5-Nov-2025 | fnmpl 15086 | mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.) |
| 4-Nov-2025 | mplelbascoe 15085 | Property of being a polynomial. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 4-Nov-2025 | mplbascoe 15084 | Base set of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 4-Nov-2025 | mplvalcoe 15083 | Value of the set of multivariate polynomials. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 25-Jun-2019.) (Revised by Jim Kingdon, 4-Nov-2025.) |
| 1-Nov-2025 | ficardon 7534 | The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.) |
| 31-Oct-2025 | bitsdc 12716 | Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.) |
| 28-Oct-2025 | nn0maxcl 11993 | The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.) |
| 28-Oct-2025 | qdcle 10683 |
Rational |
| 17-Oct-2025 | plycoeid3 15860 | 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 7237 | 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 7235 | 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 3637 | 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 13019 | A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.) |
| 7-Oct-2025 | df-mplcoe 15050 |
Define the subalgebra of the power series algebra generated by the
variables; this is the polynomial algebra (the set of power series with
finite degree).
The index set (which has an element for each variable) is |
| 6-Oct-2025 | dvconstss 15801 | Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.) |
| 6-Oct-2025 | dcfrompeirce 1499 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromcon 1498 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromnotnotr 1497 |
The decidability of a proposition |
| 3-Oct-2025 | dvidre 15800 | Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvconstre 15799 | Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvidsslem 15796 |
Lemma for dvconstss 15801. Analogue of dvidlemap 15794 where |
| 3-Oct-2025 | dvidrelem 15795 | Lemma for dvidre 15800 and dvconstre 15799. Analogue of dvidlemap 15794 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 28-Sep-2025 | metuex 14894 | Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 28-Sep-2025 | cndsex 14892 | The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 25-Sep-2025 | cntopex 14893 | The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.) |
| 24-Sep-2025 | mopnset 14891 |
Getting a set by applying |
| 24-Sep-2025 | blfn 14890 | The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.) |
| 23-Sep-2025 | elfzoext 10612 | Membership of an integer in an extended open range of integers, extension added to the right. (Contributed by AV, 30-Apr-2020.) (Proof shortened by AV, 23-Sep-2025.) |
| 22-Sep-2025 | plycjlemc 15863 | Lemma for plycj 15864. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.) |
| 22-Sep-2025 | asclelbas 15028 | Lifted scalars are in the base set of the algebra. (Contributed by Zhi Wang, 11-Sep-2025.) (Proof shortened by Thierry Arnoux, 22-Sep-2025.) |
| 20-Sep-2025 | plycolemc 15861 |
Lemma for plyco 15862. The result expressed as a sum, with a
degree and
coefficients for |
| 18-Sep-2025 | elfzoextl 10611 | Membership of an integer in an extended open range of integers, extension added to the left. (Contributed by AV, 31-Aug-2025.) Generalized by replacing the left border of the ranges. (Revised by SN, 18-Sep-2025.) |
| 16-Sep-2025 | lgsquadlemofi 16207 |
Lemma for lgsquad 16211. There are finitely many members of |
| 16-Sep-2025 | lgsquadlemsfi 16206 |
Lemma for lgsquad 16211. |
| 16-Sep-2025 | opabfi 7247 | 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 6371 |
Principle of unique choice. This is also called non-choice. The name
choice results in its similarity to something like acfun 7563 (with the key
difference being the change of |
| 11-Sep-2025 | assa2ass2 15012 | Left- and right-associative property of an associative algebra. Notice that the scalars are not commuted! (Contributed by Zhi Wang, 11-Sep-2025.) |
| 11-Sep-2025 | assa2ass 15011 | Left- and right-associative property of an associative algebra. Notice that the scalars are commuted! (Contributed by AV, 14-Aug-2019.) (Proof shortened by Zhi Wang, 11-Sep-2025.) |
| 11-Sep-2025 | expghmap 14944 | 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 14926 | The invertible complex numbers are exactly those apart from zero. This is recapb 9002 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.) |
| 9-Sep-2025 | gzsummhm2 14148 | 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 | gzsummhm 14147 | 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 12704 | 5 does not divide 6. (Contributed by AV, 8-Sep-2025.) |
| 8-Sep-2025 | 5ndvds3 12703 | 5 does not divide 3. (Contributed by AV, 8-Sep-2025.) |
| 7-Sep-2025 | 5eluz3 9963 | 5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.) |
| 6-Sep-2025 | gzsumconst 14145 | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.) |
| 5-Sep-2025 | uzuzle34 9966 | An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.) |
| 30-Aug-2025 | gzsumsubmcl 14144 | 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 10913 | 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 10960 |
Rearrange a sum via an arbitrary bijection on |
| 25-Aug-2025 | irrmulap 10050 | 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 10049. (Contributed by Jim Kingdon, 25-Aug-2025.) |
| 19-Aug-2025 | seqp1g 10905 | 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 10902 | 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 11313 | A zero-based sequence is a word. In iswrdinn0 11311 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 | gzsumcl 13806 | Closure of an ordered 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 11311 | 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.) |
| 14-Aug-2025 | gzsumfzval 13713 |
An expression for |
| 13-Aug-2025 | znidom 14994 |
The ℤ/nℤ structure is an integral domain when |
| 12-Aug-2025 | rrgmex 14571 | A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.) |
| 10-Aug-2025 | gausslemma2dlem1cl 16190 |
Lemma for gausslemma2dlem1 16192. Closure of the body of the
definition
of |
| 9-Aug-2025 | gausslemma2dlem1f1o 16191 | Lemma for gausslemma2dlem1 16192. (Contributed by Jim Kingdon, 9-Aug-2025.) |
| 7-Aug-2025 | qdclt 10682 |
Rational |
| 22-Jul-2025 | ivthdich 15756 |
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 15746 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 15755 | 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 15754 | Lemma for ivthdich 15756. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hovergt0 15753 | The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hoverlt1 15752 | The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 21-Jul-2025 | hoverb 15751 | A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | hovera 15750 | A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrrdv 2760 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrrdv 2759 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrdv 2758 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrdv 2757 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 20-Jul-2025 | hovercncf 15749 | 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 15719 | The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.) |
| 18-Jul-2025 | maxcncf 15718 | The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.) |
| 14-Jul-2025 | xnn0nnen 10876 | 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 7463 | 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 12819 | Lemma for nninfct 12820. (Contributed by Jim Kingdon, 10-Jul-2025.) |
| 8-Jul-2025 | nnnninfen 17076 | 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 12820 | The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 8-Jul-2025 | nninfinf 10882 | ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 7-Jul-2025 | ivthreinc 15748 |
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 15746).
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 | fngzsum 13710 | Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.) |
| 28-Jun-2025 | iotaexel 6043 | 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-gzsum 13615 |
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. But see df-gsumfi 14153
for the case where (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.) |
| 20-Jun-2025 | opprnzrbg 14494 | The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14495. (Contributed by SN, 20-Jun-2025.) |
| 16-Jun-2025 | fnpsr 15053 | The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.) |
| 14-Jun-2025 | basm 13416 | A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 14-Jun-2025 | elfvm 5729 | If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 6-Jun-2025 | pcxqcl 13093 | The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.) |
| 5-Jun-2025 | xqltnle 10704 |
"Less than" expressed in terms of "less than or equal to",
for extended
numbers which are rational or |
| 5-Jun-2025 | ceqsexv2d 2862 | 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.) |
| 31-May-2025 | vtocl4ga 2895 | Implicit substitution of 4 classes for 4 setvar variables. (Contributed by AV, 22-Jan-2019.) (Proof shortened by Wolf Lammen, 31-May-2025.) |
| 30-May-2025 | 4sqexercise2 13180 | Exercise which may help in understanding the proof of 4sqlemsdc 13181. (Contributed by Jim Kingdon, 30-May-2025.) |
| 27-May-2025 | iotaexab 5356 |
Existence of the |
| 25-May-2025 | 4sqlemsdc 13181 |
Lemma for 4sq 13191. The property of being the sum of four
squares is
decidable.
The proof involves showing that (for a particular |
| 25-May-2025 | 4sqexercise1 13179 | Exercise which may help in understanding the proof of 4sqlemsdc 13181. (Contributed by Jim Kingdon, 25-May-2025.) |
| 24-May-2025 | 4sqleminfi 13178 |
Lemma for 4sq 13191. |
| 24-May-2025 | 4sqlemffi 13177 |
Lemma for 4sq 13191. |
| 24-May-2025 | 4sqlemafi 13176 |
Lemma for 4sq 13191. |
| 24-May-2025 | infidc 7248 | 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 14958 |
Set existence for |
| 16-May-2025 | rhmex 14466 | Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.) |
| 15-May-2025 | ghmex 14060 | The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 15-May-2025 | mhmex 13771 | The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 14-May-2025 | idomcringd 14589 | 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 14579 | 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 14255 | 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 13427. (Contributed by Jim Kingdon, 5-May-2025.) |
| 5-May-2025 | ablressid 14141 | 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 13427. (Contributed by Jim Kingdon, 5-May-2025.) |
| 30-Apr-2025 | dvply2g 15869 | 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 14799 | Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 29-Apr-2025 | ressbasid 13426 | The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 28-Apr-2025 | lssmex 14694 | 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 14903 | 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 14901 | 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 14812 | Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 27-Apr-2025 | lssex 14693 | Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 25-Apr-2025 | rspex 14813 | Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | lspex 14734 | Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | eqgex 14026 | The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | qusex 13648 | Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 23-Apr-2025 | 1dom1el 7107 | 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 13928 | Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.) |
| 21-Apr-2025 | uspgruhgr 16440 | An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.) |
| 20-Apr-2025 | uspgriedgedg 16432 | In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.) |
| 20-Apr-2025 | uspgredgiedg 16431 | In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.) |
| 20-Apr-2025 | elovmpod 6287 | Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6288 in deduction form. (Revised by AV, 20-Apr-2025.) |
| 20-Apr-2025 | fdmeu 5746 | There is exactly one codomain element for each element of the domain of a function. (Contributed by AV, 20-Apr-2025.) |
| 18-Apr-2025 | fsumdvdsmul 16111 |
Product of two divisor sums. (This is also the main part of the proof
that " |
| 18-Apr-2025 | mpodvdsmulf1o 16110 |
If |
| 18-Apr-2025 | df2idl2 14848 | 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 14840 | 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 14827 | 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 14814 | 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 14768 | 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 14785 | Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.) |
| 14-Apr-2025 | grpmgmd 13833 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) |
| 12-Apr-2025 | psraddcl 15073 | 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 17121 | Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.) |
| 4-Apr-2025 | ghmf1 14078 | 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 14872 | 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 14907 | 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 14896. (Revised by GG, 31-Mar-2025.) |
| 31-Mar-2025 | cnfldle 14906 |
The ordering of the field of complex numbers. Note that this is not
actually an ordering on |
| 31-Mar-2025 | cnfldtset 14905 | 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 14902 | The multiplication operation of the field of complex numbers. Version of cnfldmul 14903 using maps-to notation, which does not require ax-mulf 8302. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | mpocnfldadd 14900 | The addition operation of the field of complex numbers. Version of cnfldadd 14901 using maps-to notation, which does not require ax-addf 8301. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | df-cnfld 14896 |
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 14898, cnfldadd 14901, cnfldmul 14903, cnfldcj 14904, cnfldtset 14905, cnfldle 14906, cnfldds 14907, and cnfldbas 14899. 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 14863 | 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 14590 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 22-Mar-2025 | idomdomd 14588 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 21-Mar-2025 | df2idl2rng 14847 | 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 14821 | 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 14820 | 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 13594 | Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.) |
| 20-Mar-2025 | homslid 13591 |
Slot property of |
| 19-Mar-2025 | ptex 13620 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) |
| 18-Mar-2025 | prdsex 14174 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) |
| 16-Mar-2025 | plycn 15865 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8302. (Revised by GG, 16-Mar-2025.) |
| 16-Mar-2025 | expcn 15672 |
The power function on complex numbers, for fixed exponent |
| 16-Mar-2025 | mpomulcn 15669 | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| 16-Mar-2025 | mpomulf 8316 | Multiplication is an operation on complex numbers. Version of ax-mulf 8302 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8277. (Contributed by GG, 16-Mar-2025.) |
| 15-Mar-2025 | lmodvscld 14644 | Closure of scalar product for a left module. (Contributed by SN, 15-Mar-2025.) |
| 13-Mar-2025 | 2idlss 14853 | 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 13628 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) |
| 11-Mar-2025 | rng2idlsubgsubrng 14859 | 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 14856 | 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 14837 |
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 14836 |
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 14835 |
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 13629 | Value of an image structure. The is a lemma for the theorems imasbas 13630, imasplusg 13631, and imasmulr 13632 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 14846 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | 2idllidld 14845 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | quseccl 14038 | 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 6194 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.) |
| 8-Mar-2025 | subgex 13981 | The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.) |
| 8-Mar-2025 | fsuppfund 7294 | A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.) |
| 7-Mar-2025 | ringrzd 14353 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | ringlzd 14352 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | qusecsub 14137 | 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.) |
| 2-Mar-2025 | isassad 15013 | Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| 2-Mar-2025 | assasca 15010 | The scalars of an associative algebra form a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by SN, 2-Mar-2025.) |
| 2-Mar-2025 | isassa 15004 | The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| 2-Mar-2025 | df-assa 15001 | Definition of an associative algebra. An associative algebra is a set equipped with a left-module structure on a ring, coupled with a multiplicative internal operation on the vectors of the module that is associative and distributive for the additive structure of the left-module (so giving the vectors a ring structure) and that is also bilinear under the scalar product. (Contributed by Mario Carneiro, 29-Dec-2014.) (Revised by SN, 2-Mar-2025.) |
| 1-Mar-2025 | quselbasg 14035 | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
| 28-Feb-2025 | qusmulrng 14871 | Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14872. Similar to qusmul2 14868. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.) |
| 28-Feb-2025 | ringressid 14370 | 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 13427. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 28-Feb-2025 | grpressid 13868 | 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 13427. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 27-Feb-2025 | imasringf1 14372 | The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.) |
| 26-Feb-2025 | strext 13461 |
Extending the upper range of a structure. This works because when we
say that a structure has components in |
| 25-Feb-2025 | subrngringnsg 14515 | A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | rngansg 14251 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | ecqusaddd 14043 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) |
| 24-Feb-2025 | ecqusaddcl 14044 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) |
| 24-Feb-2025 | quseccl0g 14036 |
Closure of the quotient map for a quotient group. (Contributed by Mario
Carneiro, 18-Sep-2015.) Generalization of quseccl 14038 for arbitrary sets
|
| 23-Feb-2025 | ltlenmkv 17132 |
If |
| 23-Feb-2025 | neap0mkv 17131 | 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 14864 | 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 14866 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | 2idlcpblrng 14862 | 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 14505 | 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 14504 | A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringring 14503 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringnzr 14502 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | islring 14501 | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | df-lring 14500 | 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 14498 | 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 14492 | 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 14259 | The quotient structure of a non-unital ring is a non-unital ring (qusring2 14373 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdir 14253 | Ring multiplication distributes over subtraction. (subdir 8713 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14364. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdi 14252 | Ring multiplication distributes over subtraction. (subdi 8712 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14363. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | abbib 2356 | Equal class abstractions require equivalent formulas, and conversely. (Contributed by NM, 25-Nov-2013.) (Revised by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-8 1557 and df-clel 2234 (by avoiding use of cleqh 2338). (Revised by BJ, 23-Jun-2019.) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025.) |
| 22-Feb-2025 | imasrngf1 14258 | 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 14257 | The image structure of a non-unital ring is a non-unital ring (imasring 14371 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | rngmgpf 14238 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 14317 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | imasabl 14142 | The image structure of an abelian group is an abelian group (imasgrp 13916 analog). (Contributed by AV, 22-Feb-2025.) |
| 21-Feb-2025 | prdssgrpd 14193 | The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | prdsplusgsgrpcl 14192 | Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | dftap2 7617 | Tight apartness with the apartness properties from df-pap 7608 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.) |
| 20-Feb-2025 | rng2idlsubg0 14861 | 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 14860 | 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 14858 | 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 14857 | 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 14855 | 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 14854 | The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | 2idlelb 14844 | Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) |
| 20-Feb-2025 | aprap 14600 | The relation given by df-apr 14592 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | setscomd 13395 | Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | ifnebibdc 3686 | The converse of ifbi 3661 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnefals 3685 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnetruedc 3684 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 18-Feb-2025 | rnglidlmcl 14819 | 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 14599 | The apartness relation given by df-apr 14592 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprsym 14598 | The apartness relation given by df-apr 14592 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprval 14593 | Expand Definition df-apr 14592. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | subrngpropd 14526 | 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 14250 | Double negation of a product in a non-unital ring (mul2neg 8725 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14362. (Revised by AV, 17-Feb-2025.) |
| 17-Feb-2025 | rngmneg2 14249 | Negation of a product in a non-unital ring (mulneg2 8723 analog). In contrast to ringmneg2 14361, 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 14248 | Negation of a product in a non-unital ring (mulneg1 8722 analog). In contrast to ringmneg1 14360, 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 14597 | The apartness relation given by df-apr 14592 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 16-Feb-2025 | rngrz 14247 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14351. (Revised by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rng0cl 14244 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rngacl 14243 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rnggrp 14239 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | aptap 8979 | Complex apartness (as defined at df-ap 8911) is a tight apartness (as defined at df-tap 7615). (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 15-Feb-2025 | subsubrng2 14525 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subsubrng 14524 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngin 14523 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngintm 14522 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprsubrngg 14521 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | issubrng2 14520 | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrngbg 14385 | A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 14384. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrng 14384 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | rngpropd 14256 | 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 13730 | 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 13726 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | tapeq2 7619 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.) |
| 14-Feb-2025 | subrngmcl 14519 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14543. (Revised by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngacl 14518 | A subring is closed under addition. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrng0 14517 | A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngbas 14516 | Base set of a subring structure. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngsubg 14514 | A subring is a subgroup. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrcl 14513 | Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrng 14512 | A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngid 14511 | Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngss 14510 | A subring is a subset. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | issubrng 14509 | The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | df-subrng 14508 | 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 14254 | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | rngdi 14241 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | exmidmotap 7627 | 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 7626 | 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 7608 |
Apartness predicate. A relation |
| 13-Feb-2025 | 2idl1 14852 | Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | 2idl0 14851 | Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl1 14850 | Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl0 14849 | Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | isridl 14843 | 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 14592 | The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14600. (Contributed by Jim Kingdon, 13-Feb-2025.) |
| 13-Feb-2025 | rngass 14240 | 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 13729 | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | eqab 2373 | One direction of eqabb 2374. (Contributed by Wolf Lammen, 13-Feb-2025.) |
| 12-Feb-2025 | eqabb 2374 |
Equality of a class variable and a class abstraction (also called a
class builder). Theorem 5.1 of [Quine] p.
34. This theorem shows the
relationship between expressions with class abstractions and expressions
with class variables. Note that abbib 2356 and its relatives are among
those useful for converting theorems with class variables to equivalent
theorems with wff variables, by first substituting a class abstraction
for each class variable.
Class variables can always be eliminated from a theorem to result in an
equivalent theorem with wff variables, and vice-versa. The idea is
roughly as follows. To convert a theorem with a wff variable (Contributed by NM, 26-May-1993.) (Proof shortened by Wolf Lammen, 12-Feb-2025.) |
| 8-Feb-2025 | 2oneel 7622 |
|
| 8-Feb-2025 | tapeq1 7618 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.) |
| 7-Feb-2025 | psrgrp 15078 | The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014.) (Proof shortened by SN, 7-Feb-2025.) |
| 7-Feb-2025 | resrhm2b 14559 | Restriction of the codomain of a (ring) homomorphism. resghm2b 14067 analog. (Contributed by SN, 7-Feb-2025.) |
| 6-Feb-2025 | zzlesq 11148 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotap 7625 |
If there is at most one tight apartness on |
| 6-Feb-2025 | 2omotaplemst 7624 | Lemma for 2omotap 7625. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotaplemap 7623 | Lemma for 2omotap 7625. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2onetap 7621 |
Negated equality is a tight apartness on |
| 5-Feb-2025 | netap 7620 | Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.) |
| 5-Feb-2025 | df-tap 7615 |
Tight apartness predicate. A relation |
| 1-Feb-2025 | mulgnn0cld 13948 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13943. (Contributed by SN, 1-Feb-2025.) |
| 31-Jan-2025 | 0subg 14004 | 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 13863 | The right inverse of a group element. Deduction associated with grprinv 13858. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplinvd 13862 | The left inverse of a group element. Deduction associated with grplinv 13857. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpinvcld 13856 | A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpridd 13841 | The identity element of a group is a right identity. Deduction associated with grprid 13839. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplidd 13840 | The identity element of a group is a left identity. Deduction associated with grplid 13838. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpassd 13819 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
| 28-Jan-2025 | dvdsrex 14407 | Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.) |
| 24-Jan-2025 | reldvdsrsrg 14401 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.) |
| 18-Jan-2025 | rerecapb 9174 | 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 9002 | 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 | flddrngd 14617 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
| 17-Jan-2025 | ressval3d 13428 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 17-Jan-2025 | strressid 13427 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 17-Jan-2025 | snelpwg 4350 | A singleton of a set is a member of the powerclass of a class if and only if that set is a member of that class. (Contributed by NM, 1-Apr-1998.) Put in closed form and avoid ax-nul 4259. (Revised by BJ, 17-Jan-2025.) |
| 16-Jan-2025 | ressex 13421 | Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 16-Jan-2025 | ressvalsets 13420 | Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 15-Jan-2025 | vsnex 4348 | A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.) |
| 12-Jan-2025 | isrim 14478 | 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 14480 | A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
| 10-Jan-2025 | isrim0 14470 | 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 14380 |
Existence of the opposite ring. If you know that |
| 10-Jan-2025 | mgpex 14225 |
Existence of the multiplication group. If |
| 6-Jan-2025 | ord3 6699 | Ordinal 3 is an ordinal class. (Contributed by BTernaryTau, 6-Jan-2025.) |
| 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 3850 | The singleton of an element of a class is a subset of the class (inference form of snssg 3849). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.) |
| 1-Jan-2025 | snssg 3849 | 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 3848 | Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.) |
| 30-Dec-2024 | rex2dom 7110 | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
| 23-Dec-2024 | en2prd 7106 | Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
| 11-Dec-2024 | elopabr 4425 | Membership in an ordered-pair class abstraction defined by a binary relation. (Contributed by AV, 16-Feb-2021.) (Proof shortened by SN, 11-Dec-2024.) |
| 10-Dec-2024 | cbvreuw 2781 | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2784 with a disjoint variable condition. (Contributed by Mario Carneiro, 15-Oct-2016.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Dec-2024.) |
| 9-Dec-2024 | nninfwlpoim 7519 | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
| 8-Dec-2024 | nninfinfwlpolem 7518 | Lemma for nninfinfwlpo 7520. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemdc 7517 | Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemginf 7516 | Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemg 7515 | Lemma for nninfwlpoim 7519. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 7-Dec-2024 | nninfwlpor 7514 | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | nninfwlporlem 7513 | Lemma for nninfwlpor 7514. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | domssr 7064 |
If |
| 7-Dec-2024 | f1dom4g 7039 | The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 7044 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 7-Dec-2024 | f1oen4g 7038 | The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 7043 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 6-Dec-2024 | nninfwlporlemd 7512 | 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 7521 | 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 7511 | The Weak Limited Principle of Omniscience (WLPO) implies that it is decidable whether an element of ℕ∞ equals the point at infinity. (Contributed by Jim Kingdon, 3-Dec-2024.) |
| 29-Nov-2024 | brdom2g 7031 | Dominance relation. This variation of brdomg 7032 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 7032. (Revised by BTernaryTau, 29-Nov-2024.) |
| 28-Nov-2024 | basmexd 13415 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
| 23-Nov-2024 | fldcrngd 14618 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
| 22-Nov-2024 | eliotaeu 5366 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 22-Nov-2024 | eliota 5365 | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 18-Nov-2024 | basmex 13414 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
| 14-Nov-2024 | dcand 945 | 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 14782 | 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 14781 | 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 13531 | The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.) |
| 11-Nov-2024 | bj-con1st 16791 | Contraposition when the antecedent is a negated stable proposition. See con1dc 868. (Contributed by BJ, 11-Nov-2024.) |
| 11-Nov-2024 | slotsdifdsndx 13581 | The index of the slot for the distance is not the index of other slots. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | plendxnocndx 13570 | The slot for the orthocomplementation is not the slot for the order in an extensible structure. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | basendxnocndx 13569 | The slot for the orthocomplementation is not the slot for the base set in an extensible structure. (Contributed by AV, 11-Nov-2024.) |
| 11-Nov-2024 | slotsdifplendx 13566 | 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 13550 | 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 6304 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) |
| 11-Nov-2024 | const 864 | Contraposition when the antecedent is a negated stable proposition. See comment of condc 865. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.) |
| 10-Nov-2024 | slotsdifunifndx 13588 | 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 13423 | 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 14383 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprbasg 14382 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprsllem 14381 | Lemma for opprbasg 14382 and oppraddg 14383. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
| 4-Nov-2024 | lgsfvalg 16136 |
Value of the function |
| 3-Nov-2024 | znmul 14979 | 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 14978 | 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 14977 | 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 14976 | Lemma for znbas 14981. (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 14968 |
Ring operation of a |
| 3-Nov-2024 | zlmplusgg 14967 |
Group operation of a |
| 3-Nov-2024 | zlmbasg 14966 |
Base set of a |
| 3-Nov-2024 | zlmlemg 14965 | Lemma for zlmbasg 14966 and zlmplusgg 14967. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| 2-Nov-2024 | zlmsca 14969 |
Scalar ring of a |
| 1-Nov-2024 | plendxnvscandx 13565 | 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 13564 | 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 13563 | 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 11089 | 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 13578 | 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 13549 | 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 13547 | 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 13546 | 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 13545 | The index of the slot for the group operation in an extensible structure is a positive integer. (Contributed by AV, 31-Oct-2024.) |
| 30-Oct-2024 | basendxltedgfndx 16263 |
The index value of the |
| 30-Oct-2024 | plendxnbasendx 13561 | 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 13560 |
The index value of the |
| 30-Oct-2024 | plendxnn 13559 | 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 14787 | 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 14784 | 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 14780 | 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 14779 | 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 14778 | 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 14777 | Lemma for srabaseg 14778 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 13580 | 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 13579 |
The slots Scalar, |
| 29-Oct-2024 | slotstnscsi 13551 |
The slots Scalar, |
| 29-Oct-2024 | ipndxnmulrndx 13530 | 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 13529 | 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 13517 | 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 13512 | 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 11275 | 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 11274 | A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 29-Oct-2024 | fiubm 11273 | Lemma for fiubz 11274 and fiubnn 11275. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 28-Oct-2024 | edgfndxid 16262 | The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 28-Oct-2024.) |
| 28-Oct-2024 | unifndxntsetndx 13587 | 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 13585 | 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 13584 | 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 13576 | 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 13575 | 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 13574 | 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 16783 |
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 17028 for the version not using the definition of
stability.
(Contributed by BJ, 9-Oct-2019.) Prove it in |
| 27-Oct-2024 | bj-imnimnn 16778 | 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 16777 as its last step. (Contributed by BJ, 27-Oct-2024.) |
| 25-Oct-2024 | nnwosdc 12818 | 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 12815 | 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 12816 | 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 17028 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 862, 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 13586 | 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 13528 | 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 13510 | 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 12921 |
Lemma for isprm5 12922. The interesting direction (showing that
one only
needs to check prime divisors up to the square root of |
| 19-Oct-2024 | resseqnbasd 13429 | 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 14690 |
The right module |
| 18-Oct-2024 | mgpress 14232 | 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 13577 | 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 13562 | 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 13548 | 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 13518 | 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 13516 | 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 13515 | 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 13511 | 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 13500 | 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 13499 | 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 13498 | 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 13469 | 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 13467 | 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 10014 |
Membership of an integer in |
| 14-Oct-2024 | 2zinfmin 12011 | 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 12010 |
Equivalence of |
| 13-Oct-2024 | edgfndxnn 16261 | The index value of the edge function extractor is a positive integer. This property should be ensured for every concrete coding because otherwise it could not be used in an extensible structure (slots must be positive integers). (Contributed by AV, 21-Sep-2020.) (Proof shortened by AV, 13-Oct-2024.) |
| 13-Oct-2024 | edgfndx 16260 | Index value of the df-edgf 16258 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.) |
| 13-Oct-2024 | prdsvallem 13623 | Lemma for prdsval 14175. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 14175, dependency on df-hom 13457 removed. (Revised by AV, 13-Oct-2024.) |
| 13-Oct-2024 | pcxnn0cl 13091 | Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0letri 10207 | Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0dcle 10206 |
Decidability of |
| 9-Oct-2024 | nn0leexp2 11150 | Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.) |
| 8-Oct-2024 | pclemdc 13069 | Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.) |
| 8-Oct-2024 | elnn0dc 10013 |
Membership of an integer in |
| 7-Oct-2024 | pclemub 13068 | 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 13067 | 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 11149 | Special case of ltexp2 16049 which we use here because we haven't yet defined df-rpcxp 15963 which is used in the current proof of ltexp2 16049. (Contributed by Jim Kingdon, 7-Oct-2024.) |
| 6-Oct-2024 | suprzcl2dc 10676 | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 8300.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) |
| 5-Oct-2024 | zsupssdc 10675 | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 8300.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
| 5-Oct-2024 | suprzubdc 10673 | 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.) |
| 3-Oct-2024 | ab0w 3550 | The class of sets verifying a property is the empty class if and only if that property is a contradiction. (Contributed by GG, 3-Oct-2024.) |
| 1-Oct-2024 | infex2g 7374 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
| 30-Sep-2024 | unbendc 13347 | 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 12910 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | dcfi 7315 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | cbvriotavw 6049 | Change bound variable in a restricted description binder. Version of cbvriotav 6051 with a disjoint variable condition. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.) |
| 30-Sep-2024 | cbviotavw 5343 | Change bound variables in a description binder. Version of cbviotav 5344 with a disjoint variable condition. (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.) |
| 29-Sep-2024 | ssnnct 13340 |
A decidable subset of |
| 29-Sep-2024 | ssnnctlemct 13339 | Lemma for ssnnct 13340. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
| 28-Sep-2024 | nninfdcex 10674 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
| 27-Sep-2024 | infregelbex 10000 | 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 13343 |
Lemma for nninfdc 13346. Each element of the sequence |
| 26-Sep-2024 | nnminle 12814 | 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 12813. (Contributed by Jim Kingdon, 26-Sep-2024.) |
| 25-Sep-2024 | nninfdclemcl 13341 | Lemma for nninfdc 13346. (Contributed by Jim Kingdon, 25-Sep-2024.) |
| 24-Sep-2024 | nninfdclemlt 13344 | Lemma for nninfdc 13346. The function from nninfdclemf 13342 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
| 23-Sep-2024 | nninfdc 13346 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf1 13345 | Lemma for nninfdc 13346. The function from nninfdclemf 13342 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf 13342 |
Lemma for nninfdc 13346. A function from the natural numbers into
|
| 23-Sep-2024 | nnmindc 12813 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | breng 7029 | Equinumerosity relation. This variation of bren 7030 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 7030. (Revised by BTernaryTau, 23-Sep-2024.) |
| 23-Sep-2024 | dfnul3 3524 | Alternate definition of the empty set. (Contributed by NM, 25-Mar-2004.) (Proof shortened by BJ, 23-Sep-2024.) |
| 23-Sep-2024 | dfnul2 3523 | Alternate definition of the empty set. Definition 5.14 of [TakeutiZaring] p. 20. (Contributed by NM, 26-Dec-1996.) Reduce axiom dependencies. (Revised by Steven Nguyen, 3-May-2023.) (Proof shortened by BJ, 23-Sep-2024.) |
| 23-Sep-2024 | dfnul4 3522 | Alternate definition of the empty class/set. (Contributed by BJ, 30-Nov-2019.) Avoid ax-13 2211, df-clel 2234. (Revised by GG, 3-Sep-2024.) Prove directly from definition to allow shortening dfnul2 3523. (Revised by BJ, 23-Sep-2024.) |
| 20-Sep-2024 | ineqcomi 3423 |
Two ways of expressing that two classes have a given intersection.
Inference form of ineqcom 3422. Disjointness inference when |
| 19-Sep-2024 | ssomct 13338 |
A decidable subset of |
| 19-Sep-2024 | 2oex 6704 |
|
| 19-Sep-2024 | ecase2d 1392 | Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.) |
| 18-Sep-2024 | fcof 5894 | Composition of a function with domain and codomain and a function as a function with domain and codomain. Generalization of fco 5552. (Contributed by AV, 18-Sep-2024.) |
| 18-Sep-2024 | eqabbw 2375 | Version of eqabb 2374 using implicit substitution. (Contributed by GG and AV, 18-Sep-2024.) |
| 17-Sep-2024 | fncofn 5893 | Composition of a function with domain and a function as a function with domain. Generalization of fnco 5491. (Contributed by AV, 17-Sep-2024.) |
| 14-Sep-2024 | nnpredlt 4771 | The predecessor (see nnpredcl 4770) of a nonzero natural number is less than (see df-iord 4511) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
| 13-Sep-2024 | nninfisollemeq 7472 |
Lemma for nninfisol 7473. The case where |
| 13-Sep-2024 | nninfisollemne 7471 |
Lemma for nninfisol 7473. A case where |
| 13-Sep-2024 | nninfisollem0 7470 |
Lemma for nninfisol 7473. The case where |
| 13-Sep-2024 | fset0 6949 | The set of functions from the empty set is the singleton containing the empty set. (Contributed by AV, 13-Sep-2024.) |
| 13-Sep-2024 | fsetsspwxp 6948 |
The class of all functions from |
| 12-Sep-2024 | nninfisol 7473 |
Finite elements of ℕ∞ are isolated. That is, given a
natural
number and any element of ℕ∞, it is decidable
whether the
natural number (when converted to an element of
ℕ∞) is equal to
the given element of ℕ∞. Stated in an online
post by Martin
Escardo. One way to understand this theorem is that you do not need to
look at an unbounded number of elements of the sequence By contrast, the point at infinity being isolated is equivalent to the Weak Limited Principle of Omniscience (WLPO) (nninfinfwlpo 7520). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
| 8-Sep-2024 | relopabv 4904 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4906. (Contributed by SN, 8-Sep-2024.) |
| 7-Sep-2024 | eulerthlemfi 13008 |
Lemma for eulerth 13013. The set |
| 7-Sep-2024 | modqexp 11106 | 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 13011 |
Lemma for eulerth 13013. A permutation of |
| 2-Sep-2024 | eulerthlemth 13012 | Lemma for eulerth 13013. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlema 13010 | Lemma for eulerth 13013. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlemrprm 13009 |
Lemma for eulerth 13013. |
| 1-Sep-2024 | qusmul2 14868 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
| 30-Aug-2024 | fprodap0f 12405 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 12390 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 12398 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
| 26-Aug-2024 | exmidontri2or 7602 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | exmidontri 7598 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontri2orexmidim 4719 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4718. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontriexmidim 4669 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4668. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 25-Aug-2024 | onntri2or 7605 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | onntri3or 7604 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | csbcow 3158 | Composition law for chained substitutions into a class. Version of csbco 3157 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 2792 | Version of cbvreuv 2788 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvrexvw 2791 | Version of cbvrexv 2787 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvralvw 2790 | Version of cbvralv 2786 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvabw 2363 | Version of cbvab 2364 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfsbv 2007 |
If |
| 25-Aug-2024 | cbvexvw 1976 | Change bound variable. See cbvexv 1974 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1501. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvalvw 1975 | Change bound variable. See cbvalv 1973 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1501. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfal 1629 |
If |
| 24-Aug-2024 | gcdcomd 12753 |
The |
| 22-Aug-2024 | fsetdmprc0 6950 | The set of functions with a proper class as domain is empty. (Contributed by AV, 22-Aug-2024.) |
| 22-Aug-2024 | abanssr 3502 | A class abstraction with a conjunction is a subset of the class abstraction with the right conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
| 22-Aug-2024 | abanssl 3501 | A class abstraction with a conjunction is a subset of the class abstraction with the left conjunct only. (Contributed by AV, 7-Aug-2024.) (Proof shortened by SN, 22-Aug-2024.) |
| 21-Aug-2024 | dvds2addd 12598 | Deduction form of dvds2add 12594. (Contributed by SN, 21-Aug-2024.) |
| 20-Aug-2024 | rspcedvdw 2936 |
Version of rspcedvd 2935 where the implicit substitution hypothesis
does
not have an antecedent, which also avoids a disjoint variable condition
on |
| 18-Aug-2024 | prdsmulr 14180 | Multiplication in a structure product. (Contributed by Mario Carneiro, 11-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsplusg 14179 | Addition in a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsbas 14178 | Base set of a structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdssca 14177 | Scalar ring of a structure product. (Contributed by Stefan O'Rear, 5-Jan-2015.) (Revised by Mario Carneiro, 15-Aug-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | prdsval 14175 | Value of the structure product. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 7-Jan-2017.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 18-Aug-2024 | df-prds 14172 | Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.) (Revised by Zhi Wang, 18-Aug-2024.) |
| 17-Aug-2024 | fprodcl2lem 12374 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
| 16-Aug-2024 | fprodunsn 12373 |
Multiply in an additional term in a finite product. See also
fprodsplitsn 12402 which is the same but with a |
| 16-Aug-2024 | if0ab 3641 | 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. (Contributed by BJ, 16-Aug-2024.) |
| 15-Aug-2024 | bj-charfundcALT 16847 | Alternate proof of bj-charfundc 16846. It was expected to be much shorter since it uses bj-charfun 16845 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 16845 |
Properties of the characteristic function on the class |
| 15-Aug-2024 | cnstab 8974 |
Equality of complex numbers is stable. Stability here means
|
| 15-Aug-2024 | subap0d 8973 | 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 4630 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwun 4629 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwund 4628 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwung 4627 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifidss 3656 | 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 3655 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
| 14-Aug-2024 | hashf1lem1 11287 | Lemma for hashf1 11289. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.) |
| 14-Aug-2024 | f1setexg 6951 | The set of injections between two sets exists. (Contributed by AV, 14-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem2 7578 | Lemma for exmidontriim 7581. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem1 7577 | Lemma for exmidontriim 7581. A variation of r19.30dc 2698. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 11-Aug-2024 | nndc 863 |
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 7581 | 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 7580 |
Lemma for exmidontriim 7581. The induction step for the induction on
|
| 10-Aug-2024 | exmidontriimlem3 7579 |
Lemma for exmidontriim 7581. What we get to do based on induction on
both
|
| 10-Aug-2024 | nnnninf2 7467 |
Canonical embedding of |
| 10-Aug-2024 | infnninf 7464 |
The point at infinity in ℕ∞ is the constant sequence
equal to
|
| 10-Aug-2024 | mapssfsetg 6946 |
The value of the set exponentiation |
| 9-Aug-2024 | ss1o0el1o 7220 |
Reformulation of ss1o0el1 4334 using |
| 9-Aug-2024 | pw1dc0el 7218 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
| 9-Aug-2024 | ss1o0el1 4334 |
A subclass of |
| 8-Aug-2024 | pw1dc1 7221 | 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.) |
| 8-Aug-2024 | mapfset 6945 |
If |
| 8-Aug-2024 | fdmexb 5939 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| 8-Aug-2024 | fndmexb 5938 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| 7-Aug-2024 | psrbagaddclfi 15063 | The sum of two finite bags is a finite bag. (Contributed by Mario Carneiro, 9-Jan-2015.) Shorten proof and remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
| 7-Aug-2024 | psrbagfsupp 15057 | Finite bags have finite support. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 18-Jul-2019.) Remove a sethood antecedent. (Revised by SN, 7-Aug-2024.) |
| 7-Aug-2024 | pw1fin 7217 |
Excluded middle is equivalent to the power set of |
| 7-Aug-2024 | mapfoss 6947 |
The value of the set exponentiation |
| 7-Aug-2024 | elomssom 4752 | 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 4753. (Revised by BJ, 7-Aug-2024.) |
| 6-Aug-2024 | bj-charfunbi 16849 |
In an ambient set
This characterization can be applied to singletons when the set |
| 6-Aug-2024 | bj-charfunr 16848 |
If a class
The hypothesis imposes that
The theorem would still hold if the codomain of |
| 6-Aug-2024 | bj-charfundc 16846 |
Properties of the characteristic function on the class |
| 6-Aug-2024 | psrbagconf1o 15066 |
Bag complementation is a bijection on the set of bags dominated by a
given bag |
| 6-Aug-2024 | psrbagconcl 15065 | The complement of a bag is a bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 6-Aug-2024.) |
| 6-Aug-2024 | prodssdc 12358 | 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 16844 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | funmptd 16843 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5414, then prove funmptd 16843 from it, and then prove funmpt 5415 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dcfal 16795 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dctru 16793 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-stfal 16782 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-sttru 16780 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | psrbagcon 15064 |
The analogue of the statement " |
| 5-Aug-2024 | psrbaglecl 15062 | The set of finite bags is downward-closed. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
| 5-Aug-2024 | psrbaglesupp 15060 | The support of a dominated bag is smaller than the dominating bag. (Contributed by Mario Carneiro, 29-Dec-2014.) Remove a sethood antecedent. (Revised by SN, 5-Aug-2024.) |
| 5-Aug-2024 | prod1dc 12355 | 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 | fcdmnn0fsuppg 9620 |
Version of fcdmnn0fsupp 9618 avoiding ax-coll 4246 by assuming |
| 5-Aug-2024 | fcdmnn0suppg 9619 |
Version of fcdmnn0supp 9617 avoiding ax-coll 4246 by assuming |
| 5-Aug-2024 | 2ssom 6797 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | suppssdc 6500 | Show that the support of a function is contained in a set. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 28-May-2019.) (Proof shortened by SN, 5-Aug-2024.) |
| 5-Aug-2024 | elsuppfng 6482 |
An element of the support of a function with a given domain. This
version of elsuppfn 6483 assumes |
| 5-Aug-2024 | suppvalfng 6480 |
The value of the operation constructing the support of a function with a
given domain. This version of suppvalfn 6481 assumes |
| 4-Aug-2024 | en3d 7055 | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.) |
| 4-Aug-2024 | en2d 7054 | Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by AV, 4-Aug-2024.) |
| 2-Aug-2024 | onntri52 7603 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri24 7601 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri45 7600 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri51 7599 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri13 7597 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri35 7596 |
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 2540 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1702. (Contributed by Jim Kingdon, 1-Aug-2024.) |
| 31-Jul-2024 | 3nsssucpw1 7595 |
Negated excluded middle implies that |
| 31-Jul-2024 | sucpw1nss3 7594 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | psrbagf 15056 | 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 7593 |
Three is not an element of the successor of the power set of |
| 30-Jul-2024 | sucpw1nel3 7592 |
The successor of the power set of |
| 30-Jul-2024 | sucpw1ne3 7591 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | pw1nel3 7590 |
Negated excluded middle implies that the power set of |
| 30-Jul-2024 | pw1ne3 7589 |
The power set of |
| 30-Jul-2024 | pw1ne1 7588 |
The power set of |
| 30-Jul-2024 | pw1ne0 7587 |
The power set of |
| 30-Jul-2024 | fsuppeqg 6488 |
Version of fsuppeq 6487 avoiding ax-coll 4246 by assuming |
| 29-Jul-2024 | ringcld 14324 | Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.) |
| 29-Jul-2024 | grpcld 13821 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
| 29-Jul-2024 | pw1on 7585 |
The power set of |
| 29-Jul-2024 | isfsuppd 7290 | Deduction form of isfsupp 7289. (Contributed by SN, 29-Jul-2024.) |
| 28-Jul-2024 | exmidpweq 7216 |
Excluded middle is equivalent to the power set of |
| 27-Jul-2024 | dcapnconstALT 17124 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 17123 by means of dceqnconst 17122. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| 27-Jul-2024 | reap0 17120 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolemgt0 17126 | Lemma for nconstwlpo 17128. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolem0 17125 | Lemma for nconstwlpo 17128. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 26-Jul-2024 | fvmptd4 5800 |
Deduction version of fvmpt 5782 (where the substitution hypothesis does not
have the antecedent |
| 24-Jul-2024 | tridceq 17118 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 17104 and redcwlpo 17117). Thus, this is an analytic analogue to lpowlpo 7508. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 24-Jul-2024 | iswomni0 17113 |
Weak omniscience stated in terms of equality with |
| 24-Jul-2024 | asclmulg 15046 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| 24-Jul-2024 | lpowlpo 7508 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7507. There is an analogue in terms of analytic omniscience principles at tridceq 17118. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 23-Jul-2024 | nconstwlpolem 17127 | Lemma for nconstwlpo 17128. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | dceqnconst 17122 | 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 17117 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 17119 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | canth 6036 |
No set |
| 22-Jul-2024 | nconstwlpo 17128 |
Existence of a certain non-constant function from reals to integers
implies |
| 16-Jul-2024 | unexd 4892 | The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
| 16-Jul-2024 | difexd 4277 | Existence of a difference. (Contributed by SN, 16-Jul-2024.) |
| 15-Jul-2024 | fprodseq 12352 | 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 2555 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 14-Jul-2024 | ralbid2 2554 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 12-Jul-2024 | 2irrexpqap 16086 |
There exist real numbers |
| 12-Jul-2024 | 2logb9irrap 16085 | Example for logbgcd1irrap 16078. 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 13655 | 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 13654 | 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 13653 | Lemma for ercpbl 13654. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfvalg 13652 | Value of the function in qusval 13646. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfval 13651 | Value of the function in qusval 13646. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 11-Jul-2024 | logbgcd1irraplemexp 16076 |
Lemma for logbgcd1irrap 16078. Apartness of |
| 11-Jul-2024 | reapef 15881 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) |
| 10-Jul-2024 | apcxp2 16047 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) |
| 9-Jul-2024 | logbgcd1irraplemap 16077 | Lemma for logbgcd1irrap 16078. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 9-Jul-2024 | apexp1 11158 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 5-Jul-2024 | logrpap0 15982 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) |
| 3-Jul-2024 | rplogbval 16053 | 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 15983 | Deduction form of logrpap0 15982. (Contributed by Jim Kingdon, 3-Jul-2024.) |
| 3-Jul-2024 | logrpap0b 15981 | 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 17036 |
Mapping zero and one between |
| 28-Jun-2024 | 012of 17035 |
Mapping zero and one between |
| 27-Jun-2024 | iooreen 17096 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
| 27-Jun-2024 | iooref1o 17095 | 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 17129 | Lemma for neapmkv 17130. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnn 17115 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnnlem 17114 | Lemma for ismkvnn 17115. 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 7501 | Lemma for enmkv 7502. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 24-Jun-2024 | neapmkv 17130 | 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 17123 |
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 17104 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 17122 and in fact this theorem can be proved using dceqnconst 17122 as shown at dcapnconstALT 17124. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
| 24-Jun-2024 | enmkv 7502 |
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 17116 | Lemma for redcwlpo 17117. A biconditionalized version of trilpolemeq1 17101. (Contributed by Jim Kingdon, 21-Jun-2024.) |
| 20-Jun-2024 | redcwlpo 17117 |
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 17116). 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 10681 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | iswomninn 17112 |
Weak omniscience stated in terms of natural numbers. Similar to
iswomnimap 7506 but it will sometimes be more convenient to
use |
| 20-Jun-2024 | iswomninnlem 17111 | Lemma for iswomnimap 7506. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | enwomni 7510 |
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 7509 | Lemma for enwomni 7510. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 19-Jun-2024 | rpabscxpbnd 16048 | 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 16030 |
The exponential function with exponent |
| 16-Jun-2024 | biadanid 622 | Deduction associated with biadani 620. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| 13-Jun-2024 | rpcxpadd 16013 | 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 16012 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcncxpcl 16010 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcxp0 16006 | 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 16004 | 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 16003 | 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 16002 | 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 15963 | Define the power function on complex numbers. Because df-relog 15962 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 17106 |
Version of trirec0 17105 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 17105 |
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 17104). (Contributed by Jim Kingdon, 10-Jun-2024.) |
| 9-Jun-2024 | omniwomnimkv 7507 |
A set is omniscient if and only if it is weakly omniscient and Markov.
The case |
| 9-Jun-2024 | iswomnimap 7506 | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | iswomni 7505 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | df-womni 7504 |
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 14342 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ringabld 14341 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | cmnmndd 14113 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ablcmnd 14097 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | grpmndd 13820 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | fndmi 5481 | The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.) |
| 29-May-2024 | pw1nct 17045 | 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 17044 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
| 28-May-2024 | fvun2d 5772 | The value of a union when the argument is in the second domain, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| 28-May-2024 | fvun1d 5771 | The value of a union when the argument is in the first domain, a deduction version. (Contributed by metakunt, 28-May-2024.) |
| 26-May-2024 | elpwi2 4294 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
| 25-May-2024 | mplnegfi 15098 | The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.) |
| 24-May-2024 | dvmptcjx 15827 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) |
| 23-May-2024 | cbvralfw 2775 | Rule used to change bound variables, using implicit substitution. Version of cbvralf 2777 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 1560 and ax-bndl 1562 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.) |
| 23-May-2024 | cbvrmow 2735 | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 2785 with a disjoint variable condition. (Contributed by NM, 16-Jun-2017.) (Revised by GG, 23-May-2024.) |
| 23-May-2024 | cbvmow 2127 | Rule used to change bound variables, using implicit substitution. Version of cbvmo 2126 with a disjoint variable condition. (Contributed by NM, 9-Mar-1995.) (Revised by GG, 23-May-2024.) |
| 22-May-2024 | efltlemlt 15877 | Lemma for eflt 15878. The converse of efltim 12467 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) |
| 21-May-2024 | eflt 15878 | The exponential function on the reals is strictly increasing. (Contributed by Paul Chapman, 21-Aug-2007.) (Revised by Jim Kingdon, 21-May-2024.) |
| 20-May-2024 | nsyl5 659 | A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.) |
| 19-May-2024 | apdifflemr 17108 | Lemma for apdiff 17109. (Contributed by Jim Kingdon, 19-May-2024.) |
| 18-May-2024 | apdifflemf 17107 |
Lemma for apdiff 17109. Being apart from the point halfway between
|
| 17-May-2024 | apdiff 17109 | 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 14635 | A left module is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | drnggrpd 14614 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | drngringd 14613 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crnggrpd 14316 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crngringd 14315 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | ringgrpd 14311 | A ring is a group. (Contributed by SN, 16-May-2024.) |
| 15-May-2024 | reeff1oleme 15875 | Lemma for reeff1o 15876. (Contributed by Jim Kingdon, 15-May-2024.) |
| 14-May-2024 | df-relog 15962 | 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 6225 | Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.) |
| 13-May-2024 | fndmexd 5581 | If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
| 12-May-2024 | dvdstrd 12599 | The divides relation is transitive, a deduction version of dvdstr 12597. (Contributed by metakunt, 12-May-2024.) |
| 7-May-2024 | ioocosf1o 15958 | 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 15956 |
Cosine is between minus one and one on the open interval between zero and
|
| 6-May-2024 | cos11 15957 |
Cosine is one-to-one over the closed interval from |
| 5-May-2024 | omiunct 13337 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 13333 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
| 5-May-2024 | ctiunctal 13334 |
Variation of ctiunct 13333 which allows |
| 5-May-2024 | suppssrgst 6502 |
A function is zero outside its support. Version of suppssrst 6501 avoiding
ax-coll 4246 by assuming |
| 5-May-2024 | ifpnst 1001 | Conditional operator for the negation of a proposition. (Contributed by BJ, 30-Sep-2019.) (Proof shortened by Wolf Lammen, 5-May-2024.) |
| 3-May-2024 | cc4n 7637 |
Countable choice with a simpler restriction on how every set in the
countable collection needs to be inhabited. That is, compared with
cc4 7636, the hypotheses only require an A(n) for each
value of |
| 3-May-2024 | cc4f 7635 |
Countable choice by showing the existence of a function |
| 1-May-2024 | cc4 7636 |
Countable choice by showing the existence of a function |
| 30-Apr-2024 | ifpdfbidc 998 | Define the biconditional as conditional logic operator. (Contributed by RP, 20-Apr-2020.) (Proof shortened by Wolf Lammen, 30-Apr-2024.) |
| 29-Apr-2024 | cc3 7634 | Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.) |
| 28-Apr-2024 | ifpbi23d 1006 | Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.) |
| 27-Apr-2024 | cc2 7633 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc2lem 7632 | Lemma for cc2 7633. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc1 7631 | 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 14771 | 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 13336 | 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.) |
| 17-Apr-2024 | ifpbi123d 1005 | Equivalence deduction for conditional operator for propositions. (Contributed by AV, 30-Dec-2020.) (Proof shortened by Wolf Lammen, 17-Apr-2024.) |
| 13-Apr-2024 | prodmodclem2 12346 | Lemma for prodmodc 12347. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) |
| 13-Apr-2024 | sspwd 3704 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
| 13-Apr-2024 | sspwi 3703 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
| 13-Apr-2024 | sspw 3702 | The powerclass preserves inclusion. See sspwb 4356 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 4356 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
| Copyright terms: Public domain | W3C HTML validation [external] |