|
|
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 | ||
| 8-Jun-2026 | ballotfilemdifcfi 13152 |
Lemma for ballotfi . The portion of an integer range which is not
part of a particular element of |
| 8-Jun-2026 | ballotfilemcinfi 13151 |
Lemma for ballotfi . The portion of a particular element of |
| 8-Jun-2026 | zfidc 9661 | 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 13150 |
Lemma for ballotfi . It is decidable whether a given integer is an
element of a particular element of |
| 5-Jun-2026 | hashpwfi 11201 | 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 7273. For the number of subsets (which need not be finite) of a set, see pw1mapen 16819. (Contributed by Jim Kingdon, 5-Jun-2026.) |
| 4-Jun-2026 | ballotfilemonn 13148 | The size of the universe is at least one. (Contributed by Jim Kingdon, 4-Jun-2026.) |
| 3-Jun-2026 | papeq2 7563 | Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.) |
| 3-Jun-2026 | papeq1 7562 | Equality theorem for apartness predicate. (Contributed by Jim Kingdon, 3-Jun-2026.) |
| 2-Jun-2026 | resq01 11027 | If a real number equals its square, it must be 0 or 1. (Contributed by Jim Kingdon, 2-Jun-2026.) |
| 31-May-2026 | aprprop 14461 | If two structures have the same ring components (properties), df-apr 14450 generates the same relation for both of them. (Contributed by Jim Kingdon, 31-May-2026.) |
| 31-May-2026 | ringunitsap0 14454 |
The set of units of a ring. If |
| 30-May-2026 | ringunitap 14453 | Elementhood in the set of units. (Contributed by Jim Kingdon, 30-May-2026.) |
| 29-May-2026 | drnglring 14467 | A division ring is a local ring. (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | isdrngtap 14466 | The predicate "is a division ring". (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | df-drngap 14464 | Define class of all division rings. A division ring is a ring in which the relation given by df-apr 14450 is a tight apartness. (Contributed by Jim Kingdon, 29-May-2026.) |
| 29-May-2026 | aprunit 14452 | The df-apr 14450 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 7569 | A tight apartness is an apartness. (Contributed by Jim Kingdon, 29-May-2026.) |
| 28-May-2026 | aprlring 14460 | A ring is a local ring if and only if the relation given by df-apr 14450 is an apartness relation. (Contributed by Jim Kingdon, 28-May-2026.) |
| 28-May-2026 | papcotr 7566 | An apartness is cotransitive. (Contributed by Jim Kingdon, 28-May-2026.) |
| 27-May-2026 | trimul0or 16894 | Real number trichotomy implies that if a product is zero, one of its factors must be zero. (Contributed by Jim Kingdon, 27-May-2026.) |
| 27-May-2026 | aprnzr 14459 | If the relation given by df-apr 14450 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 7565 | An apartness is symmetric. (Contributed by Jim Kingdon, 27-May-2026.) |
| 27-May-2026 | papirr 7564 | An apartness is irreflexive. (Contributed by Jim Kingdon, 27-May-2026.) |
| 24-May-2026 | gfsumz 16918 | Value of a finite group sum over the zero element. (Contributed by Jim Kingdon, 24-May-2026.) |
| 22-May-2026 | sshashneg 11213 |
Subsets of a class of a negative size (a degenerate case). Together
with ssenneg 11212 this shows that sseqn 11211 could not be extended beyond
|
| 22-May-2026 | ssenneg 11212 |
Subsets of a class of a negative size (a degenerate case). Together
with sshashneg 11213 this shows that sseqn 11211 could not be extended beyond
|
| 22-May-2026 | sseqn 11211 |
Two ways to express the subsets of a class of a given size. It might
seem that |
| 20-May-2026 | ballotfilemofi 13146 |
|
| 19-May-2026 | fipwfi 7274 | The set of finite subsets of a finite set is finite. (Contributed by Jim Kingdon, 19-May-2026.) |
| 18-May-2026 | 2omapfi 7273 | The number of finite subsets of a finite set. For a similar theorem with set size expressed using ♯ (df-ihash 11147), see hashpwfi 11201. (Contributed by Jim Kingdon, 18-May-2026.) |
| 18-May-2026 | fissfi 7218 | A finite subset of a finite set is a decidable subset. (Contributed by Jim Kingdon, 18-May-2026.) |
| 18-May-2026 | fresaunres1disj 5548 | 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 5547 | 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 7256 |
The composition of a 1-1 function with a finitely supported function is
finitely supported. The purpose of the |
| 13-May-2026 | lincmble 10343 |
A linear combination of two reals which lies in the interval between them.
Like lincmb01cmp 10342 but generalized to require merely |
| 5-May-2026 | fmelpw1o 7559 |
With a formula
As proved in if0ab 3625, the associated element of |
| 5-May-2026 | if0elpw 4273 | 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 4604. (Contributed by BJ, 5-May-2026.) |
| 5-May-2026 | if0ss 3626 | 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 16861 |
Piecewise definition on the reals yields a function. The function
agrees with |
| 27-Apr-2026 | repiecege0 16860 | Piecewise definition on the reals agrees with the nonnegative part of the definition. See repiecef 16861 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.) |
| 27-Apr-2026 | repiecele0 16859 | Piecewise definition on the reals agrees with the nonpositive part of the definition. See repiecef 16861 for more on this construction. (Contributed by Jim Kingdon, 27-Apr-2026.) |
| 27-Apr-2026 | repiecelem 16858 |
Lemma for repiecele0 16859, repiecege0 16860, and repiecef 16861. The function
|
| 24-Apr-2026 | qdiff 16882 | 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 16881 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 16830 |
Excluded middle is equivalent to Peirce's law. Read an element of
|
| 22-Apr-2026 | exmidcon 16829 |
Excluded middle is equivalent to the form of contraposition which
removes negation. Read an element of |
| 22-Apr-2026 | exmidnotnotr 16828 |
Excluded middle is equivalent to double negation elimination. Read an
element of |
| 18-Apr-2026 | hashtpglem 11226 | Lemma for hashtpg 11227. 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 11225 | 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 16553 | Theorem related to a dependently typed induction principle in type theory. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem3 16552 | Lemma for depind 16553. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem2 16551 | Lemma for depind 16553. (Contributed by Matthew House, 14-Apr-2026.) |
| 14-Apr-2026 | depindlem1 16550 | Lemma for depind 16553. (Contributed by Matthew House, 14-Apr-2026.) |
| 8-Apr-2026 | gfsumcl 16919 | Closure of a finite group sum. (Contributed by Jim Kingdon, 8-Apr-2026.) |
| 4-Apr-2026 | gsumsplit0 14084 |
Splitting off the rightmost summand of a group sum (even if it is the
only summand). Similar to gsumsplit1r 13632 except that |
| 4-Apr-2026 | fzf1o 12069 | A finite set can be enumerated by integers starting at one. (Contributed by Jim Kingdon, 4-Apr-2026.) |
| 3-Apr-2026 | gfsump1 16917 | 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 | gfsumsn 16916 | Group sum of a singleton. (Contributed by Jim Kingdon, 2-Apr-2026.) |
| 31-Mar-2026 | sspw1or2 7497 | 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 7195 | The image of a finite set under a one-to-one mapping is finite. (Contributed by Jim Kingdon, 28-Mar-2026.) |
| 26-Mar-2026 | gsumgfsumlem 16914 | Shifting the indexes of a group sum indexed by consecutive integers. (Contributed by Jim Kingdon, 26-Mar-2026.) |
| 26-Mar-2026 | gfsum0 16913 | An empty finite group sum is the identity. (Contributed by Jim Kingdon, 26-Mar-2026.) |
| 25-Mar-2026 | gsumgfsum 16915 |
On an integer range, |
| 25-Mar-2026 | gsumgfsum1 16912 |
On an integer range starting at one, |
| 24-Mar-2026 | gfsumval 16911 | Value of the finite group sum over an unordered finite set. (Contributed by Jim Kingdon, 24-Mar-2026.) |
| 23-Mar-2026 | df-gfsum 16910 | Define the finite group sum (iterated sum) over an unordered finite set. As currently defined, df-igsum 13493 is indexed by consecutive integers, but in the case of a commutative monoid, the order of the sum doesn't matter and we can define a sum indexed by any finite set without needing to specify an order. (Contributed by Jim Kingdon, 23-Mar-2026.) |
| 20-Mar-2026 | exmidssfi 7201 | 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 16169 | A graph with one non-loop edge is a multigraph. (Contributed by Jim Kingdon, 18-Mar-2026.) |
| 18-Mar-2026 | upgr1een 16168 | A graph with one non-loop edge is a pseudograph. Variation of upgr1edc 16165 for a different way of specifying a graph with one edge. (Contributed by Jim Kingdon, 18-Mar-2026.) |
| 14-Mar-2026 | trlsex 16431 | The class of trails on a graph is a set. (Contributed by Jim Kingdon, 14-Mar-2026.) |
| 13-Mar-2026 | eupthv 16490 | The classes involved in a Eulerian path are sets. (Contributed by Jim Kingdon, 13-Mar-2026.) |
| 13-Mar-2026 | 1hevtxdg0fi 16351 |
The vertex degree of vertex |
| 11-Mar-2026 | en1hash 11171 | A set equinumerous to the ordinal one has size 1 . (Contributed by Jim Kingdon, 11-Mar-2026.) |
| 4-Mar-2026 | elmpom 6436 | 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 16451 | 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 16442 | Existence of the set of closed walks (represented by words). (Contributed by Jim Kingdon, 21-Feb-2026.) |
| 17-Feb-2026 | vtxdgfif 16337 | 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 16334 | 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 16333 | 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 7165 | 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 16814 |
The powerset of |
| 14-Feb-2026 | pw1ndom3 16813 |
The powerset of |
| 14-Feb-2026 | pw1ndom3lem 16812 | Lemma for pw1ndom3 16813. (Contributed by Jim Kingdon, 14-Feb-2026.) |
| 12-Feb-2026 | pw1dceq 16827 |
The powerset of |
| 12-Feb-2026 | 3dom 16811 | A set that dominates ordinal 3 has at least 3 different members. (Contributed by Jim Kingdon, 12-Feb-2026.) |
| 11-Feb-2026 | elssdc 7164 | Membership in a finite subset of a set with decidable equality is decidable. (Contributed by Jim Kingdon, 11-Feb-2026.) |
| 10-Feb-2026 | vtxdgfifival 16335 | The degree of a vertex for graphs with finite vertex and edge sets. (Contributed by Jim Kingdon, 10-Feb-2026.) |
| 10-Feb-2026 | fidcen 7158 | Equinumerosity of finite sets is decidable. (Contributed by Jim Kingdon, 10-Feb-2026.) |
| 8-Feb-2026 | wlkvtxm 16384 | A graph with a walk has at least one vertex. (Contributed by Jim Kingdon, 8-Feb-2026.) |
| 7-Feb-2026 | trlsv 16428 | The classes involved in a trail are sets. (Contributed by Jim Kingdon, 7-Feb-2026.) |
| 7-Feb-2026 | wlkex 16369 | The class of walks on a graph is a set. (Contributed by Jim Kingdon, 7-Feb-2026.) |
| 3-Feb-2026 | dom1oi 7072 | A set with an element dominates one. (Contributed by Jim Kingdon, 3-Feb-2026.) |
| 2-Feb-2026 | edginwlkd 16399 | 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 16393 | A walk is an ordered pair. (Contributed by Jim Kingdon, 2-Feb-2026.) |
| 1-Feb-2026 | wlkcprim 16394 | 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 16363 | If there are walks on a graph, the graph is a set. (Contributed by Jim Kingdon, 1-Feb-2026.) |
| 31-Jan-2026 | fvmbr 5707 | 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 5706 | If a function value is inhabited, the function value is a set. (Contributed by Jim Kingdon, 30-Jan-2026.) |
| 30-Jan-2026 | reldmm 4977 | A relation is inhabited iff its domain is inhabited. (Contributed by Jim Kingdon, 30-Jan-2026.) |
| 25-Jan-2026 | ifp2 989 | Forward direction of dfifp2dc 990. This direction does not require decidability. (Contributed by Jim Kingdon, 25-Jan-2026.) |
| 25-Jan-2026 | ifpdc 988 | The conditional operator for propositions implies decidability. (Contributed by Jim Kingdon, 25-Jan-2026.) |
| 20-Jan-2026 | cats1fvd 11466 | 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 11465 | 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 11469 | 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 11468 | 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 11467 | 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 2650 | 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 16199 |
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 7492 | 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 16819 |
Equinumerosity of |
| 10-Jan-2026 | pw1if 7537 |
Expressing a truth value in terms of an |
| 10-Jan-2026 | pw1m 7536 | A truth value which is inhabited is equal to true. This is a variation of pwntru 4314 and pwtrufal 16820. (Contributed by Jim Kingdon, 10-Jan-2026.) |
| 10-Jan-2026 | 1ndom2 7121 | Two is not dominated by one. (Contributed by Jim Kingdon, 10-Jan-2026.) |
| 9-Jan-2026 | pw1map 16818 |
Mapping between |
| 9-Jan-2026 | iftrueb01 7535 |
Using an |
| 8-Jan-2026 | pfxclz 11379 |
Closure of the prefix extractor. This extends pfxclg 11378 from |
| 8-Jan-2026 | fnpfx 11377 | The domain of the prefix extractor. (Contributed by Jim Kingdon, 8-Jan-2026.) |
| 7-Jan-2026 | pr1or2 7493 | 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 16164 | Lemma for upgr1edc 16165. (Contributed by AV, 16-Oct-2020.) (Revised by Jim Kingdon, 6-Jan-2026.) |
| 3-Jan-2026 | df-umgren 16138 |
Define the class of all undirected multigraphs. An (undirected)
multigraph consists of a set |
| 3-Jan-2026 | df-upgren 16137 |
Define the class of all undirected pseudographs. An (undirected)
pseudograph consists of a set |
| 3-Jan-2026 | dom1o 7071 | Two ways of saying that a set is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 3-Jan-2026 | en2m 7068 | A set with two elements is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 3-Jan-2026 | en1m 7047 | A set with one element is inhabited. (Contributed by Jim Kingdon, 3-Jan-2026.) |
| 31-Dec-2025 | pw0ss 16127 | There are no inhabited subsets of the empty set. (Contributed by Jim Kingdon, 31-Dec-2025.) |
| 31-Dec-2025 | df-ushgrm 16114 |
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 16113 |
Define the class of all undirected hypergraphs. An undirected
hypergraph consists of a set |
| 29-Dec-2025 | iedgex 16063 | Applying the indexed edge function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | vtxex 16062 | Applying the vertex function yields a set. (Contributed by Jim Kingdon, 29-Dec-2025.) |
| 29-Dec-2025 | snmb 3815 | 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 11284 | Existence of the last symbol. The last symbol of a word is a set. See lsw0g 11281 or lswcl 11283 if you want more specific results for empty or nonempty words, respectively. (Contributed by Jim Kingdon, 27-Dec-2025.) |
| 23-Dec-2025 | fzowrddc 11347 | 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 11290 | 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 11279 | 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 13352 | 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 16076 | 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 16075 | 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 16074 | 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 16073 | 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 11223 | Two equivalent ways to say a set has two elements. (Contributed by Jim Kingdon, 4-Dec-2025.) |
| 30-Nov-2025 | nninfnfiinf 16850 | An element of ℕ∞ which is not finite is infinite. (Contributed by Jim Kingdon, 30-Nov-2025.) |
| 30-Nov-2025 | eluz3nn 9905 | 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 14880 | Simpler form of psrelbas 14879 when the index set is finite. (Contributed by Jim Kingdon, 27-Nov-2025.) |
| 26-Nov-2025 | mplsubgfileminv 14904 | Lemma for mplsubgfi 14905. The additive inverse of a polynomial is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 26-Nov-2025 | mplsubgfilemcl 14903 | Lemma for mplsubgfi 14905. The sum of two polynomials is a polynomial. (Contributed by Jim Kingdon, 26-Nov-2025.) |
| 25-Nov-2025 | nninfinfwlpo 7473 | 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 7426). (Contributed by Jim Kingdon, 25-Nov-2025.) |
| 23-Nov-2025 | psrbagfi 14872 | A finite index set gives a simpler expression for finite bags. (Contributed by Jim Kingdon, 23-Nov-2025.) |
| 22-Nov-2025 | df-acnm 7478 |
Define a local and length-limited version of the axiom of choice. The
definition of the predicate |
| 21-Nov-2025 | mplsubgfilemm 14902 | Lemma for mplsubgfi 14905. There exists a polynomial. (Contributed by Jim Kingdon, 21-Nov-2025.) |
| 15-Nov-2025 | uzuzle35 9903 | 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 7272 |
Equinumerosity of |
| 12-Nov-2025 | 2omap 7271 |
Mapping between |
| 11-Nov-2025 | domomsubct 16824 |
A set dominated by |
| 10-Nov-2025 | prdsbaslemss 13508 | Lemma for prdsbas 13510 and similar theorems. (Contributed by Jim Kingdon, 10-Nov-2025.) |
| 5-Nov-2025 | fnmpl 14897 | mPoly has universal domain. (Contributed by Jim Kingdon, 5-Nov-2025.) |
| 4-Nov-2025 | mplelbascoe 14896 | 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 14895 | 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 14894 | 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 7487 | The cardinal number of a finite set is an ordinal. (Contributed by Jim Kingdon, 1-Nov-2025.) |
| 31-Oct-2025 | bitsdc 12641 | Whether a bit is set is decidable. (Contributed by Jim Kingdon, 31-Oct-2025.) |
| 28-Oct-2025 | nn0maxcl 11918 | The maximum of two nonnegative integers is a nonnegative integer. (Contributed by Jim Kingdon, 28-Oct-2025.) |
| 28-Oct-2025 | qdcle 10613 |
Rational |
| 17-Oct-2025 | plycoeid3 15671 | 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 7192 | 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 7190 | 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 3621 | 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 12944 | A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.) |
| 7-Oct-2025 | df-mplcoe 14861 |
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 15612 | Derivative of a constant function defined on an open set. (Contributed by Jim Kingdon, 6-Oct-2025.) |
| 6-Oct-2025 | dcfrompeirce 1495 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromcon 1494 |
The decidability of a proposition |
| 6-Oct-2025 | dcfromnotnotr 1493 |
The decidability of a proposition |
| 3-Oct-2025 | dvidre 15611 | Real derivative of the identity function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvconstre 15610 | Real derivative of a constant function. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 3-Oct-2025 | dvidsslem 15607 |
Lemma for dvconstss 15612. Analogue of dvidlemap 15605 where |
| 3-Oct-2025 | dvidrelem 15606 | Lemma for dvidre 15611 and dvconstre 15610. Analogue of dvidlemap 15605 for real numbers rather than complex numbers. (Contributed by Jim Kingdon, 3-Oct-2025.) |
| 28-Sep-2025 | metuex 14752 | Applying metUnif yields a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 28-Sep-2025 | cndsex 14750 | The standard distance function on the complex numbers is a set. (Contributed by Jim Kingdon, 28-Sep-2025.) |
| 25-Sep-2025 | cntopex 14751 | The standard topology on the complex numbers is a set. (Contributed by Jim Kingdon, 25-Sep-2025.) |
| 24-Sep-2025 | mopnset 14749 |
Getting a set by applying |
| 24-Sep-2025 | blfn 14748 | The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.) |
| 23-Sep-2025 | elfzoext 10544 | 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 15674 | Lemma for plycj 15675. (Contributed by Mario Carneiro, 24-Jul-2014.) (Revised by Jim Kingdon, 22-Sep-2025.) |
| 20-Sep-2025 | plycolemc 15672 |
Lemma for plyco 15673. The result expressed as a sum, with a
degree and
coefficients for |
| 18-Sep-2025 | elfzoextl 10543 | 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 15998 |
Lemma for lgsquad 16002. There are finitely many members of |
| 16-Sep-2025 | lgsquadlemsfi 15997 |
Lemma for lgsquad 16002. |
| 16-Sep-2025 | opabfi 7202 | 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 6333 |
Principle of unique choice. This is also called non-choice. The name
choice results in its similarity to something like acfun 7516 (with the key
difference being the change of |
| 11-Sep-2025 | expghmap 14804 | 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 14786 | The invertible complex numbers are exactly those apart from zero. This is recapb 8950 but expressed in terms of ℂfld. (Contributed by Jim Kingdon, 11-Sep-2025.) |
| 9-Sep-2025 | gsumfzfsumlemm 14784 | Lemma for gsumfzfsum 14785. The case where the sum is inhabited. (Contributed by Jim Kingdon, 9-Sep-2025.) |
| 9-Sep-2025 | gsumfzfsumlem0 14783 | Lemma for gsumfzfsum 14785. The case where the sum is empty. (Contributed by Jim Kingdon, 9-Sep-2025.) |
| 9-Sep-2025 | gsumfzmhm2 14082 | Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) (Revised by Jim Kingdon, 9-Sep-2025.) |
| 8-Sep-2025 | gsumfzmhm 14081 | 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 12629 | 5 does not divide 6. (Contributed by AV, 8-Sep-2025.) |
| 8-Sep-2025 | 5ndvds3 12628 | 5 does not divide 3. (Contributed by AV, 8-Sep-2025.) |
| 7-Sep-2025 | 5eluz3 9899 | 5 is an integer greater than or equal to 3. (Contributed by AV, 7-Sep-2025.) |
| 6-Sep-2025 | gsumfzconst 14079 | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Jim Kingdon, 6-Sep-2025.) |
| 5-Sep-2025 | uzuzle34 9902 | An integer greater than or equal to 4 is an integer greater than or equal to 3. (Contributed by AV, 5-Sep-2025.) |
| 31-Aug-2025 | gsumfzmptfidmadd 14077 | The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) (Revised by Jim Kingdon, 31-Aug-2025.) |
| 30-Aug-2025 | gsumfzsubmcl 14076 | 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 10843 | 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 10890 |
Rearrange a sum via an arbitrary bijection on |
| 25-Aug-2025 | irrmulap 9986 | 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 9985. (Contributed by Jim Kingdon, 25-Aug-2025.) |
| 19-Aug-2025 | seqp1g 10835 | 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 10832 | 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 11239 | A zero-based sequence is a word. In iswrdinn0 11237 we can specify a length as an nonnegative integer. However, it will occasionally be helpful to allow a negative length, as well as zero, to specify an empty sequence. (Contributed by Jim Kingdon, 18-Aug-2025.) |
| 16-Aug-2025 | gsumfzcl 13733 | Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.) |
| 16-Aug-2025 | iswrdinn0 11237 | A zero-based sequence is a word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 26-Feb-2016.) (Revised by Jim Kingdon, 16-Aug-2025.) |
| 15-Aug-2025 | gsumfzz 13729 | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.) |
| 14-Aug-2025 | gsumfzval 13625 |
An expression for |
| 13-Aug-2025 | znidom 14854 |
The ℤ/nℤ structure is an integral domain when |
| 12-Aug-2025 | rrgmex 14429 | A structure whose set of left-regular elements is inhabited is a set. (Contributed by Jim Kingdon, 12-Aug-2025.) |
| 10-Aug-2025 | gausslemma2dlem1cl 15981 |
Lemma for gausslemma2dlem1 15983. Closure of the body of the
definition
of |
| 9-Aug-2025 | gausslemma2dlem1f1o 15982 | Lemma for gausslemma2dlem1 15983. (Contributed by Jim Kingdon, 9-Aug-2025.) |
| 7-Aug-2025 | qdclt 10612 |
Rational |
| 22-Jul-2025 | ivthdich 15567 |
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 15557 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 15566 | 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 15565 | Lemma for ivthdich 15567. The result, with a few notational conveniences. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hovergt0 15564 | The hover function evaluated at a point greater than zero. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 22-Jul-2025 | hoverlt1 15563 | The hover function evaluated at a point less than one. (Contributed by Jim Kingdon, 22-Jul-2025.) |
| 21-Jul-2025 | hoverb 15562 | A point at which the hover function is greater than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | hovera 15561 | A point at which the hover function is less than a given value. (Contributed by Jim Kingdon, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrrdv 2754 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrrdv 2753 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | rexeqtrdv 2752 | Substitution of equal classes into a restricted existential quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 21-Jul-2025 | raleqtrdv 2751 | Substitution of equal classes into a restricted universal quantifier. (Contributed by Matthew House, 21-Jul-2025.) |
| 20-Jul-2025 | hovercncf 15560 | 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 15530 | The minimum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 19-Jul-2025.) |
| 18-Jul-2025 | maxcncf 15529 | The maximum of two continuous real functions is continuous. (Contributed by Jim Kingdon, 18-Jul-2025.) |
| 14-Jul-2025 | xnn0nnen 10806 | 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 7416 | 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 12744 | Lemma for nninfct 12745. (Contributed by Jim Kingdon, 10-Jul-2025.) |
| 8-Jul-2025 | nnnninfen 16848 | 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 12745 | The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 8-Jul-2025 | nninfinf 10812 | ℕ∞ is infinte. (Contributed by Jim Kingdon, 8-Jul-2025.) |
| 7-Jul-2025 | ivthreinc 15559 |
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 15557).
Being able to have a hypothesis stating the intermediate value theorem
will be helpful when it comes time to show that it implies a
constructive taboo. This version of the theorem requires that the
function |
| 28-Jun-2025 | fngsum 13622 | Iterated sum has a universal domain. (Contributed by Jim Kingdon, 28-Jun-2025.) |
| 28-Jun-2025 | iotaexel 6010 | Set existence of an iota expression in which all values are contained within a set. (Contributed by Jim Kingdon, 28-Jun-2025.) |
| 27-Jun-2025 | df-igsum 13493 |
Define a finite group sum (also called "iterated sum") of a
structure.
Given
1. If
2. If 3. This definition does not handle other cases. (Contributed by FL, 5-Sep-2010.) (Revised by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 27-Jun-2025.) |
| 20-Jun-2025 | opprnzrbg 14352 | The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14353. (Contributed by SN, 20-Jun-2025.) |
| 16-Jun-2025 | fnpsr 14864 | The multivariate power series constructor has a universal domain. (Contributed by Jim Kingdon, 16-Jun-2025.) |
| 14-Jun-2025 | basm 13295 | A structure whose base is inhabited is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 14-Jun-2025 | elfvm 5705 | If a function value has a member, the function is inhabited. (Contributed by Jim Kingdon, 14-Jun-2025.) |
| 6-Jun-2025 | pcxqcl 13018 | The general prime count function is an integer or infinite. (Contributed by Jim Kingdon, 6-Jun-2025.) |
| 5-Jun-2025 | xqltnle 10634 |
"Less than" expressed in terms of "less than or equal to",
for extended
numbers which are rational or |
| 5-Jun-2025 | ceqsexv2d 2856 | 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 2889 | 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 13105 | Exercise which may help in understanding the proof of 4sqlemsdc 13106. (Contributed by Jim Kingdon, 30-May-2025.) |
| 27-May-2025 | iotaexab 5333 |
Existence of the |
| 25-May-2025 | 4sqlemsdc 13106 |
Lemma for 4sq 13116. The property of being the sum of four
squares is
decidable.
The proof involves showing that (for a particular |
| 25-May-2025 | 4sqexercise1 13104 | Exercise which may help in understanding the proof of 4sqlemsdc 13106. (Contributed by Jim Kingdon, 25-May-2025.) |
| 24-May-2025 | 4sqleminfi 13103 |
Lemma for 4sq 13116. |
| 24-May-2025 | 4sqlemffi 13102 |
Lemma for 4sq 13116. |
| 24-May-2025 | 4sqlemafi 13101 |
Lemma for 4sq 13116. |
| 24-May-2025 | infidc 7203 | 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 14818 |
Set existence for |
| 16-May-2025 | rhmex 14324 | Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.) |
| 15-May-2025 | ghmex 13993 | The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 15-May-2025 | mhmex 13696 | The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.) |
| 14-May-2025 | idomcringd 14447 | 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 14437 | 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 14119 | 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 13305. (Contributed by Jim Kingdon, 5-May-2025.) |
| 5-May-2025 | ablressid 14073 | 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 13305. (Contributed by Jim Kingdon, 5-May-2025.) |
| 30-Apr-2025 | dvply2g 15680 | 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 14657 | Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 29-Apr-2025 | ressbasid 13304 | The trivial structure restriction leaves the base set unchanged. (Contributed by Jim Kingdon, 29-Apr-2025.) |
| 28-Apr-2025 | lssmex 14552 | 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 14761 | 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 14759 | 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 14670 | Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 27-Apr-2025 | lssex 14551 | Existence of a linear subspace. (Contributed by Jim Kingdon, 27-Apr-2025.) |
| 25-Apr-2025 | rspex 14671 | Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | lspex 14592 | Existence of the span of a set of vectors. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | eqgex 13959 | The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 25-Apr-2025 | qusex 13559 | Existence of a quotient structure. (Contributed by Jim Kingdon, 25-Apr-2025.) |
| 23-Apr-2025 | 1dom1el 7062 | 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 13861 | Existence of the group multiple operation. (Contributed by Jim Kingdon, 22-Apr-2025.) |
| 21-Apr-2025 | uspgruhgr 16231 | An undirected simple pseudograph is an undirected hypergraph. (Contributed by AV, 21-Apr-2025.) |
| 20-Apr-2025 | uspgriedgedg 16223 | In a simple pseudograph, for each indexed edge there is exactly one edge. (Contributed by AV, 20-Apr-2025.) |
| 20-Apr-2025 | uspgredgiedg 16222 | In a simple pseudograph, for each edge there is exactly one indexed edge. (Contributed by AV, 20-Apr-2025.) |
| 20-Apr-2025 | elovmpod 6254 | Utility lemma for two-parameter classes. (Contributed by Stefan O'Rear, 21-Jan-2015.) Variant of elovmpo 6255 in deduction form. (Revised by AV, 20-Apr-2025.) |
| 20-Apr-2025 | fdmeu 5722 | 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 15908 |
Product of two divisor sums. (This is also the main part of the proof
that " |
| 18-Apr-2025 | mpodvdsmulf1o 15907 |
If |
| 18-Apr-2025 | df2idl2 14706 | 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 14698 | 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 14685 | 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 14672 | 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 14626 | 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 14643 | Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.) |
| 14-Apr-2025 | grpmgmd 13760 | A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.) |
| 12-Apr-2025 | psraddcl 14884 | 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 16893 | Real number trichotomy is equivalent to decidability of complex number apartness. (Contributed by Jim Kingdon, 10-Apr-2025.) |
| 4-Apr-2025 | ghmf1 14011 | 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 14730 | 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 14765 | 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 14754. (Revised by GG, 31-Mar-2025.) |
| 31-Mar-2025 | cnfldle 14764 |
The ordering of the field of complex numbers. Note that this is not
actually an ordering on |
| 31-Mar-2025 | cnfldtset 14763 | 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 14760 | The multiplication operation of the field of complex numbers. Version of cnfldmul 14761 using maps-to notation, which does not require ax-mulf 8255. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | mpocnfldadd 14758 | The addition operation of the field of complex numbers. Version of cnfldadd 14759 using maps-to notation, which does not require ax-addf 8254. (Contributed by GG, 31-Mar-2025.) |
| 31-Mar-2025 | df-cnfld 14754 |
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 14756, cnfldadd 14759, cnfldmul 14761, cnfldcj 14762, cnfldtset 14763, cnfldle 14764, cnfldds 14765, and cnfldbas 14757. 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 14721 | 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 14448 | An integral domain is a ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 22-Mar-2025 | idomdomd 14446 | An integral domain is a domain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| 21-Mar-2025 | df2idl2rng 14705 | 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 14679 | 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 14678 | 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 13472 | Slot property of comp. (Contributed by Jim Kingdon, 20-Mar-2025.) |
| 20-Mar-2025 | homslid 13469 |
Slot property of |
| 19-Mar-2025 | ptex 13498 | Existence of the product topology. (Contributed by Jim Kingdon, 19-Mar-2025.) |
| 18-Mar-2025 | prdsex 13503 | Existence of the structure product. (Contributed by Jim Kingdon, 18-Mar-2025.) |
| 16-Mar-2025 | plycn 15676 | A polynomial is a continuous function. (Contributed by Mario Carneiro, 23-Jul-2014.) Avoid ax-mulf 8255. (Revised by GG, 16-Mar-2025.) |
| 16-Mar-2025 | expcn 15483 |
The power function on complex numbers, for fixed exponent |
| 16-Mar-2025 | mpomulcn 15480 | Complex number multiplication is a continuous function. (Contributed by GG, 16-Mar-2025.) |
| 16-Mar-2025 | mpomulf 8269 | Multiplication is an operation on complex numbers. Version of ax-mulf 8255 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8230. (Contributed by GG, 16-Mar-2025.) |
| 13-Mar-2025 | 2idlss 14711 | 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 13539 | Existence of the image structure. (Contributed by Jim Kingdon, 13-Mar-2025.) |
| 11-Mar-2025 | rng2idlsubgsubrng 14717 | 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 14714 | 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 14695 |
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 14694 |
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 14693 |
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 13540 | Value of an image structure. The is a lemma for the theorems imasbas 13541, imasplusg 13542, and imasmulr 13543 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 14704 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | 2idllidld 14703 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| 9-Mar-2025 | quseccl 13971 | 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 6161 | Closure law for an operation. (Contributed by NM, 19-Apr-2007.) (Proof shortened by AV, 9-Mar-2025.) |
| 8-Mar-2025 | subgex 13914 | The class of subgroups of a group is a set. (Contributed by Jim Kingdon, 8-Mar-2025.) |
| 8-Mar-2025 | fsuppfund 7249 | A finitely supported function is a function. (Contributed by SN, 8-Mar-2025.) |
| 7-Mar-2025 | ringrzd 14211 | The zero of a unital ring is a right-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | ringlzd 14210 | The zero of a unital ring is a left-absorbing element. (Contributed by SN, 7-Mar-2025.) |
| 7-Mar-2025 | qusecsub 14069 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
| 1-Mar-2025 | quselbasg 13968 | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
| 28-Feb-2025 | qusmulrng 14729 | Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14730. Similar to qusmul2 14726. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.) |
| 28-Feb-2025 | ringressid 14228 | 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 13305. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 28-Feb-2025 | grpressid 13795 | 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 13305. (Contributed by Jim Kingdon, 28-Feb-2025.) |
| 27-Feb-2025 | imasringf1 14230 | The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.) |
| 26-Feb-2025 | strext 13339 |
Extending the upper range of a structure. This works because when we
say that a structure has components in |
| 25-Feb-2025 | subrngringnsg 14373 | A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | rngansg 14115 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) |
| 25-Feb-2025 | ecqusaddd 13976 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) |
| 24-Feb-2025 | ecqusaddcl 13977 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) |
| 24-Feb-2025 | quseccl0g 13969 |
Closure of the quotient map for a quotient group. (Contributed by Mario
Carneiro, 18-Sep-2015.) Generalization of quseccl 13971 for arbitrary sets
|
| 23-Feb-2025 | ltlenmkv 16905 |
If |
| 23-Feb-2025 | neap0mkv 16904 | 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 14722 | 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 14724 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | 2idlcpblrng 14720 | 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 14363 | 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 14362 | A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringring 14361 | A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.) |
| 23-Feb-2025 | lringnzr 14360 | A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | islring 14359 | The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.) |
| 23-Feb-2025 | df-lring 14358 | 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 14356 | 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 14350 | 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 14123 | The quotient structure of a non-unital ring is a non-unital ring (qusring2 14231 analog). (Contributed by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdir 14117 | Ring multiplication distributes over subtraction. (subdir 8664 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 14222. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | rngsubdi 14116 | Ring multiplication distributes over subtraction. (subdi 8663 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 14221. (Revised by AV, 23-Feb-2025.) |
| 23-Feb-2025 | abbib 2352 | 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 1553 and df-clel 2230 (by avoiding use of cleqh 2334). (Revised by BJ, 23-Jun-2019.) Definitial form. (Revised by Wolf Lammen, 23-Feb-2025.) |
| 22-Feb-2025 | imasrngf1 14122 | 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 14121 | The image structure of a non-unital ring is a non-unital ring (imasring 14229 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | rngmgpf 14102 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 14176 analog). (Contributed by AV, 22-Feb-2025.) |
| 22-Feb-2025 | imasabl 14074 | The image structure of an abelian group is an abelian group (imasgrp 13849 analog). (Contributed by AV, 22-Feb-2025.) |
| 21-Feb-2025 | prdssgrpd 13649 | The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | prdsplusgsgrpcl 13648 | Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.) |
| 21-Feb-2025 | dftap2 7570 | Tight apartness with the apartness properties from df-pap 7561 expanded. (Contributed by Jim Kingdon, 21-Feb-2025.) |
| 20-Feb-2025 | rng2idlsubg0 14719 | 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 14718 | 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 14716 | 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 14715 | 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 14713 | 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 14712 | The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.) |
| 20-Feb-2025 | 2idlelb 14702 | Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) |
| 20-Feb-2025 | aprap 14458 | The relation given by df-apr 14450 for a local ring is an apartness relation. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | setscomd 13274 | Different components can be set in any order. (Contributed by Jim Kingdon, 20-Feb-2025.) |
| 20-Feb-2025 | ifnebibdc 3670 | The converse of ifbi 3645 holds if the two values are not equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnefals 3669 | Deduce falsehood from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 20-Feb-2025 | ifnetruedc 3668 | Deduce truth from a conditional operator value. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| 18-Feb-2025 | rnglidlmcl 14677 | 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 14457 | The apartness relation given by df-apr 14450 for a local ring is cotransitive. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprsym 14456 | The apartness relation given by df-apr 14450 for a ring is symmetric. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | aprval 14451 | Expand Definition df-apr 14450. (Contributed by Jim Kingdon, 17-Feb-2025.) |
| 17-Feb-2025 | subrngpropd 14384 | 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 14114 | Double negation of a product in a non-unital ring (mul2neg 8676 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 14220. (Revised by AV, 17-Feb-2025.) |
| 17-Feb-2025 | rngmneg2 14113 | Negation of a product in a non-unital ring (mulneg2 8674 analog). In contrast to ringmneg2 14219, 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 14112 | Negation of a product in a non-unital ring (mulneg1 8673 analog). In contrast to ringmneg1 14218, 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 14455 | The apartness relation given by df-apr 14450 for a nonzero ring is irreflexive. (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 16-Feb-2025 | rngrz 14111 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 14209. (Revised by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rng0cl 14108 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rngacl 14107 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | rnggrp 14103 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
| 16-Feb-2025 | aptap 8929 | Complex apartness (as defined at df-ap 8861) is a tight apartness (as defined at df-tap 7568). (Contributed by Jim Kingdon, 16-Feb-2025.) |
| 15-Feb-2025 | subsubrng2 14383 | The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subsubrng 14382 | A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngin 14381 | The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | subrngintm 14380 | The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprsubrngg 14379 | Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | issubrng2 14378 | Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrngbg 14243 | A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 14242. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | opprrng 14242 | An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | rngpropd 14120 | 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 13647 | 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 13643 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) |
| 15-Feb-2025 | tapeq2 7572 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 15-Feb-2025.) |
| 14-Feb-2025 | subrngmcl 14377 | A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14401. (Revised by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngacl 14376 | A subring is closed under addition. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrng0 14375 | A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngbas 14374 | Base set of a subring structure. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngsubg 14372 | A subring is a subgroup. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrcl 14371 | Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngrng 14370 | A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngid 14369 | Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | subrngss 14368 | A subring is a subset. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | issubrng 14367 | The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | df-subrng 14366 | 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 14118 | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | rngdi 14105 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
| 14-Feb-2025 | exmidmotap 7580 | 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 7579 | 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 7561 |
Apartness predicate. A relation |
| 13-Feb-2025 | 2idl1 14710 | Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | 2idl0 14709 | Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl1 14708 | Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | ridl0 14707 | Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | isridl 14701 | 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 14450 | The relation between elements whose difference is invertible, which for a local ring is an apartness relation by aprap 14458. (Contributed by Jim Kingdon, 13-Feb-2025.) |
| 13-Feb-2025 | rngass 14104 | 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 13646 | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) |
| 13-Feb-2025 | eqab 2369 | One direction of eqabb 2370. (Contributed by Wolf Lammen, 13-Feb-2025.) |
| 12-Feb-2025 | eqabb 2370 |
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 2352 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 7575 |
|
| 8-Feb-2025 | tapeq1 7571 | Equality theorem for tight apartness predicate. (Contributed by Jim Kingdon, 8-Feb-2025.) |
| 7-Feb-2025 | psrgrp 14889 | 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 14417 | Restriction of the codomain of a (ring) homomorphism. resghm2b 14000 analog. (Contributed by SN, 7-Feb-2025.) |
| 6-Feb-2025 | zzlesq 11078 | An integer is less than or equal to its square. (Contributed by BJ, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotap 7578 |
If there is at most one tight apartness on |
| 6-Feb-2025 | 2omotaplemst 7577 | Lemma for 2omotap 7578. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2omotaplemap 7576 | Lemma for 2omotap 7578. (Contributed by Jim Kingdon, 6-Feb-2025.) |
| 6-Feb-2025 | 2onetap 7574 |
Negated equality is a tight apartness on |
| 5-Feb-2025 | netap 7573 | Negated equality on a set with decidable equality is a tight apartness. (Contributed by Jim Kingdon, 5-Feb-2025.) |
| 5-Feb-2025 | df-tap 7568 |
Tight apartness predicate. A relation |
| 1-Feb-2025 | mulgnn0cld 13881 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 13876. (Contributed by SN, 1-Feb-2025.) |
| 31-Jan-2025 | 0subg 13937 | 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 13790 | The right inverse of a group element. Deduction associated with grprinv 13785. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplinvd 13789 | The left inverse of a group element. Deduction associated with grplinv 13784. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpinvcld 13783 | A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpridd 13768 | The identity element of a group is a right identity. Deduction associated with grprid 13766. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grplidd 13767 | The identity element of a group is a left identity. Deduction associated with grplid 13765. (Contributed by SN, 29-Jan-2025.) |
| 29-Jan-2025 | grpassd 13746 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
| 28-Jan-2025 | dvdsrex 14265 | Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.) |
| 24-Jan-2025 | reldvdsrsrg 14259 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.) |
| 18-Jan-2025 | rerecapb 9122 | 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 8950 | 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 14475 | A field is a division ring. (Contributed by SN, 17-Jan-2025.) |
| 17-Jan-2025 | ressval3d 13306 | Value of structure restriction, deduction version. (Contributed by AV, 14-Mar-2020.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 17-Jan-2025 | strressid 13305 | Behavior of trivial restriction. (Contributed by Stefan O'Rear, 29-Nov-2014.) (Revised by Jim Kingdon, 17-Jan-2025.) |
| 17-Jan-2025 | snelpwg 4328 | 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 4238. (Revised by BJ, 17-Jan-2025.) |
| 16-Jan-2025 | ressex 13299 | Existence of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 16-Jan-2025 | ressvalsets 13298 | Value of structure restriction. (Contributed by Jim Kingdon, 16-Jan-2025.) |
| 15-Jan-2025 | vsnex 4326 | A singleton built on a setvar is a set. (Contributed by BJ, 15-Jan-2025.) |
| 12-Jan-2025 | isrim 14336 | 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 14338 | A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.) |
| 10-Jan-2025 | isrim0 14328 | 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 14238 |
Existence of the opposite ring. If you know that |
| 10-Jan-2025 | mgpex 14090 |
Existence of the multiplication group. If |
| 6-Jan-2025 | ord3 6661 | 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 3831 | The singleton of an element of a class is a subset of the class (inference form of snssg 3830). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 21-Jun-1993.) (Proof shortened by BJ, 1-Jan-2025.) |
| 1-Jan-2025 | snssg 3830 | 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 3829 | Characterization of the inclusion of a singleton in a class. (Contributed by BJ, 1-Jan-2025.) |
| 30-Dec-2024 | rex2dom 7065 | A set that has at least 2 different members dominates ordinal 2. (Contributed by BTernaryTau, 30-Dec-2024.) |
| 23-Dec-2024 | en2prd 7061 | Two proper unordered pairs are equinumerous. (Contributed by BTernaryTau, 23-Dec-2024.) |
| 11-Dec-2024 | elopabr 4403 | 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 2775 | Change the bound variable of a restricted unique existential quantifier using implicit substitution. Version of cbvreu 2778 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 7472 | Decidable equality for ℕ∞ implies the Weak Limited Principle of Omniscience (WLPO). (Contributed by Jim Kingdon, 9-Dec-2024.) |
| 8-Dec-2024 | nninfinfwlpolem 7471 | Lemma for nninfinfwlpo 7473. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemdc 7470 | Lemma for nninfwlpoim 7472. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemginf 7469 | Lemma for nninfwlpoim 7472. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 8-Dec-2024 | nninfwlpoimlemg 7468 | Lemma for nninfwlpoim 7472. (Contributed by Jim Kingdon, 8-Dec-2024.) |
| 7-Dec-2024 | nninfwlpor 7467 | The Weak Limited Principle of Omniscience (WLPO) implies that equality for ℕ∞ is decidable. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | nninfwlporlem 7466 | Lemma for nninfwlpor 7467. The result. (Contributed by Jim Kingdon, 7-Dec-2024.) |
| 7-Dec-2024 | domssr 7019 |
If |
| 7-Dec-2024 | f1dom4g 6994 | The domain of a one-to-one set function is dominated by its codomain when the latter is a set. This variation of f1domg 6999 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 7-Dec-2024 | f1oen4g 6993 | The domain and range of a one-to-one, onto set function are equinumerous. This variation of f1oeng 6998 does not require the Axiom of Collection nor the Axiom of Union. (Contributed by BTernaryTau, 7-Dec-2024.) |
| 6-Dec-2024 | nninfwlporlemd 7465 | 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 7474 | 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 7464 | 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 6986 | Dominance relation. This variation of brdomg 6987 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of brdomg 6987. (Revised by BTernaryTau, 29-Nov-2024.) |
| 28-Nov-2024 | basmexd 13294 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 28-Nov-2024.) |
| 23-Nov-2024 | fldcrngd 14476 | A field is a commutative ring. (Contributed by SN, 23-Nov-2024.) |
| 22-Nov-2024 | eliotaeu 5343 | An inhabited iota expression has a unique value. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 22-Nov-2024 | eliota 5342 | An element of an iota expression. (Contributed by Jim Kingdon, 22-Nov-2024.) |
| 18-Nov-2024 | basmex 13293 | A structure whose base is inhabited is a set. (Contributed by Jim Kingdon, 18-Nov-2024.) |
| 14-Nov-2024 | dcand 941 | 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 14640 | 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 14639 | 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 13409 | The slot for the scalar is not the index of other slots. (Contributed by AV, 12-Nov-2024.) |
| 11-Nov-2024 | bj-con1st 16572 | Contraposition when the antecedent is a negated stable proposition. See con1dc 864. (Contributed by BJ, 11-Nov-2024.) |
| 11-Nov-2024 | slotsdifdsndx 13459 | 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 13448 | 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 13447 | 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 13444 | 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 13428 | 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 6270 | Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024.) |
| 11-Nov-2024 | const 860 | Contraposition when the antecedent is a negated stable proposition. See comment of condc 861. (Contributed by BJ, 18-Nov-2023.) (Proof shortened by BJ, 11-Nov-2024.) |
| 10-Nov-2024 | slotsdifunifndx 13466 | 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 13301 | 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 14241 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprbasg 14240 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
| 6-Nov-2024 | opprsllem 14239 | Lemma for opprbasg 14240 and oppraddg 14241. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
| 4-Nov-2024 | lgsfvalg 15927 |
Value of the function |
| 3-Nov-2024 | znmul 14839 | 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 14838 | 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 14837 | 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 14836 | Lemma for znbas 14841. (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 14828 |
Ring operation of a |
| 3-Nov-2024 | zlmplusgg 14827 |
Group operation of a |
| 3-Nov-2024 | zlmbasg 14826 |
Base set of a |
| 3-Nov-2024 | zlmlemg 14825 | Lemma for zlmbasg 14826 and zlmplusgg 14827. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 3-Nov-2024.) |
| 2-Nov-2024 | zlmsca 14829 |
Scalar ring of a |
| 1-Nov-2024 | plendxnvscandx 13443 | 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 13442 | 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 13441 | 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 11019 | 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 13456 | 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 13427 | 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 13425 | 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 13424 | 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 13423 | 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 16054 |
The index value of the |
| 30-Oct-2024 | plendxnbasendx 13439 | 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 13438 |
The index value of the |
| 30-Oct-2024 | plendxnn 13437 | 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 14645 | 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 14642 | 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 14638 | 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 14637 | 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 14636 | 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 14635 | Lemma for srabaseg 14636 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 13458 | 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 13457 |
The slots Scalar, |
| 29-Oct-2024 | slotstnscsi 13429 |
The slots Scalar, |
| 29-Oct-2024 | ipndxnmulrndx 13408 | 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 13407 | 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 13395 | 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 13390 | 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 11205 | 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 11204 | A finite set of integers has an upper bound which is an integer. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 29-Oct-2024 | fiubm 11203 | Lemma for fiubz 11204 and fiubnn 11205. A general form of those theorems. (Contributed by Jim Kingdon, 29-Oct-2024.) |
| 28-Oct-2024 | edgfndxid 16053 | 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 13465 | 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 13463 | 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 13462 | 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 13454 | 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 13453 | 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 13452 | 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 16564 |
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 16809 for the version not using the definition of
stability.
(Contributed by BJ, 9-Oct-2019.) Prove it in |
| 27-Oct-2024 | bj-imnimnn 16559 | 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 16558 as its last step. (Contributed by BJ, 27-Oct-2024.) |
| 25-Oct-2024 | nnwosdc 12743 | 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 12740 | 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 12741 | 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 16809 | Double negation of double negation elimination. Suggested by an online post by Martin Escardo. Although this statement resembles nnexmid 858, 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 13464 | 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 13406 | 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 13388 | 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 12846 |
Lemma for isprm5 12847. The interesting direction (showing that
one only
needs to check prime divisors up to the square root of |
| 19-Oct-2024 | resseqnbasd 13307 | 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 14548 |
The right module |
| 18-Oct-2024 | mgpress 14096 | 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 13455 | 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 13440 | 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 13426 | 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 13396 | 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 13394 | 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 13393 | 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 13389 | 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 13378 | 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 13377 | 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 13376 | 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 13347 | 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 13345 | 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 9950 |
Membership of an integer in |
| 14-Oct-2024 | 2zinfmin 11936 | 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 11935 |
Equivalence of |
| 13-Oct-2024 | edgfndxnn 16052 | 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 16051 | Index value of the df-edgf 16049 slot. (Contributed by AV, 13-Oct-2024.) (New usage is discouraged.) |
| 13-Oct-2024 | prdsvallem 13506 | Lemma for prdsval 13507. (Contributed by Stefan O'Rear, 3-Jan-2015.) Extracted from the former proof of prdsval 13507, dependency on df-hom 13335 removed. (Revised by AV, 13-Oct-2024.) |
| 13-Oct-2024 | pcxnn0cl 13016 | Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0letri 10142 | Dichotomy for extended nonnegative integers. (Contributed by Jim Kingdon, 13-Oct-2024.) |
| 13-Oct-2024 | xnn0dcle 10141 |
Decidability of |
| 9-Oct-2024 | nn0leexp2 11080 | Ordering law for exponentiation. (Contributed by Jim Kingdon, 9-Oct-2024.) |
| 8-Oct-2024 | pclemdc 12994 | Lemma for the prime power pre-function's properties. (Contributed by Jim Kingdon, 8-Oct-2024.) |
| 8-Oct-2024 | elnn0dc 9949 |
Membership of an integer in |
| 7-Oct-2024 | pclemub 12993 | 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 12992 | 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 11079 | Special case of ltexp2 15855 which we use here because we haven't yet defined df-rpcxp 15773 which is used in the current proof of ltexp2 15855. (Contributed by Jim Kingdon, 7-Oct-2024.) |
| 6-Oct-2024 | suprzcl2dc 10606 | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 8253.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) |
| 5-Oct-2024 | zsupssdc 10605 | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 8253.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
| 5-Oct-2024 | suprzubdc 10603 | The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
| 1-Oct-2024 | infex2g 7327 | Existence of infimum. (Contributed by Jim Kingdon, 1-Oct-2024.) |
| 30-Sep-2024 | unbendc 13226 | 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 12835 | Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | dcfi 7270 | Decidability of a family of propositions indexed by a finite set. (Contributed by Jim Kingdon, 30-Sep-2024.) |
| 30-Sep-2024 | cbvriotavw 6016 | Change bound variable in a restricted description binder. Version of cbvriotav 6018 with a disjoint variable condition. (Contributed by NM, 18-Mar-2013.) (Revised by GG, 30-Sep-2024.) |
| 30-Sep-2024 | cbviotavw 5320 | Change bound variables in a description binder. Version of cbviotav 5321 with a disjoint variable condition. (Contributed by Andrew Salmon, 1-Aug-2011.) (Revised by GG, 30-Sep-2024.) |
| 29-Sep-2024 | ssnnct 13219 |
A decidable subset of |
| 29-Sep-2024 | ssnnctlemct 13218 | Lemma for ssnnct 13219. The result. (Contributed by Jim Kingdon, 29-Sep-2024.) |
| 28-Sep-2024 | nninfdcex 10604 | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
| 27-Sep-2024 | infregelbex 9936 | 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 13222 |
Lemma for nninfdc 13225. Each element of the sequence |
| 26-Sep-2024 | nnminle 12739 | 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 12738. (Contributed by Jim Kingdon, 26-Sep-2024.) |
| 25-Sep-2024 | nninfdclemcl 13220 | Lemma for nninfdc 13225. (Contributed by Jim Kingdon, 25-Sep-2024.) |
| 24-Sep-2024 | nninfdclemlt 13223 | Lemma for nninfdc 13225. The function from nninfdclemf 13221 is strictly monotonic. (Contributed by Jim Kingdon, 24-Sep-2024.) |
| 23-Sep-2024 | nninfdc 13225 | An unbounded decidable set of positive integers is infinite. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf1 13224 | Lemma for nninfdc 13225. The function from nninfdclemf 13221 is one-to-one. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | nninfdclemf 13221 |
Lemma for nninfdc 13225. A function from the natural numbers into
|
| 23-Sep-2024 | nnmindc 12738 | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
| 23-Sep-2024 | breng 6984 | Equinumerosity relation. This variation of bren 6985 does not require the Axiom of Union. (Contributed by NM, 15-Jun-1998.) Extract from a subproof of bren 6985. (Revised by BTernaryTau, 23-Sep-2024.) |
| 20-Sep-2024 | ineqcomi 3415 |
Two ways of expressing that two classes have a given intersection.
Inference form of ineqcom 3414. Disjointness inference when |
| 19-Sep-2024 | ssomct 13217 |
A decidable subset of |
| 19-Sep-2024 | 2oex 6666 |
|
| 19-Sep-2024 | ecase2d 1388 | Deduction for elimination by cases. (Contributed by NM, 21-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Sep-2024.) |
| 18-Sep-2024 | fcof 5865 | Composition of a function with domain and codomain and a function as a function with domain and codomain. Generalization of fco 5529. (Contributed by AV, 18-Sep-2024.) |
| 17-Sep-2024 | fncofn 5864 | Composition of a function with domain and a function as a function with domain. Generalization of fnco 5468. (Contributed by AV, 17-Sep-2024.) |
| 14-Sep-2024 | nnpredlt 4748 | The predecessor (see nnpredcl 4747) of a nonzero natural number is less than (see df-iord 4489) that number. (Contributed by Jim Kingdon, 14-Sep-2024.) |
| 13-Sep-2024 | nninfisollemeq 7425 |
Lemma for nninfisol 7426. The case where |
| 13-Sep-2024 | nninfisollemne 7424 |
Lemma for nninfisol 7426. A case where |
| 13-Sep-2024 | nninfisollem0 7423 |
Lemma for nninfisol 7426. The case where |
| 12-Sep-2024 | nninfisol 7426 |
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 7473). (Contributed by BJ and Jim Kingdon, 12-Sep-2024.) |
| 8-Sep-2024 | relopabv 4881 | A class of ordered pairs is a relation. For a version without a disjoint variable condition, see relopab 4883. (Contributed by SN, 8-Sep-2024.) |
| 7-Sep-2024 | eulerthlemfi 12933 |
Lemma for eulerth 12938. The set |
| 7-Sep-2024 | modqexp 11036 | 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 12936 |
Lemma for eulerth 12938. A permutation of |
| 2-Sep-2024 | eulerthlemth 12937 | Lemma for eulerth 12938. The result. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlema 12935 | Lemma for eulerth 12938. (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by Jim Kingdon, 2-Sep-2024.) |
| 2-Sep-2024 | eulerthlemrprm 12934 |
Lemma for eulerth 12938. |
| 1-Sep-2024 | qusmul2 14726 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
| 30-Aug-2024 | fprodap0f 12330 | A finite product of terms apart from zero is apart from zero. A version of fprodap0 12315 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 12323 | The finite product of reciprocals is the reciprocal of the product. (Contributed by Jim Kingdon, 28-Aug-2024.) |
| 26-Aug-2024 | exmidontri2or 7555 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | exmidontri 7551 | Ordinal trichotomy is equivalent to excluded middle. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontri2orexmidim 4696 | Ordinal trichotomy implies excluded middle. Closed form of ordtri2or2exmid 4695. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 26-Aug-2024 | ontriexmidim 4646 | Ordinal trichotomy implies excluded middle. Closed form of ordtriexmid 4645. (Contributed by Jim Kingdon, 26-Aug-2024.) |
| 25-Aug-2024 | onntri2or 7558 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | onntri3or 7557 | Double negated ordinal trichotomy. (Contributed by Jim Kingdon, 25-Aug-2024.) |
| 25-Aug-2024 | csbcow 3151 | Composition law for chained substitutions into a class. Version of csbco 3150 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 2786 | Version of cbvreuv 2782 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvrexvw 2785 | Version of cbvrexv 2781 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvralvw 2784 | Version of cbvralv 2780 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvabw 2359 | Version of cbvab 2360 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) Reduce axiom usage. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfsbv 2003 |
If |
| 25-Aug-2024 | cbvexvw 1972 | Change bound variable. See cbvexv 1970 for a version with fewer disjoint variable conditions. (Contributed by NM, 19-Apr-2017.) Avoid ax-7 1497. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | cbvalvw 1971 | Change bound variable. See cbvalv 1969 for a version with fewer disjoint variable conditions. (Contributed by NM, 9-Apr-2017.) Avoid ax-7 1497. (Revised by GG, 25-Aug-2024.) |
| 25-Aug-2024 | nfal 1625 |
If |
| 24-Aug-2024 | gcdcomd 12678 |
The |
| 21-Aug-2024 | dvds2addd 12523 | Deduction form of dvds2add 12519. (Contributed by SN, 21-Aug-2024.) |
| 18-Aug-2024 | prdsmulr 13512 | 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 13511 | 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 13510 | 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 13509 | 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 13507 | 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 13501 | 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 12299 | Finite product closure lemma. (Contributed by Scott Fenton, 14-Dec-2017.) (Revised by Jim Kingdon, 17-Aug-2024.) |
| 16-Aug-2024 | fprodunsn 12298 |
Multiply in an additional term in a finite product. See also
fprodsplitsn 12327 which is the same but with a |
| 16-Aug-2024 | if0ab 3625 | 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 16628 | Alternate proof of bj-charfundc 16627. It was expected to be much shorter since it uses bj-charfun 16626 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 16626 |
Properties of the characteristic function on the class |
| 15-Aug-2024 | cnstab 8924 |
Equality of complex numbers is stable. Stability here means
|
| 15-Aug-2024 | subap0d 8923 | 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 4607 | Existence of a conditional class (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwun 4606 | Existence of a conditional class, quantitative version (inference form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwund 4605 | Existence of a conditional class, quantitative version (deduction form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifelpwung 4604 | Existence of a conditional class, quantitative version (closed form). (Contributed by BJ, 15-Aug-2024.) |
| 15-Aug-2024 | ifidss 3640 | 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 3639 | A conditional class is included in the union of its two alternatives. (Contributed by BJ, 15-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem2 7531 | Lemma for exmidontriim 7534. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 12-Aug-2024 | exmidontriimlem1 7530 | Lemma for exmidontriim 7534. A variation of r19.30dc 2692. (Contributed by Jim Kingdon, 12-Aug-2024.) |
| 11-Aug-2024 | nndc 859 |
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 7534 | 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 7533 |
Lemma for exmidontriim 7534. The induction step for the induction on
|
| 10-Aug-2024 | exmidontriimlem3 7532 |
Lemma for exmidontriim 7534. What we get to do based on induction on
both
|
| 10-Aug-2024 | nnnninf2 7420 |
Canonical embedding of |
| 10-Aug-2024 | infnninf 7417 |
The point at infinity in ℕ∞ is the constant sequence
equal to
|
| 9-Aug-2024 | ss1o0el1o 7175 |
Reformulation of ss1o0el1 4312 using |
| 9-Aug-2024 | pw1dc0el 7173 | Another equivalent of excluded middle, which is a mere reformulation of the definition. (Contributed by BJ, 9-Aug-2024.) |
| 9-Aug-2024 | ss1o0el1 4312 |
A subclass of |
| 8-Aug-2024 | pw1dc1 7176 | 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 | fdmexb 5910 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| 8-Aug-2024 | fndmexb 5909 | The domain of a function is a set iff the function is a set. (Contributed by AV, 8-Aug-2024.) |
| 7-Aug-2024 | psrbagaddclfi 14874 | 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 14868 | 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 7172 |
Excluded middle is equivalent to the power set of |
| 7-Aug-2024 | elomssom 4729 | 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 4730. (Revised by BJ, 7-Aug-2024.) |
| 6-Aug-2024 | bj-charfunbi 16630 |
In an ambient set
This characterization can be applied to singletons when the set |
| 6-Aug-2024 | bj-charfunr 16629 |
If a class
The hypothesis imposes that
The theorem would still hold if the codomain of |
| 6-Aug-2024 | bj-charfundc 16627 |
Properties of the characteristic function on the class |
| 6-Aug-2024 | psrbagconf1o 14877 |
Bag complementation is a bijection on the set of bags dominated by a
given bag |
| 6-Aug-2024 | psrbagconcl 14876 | 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 12283 | 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 16625 | The maps-to notation defines a function with domain (deduction form). (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | funmptd 16624 |
The maps-to notation defines a function (deduction form).
Note: one should similarly prove a deduction form of funopab4 5391, then prove funmptd 16624 from it, and then prove funmpt 5392 from that: this would reduce global proof length. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dcfal 16576 | The false truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-dctru 16574 | The true truth value is decidable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-stfal 16563 | The false truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | bj-sttru 16561 | The true truth value is stable. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | psrbagcon 14875 |
The analogue of the statement " |
| 5-Aug-2024 | psrbaglecl 14873 | 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 14871 | 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 12280 | 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 9556 |
Version of fcdmnn0fsupp 9554 avoiding ax-coll 4227 by assuming |
| 5-Aug-2024 | fcdmnn0suppg 9555 |
Version of fcdmnn0supp 9553 avoiding ax-coll 4227 by assuming |
| 5-Aug-2024 | 2ssom 6759 | The ordinal 2 is included in the set of natural number ordinals. (Contributed by BJ, 5-Aug-2024.) |
| 5-Aug-2024 | suppssdc 6462 | 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 6444 |
An element of the support of a function with a given domain. This
version of elsuppfn 6445 assumes |
| 5-Aug-2024 | suppvalfng 6442 |
The value of the operation constructing the support of a function with a
given domain. This version of suppvalfn 6443 assumes |
| 4-Aug-2024 | en3d 7010 | 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 7009 | 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 7556 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri24 7554 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri45 7553 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri51 7552 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri13 7550 | Double negated ordinal trichotomy. (Contributed by James E. Hanson and Jim Kingdon, 2-Aug-2024.) |
| 2-Aug-2024 | onntri35 7549 |
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 2534 | The double negation of a universal quantification implies the universal quantification of the double negation. Restricted quantifier version of nnal 1698. (Contributed by Jim Kingdon, 1-Aug-2024.) |
| 31-Jul-2024 | 3nsssucpw1 7548 |
Negated excluded middle implies that |
| 31-Jul-2024 | sucpw1nss3 7547 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | psrbagf 14867 | 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 7546 |
Three is not an element of the successor of the power set of |
| 30-Jul-2024 | sucpw1nel3 7545 |
The successor of the power set of |
| 30-Jul-2024 | sucpw1ne3 7544 |
Negated excluded middle implies that the successor of the power set of
|
| 30-Jul-2024 | pw1nel3 7543 |
Negated excluded middle implies that the power set of |
| 30-Jul-2024 | pw1ne3 7542 |
The power set of |
| 30-Jul-2024 | pw1ne1 7541 |
The power set of |
| 30-Jul-2024 | pw1ne0 7540 |
The power set of |
| 30-Jul-2024 | fsuppeqg 6450 |
Version of fsuppeq 6449 avoiding ax-coll 4227 by assuming |
| 29-Jul-2024 | grpcld 13748 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
| 29-Jul-2024 | pw1on 7538 |
The power set of |
| 29-Jul-2024 | isfsuppd 7245 | Deduction form of isfsupp 7244. (Contributed by SN, 29-Jul-2024.) |
| 28-Jul-2024 | exmidpweq 7171 |
Excluded middle is equivalent to the power set of |
| 27-Jul-2024 | dcapnconstALT 16897 | Decidability of real number apartness implies the existence of a certain non-constant function from real numbers to integers. A proof of dcapnconst 16896 by means of dceqnconst 16895. (Contributed by Jim Kingdon, 27-Jul-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
| 27-Jul-2024 | reap0 16892 | Real number trichotomy is equivalent to decidability of apartness from zero. (Contributed by Jim Kingdon, 27-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolemgt0 16899 | Lemma for nconstwlpo 16901. If one of the terms of series is positive, so is the sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 26-Jul-2024 | nconstwlpolem0 16898 | Lemma for nconstwlpo 16901. If all the terms of the series are zero, so is their sum. (Contributed by Jim Kingdon, 26-Jul-2024.) |
| 24-Jul-2024 | tridceq 16890 | Real trichotomy implies decidability of real number equality. Or in other words, analytic LPO implies analytic WLPO (see trilpo 16876 and redcwlpo 16889). Thus, this is an analytic analogue to lpowlpo 7461. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 24-Jul-2024 | iswomni0 16885 |
Weak omniscience stated in terms of equality with |
| 24-Jul-2024 | lpowlpo 7461 | LPO implies WLPO. Easy corollary of the more general omniwomnimkv 7460. There is an analogue in terms of analytic omniscience principles at tridceq 16890. (Contributed by Jim Kingdon, 24-Jul-2024.) |
| 23-Jul-2024 | nconstwlpolem 16900 | Lemma for nconstwlpo 16901. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | dceqnconst 16895 | 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 16889 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 16891 | Two ways to express decidability of real number equality. (Contributed by Jim Kingdon, 23-Jul-2024.) |
| 23-Jul-2024 | canth 6003 |
No set |
| 22-Jul-2024 | nconstwlpo 16901 |
Existence of a certain non-constant function from reals to integers
implies |
| 16-Jul-2024 | unexd 4869 | The union of two sets is a set. (Contributed by SN, 16-Jul-2024.) |
| 15-Jul-2024 | fprodseq 12277 | 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 2549 | Formula-building rule for restricted existential quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 14-Jul-2024 | ralbid2 2548 | Formula-building rule for restricted universal quantifier (deduction form). (Contributed by BJ, 14-Jul-2024.) |
| 12-Jul-2024 | 2irrexpqap 15892 |
There exist real numbers |
| 12-Jul-2024 | 2logb9irrap 15891 | Example for logbgcd1irrap 15884. 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 13566 | 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 13565 | 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 13564 | Lemma for ercpbl 13565. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfvalg 13563 | Value of the function in qusval 13557. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 12-Jul-2024 | divsfval 13562 | Value of the function in qusval 13557. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) (Revised by AV, 12-Jul-2024.) |
| 11-Jul-2024 | logbgcd1irraplemexp 15882 |
Lemma for logbgcd1irrap 15884. Apartness of |
| 11-Jul-2024 | reapef 15692 | Apartness and the exponential function for reals. (Contributed by Jim Kingdon, 11-Jul-2024.) |
| 10-Jul-2024 | apcxp2 15853 | Apartness and real exponentiation. (Contributed by Jim Kingdon, 10-Jul-2024.) |
| 9-Jul-2024 | logbgcd1irraplemap 15883 | Lemma for logbgcd1irrap 15884. The result, with the rational number expressed as numerator and denominator. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 9-Jul-2024 | apexp1 11088 | Exponentiation and apartness. (Contributed by Jim Kingdon, 9-Jul-2024.) |
| 5-Jul-2024 | logrpap0 15791 | The logarithm is apart from 0 if its argument is apart from 1. (Contributed by Jim Kingdon, 5-Jul-2024.) |
| 3-Jul-2024 | rplogbval 15859 | 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 15792 | Deduction form of logrpap0 15791. (Contributed by Jim Kingdon, 3-Jul-2024.) |
| 3-Jul-2024 | logrpap0b 15790 | 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 16817 |
Mapping zero and one between |
| 28-Jun-2024 | 012of 16816 |
Mapping zero and one between |
| 27-Jun-2024 | iooreen 16868 | An open interval is equinumerous to the real numbers. (Contributed by Jim Kingdon, 27-Jun-2024.) |
| 27-Jun-2024 | iooref1o 16867 | 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 16902 | Lemma for neapmkv 16903. The result, with a few hypotheses broken out for convenience. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnn 16887 | The predicate of being Markov stated in terms of set exponentiation. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 25-Jun-2024 | ismkvnnlem 16886 | Lemma for ismkvnn 16887. 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 7454 | Lemma for enmkv 7455. One direction of the biconditional. (Contributed by Jim Kingdon, 25-Jun-2024.) |
| 24-Jun-2024 | neapmkv 16903 | 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 16896 |
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 16876 for more
discussion of decidability of real number apartness.
This is a weaker form of dceqnconst 16895 and in fact this theorem can be proved using dceqnconst 16895 as shown at dcapnconstALT 16897. (Contributed by BJ and Jim Kingdon, 24-Jun-2024.) |
| 24-Jun-2024 | enmkv 7455 |
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 16888 | Lemma for redcwlpo 16889. A biconditionalized version of trilpolemeq1 16873. (Contributed by Jim Kingdon, 21-Jun-2024.) |
| 20-Jun-2024 | redcwlpo 16889 |
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 16888). 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 10611 for real numbers. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | iswomninn 16884 |
Weak omniscience stated in terms of natural numbers. Similar to
iswomnimap 7459 but it will sometimes be more convenient to
use |
| 20-Jun-2024 | iswomninnlem 16883 | Lemma for iswomnimap 7459. The result, with a hypothesis for convenience. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 20-Jun-2024 | enwomni 7463 |
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 7462 | Lemma for enwomni 7463. One direction of the biconditional. (Contributed by Jim Kingdon, 20-Jun-2024.) |
| 19-Jun-2024 | rpabscxpbnd 15854 | 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 15836 |
The exponential function with exponent |
| 16-Jun-2024 | biadanid 618 | Deduction associated with biadani 616. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
| 13-Jun-2024 | rpcxpadd 15819 | 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 15818 | Complex exponentiation is apart from zero. (Contributed by Mario Carneiro, 2-Aug-2014.) (Revised by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcncxpcl 15816 | Closure of the complex power function. (Contributed by Jim Kingdon, 12-Jun-2024.) |
| 12-Jun-2024 | rpcxp0 15812 | 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 15810 | 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 15809 | 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 15808 | 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 15773 | Define the power function on complex numbers. Because df-relog 15772 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 16878 |
Version of trirec0 16877 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 16877 |
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 16876). (Contributed by Jim Kingdon, 10-Jun-2024.) |
| 9-Jun-2024 | omniwomnimkv 7460 |
A set is omniscient if and only if it is weakly omniscient and Markov.
The case |
| 9-Jun-2024 | iswomnimap 7459 | The predicate of being weakly omniscient stated in terms of set exponentiation. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | iswomni 7458 | The predicate of being weakly omniscient. (Contributed by Jim Kingdon, 9-Jun-2024.) |
| 9-Jun-2024 | df-womni 7457 |
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 14200 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ringabld 14199 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | cmnmndd 14046 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | ablcmnd 14030 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | grpmndd 13747 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
| 1-Jun-2024 | fndmi 5458 | The domain of a function. (Contributed by Wolf Lammen, 1-Jun-2024.) |
| 29-May-2024 | pw1nct 16826 | 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 16825 | Any two elements of a subset of a singleton are equal. (Contributed by Jim Kingdon, 28-May-2024.) |
| 26-May-2024 | elpwi2 4272 | Membership in a power class. (Contributed by Glauco Siliprandi, 3-Mar-2021.) (Proof shortened by Wolf Lammen, 26-May-2024.) |
| 25-May-2024 | mplnegfi 14909 | The negative function on multivariate polynomials. (Contributed by SN, 25-May-2024.) |
| 24-May-2024 | dvmptcjx 15638 | Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 24-May-2024.) |
| 23-May-2024 | cbvralfw 2769 | Rule used to change bound variables, using implicit substitution. Version of cbvralf 2771 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 1556 and ax-bndl 1558 in the proof. (Contributed by NM, 7-Mar-2004.) (Revised by GG, 23-May-2024.) |
| 23-May-2024 | cbvrmow 2729 | Change the bound variable of a restricted at-most-one quantifier using implicit substitution. Version of cbvrmo 2779 with a disjoint variable condition. (Contributed by NM, 16-Jun-2017.) (Revised by GG, 23-May-2024.) |
| 23-May-2024 | cbvmow 2123 | Rule used to change bound variables, using implicit substitution. Version of cbvmo 2122 with a disjoint variable condition. (Contributed by NM, 9-Mar-1995.) (Revised by GG, 23-May-2024.) |
| 22-May-2024 | efltlemlt 15688 | Lemma for eflt 15689. The converse of efltim 12392 plus the epsilon-delta setup. (Contributed by Jim Kingdon, 22-May-2024.) |
| 21-May-2024 | eflt 15689 | 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 655 | A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.) |
| 19-May-2024 | apdifflemr 16880 | Lemma for apdiff 16881. (Contributed by Jim Kingdon, 19-May-2024.) |
| 18-May-2024 | apdifflemf 16879 |
Lemma for apdiff 16881. Being apart from the point halfway between
|
| 17-May-2024 | apdiff 16881 | 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 14494 | A left module is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | drnggrpd 14472 | A division ring is a group (deduction form). (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | drngringd 14471 | A division ring is a ring. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crnggrpd 14175 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | crngringd 14174 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
| 16-May-2024 | ringgrpd 14170 | A ring is a group. (Contributed by SN, 16-May-2024.) |
| 15-May-2024 | reeff1oleme 15686 | Lemma for reeff1o 15687. (Contributed by Jim Kingdon, 15-May-2024.) |
| 14-May-2024 | df-relog 15772 | 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 6192 | Value of an operation given by maps-to notation. (Contributed by Rohan Ridenour, 14-May-2024.) |
| 13-May-2024 | fndmexd 5558 | If a function is a set, its domain is a set. (Contributed by Rohan Ridenour, 13-May-2024.) |
| 12-May-2024 | dvdstrd 12524 | The divides relation is transitive, a deduction version of dvdstr 12522. (Contributed by metakunt, 12-May-2024.) |
| 7-May-2024 | ioocosf1o 15768 | 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 15766 |
Cosine is between minus one and one on the open interval between zero and
|
| 6-May-2024 | cos11 15767 |
Cosine is one-to-one over the closed interval from |
| 5-May-2024 | omiunct 13216 | The union of a countably infinite collection of countable sets is countable. Theorem 8.1.28 of [AczelRathjen], p. 78. Compare with ctiunct 13212 which has a stronger hypothesis but does not require countable choice. (Contributed by Jim Kingdon, 5-May-2024.) |
| 5-May-2024 | ctiunctal 13213 |
Variation of ctiunct 13212 which allows |
| 5-May-2024 | suppssrgst 6464 |
A function is zero outside its support. Version of suppssrst 6463 avoiding
ax-coll 4227 by assuming |
| 5-May-2024 | ifpnst 997 | 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 7590 |
Countable choice with a simpler restriction on how every set in the
countable collection needs to be inhabited. That is, compared with
cc4 7589, the hypotheses only require an A(n) for each
value of |
| 3-May-2024 | cc4f 7588 |
Countable choice by showing the existence of a function |
| 1-May-2024 | cc4 7589 |
Countable choice by showing the existence of a function |
| 30-Apr-2024 | ifpdfbidc 994 | 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 7587 | 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 1002 | Equivalence deduction for conditional operator for propositions. Convenience theorem for a frequent case. (Contributed by Wolf Lammen, 28-Apr-2024.) |
| 27-Apr-2024 | cc2 7586 | Countable choice using sequences instead of countable sets. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc2lem 7585 | Lemma for cc2 7586. (Contributed by Jim Kingdon, 27-Apr-2024.) |
| 27-Apr-2024 | cc1 7584 | 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 14629 | 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 13215 | 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 1001 | 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 12271 | Lemma for prodmodc 12272. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 13-Apr-2024.) |
| 13-Apr-2024 | sspwd 3686 | The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.) |
| 13-Apr-2024 | sspwi 3685 | The powerclass preserves inclusion (inference form). (Contributed by BJ, 13-Apr-2024.) |
| 13-Apr-2024 | sspw 3684 | The powerclass preserves inclusion. See sspwb 4334 for the biconditional version. (Contributed by NM, 13-Oct-1996.) Extract forward implication of sspwb 4334 since it requires fewer axioms. (Revised by BJ, 13-Apr-2024.) |
| 11-Apr-2024 | prodmodclem2a 12270 | Lemma for prodmodc 12272. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
| 11-Apr-2024 | prodmodclem3 12269 | Lemma for prodmodc 12272. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 11-Apr-2024.) |
| 10-Apr-2024 | jcnd 658 | Deduction joining the consequents of two premises. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Proof shortened by Wolf Lammen, 10-Apr-2024.) |
| 4-Apr-2024 | prodrbdclem 12265 | Lemma for prodrbdc 12268. (Contributed by Scott Fenton, 4-Dec-2017.) (Revised by Jim Kingdon, 4-Apr-2024.) |
| 24-Mar-2024 | prodfdivap 12241 | The quotient of two products. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
| 24-Mar-2024 | prodfrecap 12240 | The reciprocal of a finite product. (Contributed by Scott Fenton, 15-Jan-2018.) (Revised by Jim Kingdon, 24-Mar-2024.) |
| 23-Mar-2024 | prodfap0 12239 | The product of finitely many terms apart from zero is apart from zero. (Contributed by Scott Fenton, 14-Jan-2018.) (Revised by Jim Kingdon, 23-Mar-2024.) |
| 22-Mar-2024 | prod3fmul 12235 | The product of two infinite products. (Contributed by Scott Fenton, 18-Dec-2017.) (Revised by Jim Kingdon, 22-Mar-2024.) |
| 21-Mar-2024 | df-proddc 12245 |
Define the product of a series with an index set of integers |
| 19-Mar-2024 | cos02pilt1 15765 |
Cosine is less than one between zero and |
| 19-Mar-2024 | cosq34lt1 15764 | Cosine is less than one in the third and fourth quadrants. (Contributed by Jim Kingdon, 19-Mar-2024.) |
| 14-Mar-2024 | coseq0q4123 15748 |
Location of the zeroes of cosine in
|
| 14-Mar-2024 | cosq23lt0 15747 | The cosine of a number in the second and third quadrants is negative. (Contributed by Jim Kingdon, 14-Mar-2024.) |
| 9-Mar-2024 | pilem3 15697 | Lemma for pi related theorems. (Contributed by Jim Kingdon, 9-Mar-2024.) |
| 9-Mar-2024 | exmidonfin 7499 | If a finite ordinal is a natural number, excluded middle follows. That excluded middle implies that a finite ordinal is a natural number is proved in the Metamath Proof Explorer. That a natural number is a finite ordinal is shown at nnfi 7129 and nnon 4734. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
| 9-Mar-2024 | exmidonfinlem 7498 | Lemma for exmidonfin 7499. (Contributed by Andrew W Swan and Jim Kingdon, 9-Mar-2024.) |
| 8-Mar-2024 | sin0pilem2 15696 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
| 8-Mar-2024 | sin0pilem1 15695 | Lemma for pi related theorems. (Contributed by Mario Carneiro and Jim Kingdon, 8-Mar-2024.) |
| 7-Mar-2024 | cosz12 15694 | Cosine has a zero between 1 and 2. (Contributed by Mario Carneiro and Jim Kingdon, 7-Mar-2024.) |
| 6-Mar-2024 | cos12dec 12462 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
| 2-Mar-2024 | clwwlknonmpo 16472 |
|
| 2-Mar-2024 | scaffvalg 14503 | The scalar multiplication operation as a function. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof shortened by AV, 2-Mar-2024.) |
| 2-Mar-2024 | dvrfvald 14300 | Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof shortened by AV, 2-Mar-2024.) |
| 2-Mar-2024 | plusffvalg 13596 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.) |
| 25-Feb-2024 | insubm 13719 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
| 25-Feb-2024 | mul2lt0pn 10103 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | mul2lt0np 10102 | The product of multiplicands of different signs is negative. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | lt0ap0 8927 | A number which is less than zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 25-Feb-2024 | negap0d 8910 | The negative of a number apart from zero is apart from zero. (Contributed by Jim Kingdon, 25-Feb-2024.) |
| 24-Feb-2024 | lt0ap0d 8928 | A real number less than zero is apart from zero. Deduction form. (Contributed by Jim Kingdon, 24-Feb-2024.) |
| 20-Feb-2024 | ivthdec 15558 | The intermediate value theorem, decreasing case, for a strictly monotonic function. (Contributed by Jim Kingdon, 20-Feb-2024.) |
| 20-Feb-2024 | ivthinclemex 15556 | Lemma for ivthinc 15557. Existence of a number between the lower cut and the upper cut. (Contributed by Jim Kingdon, 20-Feb-2024.) |
| 19-Feb-2024 | ivthinclemuopn 15552 | Lemma for ivthinc 15557. The upper cut is open. (Contributed by Jim Kingdon, 19-Feb-2024.) |
| 19-Feb-2024 | dedekindicc 15547 | A Dedekind cut identifies a unique real number. Similar to df-inp 7786 except that the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 19-Feb-2024.) |
| 19-Feb-2024 | grpsubfvalg 13779 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) |
| 18-Feb-2024 | ivthinclemloc 15555 | Lemma for ivthinc 15557. Locatedness. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemdisj 15554 | Lemma for ivthinc 15557. The lower and upper cuts are disjoint. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemur 15553 | Lemma for ivthinc 15557. The upper cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemlr 15551 | Lemma for ivthinc 15557. The lower cut is rounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemum 15549 | Lemma for ivthinc 15557. The upper cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 18-Feb-2024 | ivthinclemlm 15548 | Lemma for ivthinc 15557. The lower cut is bounded. (Contributed by Jim Kingdon, 18-Feb-2024.) |
| 17-Feb-2024 | 0subm 13718 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
| 17-Feb-2024 | mndissubm 13709 | If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. (Contributed by AV, 17-Feb-2024.) |
| 17-Feb-2024 | mgmsscl 13595 | If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemeu 15545 | Lemma for dedekindicc 15547. Part of proving uniqueness. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemlu 15544 | Lemma for dedekindicc 15547. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemlub 15543 | Lemma for dedekindicc 15547. The set L has a least upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemloc 15542 | Lemma for dedekindicc 15547. The set L is located. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemub 15541 | Lemma for dedekindicc 15547. The lower cut has an upper bound. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 15-Feb-2024 | dedekindicclemuub 15540 | Lemma for dedekindicc 15547. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 15-Feb-2024.) |
| 14-Feb-2024 | suplociccex 15539 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8351 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
| 14-Feb-2024 | suplociccreex 15538 | An inhabited, bounded-above, located set of reals in a closed interval has a supremum. A similar theorem is axsuploc 8351 but that one is for the entire real line rather than a closed interval. (Contributed by Jim Kingdon, 14-Feb-2024.) |
| 10-Feb-2024 | cbvexdvaw 1983 | Rule used to change the bound variable in an existential quantifier with implicit substitution. Deduction form. Version of cbvexdva 1981 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.) |
| 10-Feb-2024 | cbvaldvaw 1982 | Rule used to change the bound variable in a universal quantifier with implicit substitution. Deduction form. Version of cbvaldva 1980 with a disjoint variable condition. (Contributed by David Moews, 1-May-2017.) (Revised by GG, 10-Jan-2024.) (Revised by Wolf Lammen, 10-Feb-2024.) |
| 6-Feb-2024 | ivthinclemlopn 15550 | Lemma for ivthinc 15557. The lower cut is open. (Contributed by Jim Kingdon, 6-Feb-2024.) |
| 5-Feb-2024 | ivthinc 15557 | The intermediate value theorem, increasing case, for a strictly monotonic function. Theorem 5.5 of [Bauer], p. 494. This is Metamath 100 proof #79. (Contributed by Jim Kingdon, 5-Feb-2024.) |
| 2-Feb-2024 | dedekindeulemuub 15531 | Lemma for dedekindeu 15537. Any element of the upper cut is an upper bound for the lower cut. (Contributed by Jim Kingdon, 2-Feb-2024.) |
| 31-Jan-2024 | dedekindeulemeu 15536 | Lemma for dedekindeu 15537. Part of proving uniqueness. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemlu 15535 | Lemma for dedekindeu 15537. There is a number which separates the lower and upper cuts. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemlub 15534 | Lemma for dedekindeu 15537. The set L has a least upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemloc 15533 | Lemma for dedekindeu 15537. The set L is located. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 31-Jan-2024 | dedekindeulemub 15532 | Lemma for dedekindeu 15537. The lower cut has an upper bound. (Contributed by Jim Kingdon, 31-Jan-2024.) |
| 30-Jan-2024 | axsuploc 8351 | An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 8253 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
| 30-Jan-2024 | iotam 5346 |
Representation of "the unique element such that |
| 29-Jan-2024 | sgrpidmndm 13654 | A semigroup with an identity element which is inhabited is a monoid. Of course there could be monoids with the empty set as identity element, but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.) |
| 29-Jan-2024 | ccatw2s1p1g 11341 | Extract the symbol of the first singleton word of a word concatenated with this singleton word and another singleton word. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 1-May-2020.) (Revised by AV, 29-Jan-2024.) |
| 28-Jan-2024 | ccat2s1fstg 11344 | The first symbol of the concatenation of a word with two single symbols. (Contributed by Alexander van der Vekens, 22-Sep-2018.) (Revised by AV, 28-Jan-2024.) |
| 28-Jan-2024 | ccat2s1fvwd 11343 | Extract a symbol of a word from the concatenation of the word with two single symbols. (Contributed by AV, 22-Sep-2018.) (Revised by AV, 13-Jan-2020.) (Proof shortened by AV, 1-May-2020.) (Revised by AV, 28-Jan-2024.) |
| 26-Jan-2024 | elovmporab1w 6257 | Implications for the value of an operation, defined by the maps-to notation with a class abstraction as a result, having an element. Here, the base set of the class abstraction depends on the first operand. (Contributed by Alexander van der Vekens, 15-Jul-2018.) (Revised by GG, 26-Jan-2024.) |
| 26-Jan-2024 | opabidw 4377 | The law of concretion. Special case of Theorem 9.5 of [Quine] p. 61. Version of opabid 4376 with a disjoint variable condition. (Contributed by NM, 14-Apr-1995.) (Revised by GG, 26-Jan-2024.) |
| 26-Jan-2024 | invdisjrab 4105 |
The restricted class abstractions |
| 24-Jan-2024 | axpre-suploclemres 8221 |
Lemma for axpre-suploc 8222. The result. The proof just needs to define
|
| 23-Jan-2024 | ax-pre-suploc 8253 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given Although this and ax-caucvg 8252 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8252. (Contributed by Jim Kingdon, 23-Jan-2024.) |
| 23-Jan-2024 | axpre-suploc 8222 |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8253. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
| 22-Jan-2024 | suplocsr 8129 | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
| 21-Jan-2024 | bj-el2oss1o 16595 | Shorter proof of el2oss1o 6678 using more axioms. (Contributed by BJ, 21-Jan-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
| 21-Jan-2024 | ltm1sr 8097 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
| 21-Jan-2024 | fvdifsuppst 6446 | Function value is zero outside of its support. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| 20-Jan-2024 | mndinvmod 13679 | Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.) |
| 20-Jan-2024 | ccats1val1g 11335 | Value of a symbol in the left half of a word concatenated with a single symbol. (Contributed by Alexander van der Vekens, 5-Aug-2018.) (Revised by JJ, 20-Jan-2024.) |
| 19-Jan-2024 | suplocsrlempr 8127 |
Lemma for suplocsr 8129. The set |
| 18-Jan-2024 | ccatval1 11293 | Value of a symbol in the left half of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) (Proof shortened by AV, 30-Apr-2020.) (Revised by JJ, 18-Jan-2024.) |
| 18-Jan-2024 | ccat0 11292 | The concatenation of two words is empty iff the two words are empty. (Contributed by AV, 4-Mar-2022.) (Revised by JJ, 18-Jan-2024.) |
| 18-Jan-2024 | suplocsrlemb 8126 |
Lemma for suplocsr 8129. The set |
| 16-Jan-2024 | suplocsrlem 8128 |
Lemma for suplocsr 8129. The set |
| 15-Jan-2024 | eqg0el 13967 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| 14-Jan-2024 | wlklenvclwlk 16417 | The number of vertices in a walk equals the length of the walk after it is "closed" (i.e. enhanced by an edge from its last vertex to its first vertex). (Contributed by Alexander van der Vekens, 29-Jun-2018.) (Revised by AV, 2-May-2021.) (Revised by JJ, 14-Jan-2024.) |
| 14-Jan-2024 | suplocexprlemlub 8044 | Lemma for suplocexpr 8045. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
| 14-Jan-2024 | suplocexprlemub 8043 | Lemma for suplocexpr 8045. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.) |
| 10-Jan-2024 | nfcsbw 3177 | Bound-variable hypothesis builder for substitution into a class. Version of nfcsb 3178 with a disjoint variable condition. (Contributed by Mario Carneiro, 12-Oct-2016.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfsbcw 3175 | Bound-variable hypothesis builder for class substitution. Version of nfsbc 3065 with a disjoint variable condition, which in the future may make it possible to reduce axiom usage. (Contributed by NM, 7-Sep-2014.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfsbcdw 3174 | Version of nfsbcd 3064 with a disjoint variable condition. (Contributed by NM, 23-Nov-2005.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvcsbw 3144 | Version of cbvcsb 3145 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvsbcw 3072 | Version of cbvsbc 3073 with a disjoint variable condition. (Contributed by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrex2vw 2792 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvrex2v 2794 with a disjoint variable condition, which does not require ax-13 2207. (Contributed by FL, 2-Jul-2012.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvral2vw 2791 | Change bound variables of double restricted universal quantification, using implicit substitution. Version of cbvral2v 2793 with a disjoint variable condition, which does not require ax-13 2207. (Contributed by NM, 10-Aug-2004.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrexw 2774 | Rule used to change bound variables, using implicit substitution. Version of cbvrexfw 2770 with more disjoint variable conditions. Although we don't do so yet, we expect the disjoint variable conditions will allow us to remove reliance on ax-i12 1556 and ax-bndl 1558 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvralw 2773 | Rule used to change bound variables, using implicit substitution. Version of cbvral 2776 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 1556 and ax-bndl 1558 in the proof. (Contributed by NM, 31-Jul-2003.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvrexfw 2770 | Rule used to change bound variables, using implicit substitution. Version of cbvrexf 2772 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 1556 and ax-bndl 1558 in the proof. (Contributed by FL, 27-Apr-2008.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | nfralw 2581 |
Bound-variable hypothesis builder for restricted quantification. See
nfralya 2584 for a version with |
| 10-Jan-2024 | nfraldw 2576 |
Not-free for restricted universal quantification where |
| 10-Jan-2024 | nfabdw 2405 | Bound-variable hypothesis builder for a class abstraction. Version of nfabd 2406 with a disjoint variable condition. (Contributed by Mario Carneiro, 8-Oct-2016.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbvex2vw 1985 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-Jul-1995.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbval2vw 1984 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 4-Feb-2005.) (Revised by GG, 10-Jan-2024.) |
| 10-Jan-2024 | cbv2w 1799 | Rule used to change bound variables, using implicit substitution. Version of cbv2 1798 with a disjoint variable condition. (Contributed by NM, 5-Aug-1993.) (Revised by GG, 10-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemloc 8041 | Lemma for suplocexpr 8045. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemdisj 8040 | Lemma for suplocexpr 8045. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemru 8039 | Lemma for suplocexpr 8045. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemrl 8037 | Lemma for suplocexpr 8045. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlem2b 8034 | Lemma for suplocexpr 8045. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 9-Jan-2024 | suplocexprlemell 8033 | Lemma for suplocexpr 8045. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.) |
| 7-Jan-2024 | suplocexpr 8045 | An inhabited, bounded-above, located set of positive reals has a supremum. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemex 8042 | Lemma for suplocexpr 8045. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemmu 8038 | Lemma for suplocexpr 8045. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemml 8036 | Lemma for suplocexpr 8045. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.) |
| 7-Jan-2024 | suplocexprlemss 8035 |
Lemma for suplocexpr 8045. |
| 5-Jan-2024 | dedekindicclemicc 15546 |
Lemma for dedekindicc 15547. Same as dedekindicc 15547, except that we
merely show |
| 5-Jan-2024 | dedekindeu 15537 | A Dedekind cut identifies a unique real number. Similar to df-inp 7786 except that the the Dedekind cut is formed by sets of reals (rather than positive rationals). But in both cases the defining property of a Dedekind cut is that it is inhabited (bounded), rounded, disjoint, and located. (Contributed by Jim Kingdon, 5-Jan-2024.) |
| 1-Jan-2024 | ccatlen 11291 | The length of a concatenated word. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by JJ, 1-Jan-2024.) |
| 31-Dec-2023 | dvmptsubcn 15637 | Function-builder for derivative, subtraction rule. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
| 31-Dec-2023 | dvmptnegcn 15636 | Function-builder for derivative, product rule for negatives. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
| 31-Dec-2023 | dvmptcmulcn 15635 | Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 31-Dec-2023.) |
| 31-Dec-2023 | rinvmod 14047 | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6250. (Contributed by AV, 31-Dec-2023.) |
| 31-Dec-2023 | brm 4162 | If two sets are in a binary relation, the relation is inhabited. (Contributed by Jim Kingdon, 31-Dec-2023.) |
| 30-Dec-2023 | dvmptccn 15629 | Function-builder for derivative: derivative of a constant. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
| 30-Dec-2023 | dvmptidcn 15628 | Function-builder for derivative: derivative of the identity. (Contributed by Mario Carneiro, 1-Sep-2014.) (Revised by Jim Kingdon, 30-Dec-2023.) |
| 30-Dec-2023 | eqwrd 11273 | Two words are equal iff they have the same length and the same symbol at each position. (Contributed by AV, 13-Apr-2018.) (Revised by JJ, 30-Dec-2023.) |
| 29-Dec-2023 | mndbn0 13665 | The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 13664). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
| 28-Dec-2023 | mulgnn0gsum 13866 | Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.) |
| 28-Dec-2023 | mulgnngsum 13865 | Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.) |
| 26-Dec-2023 | gsumfzreidx 14075 |
Re-index a finite group sum using a bijection. Corresponds to the first
equation in [Lang] p. 5 with |
| 26-Dec-2023 | gsumsplit1r 13632 | Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.) |
| 26-Dec-2023 | lidrididd 13616 |
If there is a left and right identity element for any binary operation
(group operation) |
| 26-Dec-2023 | lidrideqd 13615 |
If there is a left and right identity element for any binary operation
(group operation) |
| 25-Dec-2023 | ctfoex 7411 | A countable class is a set. (Contributed by Jim Kingdon, 25-Dec-2023.) |
| 23-Dec-2023 | enct 13205 | Countability is invariant relative to equinumerosity. (Contributed by Jim Kingdon, 23-Dec-2023.) |
| 23-Dec-2023 | enctlem 13204 | Lemma for enct 13205. One direction of the biconditional. (Contributed by Jim Kingdon, 23-Dec-2023.) |
| 23-Dec-2023 | omct 7410 |
|
| 21-Dec-2023 | dvcoapbr 15621 |
The chain rule for derivatives at a point. The
|
| 19-Dec-2023 | apsscn 8926 | The points apart from a given point are complex numbers. (Contributed by Jim Kingdon, 19-Dec-2023.) |
| Copyright terms: Public domain | W3C HTML validation [external] |