Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 13-Jul-2018 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (10-May-2018) George Szpiro, journalist and author of several books on popular mathematics such as Poincare's Prize and Numbers Rule, used a genetic algorithm to find shorter D-proofs of "*3.37" and "meredith" in our Shortest known proofs... file.
(19-Apr-2018) The EMetamath Eclipse plugin has undergone many improvements since its initial release as the change log indicates. Thierry uses it as his main proof assistant and writes, "I added support for mmj2's auto-transformations, which allows it to infer several steps when building proofs. This added a lot of comfort for writing proofs.... I can now switch back and forth between the proof assistant and editing the Metamath file.... I think no other proof assistant has this feature."
(11-Apr-2018) Benoît Jubin solved an open problem about the "Axiom of Twoness", showing that it is necessary for completeness. See item 14 on the "Open problems and miscellany" page.
(30-Mar-2018) Filip Cernatescu's Milpgame has been updated to version 0.6, which reduces the set.mm load time to about 40 seconds. A new how-to has also been added to its web page.
(25-Mar-2018) Giovanni Mascellani has announced mmpp, a new proof editing environment for the Metamath language.
(27-Feb-2018) Bill Hale has released an app for the Apple iPad and desktop computer that allows you to browse Metamath theorems and their proofs.
(17-Jan-2018) Dylan Houlihan has kindly provided a new mirror site. He has also provided an rsync server; type "rsync uk.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(15-Jan-2018) The metamath program, version 0.157, has been updated to implement the file inclusion conventions described in the 21-Dec-2017 entry of mmnotes.txt.
(11-Dec-2017) I added a paragraph, suggested by Gérard Lang, to the distinct variable description here.
(10-Dec-2017) Per FL's request, his mathbox will be removed from set.mm. If you wish to export any of his theorems, today's version (master commit 1024a3a) is the last one that will contain it.
(11-Nov-2017) Alan Sare updated his completeusersproof program.
(3-Oct-2017) Sean B. Palmer created a web page that runs the metamath program under emulated Linux in JavaScript. He also wrote some programs to work with our shortest known proofs of the PM propositional calculus theorems.
(28-Sep-2017) Ivan Kuckir wrote a tutorial blog entry, Introduction to Metamath, that summarizes the language syntax. (It may have been written some time ago, but I was not aware of it before.)
(26-Sep-2017) The default directory for the Metamath Proof Explorer (MPE) has been changed from the GIF version (mpegif) to the Unicode version (mpeuni) throughout the site. Please let me know if you find broken links or other issues.
(24-Sep-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Ceva's Theorem cevath, bringing the Metamath total to 67.
(3-Sep-2017) Brendan Leahy added a new proof to the 100 theorem list, Area of a Circle areacirc, bringing the Metamath total to 66.
(7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.
(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
14-Jul-2018 | sbie 2150 | Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 14-Jul-2018.) |
14-Jul-2018 | sbequi 2111 | An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Jul-2018.) |
14-Jul-2018 | 4syl 20 | Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it causes the "minimize" command to have very long run times. However, feel free to override it to use directly or in small "minimize" runs. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.) |
13-Jul-2018 | mblfinlem4 26247 | Backward direction of ismblfin 26248. (Contributed by Brendan Leahy, 28-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
13-Jul-2018 | mblfinlem3 26246 | The difference between two sets measurable by the criterion in ismblfin 26248 is itself measurable by the same. Corollary 0.3 of [Viaclovsky7] p. 3. (Contributed by Brendan Leahy, 25-Mar-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
13-Jul-2018 | mblfinlem2 26245 | Lemma for ismblfin 26248, effectively one direction of the same fact for open sets, made necessary by Viaclovsky's slightly different defintion of outer measure. Note that unlike the main theorem, this holds for sets of infinite measure. (Contributed by Brendan Leahy, 21-Feb-2018.) (Revised by Brendan Leahy, 13-Jul-2018.) |
13-Jul-2018 | mblfinlem1 26244 | Lemma for ismblfin 26248, ordering the sets of dyadic intervals that are antichains under subset and whose unions are contained entirely in . (Contributed by Brendan Leahy, 13-Jul-2018.) |
13-Jul-2018 | opnmbllem0 26243 | Lemma for ismblfin 26248; could also be used to shorten proof of opnmbllem 19494. (Contributed by Brendan Leahy, 13-Jul-2018.) |
11-Jul-2018 | areacirc 26298 | The area of a circle of radius is . (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
area | ||
11-Jul-2018 | areacirclem5 26297 | Finding the cross-section of a circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 22-Sep-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
11-Jul-2018 | areacirclem4 26296 | Endpoint-inclusive continuity of antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 31-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
arcsin | ||
11-Jul-2018 | areacirclem3 26295 | Integrability of cross-section of circle. (Contributed by Brendan Leahy, 26-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
11-Jul-2018 | areacirclem2 26294 | Endpoint-inclusive continuity of Cartesian ordinate of circle. (Contributed by Brendan Leahy, 29-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
11-Jul-2018 | areacirclem1 26293 | Antiderivative of cross-section of circle. (Contributed by Brendan Leahy, 28-Aug-2017.) (Revised by Brendan Leahy, 11-Jul-2018.) |
arcsin | ||
10-Jul-2018 | cusgraisrusgra 28378 | A complete undirected simple graph with n vertices (at least one) is (n-1)-regular. (Contributed by Alexander van der Vekens, 10-Jul-2018.) |
ComplUSGrph RegUSGrph | ||
10-Jul-2018 | 0vgrargra 28377 | A graph with no vertices is k-regular for every k. (Contributed by Alexander van der Vekens, 10-Jul-2018.) |
RegGrph | ||
9-Jul-2018 | vdcusgra 28365 | In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.) |
ComplUSGrph VDeg | ||
9-Jul-2018 | usgrauvtxvd 28364 | In a finite complete undirected simple graph with n vertices every vertex has degree (n-1). (Contributed by Alexander van der Vekens, 9-Jul-2018.) |
USGrph UnivVertex VDeg | ||
9-Jul-2018 | vdusgravaledg 28363 | The value of the vertex degree function for simple undirected graphs in terms of edges. (Contributed by Alexander van der Vekens, 9-Jul-2018.) |
USGrph VDeg | ||
8-Jul-2018 | 0egra0rgra 28376 | A graph is 0-regular if it has no edges. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
RegGrph | ||
8-Jul-2018 | rusisusgra 28375 | Any k-regular undirected simple graph is an undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
RegUSGrph USGrph | ||
8-Jul-2018 | rusgrargra 28374 | A k-regular undirected simple graph is a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
RegUSGrph RegGrph | ||
8-Jul-2018 | rusgraprop 28373 | The properties of a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
RegUSGrph USGrph VDeg | ||
8-Jul-2018 | rgraprop 28372 | The properties of a k-regular graph. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
RegGrph VDeg | ||
8-Jul-2018 | oprabv 28086 | If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
8-Jul-2018 | opelopabgf 28072 | The law of concretion. Theorem 9.5 of [Quine] p. 61. This version of opelopabg 4474 uses bound-variable hypotheses in place of distinct variable conditions." (Contributed by Alexander van der Vekens, 8-Jul-2018.) |
7-Jul-2018 | isrusgra 28371 | The property of being a k-regular undirected simple graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
RegUSGrph USGrph VDeg | ||
7-Jul-2018 | isrgra 28370 | The property of being a k-regular graph. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
RegGrph VDeg | ||
7-Jul-2018 | breqn0 28070 | If two sets are in a binary relation, the relation cannot be empty. (Contributed by Alexander van der Vekens, 7-Jul-2018.) |
7-Jul-2018 | nelir 2699 | Inference associated with df-nel 2603. (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | neli 2698 | Inference associated with df-nel 2603. (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | nesymir 2643 | Inference associated with nesym 2641. (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | nesymi 2642 | Inference associated with nesym 2641. (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | nesym 2641 | Characterization of inequality in terms of reversed equality (see bicom 193). (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | neir 2605 | Inference associated with df-ne 2602. (Contributed by BJ, 7-Jul-2018.) |
7-Jul-2018 | neii 2604 | Inference associated with df-ne 2602. (Contributed by BJ, 7-Jul-2018.) |
6-Jul-2018 | df-rusgra 28369 | Define the set of k-regular undirected simple graphs. (Contributed by Alexander van der Vekens, 6-Jul-2018.) |
RegUSGrph USGrph RegGrph | ||
6-Jul-2018 | df-rgra 28368 | Define the set of k-regular "graphs". (Contributed by Alexander van der Vekens, 6-Jul-2018.) |
RegGrph VDeg | ||
5-Jul-2018 | swdeq 28197 | If two words have the same prefix, their symbols are identical with this prefix. (Contributed by Alexander van der Vekens, 5-Jul-2018.) |
Word Word substr substr ..^ | ||
3-Jul-2018 | usg2wlkeq 28305 | Conditions for which two walks within the same undirected simple graph are the same. It is sufficient that the vertices (in the same order) are identical. (Contributed by Alexander van der Vekens, 3-Jul-2018.) |
USGrph Walks Walks | ||
1-Jul-2018 | 2wlkeq 28304 | Conditions for which two walks (within the same graph) are the same. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
Walks Walks ..^ | ||
1-Jul-2018 | wlklenfislenpm1 28300 | The number of edges of a walk (in an undirected graph) is the number of its vertices minus 1. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
Walks | ||
1-Jul-2018 | 2wrdeq 28176 | Two words are equal if and only if they have the same length and the same symbols at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
Word Word ..^ | ||
1-Jul-2018 | 2ffzoeq 28141 | Two functions over a zero-based half-open integer range are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
..^ ..^ ..^ | ||
1-Jul-2018 | fzoopth 28140 | A half-open range of integers can represent an ordered pair, analogous to fzopth 11090. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
..^ ..^ | ||
1-Jul-2018 | el2fzo 28139 | The lower limit of a half-open range of integers which is equal to a non-empty empty half-open range of integers is element of the half-open range. (Contributed by Alexander van der Vekens, 1-Jul-2018.) |
..^ ..^ ..^ | ||
30-Jun-2018 | wlkop 28298 | A walk (in an undirected simple graph) is an ordered pair. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
Walks | ||
30-Jun-2018 | relwlk 28297 | The walks (in an undirected simple graph) are (ordered) pairs. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
Walks | ||
30-Jun-2018 | 2ffzeq 28122 | Two functions over a zero-based finite interval of integers are equal if and only if their domains have the same length and the function values are the same at each position. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
30-Jun-2018 | f0bi 28076 | A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018.) |
30-Jun-2018 | sbceq1dd 3168 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.) |
30-Jun-2018 | sbceq1d 3167 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by NM, 30-Jun-2018.) |
29-Jun-2018 | wlklenpislenfp1 28299 | The number of vertices of a walk (in an undirected graph) is the number of its edges plus 1. (Contributed by Alexander van der Vekens, 29-Jun-2018.) |
Walks | ||
28-Jun-2018 | lstccats1fst 28264 | The last symbol of a non-empty word concatenated with its first symbol is the first symbol. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
Word LastS concat concat | ||
28-Jun-2018 | ccats1swrdid 28192 | A non-empty word is the prefix of the word concatenated with its first symbol. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
Word concat substr | ||
28-Jun-2018 | wrdlenccats1lenm1 28181 | The length of a non-empty word is the length of the word concatenated with its first symbol minus 1. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
Word concat | ||
28-Jun-2018 | wrdsymb1 28175 | The first symbol within a non-empty word over a set belongs to this set. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
Word | ||
28-Jun-2018 | wrdsymb 28174 | A symbol within a word over a set belongs to this set. (Contributed by Alexander van der Vekens, 28-Jun-2018.) |
Word ..^ | ||
25-Jun-2018 | fz0hash 28169 | The value of the size function on a finite 0-based sequence. (Contributed by Alexander van der Vekens, 25-Jun-2018.) |
24-Jun-2018 | swrd0fvls 28265 | The last symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
Word LastS substr | ||
24-Jun-2018 | 3an4anass 28050 | Associative law for four conjunctions with a triple conjunction. (Contributed by Alexander van der Vekens, 24-Jun-2018.) |
24-Jun-2018 | sbcom 2165 | A commutativity law for substitution. (Contributed by NM, 27-May-1997.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) |
24-Jun-2018 | sbied 2151 | Conversion of implicit substitution to explicit substitution (deduction version of sbie 2150). (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 24-Jun-2018.) |
23-Jun-2018 | wlkcompim 28303 | Implications for the properties of the components of a walk. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
Walks Word ..^ | ||
23-Jun-2018 | wlkcomp 28302 | A walk expressed by properties of its components. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
Walks Word ..^ | ||
23-Jun-2018 | iswlkg 28301 | Generalisation of iswlk 21528: Properties of a pair of functions to be a walk (in an undirected graph). (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
Walks Word ..^ | ||
23-Jun-2018 | wlkelwrd 28296 | The components of a walk are words/functions over a zero based range of integers. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
Walks Word | ||
23-Jun-2018 | elopaelxp 28071 | Membership in an ordered pair class builder implies membership in a cross product. (Contributed by Alexander van der Vekens, 23-Jun-2018.) |
19-Jun-2018 | ftc2nc 26290 | Choice-free proof of ftc2 19929. (Contributed by Brendan Leahy, 19-Jun-2018.) |
19-Jun-2018 | ftc1anclem2 26282 | Lemma for ftc1anc 26289- restriction of an integrable function to the absolute value of its real or imaginary part. (Contributed by Brendan Leahy, 19-Jun-2018.) |
19-Jun-2018 | itgabsnc 26275 | Choice-free analogue of itgabs 19727. (Contributed by Brendan Leahy, 19-Nov-2017.) (Revised by Brendan Leahy, 19-Jun-2018.) |
MblFn MblFn | ||
18-Jun-2018 | wrdlenge2n0 28177 | A word with length at least 2 is not empty. (Contributed by Alexander van der Vekens, 18-Jun-2018.) |
Word | ||
18-Jun-2018 | ftc1anclem1 26281 | Lemma for ftc1anc 26289- the absolute value of a real-valued measurable function is measurable. Would be trivial with cncombf 19551, but this proof avoids ax-cc 8316. (Contributed by Brendan Leahy, 18-Jun-2018.) |
MblFn MblFn | ||
17-Jun-2018 | uzletr 28104 | An upper integer is also an upper integer with a smaller bound. (Contributed by Alexander van der Vekens, 17-Jun-2018.) |
17-Jun-2018 | ftc1anclem5 26285 | Lemma for ftc1anc 26289, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.) |
17-Jun-2018 | ftc1anclem4 26284 | Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 17-Jun-2018.) |
16-Jun-2018 | swrdtrcfvl 28266 | The last symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
Word LastS substr | ||
16-Jun-2018 | swrdtrcfv0 28196 | The first symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
Word substr | ||
16-Jun-2018 | swrdtrcfv 28195 | A symbol in a word truncated by one symbol. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
Word ..^ substr | ||
16-Jun-2018 | swrd0fv0 28194 | The first symbol in a left-anchored subword. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
Word substr | ||
16-Jun-2018 | swrd0fv 28193 | A symbol in an left-anchored subword, indexed using the subword's indices. (Contributed by Alexander van der Vekens, 16-Jun-2018.) |
Word ..^ substr | ||
16-Jun-2018 | wlimss 25581 | The class of limit points is a subclass of the base class. (Contributed by Scott Fenton, 16-Jun-2018.) |
WLim | ||
16-Jun-2018 | wsuclb 25580 | A well-founded successor is a lower bound on points after . (Contributed by Scott Fenton, 16-Jun-2018.) |
Se wsuc | ||
16-Jun-2018 | wsucex 25578 | Existence theorem for well-founded successor. (Contributed by Scott Fenton, 16-Jun-2018.) |
wsuc | ||
15-Jun-2018 | fzisfzounsn 28138 | A finite interval of integers as union of a half-open range of integers and a singleton. (Contributed by Alexander van der Vekens, 15-Jun-2018.) |
..^ | ||
15-Jun-2018 | fzofzim 28137 | If a non-negative integer in a finite interval of integers is not the upper bound of the interval, it is contained in the corresponding half-open range of integers. (Contributed by Alexander van der Vekens, 15-Jun-2018.) |
..^ | ||
15-Jun-2018 | wsuccl 25579 | If is a set with an successor in , then its well-founded successor is a member of . (Contributed by Scott Fenton, 15-Jun-2018.) |
Se wsuc | ||
15-Jun-2018 | wsuclem 25577 | Lemma for the supremum properties of well-founded successor. (Contributed by Scott Fenton, 15-Jun-2018.) |
Se | ||
15-Jun-2018 | elwlim 25575 | Membership in the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim | ||
15-Jun-2018 | nfwlim 25574 | Bound-variable hypothesis builder for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim | ||
15-Jun-2018 | wlimeq2 25573 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim WLim | ||
15-Jun-2018 | wlimeq1 25572 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim WLim | ||
15-Jun-2018 | wlimeq12 25571 | Equality theorem for the limit class. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim WLim | ||
15-Jun-2018 | df-wlim 25565 | Define the class of limit points of a well-founded set. (Contributed by Scott Fenton, 15-Jun-2018.) |
WLim | ||
13-Jun-2018 | sineq0ALT 29050 | A complex number whose sine is zero is an integer multiple of . The Virtual Deduction form of the proof is http://www.virtualdeduction.com/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 29050. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 20430. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/sineq0altro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) |
13-Jun-2018 | not12an2impnot1 28660 | If a double conjunction is false and the second conjunct is true, then the first conjunct is false. http://www.virtualdeduction.com/not12an2impnot1vd.html is the Virtual Deduction proof verified by automatically transforming it into the Metamath proof of not12an2impnot1 28660 using completeusersproof, which is verified by the Metamath program. http://www.virtualdeduction.com/not12an2impnot1ro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) |
13-Jun-2018 | wzel 25576 | The zero of a well-founded set is a member of that set. (Contributed by Scott Fenton, 13-Jun-2018.) |
Se | ||
13-Jun-2018 | nfwsuc 25570 | Bound-variable hypothesis builder for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc | ||
13-Jun-2018 | wsuceq3 25569 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc wsuc | ||
13-Jun-2018 | wsuceq2 25568 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc wsuc | ||
13-Jun-2018 | wsuceq1 25567 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc wsuc | ||
13-Jun-2018 | wsuceq123 25566 | Equality theorem for well-founded successor. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc wsuc | ||
13-Jun-2018 | df-wsuc 25564 | Define the concept of a successor in a well-founded set. (Contributed by Scott Fenton, 13-Jun-2018.) |
wsuc | ||
13-Jun-2018 | dfpred3g 25451 | An alternate definition of predecessor class when is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
13-Jun-2018 | dfpred3 25450 | An alternate definition of predecessor class when is a set. (Contributed by Scott Fenton, 13-Jun-2018.) |
13-Jun-2018 | predeq123 25441 | Equality theorem for the predecessor class. (Contributed by Scott Fenton, 13-Jun-2018.) |
13-Jun-2018 | socnv 25389 | The converse of a strict ordering is still a strict ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
13-Jun-2018 | pocnv 25388 | The converse of a partial ordering is still a partial ordering. (Contributed by Scott Fenton, 13-Jun-2018.) |
13-Jun-2018 | supeq3 7455 | Equality theorem for supremum. (Contributed by Scott Fenton, 13-Jun-2018.) |
12-Jun-2018 | suctr 4666 | The sucessor of a transitive class is transitive. The proof of http://www.virtualdeduction.com/suctrvd.html is a Virtual Deduction proof verified by automatically transforming it into the Metamath proof of suctr 4666 using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/suctrro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 11-Apr-2009.) See suctrALT 4665 for the original proof before this revision. (Revised by Alan Sare, 12-Jun-2018.) (Proof modification is discouraged.) |
9-Jun-2018 | fz0addcom 28114 | The addition of two members of a finite set of sequential integers starting at 0 is commutative. (Contributed by Alexander van der Vekens, 22-May-2018.) (Revised by Alexander van der Vekens, 9-Jun-2018.) |
9-Jun-2018 | nfwrecs 25534 | Bound-variable hypothesis builder for the well-founded recursive function generator. (Contributed by Scott Fenton, 9-Jun-2018.) |
wrecs | ||
9-Jun-2018 | nfpred 25445 | Bound-variable hypothesis builder for the predecessor class. (Contributed by Scott Fenton, 9-Jun-2018.) |
8-Jun-2018 | cshwsexa 28292 | The class of (different!) words resulting by cyclically shifting something (not necessarily a word) is a set. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift | ||
8-Jun-2018 | cshwssize 28291 | If a word has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word or 1. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift | ||
8-Jun-2018 | cshwssizensame 28290 | If a word (not consisting of identical symbols) has a length being a prime number, the size of the set of (different!) words resulting by cyclically shifting the original word equals the length of the original word. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift ..^ | ||
8-Jun-2018 | cshwssizesame 28289 | If a word consists of identical symbols, the size of the set of (different!) words resulting by cyclically shifting the original word (not necessarily of length being a prime number) equals 1. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift ..^ | ||
8-Jun-2018 | cshwsex 28288 | The class of (different!) words resulting by cyclically shifting a given word (not necessarily of length being a prime number) is a set. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift | ||
8-Jun-2018 | cshwsiun 28287 | The set of (different!) words resulting by cyclically shifting a given word (not necessarily of length being a prime number) is an indexed union. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word Word ..^ CyclShift ..^ CyclShift | ||
8-Jun-2018 | cshwsdisj 28286 | The singletons resulting by cyclically shifting a given word of length being a prime number and not consisting of identical symbols is a disjoint collection. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ Disj ..^ CyclShift | ||
8-Jun-2018 | cshwssizelem4 28285 | If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ ..^ ..^ CyclShift CyclShift | ||
8-Jun-2018 | cshwssizelem4a 28284 | If cyclically shifting a word of length being a prime number and not of identical symbols by different numbers of positions, the resulting words are different. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ ..^ ..^ CyclShift CyclShift | ||
8-Jun-2018 | cshwssizelem3 28283 | If cyclically shifting a word of length being a prime number not consisting of identical symbols by at least one position (and not by as many positions as the length of the word), the result will not be the word itself. (Contributed by Alexander van der Vekens, 19-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ ..^ CyclShift | ||
8-Jun-2018 | cshwssizelem2 28282 | If cyclically shifting a word of length being a prime number results in the word itself, the shift must be either by 0 or by as much positions as the length of the word or the word must be build of identical symbols. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word CyclShift ..^ | ||
8-Jun-2018 | cshwssizelem1 28281 | If cyclically shifting a word of length being a prime number by at least two positions (and not by as many positions as the length of the word) results in the word itself, the word is build of identical symbols. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ CyclShift ..^ | ||
8-Jun-2018 | cshwssizelem1a 28280 | If cyclically shifting a word of length being a prime number by at least two positions (and not by as much positions as the length of the word) results in the word itself, the word is build of identical symbols, with the possible exception of the first one. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ CyclShift ..^ | ||
8-Jun-2018 | cshwsame0 28279 | If cyclically shifting a word consisting of identical symbols by different amounts of positions, the resulting words are identical. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ ..^ ..^ CyclShift CyclShift | ||
8-Jun-2018 | cshwsame 28278 | Cyclically shifting a word consisting of identical symbols results in the word itself. (Contributed by Alexander van der Vekens, 18-May-2018.) (Revised by Alexander van der Vekens, 8-Jun-2018.) |
Word ..^ ..^ CyclShift | ||
8-Jun-2018 | 2cshwmod 28258 | Cyclically shifting a word two times using . (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Word CyclShift CyclShift CyclShift | ||
8-Jun-2018 | 2txmodxeq0 28163 | Two times a positive real number module the real number is zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | fz0addge0 28121 | The sum of two integers in zero based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | 2eluzge1 28103 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | 2eluzge0 28102 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | 1eluzge0 28101 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | ltnltne 28095 | Variant of trichotomy law for 'less than'. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | 2txmxeqx 28091 | Two times a complex number minus the number itself results in the number itself. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
8-Jun-2018 | wfrlem6 25544 | Lemma for well-founded recursion. The definition generates a relationship. (Contributed by Scott Fenton, 8-Jun-2018.) |
wrecs | ||
7-Jun-2018 | cshw1v 28277 | If cyclically shifting a (not empty) word by 1 position results in the word itself, the word is build of identical symbols. (Contributed by Alexander van der Vekens, 14-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word CyclShift ..^ | ||
7-Jun-2018 | cshw1 28276 | If cyclically shifting a word by 1 position results in the word itself, the word is build of identical symbols. Remark: also "valid" for an empty word! (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word CyclShift ..^ | ||
7-Jun-2018 | cshweqrep 28275 | If cyclically shifting a word by L position results in the word itself, the symbol at any position is repeated at multiples of L (modulo the length of the word) positions in the word. (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word ..^ CyclShift ..^ | ||
7-Jun-2018 | cshwsym 28274 | If cyclically shifting a word A by n positions results in word B, then cyclically shifting the word B by (N-n) positions results in word A. (Contributed by Alexander van der Vekens, 22-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word CyclShift CyclShift | ||
7-Jun-2018 | cshweqdifid 28273 | If cyclically shifting a word by two positions results in the same word, cyclically shifting the word by the difference of these two positions results in the original word itself. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word CyclShift CyclShift CyclShift | ||
7-Jun-2018 | cshweqdif2s 28272 | If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by Alexander van der Vekens, 22-Apr-2018.) (Revised by Alexander van der Vekens, 7-Jun-2018.) |
Word Word CyclShift CyclShift CyclShift | ||
7-Jun-2018 | wrecseq3 25537 | Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
wrecs wrecs | ||
7-Jun-2018 | wrecseq2 25536 | Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
wrecs wrecs | ||
7-Jun-2018 | wrecseq1 25535 | Equality theorem for the well-founded recusive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
wrecs wrecs | ||
7-Jun-2018 | wrecseq123 25533 | General equality theorem for the well-founded recursive function generator. (Contributed by Scott Fenton, 7-Jun-2018.) |
wrecs wrecs | ||
7-Jun-2018 | df-wrecs 25532 | Here we define the well-founded recusive function generator. This is similar to recs, but works with arbitrary well-founded relationships. (Contributed by Scott Fenton, 7-Jun-2018.) (New usage is discouraged.) |
wrecs | ||
6-Jun-2018 | cshweqdif2 28271 | If cyclically shifting two words (of the same length) results in the same word, cyclically shifting one of the words by the difference of the numbers of shifts results in the other word. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 6-Jun-2018.) |
Word Word CyclShift CyclShift CyclShift | ||
6-Jun-2018 | 3cshw 28270 | Cyclically shifting a word three times results in a once cyclically shifted word under certain circumstances. (Contributed by Alexander van der Vekens, 6-Jun-2018.) |
Word CyclShift CyclShift CyclShift CyclShift | ||
6-Jun-2018 | fz0fzdiffz0 28120 | The difference of a nonnegative integer in a finite set of sequential integers and a member of a finite set of sequential integers with the same upper bound and the nonnegative integer as lower bound is a member of the finite set of sequential integers. (Contributed by Alexander van der Vekens, 6-Jun-2018.) |
5-Jun-2018 | cshwleneq 28269 | If the results of cyclically shifting two words are equal, the length of the two words was equal. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.) |
Word Word CyclShift CyclShift | ||
5-Jun-2018 | 2cshwcom 28268 | Cyclically shifting a word two times is commutative. (Contributed by Alexander van der Vekens, 21-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.) |
Word CyclShift CyclShift CyclShift CyclShift | ||
5-Jun-2018 | lswrdcshw 28267 | The last symbol of a word cyclically shifted by N positions is the symbol at index (N-1) of the original word. (Contributed by Alexander van der Vekens, 21-Mar-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.) |
Word ..^ LastS CyclShift | ||
5-Jun-2018 | 2cshwid 28259 | Cyclically shifting a word two times resulting in the word itself. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 5-Jun-2018.) |
Word CyclShift CyclShift | ||
4-Jun-2018 | 2cshw 28257 | Cyclically shifting a word two times. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.) |
Word CyclShift CyclShift CyclShift CyclShift | ||
4-Jun-2018 | 2cshw2 28256 | Cyclically shifting a word two times (with "overflow"). (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.) |
Word CyclShift CyclShift CyclShift | ||
4-Jun-2018 | 2cshw2lem3 28255 | Lemma 3 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 6-Apr-2018.) (Revised by Alexander van der Vekens, 4-Jun-2018.) |
Word substr concat substr concat substr CyclShift | ||
1-Jun-2018 | 2cshw2lem2 28254 | Lemma 2 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 1-Jun-2018.) |
Word substr concat substr substr substr concat substr | ||
31-May-2018 | 2cshw2lem1 28253 | Lemma 1 for 2cshw2 28256. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
Word substr concat substr substr substr | ||
31-May-2018 | 2cshw1 28252 | Cyclically shifting a word two times (without "overflow"). (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
Word CyclShift CyclShift CyclShift | ||
31-May-2018 | 2cshw1lem2 28250 | Lemma 2 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
Word substr concat substr substr substr | ||
31-May-2018 | 2cshw1lem1 28249 | Lemma 1 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
Word substr concat substr substr substr concat substr | ||
31-May-2018 | swrdccatin12d 28223 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.) |
Word Word concat substr substr concat substr | ||
31-May-2018 | swrdccatin2d 28222 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.) |
Word Word concat substr substr | ||
31-May-2018 | swrdccatin1d 28221 | The subword of a concatenation of two words within the first of the concatenated words. (Contributed by Alexander van der Vekens, 31-May-2018.) |
Word Word concat substr substr | ||
31-May-2018 | 2elfz2melfz 28118 | If the sum of two integers of a finite set of sequential nonnegative integers is greater than the upper bound, the difference between one of the integers and the difference between the upper bound and the other integer is in the finite set of sequential nonnegative integers right bounded by the first integer. (Contributed by Alexander van der Vekens, 7-Apr-2018.) (Revised by Alexander van der Vekens, 31-May-2018.) |
31-May-2018 | elfzubelfz 28117 | If there is a member in a finite set of sequential integers, the upper bound is also a member of this finite set of sequential integers. (Contributed by Alexander van der Vekens, 31-May-2018.) |
31-May-2018 | ftc1anclem6 26286 | Lemma for ftc1anc 26289- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued . (Contributed by Brendan Leahy, 31-May-2018.) |
30-May-2018 | 4an4132 28583 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) |
30-May-2018 | 4an31 28582 | A rearrangement of conjuncts for a 4-right-nested conjunction. (Contributed by Alan Sare, 30-May-2018.) |
30-May-2018 | 4animp1 28581 | A single hypothesis unification deduction with an assertion which is an implication with a 4-right-nested conjunction antecedent. (Contributed by Alan Sare, 30-May-2018.) |
30-May-2018 | swrdccat3b 28220 | A suffix of a concatenation is either a suffix of the second concatenated word or a concatenation of a suffix of the first word with the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 30-May-2018.) |
Word Word concat substr substr substr concat | ||
30-May-2018 | swrdccat3blem 28219 | Lemma for swrdccat3b 28220. (Contributed by Alexander van der Vekens, 30-May-2018.) |
Word Word substr substr concat substr | ||
30-May-2018 | leaddle0 28094 | If adding a real number to a real number results in a value less then the second real number, the first real number must be not positive. (Contributed by Alexander van der Vekens, 30-May-2018.) |
29-May-2018 | swrdccat3a 28218 | A prefix of a concatenation is either a prefix of the first concatenated word or a concatenation of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 31-Mar-2018.) (Revised by Alexander van der Vekens, 29-May-2018.) |
Word Word concat substr substr concat substr | ||
29-May-2018 | swrdccat 28217 | The subword of a concatenation of two words as concatenation of subwords of the two concatenated words. (Contributed by Alexander van der Vekens, 29-May-2018.) |
Word Word concat substr substr concat substr | ||
29-May-2018 | ftc1anclem8 26288 | Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 29-May-2018.) |
28-May-2018 | swrdccat3 28216 | The subword of a concatenation is either a subword of the first concatenated word or a subword of the second concatenated word or a concatenation of a suffix of the first word with a prefix of the second word. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 28-May-2018.) |
Word Word concat substr substr substr substr concat substr | ||
27-May-2018 | swrdccatin12 28215 | The subword of a concatenation of two words within both of the concatenated words. (Contributed by Alexander van der Vekens, 5-Apr-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
Word Word concat substr substr concat substr | ||
27-May-2018 | swrdccatin12lem4 28214 | Lemma 4 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
Word Word ..^ ..^ concat substr substr | ||
27-May-2018 | swrdccatin12lem3 28213 | Lemma 3 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
Word Word ..^ ..^ concat substr substr substr | ||
27-May-2018 | swrdccatin12lem3c 28212 | Lemma for swrdccatin12lem3 28213 and swrdccatin12lem4 28214. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
Word Word concat Word concat | ||
27-May-2018 | swrdccatin2 28211 | The subword of a concatenation of two words within the second of the concatenated words. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
Word Word concat substr substr | ||
27-May-2018 | swrdccatin12lem3b 28210 | Lemma 2 for swrdccatin12lem3 28213. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
..^ ..^ ..^ | ||
27-May-2018 | swrdccatin12lem3a 28209 | Lemma 1 for swrdccatin12lem3 28213. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 27-May-2018.) |
..^ ..^ ..^ | ||
27-May-2018 | swrdccatfn 28205 | The subword of a concatenation as function. (Contributed by Alexander van der Vekens, 27-May-2018.) |
Word Word concat substr ..^ | ||
27-May-2018 | fzmmmeqm 28116 | Subtracting the difference of a member of a finite range of integers and the lower bound of the range from the difference of the upper bound and the lower bound of the range equals the difference of the upper bound of the range and the member. (Contributed by Alexander van der Vekens, 27-May-2018.) |
27-May-2018 | elfz0fzfz0 28115 | A member of a finite set of sequential integers starting at 0 is a member of a finite set of sequential integers from 0 to a member of a finite set of sequential integers starting at the right border of the first finite set of sequential integers. (Contributed by Alexander van der Vekens, 27-May-2018.) |
27-May-2018 | ftc1anclem3 26283 | Lemma for ftc1anc 26289- the absolute value of the sum of a simple function and times another simple function is itself a simple function. (Contributed by Brendan Leahy, 27-May-2018.) |
26-May-2018 | swrdvalodm2 28189 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 26-May-2018.) |
Word substr | ||
26-May-2018 | ccatsymb 28180 | The symbol at a given position in a concatenated word. (Contributed by Alexander van der Vekens, 26-May-2018.) |
Word Word concat | ||
26-May-2018 | wrdsymb0 28171 | A symbol at a position "outside" of a word. (Contributed by Alexander van der Vekens, 26-May-2018.) |
Word | ||
25-May-2018 | elfz2z 28106 | Membership of an integer in a finite set of sequential integers starting at 0. (Contributed by Alexander van der Vekens, 25-May-2018.) |
25-May-2018 | jaoi3 28049 | Inference separating a disjunct of an antecedent. (Contributed by Alexander van der Vekens, 25-May-2018.) |
24-May-2018 | ax7w18AUX7 29678 | Weak version of ax-7 1750 not requiring ax-7 1750. (Contributed by NM, 24-May-2018.) |
24-May-2018 | ax7w17lem2AUX7 29677 | Experimental lemma with the goal of deriving hbae 2041 from ax-7v 29443. Looks like a dead end because we apparently need hbae 2041 to eliminate the first 2 hypotheses for those that satisfy the 3rd and 4th hypotheses. (Contributed by NM, 24-May-2018.) |
24-May-2018 | ax7w17lem1AUX7 29676 | Lemma for ax7w17lem2AUX7 29677. (Contributed by NM, 24-May-2018.) |
24-May-2018 | ax7w16AUX7 29675 | Special case of ax-7 1750 derived from ax-7v 29443. This is the "easy" direction. The other direction is still conjectured. (Contributed by NM, 24-May-2018.) |
24-May-2018 | nfsbdwAUX7 29579 | Deduction version of nfsbwAUX7 29666. (Contributed by NM, 24-May-2018.) |
24-May-2018 | swrdvalodm 28190 | Value of the subword extractor outside its intended domain. (Contributed by Alexander van der Vekens, 24-May-2018.) |
Word substr | ||
24-May-2018 | swrdvalodmlem1 28188 | Lemma for swrdvalodm 28190. (Contributed by Alexander van der Vekens, 24-May-2018.) |
..^ ..^ | ||
23-May-2018 | ax7w15lemxAUX7 29667 | Lemma for ax7w14AUX7 29671. (Contributed by NM, 23-May-2018.) |
23-May-2018 | swrdccatin12lem2 28208 | Lemma 2 for swrdccatin12 28215. (Contributed by Alexander van der Vekens, 30-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
..^ ..^ ..^ | ||
23-May-2018 | swrdccat3a0 28204 | The subword of a concatenation of an empty word with another word is the subword of the second concatenated word. (Contributed by Alexander van der Vekens, 27-Mar-2018.) (Revised by Alexander van der Vekens, 23-May-2018.) |
Word concat substr substr | ||
22-May-2018 | ax7w14AUX7 29671 | Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 22-May-2018.) |
22-May-2018 | ax7w14lemAUX7 29670 | Lemma for ax7w14AUX7 29671. (Contributed by NM, 22-May-2018.) |
22-May-2018 | ax7w15AUX7 29669 | Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 22-May-2018.) |
22-May-2018 | ax7w15lemAUX7 29668 | Lemma for ax7w15AUX7 29669. (Contributed by NM, 22-May-2018.) |
22-May-2018 | nfsbwAUX7 29666 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Revised by NM, 22-May-2018.) |
22-May-2018 | dvelimfwAUX7 29665 | Version of dvelimvNEW7 29463. (Contributed by Mario Carneiro, 6-Oct-2016.) (Revised by NM, 22-May-2018.) |
22-May-2018 | sb8dwAUX7 29591 | Weak version of sb8 2169 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.) |
22-May-2018 | sb8iwAUX7 29590 | Version of sb8 2169 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.) |
22-May-2018 | cbv3dwAUX7 29517 | Weak deduction version of cbv3 1972 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.) |
22-May-2018 | cbvaldwAUX7 29516 | Weak version of cbvald 1987 not requiring ax-7 1750. (Contributed by NM, 22-May-2018.) |
22-May-2018 | 2cshw1lem3 28251 | Lemma 3 for 2cshw1 28252. (Contributed by Alexander van der Vekens, 1-Apr-2018.) (Revised by Alexander van der Vekens, 22-May-2018.) |
Word substr concat substr concat substr CyclShift | ||
21-May-2018 | ax7w13AUX7 29674 | Special case of ax-7 1750 derived from ax-7v 29443. Example illustrating use of ax7w12AUX7 29672. (Contributed by NM, 21-May-2018.) |
21-May-2018 | elsb34AUX7 29673 | Substitution applied to an atomic membership wff. (Contributed by NM, 21-May-2018.) |
21-May-2018 | ax7w12AUX7 29672 | Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 21-May-2018.) |
21-May-2018 | cshwidxn 28248 | The symbol at index (n-1) of a cyclically shifted word of length n (not 0) is the symbol at index (N-1) of the original word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
..^ Word CyclShift | ||
21-May-2018 | cshwidxm 28247 | The symbol at index (n-N) of a cyclically shifted word of length n (not 0) is the symbol at index 0 of the original word. (Contributed by Alexander van der Vekens, 18-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word ..^ CyclShift | ||
21-May-2018 | cshwidxm1 28246 | The symbol at index ((n-N)-1) of a cyclically shifted word of length n (not 0) is the symbol at index (n-1) of the original word. (Contributed by Alexander van der Vekens, 23-Mar-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word ..^ CyclShift | ||
21-May-2018 | cshwidx0 28245 | The symbol at index 0 of a cyclically shifted word is the symbol at index N of the original word. (Contributed by Alexander van der Vekens, 15-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word ..^ CyclShift | ||
21-May-2018 | cshwidxmod 28244 | The symbol at a given index of a cyclically shifted word is the symbol at the shifted index of the original word. (Contributed by Alexander van der Vekens, 13-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word ..^ ..^ CyclShift | ||
21-May-2018 | cshwidx 28243 | The symbol at a given index of a cyclically shifted word is the symbol at the shifted index of the original word. (Contributed by Alexander van der Vekens, 17-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word ..^ ..^ CyclShift | ||
21-May-2018 | cshwcl 28241 | A cyclically shifted word is a word over the same set as for the original word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word CyclShift Word | ||
21-May-2018 | cshwoor 28238 | A cyclically shifted word is the empty set if the number of shifts is out of the range of the word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 21-May-2018.) |
Word CyclShift | ||
21-May-2018 | cshnnn0 28237 | A cyclical shift is the empty set if the number of shifts is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
CyclShift | ||
21-May-2018 | modifeq2int 28162 | If a nonnegative integer is less than the double of a positive integer, the nonnegative integer modulo the positive integer equals the nonnegative integer or the nonnegative integer minus the positive integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
21-May-2018 | subsubelfzo0 28136 | Subtracting a difference from a number which is not less than the difference results in a bounded nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
..^ ..^ ..^ | ||
21-May-2018 | elfzonn0 28123 | A member of a half-open integer range starting at 0 is a nonnegative integer. (Contributed by Alexander van der Vekens, 21-May-2018.) |
..^ | ||
21-May-2018 | 2leaddle2 28093 | If two real numbers are less than a third real number, the sum of the real numbers is less then twice the third real number. (Contributed by Alexander van der Vekens, 21-May-2018.) |
21-May-2018 | fvifeq 28077 | Equality of function values with conditional arguments, see also fvif 5744. (Contributed by Alexander van der Vekens, 21-May-2018.) |
21-May-2018 | axio 2408 | Definition of 'or' (intuitionistic logic axiom ax-io). (Contributed by Jim Kingdon, 21-May-2018.) |
21-May-2018 | axin2 2407 | 'Not' elimination (intuitionistic logic axiom ax-in2). (Contributed by Jim Kingdon, 21-May-2018.) |
21-May-2018 | axin1 2406 | 'Not' introduction (intuitionistic logic axiom ax-in1). (Contributed by Jim Kingdon, 21-May-2018.) |
21-May-2018 | axia3 2405 | 'And' introduction (intuitionistic logic axiom ax-ia3). (Contributed by Jim Kingdon, 21-May-2018.) |
21-May-2018 | axia2 2404 | Right 'and' elimination (intuitionistic logic axiom ax-ia2). (Contributed by Jim Kingdon, 21-May-2018.) |
21-May-2018 | axia1 2403 | Left 'and' elimination (intuitionistic logic axiom ax-ia1). (Contributed by Jim Kingdon, 21-May-2018.) |
20-May-2018 | ax7w11AUX7 29664 | Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 20-May-2018.) |
20-May-2018 | ax7w10AUX7 29663 | Special case of ax-7 1750 derived from ax-7v 29443. (Contributed by NM, 20-May-2018.) |
20-May-2018 | cshwlen 28242 | The length of a cyclically shifted word is the same as the length of the original word. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.) |
Word CyclShift | ||
20-May-2018 | cshwn 28240 | A word cyclically shifted by its length is the word itself. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.) |
Word CyclShift | ||
20-May-2018 | cshw0 28239 | A word cyclically shifted by 0 is the word itself. (Contributed by Alexander van der Vekens, 16-May-2018.) (Revised by Alexander van der Vekens, 20-May-2018.) |
Word CyclShift | ||
20-May-2018 | cshword 28236 | Perform a cyclic shift for a word. (Contributed by Alexander van der Vekens, 20-May-2018.) |
Word CyclShift substr concat substr | ||
20-May-2018 | cshfn 28235 | Perform a cyclic shift for a function over a range of nonnegative integers. (Contributed by Alexander van der Vekens, 20-May-2018.) |
..^ CyclShift substr concat substr | ||
20-May-2018 | df-csh 28233 | Perform a cyclic shift for an arbitrary class. Meaningful only for words Word or at least functions over an half-open range of nonnegative integers. The result is also only meaningful if . (Contributed by Alexander van der Vekens, 20-May-2018.) |
CyclShift ..^ substr concat substr | ||
19-May-2018 | fzonmapblen 28135 | The result of subtracting a nonnegative integer from a positive integer and adding another nonnegative integer which is less than the first one, is less then the positive integer. (Contributed by Alexander van der Vekens, 19-May-2018.) |
..^ ..^ | ||
18-May-2018 | fzo0sn0fzo1 28126 | A half open integer range starting from 0 is the union of the singleton set containing 0 and a half open integer range starting from 1. (Contributed by Alexander van der Vekens, 18-May-2018.) |
..^ ..^ | ||
17-May-2018 | modprm0g 28230 | For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.) |
..^ ..^ ..^ | ||
17-May-2018 | modprm0 28229 | For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.) |
..^ ..^ ..^ | ||
17-May-2018 | modprminveq 28227 | The modular inverse of is unique. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modprm1div 28225 | A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | prmgt1 28224 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modidmul0 28161 | The product of an integer and a positive integer is 0 modulo the positive integer. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modaddmulmod 28159 | The sum of a real number and the product of a second real number modulo a positive real number and an integer equals the sum of the real number and the product of the other real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modmulmod 28158 | The product of a real number modulo a positive real number and an integer equals the product of the real number and the integer modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modsubmodmod 28157 | The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modsubmod 28156 | The difference of a real number modulo a positive real number and another real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
17-May-2018 | modadd2mod 28155 | The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018.) |
15-May-2018 | modprminv 28226 | Show an explicit expression for the modular inverse of . This is an application of prmdiv 13175. (Contributed by Alexander van der Vekens, 15-May-2018.) |
15-May-2018 | modid0 28160 | A positive real number modulo itself is 0 . (Contributed by Alexander van der Vekens, 15-May-2018.) |
14-May-2018 | exdistrf 2067 | Distribution of existential quantifiers, with a bound-variable hypothesis saying that is not free in , but can be free in (and there is no distinct variable condition on and ). (Contributed by Mario Carneiro, 20-Mar-2013.) (Proof shortened by Wolf Lammen, 14-May-2018.) |
13-May-2018 | modaddmod 28154 | The sum of a real number modulo a positive real number and another real number equals the sum of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.) |
13-May-2018 | 2submod 28153 | If a real number is between a positive real number and the double of the positive real number, the real number modulo the positive real number equals the real number minus the positive real number. (Contributed by Alexander van der Vekens, 13-May-2018.) |
13-May-2018 | fzossnn0 28125 | A half open integer range starting from a nonnegative integer is a subset of the nonnegative integers. (Contributed by Alexander van der Vekens, 13-May-2018.) |
..^ | ||
13-May-2018 | ftc1anclem7 26287 | Lemma for ftc1anc 26289. (Contributed by Brendan Leahy, 13-May-2018.) |
13-May-2018 | cbvald 1987 | Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2074. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) |
13-May-2018 | cbv2 1981 | Rule used to change bound variables, using implicit substitution. Revised to align format of hypotheses to common style. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) |
13-May-2018 | cbv1h 1975 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-May-2018.) |
13-May-2018 | cbv1 1974 | Rule used to change bound variables, using implicit substitution. Revised to format hypotheses to common style. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.) |
12-May-2018 | reumodprminv 28228 | For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.) |
..^ | ||
12-May-2018 | cbv3h 1973 | Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
12-May-2018 | cbv3 1972 | Rule used to change bound variables, using implicit substitution, that does not use ax-12o 2220. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
12-May-2018 | spei 1967 | Inference from existential specialization, using implicit substitution. Revised to remove a distinct variable constraint. (Contributed by NM, 19-Aug-1993.) (Proof shortened by Wolf Lammen, 12-May-2018.) |
11-May-2018 | ftc1anc 26289 | ftc1a 19922 holds for functions that obey the triangle inequality in the absence of ax-cc 8316. Theorem 565Ma of [Fremlin5] p. 220. (Contributed by Brendan Leahy, 11-May-2018.) |
11-May-2018 | nfsb4t 2128 | A variable not free remains so after substitution with a distinct variable (closed form of nfsb4 2130). (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
11-May-2018 | dvelimh 2072 | Version of dvelim 2074 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
11-May-2018 | dvelimdf 2071 | Deduction form of dvelimf 2069. This version may be useful if we want to avoid ax-17 1627 and use ax-16 2222 instead. (Contributed by NM, 7-Apr-2004.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
11-May-2018 | dvelimf 2069 | Version of dvelimv 2075 without any variable restrictions. (Contributed by NM, 1-Oct-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 11-May-2018.) |
8-May-2018 | elima4 25405 | Quantifier-free expression saying that a class is a member of an image. (Contributed by Scott Fenton, 8-May-2018.) |
8-May-2018 | snnzb 25403 | A singleton is non-empty iff its argument is a set. (Contributed by Scott Fenton, 8-May-2018.) |
6-May-2018 | opelco3 25404 | Alternate way of saying that an ordered pair is in a composition. (Contributed by Scott Fenton, 6-May-2018.) |
5-May-2018 | wl-nfnbi 26234 | Being free does not depend on an outside negation in an expression. This theorem is slightly more general than nfn 1812 or nfnd 1810. (Contributed by Wolf Lammen, 5-May-2018.) |
5-May-2018 | drnf2 2063 | Formula-building lemma for use with the Distinctor Reduction Theorem. (Contributed by Mario Carneiro, 4-Oct-2016.) (Proof shortened by Wolf Lammen, 5-May-2018.) |
3-May-2018 | brlb 25801 | Binary relationship form of the lower bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
LB | ||
3-May-2018 | brub 25800 | Binary relationship form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018.) |
UB | ||
3-May-2018 | df-lb 25722 | Define the lower bound relationship functor. See brlb 25801 for value. (Contributed by Scott Fenton, 3-May-2018.) |
LB UB | ||
3-May-2018 | df-ub 25721 | Define the upper bound relationship functor. See brub 25800 for value. (Contributed by Scott Fenton, 3-May-2018.) |
UB | ||
3-May-2018 | sbft 2116 | Substitution has no effect on a non-free variable. (Contributed by NM, 30-May-2009.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
3-May-2018 | spsbe 1664 | A specialization theorem. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-May-2018.) |
30-Apr-2018 | sbn 2131 | Negation inside and outside of substitution are equivalent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) |
30-Apr-2018 | dvelimv 2075 | Similar to dvelim 2074 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.) (Proof shortened by Wolf Lammen, 30-Apr-2018.) |
29-Apr-2018 | dveeq1 2022 | Quantifier introduction when one pair of variables is distinct. Revised to be independent of dvelimv 2075. (Contributed by NM, 2-Jan-2002.) (Revised by Wolf Lammen, 29-Apr-2018.) |
29-Apr-2018 | ax12o 2011 | Derive set.mm's original ax-12o 2220 from the shorter ax-12 1951. (Contributed by NM, 29-Nov-2015.) (Revised by NM, 24-Dec-2015.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) |
29-Apr-2018 | nfeqf 2010 | A variable is effectively not free in an equality if it is not either of the involved variables. version of ax-12o 2220. (Contributed by Mario Carneiro, 6-Oct-2016.) (Proof shortened by Wolf Lammen, 29-Apr-2018.) |
29-Apr-2018 | ax12olem4 2009 | Lemma for nfeqf 2010. A technical step to remove a distinct variable constraint from ax12v 1952. (Contributed by Wolf Lammen, 29-Apr-2018.) |
29-Apr-2018 | ax12olem3 2008 | Lemma for nfeqf 2010 and dveeq1 2022. Convert ax12olem2 2007 into a more general form. (Contributed by Wolf Lammen, 29-Apr-2018.) |
29-Apr-2018 | ax12olem2 2007 | Lemma for nfeqf 2010 and dveeq1 2022. This lemma is equivalent to ax12v 1952 with one distinct variable constraint removed. (Contributed by Wolf Lammen, 29-Apr-2018.) |
27-Apr-2018 | wl-aleq 26236 | The semantics of . (Contributed by Wolf Lammen, 27-Apr-2018.) |
27-Apr-2018 | wl-exeq 26235 | The semantics of . (Contributed by Wolf Lammen, 27-Apr-2018.) |
< |