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 8-Dec-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (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.
(3-Oct-2017) Sean B. Palmer 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).
(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.
(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.
(28-Feb-2017) David Moews added a new proof to the 100 theorem list, Product of Segments of Chords chordthm, bringing the Metamath total to 62.
(18-Feb-2017) Filip Cernatescu announced Milpgame 0.1 (MILP: Math is like a puzzle!).
(1-Jan-2017) Saveliy Skresanov added a new proof to the 100 theorem list, Isosceles triangle theorem isosctr, bringing the Metamath total to 61.
(1-Jan-2017) Mario Carneiro added 2 new proofs to the 100 theorem list, L'Hôpital's Rule lhop and Taylor's Theorem taylth, bringing the Metamath total to 60. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
7-Dec-2017 | fprodf1o 24172 | Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.) |
∏ ∏ | ||
7-Dec-2017 | prodfc 24171 | A lemma to facilitate conversions from the function form to the class-variable form of a product. (Contributed by Scott Fenton, 7-Dec-2017.) |
∏ ∏ | ||
7-Dec-2017 | prod2id 24170 | The second class argument to a product can be chosen so that it is always a set. (Contributed by Scott Fenton, 7-Dec-2017.) |
∏ ∏ | ||
7-Dec-2017 | prod1 24169 | Any product of one over a valid set is one. (Contributed by Scott Fenton, 7-Dec-2017.) |
∏ | ||
6-Dec-2017 | fprod 24164 | The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017.) |
∏ | ||
6-Dec-2017 | iprodn0 24163 | Non-zero series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 6-Dec-2017.) |
∏ | ||
6-Dec-2017 | zprodn0 24162 | Non-zero series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 6-Dec-2017.) |
∏ | ||
5-Dec-2017 | cprod0 24168 | A product over the empty set is one. (Contributed by Scott Fenton, 5-Dec-2017.) |
∏ | ||
5-Dec-2017 | prodfclim1 24167 | The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017.) |
5-Dec-2017 | prodf1f 24166 | A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017.) |
5-Dec-2017 | prodf1 24165 | The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017.) |
5-Dec-2017 | iprod 24161 | Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017.) |
∏ | ||
5-Dec-2017 | zprod 24160 | Series product with index set a subset of the upper integers. (Contributed by Scott Fenton, 5-Dec-2017.) |
∏ | ||
4-Dec-2017 | funpartlem 24552 | Lemma for funpartfun 24553. Show membership in the restriction. (Contributed by Scott Fenton, 4-Dec-2017.) |
Image Singleton | ||
4-Dec-2017 | prodmo 24159 | A product has at most one limit. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodmolem2 24158 | Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodmolem2a 24157 | Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodmolem3 24156 | Lemma for prodmo 24159. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodrb 24155 | Rebase the starting point of a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodrblem2 24154 | Lemma for prodrb 24155. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | fprodcvg 24153 | The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodrblem 24152 | Lemma for prodrb 24155. (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | prodf 24151 | An infinite product of complex terms is a function from an upper set of integers to . (Contributed by Scott Fenton, 4-Dec-2017.) |
4-Dec-2017 | cprod2id 24150 | The second class argument to a sum can be chosen so that it is always a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq12rdv 24149 | Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq12dv 24148 | Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | 2cprodeq2dv 24147 | Equality deduction for double sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ ∏ ∏ | ||
4-Dec-2017 | cprodeq2sdv 24146 | Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2dv 24145 | Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2d 24144 | Equality deduction for sum. Note that unlike cprodeq2dv 24145, may occur in . (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq1d 24143 | Equality deduction for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq12i 24142 | Equality inference for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2i 24141 | Equality inference for sum. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq1i 24140 | Equality inference for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cbvcprodi 24139 | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cbvcprodv 24138 | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cbvcprod 24137 | Change bound variable in a product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2 24136 | Equality theorem for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2ii 24135 | Equality theorem for product, with the class expressions and guarded by to be always sets. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | cprodeq2w 24134 | Equality theorem for product, when the class expressions and are equal everywhere. Proved using only Extensionality. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ ∏ | ||
4-Dec-2017 | nfcprod1 24132 | Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ | ||
4-Dec-2017 | cprodex 24129 | A product is a set. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ | ||
4-Dec-2017 | df-cprod 24128 | Define the product of a series with an index set of integers . This definition takes most of the aspects of df-sum 12175 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums. (Contributed by Scott Fenton, 4-Dec-2017.) |
∏ | ||
4-Dec-2017 | spvw 1655 | Version of sp 1728 when does not occur in . This provides the other direction of ax-17 1606. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 10-Apr-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) |
4-Dec-2017 | 19.3v 1654 | Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.) |
4-Dec-2017 | 19.9v 1653 | Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.) |
4-Dec-2017 | 19.8w 1649 | Weak version of 19.8a 1730. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 4-Dec-2017.) |
4-Dec-2017 | 19.2 1648 | Theorem 19.2 of [Margaris] p. 89. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1792 for a more conventional proof. (Contributed by NM, 2-Aug-2017.) (Revised by Wolf Lammen to remove dependency on ax-8, 4-Dec-2017.) |
4-Dec-2017 | exlimdv 1626 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.) |
4-Dec-2017 | exlimiv 1624 |
Inference from Theorem 19.23 of [Margaris] p.
90.
This inference, along with our many variants such as rexlimdv 2679, is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~hirstjl/primer/hirst.pdf. In informal proofs, the statement "Let be an element such that..." almost always means an implicit application of Rule C. In essence, Rule C states that if we can prove that some element exists satisfying a wff, i.e. where has free, then we can use as a hypothesis for the proof where is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier. We cannot do this in Metamath directly. Instead, we use the original (containing ) as an antecedent for the main part of the proof. We eventually arrive at where is the theorem to be proved and does not contain . Then we apply exlimiv 1624 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 8 to arrive at the final theorem . (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen to remove dependency on ax-9 and ax-8, 4-Dec-2017.) |
4-Dec-2017 | ax17e 1608 | A rephrasing of ax-17 1606 using the existential quantifier. (Contributed by Wolf Lammen, 4-Dec-2017.) |
1-Dec-2017 | nfcprod 24133 | Bound-variable hypothesis builder for product: if is (effectively) not free in and , it is not free in ∏ . (Contributed by Scott Fenton, 1-Dec-2017.) |
∏ | ||
1-Dec-2017 | cprodeq1 24131 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
∏ ∏ | ||
1-Dec-2017 | cprodeq1f 24130 | Equality theorem for a product. (Contributed by Scott Fenton, 1-Dec-2017.) |
∏ ∏ | ||
29-Nov-2017 | tz6.12-1-afv 28142 | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12-1 5560. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
''' | ||
29-Nov-2017 | tz6.12-afv 28141 | Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 5561. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
''' | ||
29-Nov-2017 | afveu 28121 | The value of a function at a unique point, analogous to fveu 5533. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
''' | ||
29-Nov-2017 | eu2ndop1stv 28083 | If there is a unique second component in an ordered pair contained in a given set, the first component must be a set. (Contributed by Alexander van der Vekens, 29-Nov-2017.) |
29-Nov-2017 | faclimlem9 24125 | Lemma for faclim 24126. Final inductive step. (Contributed by Scott Fenton, 29-Nov-2017.) |
29-Nov-2017 | faclimlem8 24124 | Lemma for faclim 24126. Base induction case. (Contributed by Scott Fenton, 29-Nov-2017.) |
28-Nov-2017 | alcomw9bAUX7 29631 | Special case of alcom 1723 proved from ax-7v 29419. (Contributed by NM, 28-Nov-2017.) |
28-Nov-2017 | ax7w9AUX7 29630 | Special case of ax-7 1720 proved from ax-7v 29419. (Contributed by NM, 28-Nov-2017.) |
28-Nov-2017 | exsbNEW7 29571 | An equivalent expression for existence. (Contributed by NM, 2-Feb-2005.) (Revised by NM, 28-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720. |
28-Nov-2017 | alneu 28082 | If a statement holds for all sets, there is not a unique set for which the statement holds. (Contributed by Alexander van der Vekens, 28-Nov-2017.) |
27-Nov-2017 | rlimdmafv 28145 | Two ways to express that a function has a limit, analogous to rlimdm 12041. (Contributed by Alexander van der Vekens, 27-Nov-2017.) |
''' | ||
26-Nov-2017 | faclimlem7 24123 | Lemma for faclim 24126. Sequence closure. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem6 24122 | Lemma for faclim 24126. Closure of the core expression. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem5 24121 | Lemma for faclim 24126. A convergence statement in the induction. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem4 24120 | Lemma for faclim 24126. Closure of a particular expression. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem3 24119 | Lemma for faclim 24126. Base case for induction. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem2 24118 | Lemma for faclim 24126. Set up substitution rules. (Contributed by Scott Fenton, 26-Nov-2017.) |
26-Nov-2017 | faclimlem1 24117 | Lemma for faclim 24126. Set up substitution rules. (Contributed by Scott Fenton, 26-Nov-2017.) |
25-Nov-2017 | nfsb4tw2AUXOLD7 29700 | Weak version of nfsb4t 2033. Still uses ax-7OLD7 29632 via nfaldOLD7 29644. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | a16nfNEW7 29525 | If dtru 4217 is false, then there is only one element in the universe, so everything satisfies . (Contributed by Mario Carneiro, 7-Oct-2016.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720. |
25-Nov-2017 | equveliNEW7 29503 | A variable elimination law for equality with no distinct variable requirements. (Compare equviniNEW7 29502.) (Contributed by NM, 1-Mar-2013.) (Proof shortened by Mario Carneiro, 17-Oct-2016.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720. |
25-Nov-2017 | nfnaew3AUX7 29501 | Weak version of nfnae 1909 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | nfaew3AUX7 29500 | Weak version of nfae 1907 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | exdistrfNEW7 29482 | 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.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720. |
25-Nov-2017 | drnf2w3AUX7 29481 | Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | drex2w3AUX7 29480 | Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | dral2w3AUX7 29479 | Weak version of dral2 1919 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | drnf2w2AUX7 29478 | Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | drex2w2AUX7 29477 | Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | dral2w2AUX7 29476 | Weak version of dral2 1919 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | nfnaew2AUX7 29462 | Weak version of nfnae 1909 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | hbnaew2AUX7 29461 | Weak version of hbnae 1908 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | nfaew2AUX7 29460 | Weak version of nfae 1907 not requiring ax-7 1720. (Contributed by NM, 25-Nov-2017.) |
25-Nov-2017 | cbv3hvNEW7 29423 | Lemma for ax10NEW7 29450. Similar to cbv3h 1936. Requires distinct variables but avoids ax-12 1878. (Contributed by NM, 25-Jul-2015.) (Revised by NM, 25-Nov-2017.) Revised to prove from ax-7v 29419 instead of ax-7 1720. |
24-Nov-2017 | eupatrl 28385 |
An Eulerian path is a trail.
Unfortunately, the edge function of an Eulerian path has the domain , whereas the edge functions of all kinds of walks defined here have the domain ..^ (i.e. the edge functions are "words of edge indices", see discussion and proposal of Mario Carneiro at https://groups.google.com/d/msg/metamath/KdVXdL3IH3k/2-BYcS_ACQAJ). Therefore, the arguments of the edge function of an Eulerian path must be shifted by 1 to obtain an edge function of a trail in this theorem, using the auxiliary theorems above (fargshiftlem 28379, fargshiftfv 28380, etc.). The definition of an Eulerian path and all related theorems should be modified as soon as the graph theory is integrated into the main part of set.mm. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
..^ EulPaths Trails | ||
24-Nov-2017 | fargshiftfva 28384 | The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
..^ ..^ | ||
24-Nov-2017 | fargshiftfo 28383 | If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.) |
..^ ..^ | ||
23-Nov-2017 | ax7wnftAUX7 29627 | Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.) |
23-Nov-2017 | ax7w7tAUX7 29626 | Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.) |
23-Nov-2017 | ax7nfAUX7 29625 | Special case of ax-7 1720. (Contributed by NM, 23-Nov-2017.) |
23-Nov-2017 | fargshiftf1 28382 | If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
..^ ..^ | ||
23-Nov-2017 | fargshiftf 28381 | If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
..^ ..^ | ||
23-Nov-2017 | fargshiftfv 28380 | If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
..^ ..^ | ||
23-Nov-2017 | fargshiftlem 28379 | If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.) |
..^ | ||
22-Nov-2017 | faclim 24126 | An infinite product expression relating to factorials. Originally due to Euler. (Contributed by Scott Fenton, 22-Nov-2017.) |
21-Nov-2017 | ex-ovoliunnfl 25002 | Demonstration of ovoliunnfl 25001. (Contributed by Brendan Leahy, 21-Nov-2017.) |
21-Nov-2017 | ovoliunnfl 25001 | ovoliun 18880 is incompatible with the Feferman-Levy model. (Contributed by Brendan Leahy, 21-Nov-2017.) |
20-Nov-2017 | ftc1cnnc 25025 | Choice-free proof of ftc1cn 19406. (Contributed by Brendan Leahy, 20-Nov-2017.) |
19-Nov-2017 | n4cyclfrgra 28440 | There is no 4-cycle in a friendship graph, see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G contains no C4 as a subgraph ...". (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
FriendGrph Cycles | ||
19-Nov-2017 | 4cycl2vnunb 28439 | In a 4-cycle, two distinct vertices have not a unique common neighbor. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
19-Nov-2017 | 4cycl2v2nb 28438 | In a (maybe degenerated) 4-cycle, two vertices have two (maybe not different) common neighbors. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
19-Nov-2017 | 3cyclfrgra 28437 | Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 19-Nov-2017.) |
FriendGrph Cycles | ||
19-Nov-2017 | ftc1cnnclem 25024 | Lemma for ftc1cnnc 25025; cf. ftc1lem4 19402. The stronger assumptions of ftc1cn 19406 are exploited to make use of weaker theorems. (Contributed by Brendan Leahy, 19-Nov-2017.) |
19-Nov-2017 | itgabsnc 25020 | Choice-free analogue of itgabs 19205. (Contributed by Brendan Leahy, 19-Nov-2017.) |
MblFn MblFn | ||
19-Nov-2017 | itgmulc2nc 25019 | Choice-free analogue of itgmulc2 19204. (Contributed by Brendan Leahy, 19-Nov-2017.) |
MblFn | ||
19-Nov-2017 | itgmulc2nclem2 25018 | Lemma for itgmulc2nc 25019; cf. itgmulc2lem2 19203. (Contributed by Brendan Leahy, 19-Nov-2017.) |
MblFn | ||
18-Nov-2017 | 4cycl4dv 28413 | In a simple graph, the vertices of a 4-cycle are mutually different. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
USGrph Word | ||
18-Nov-2017 | usgraf1 28243 | The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
USGrph | ||
18-Nov-2017 | usgraf1o 28242 | The edge function of an undirected simple graph without loops is a one to one function. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
USGrph | ||
18-Nov-2017 | 4fvwrd4 28220 | The first four function values of a word of length at least 4. (Contributed by Alexander van der Vekens, 18-Nov-2017.) |
17-Nov-2017 | constr3cyclpe 28409 | If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph containing one of these vertices. (Contributed by Alexander van der Vekens, 17-Nov-2017.) |
USGrph Cycles | ||
17-Nov-2017 | constr3cyclp 28408 | Construction of a 3-cycle from three given edges in a graph, containing an endpoint of one of these edges. (Contributed by Alexander van der Vekens, 17-Nov-2017.) |
USGrph Cycles | ||
17-Nov-2017 | fzo0to42pr 28211 | A half-open integer range from 0 to 4 is a union of two unordered pairs. (Contributed by Alexander van der Vekens, 17-Nov-2017.) |
..^ | ||
17-Nov-2017 | itgmulc2nclem1 25017 | Lemma for itgmulc2nc 25019; cf. itgmulc2lem1 19202. (Contributed by Brendan Leahy, 17-Nov-2017.) |
MblFn | ||
17-Nov-2017 | iblmulc2nc 25016 | Choice-free analogue of iblmulc2 19201. (Contributed by Brendan Leahy, 17-Nov-2017.) |
MblFn | ||
16-Nov-2017 | 3cyclfrgrarn 28436 | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
FriendGrph | ||
16-Nov-2017 | 3cyclfrgrarn1 28435 | Every vertex in a friendship graph ( with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
FriendGrph | ||
16-Nov-2017 | 2pthfrgrarn2 28434 | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 16-Nov-2017.) |
FriendGrph | ||
16-Nov-2017 | itggt0cn 25023 | itggt0 19212 holds for continuous functions in the absence of ax-cc 8077. (Contributed by Brendan Leahy, 16-Nov-2017.) |
16-Nov-2017 | itg2gt0cn 25006 | itg2gt0 19131 holds on functions continuous on an open interval in the absence of ax-cc 8077. The fourth hypothesis is made unnecessary by the continuity hypothesis. (Contributed by Brendan Leahy, 16-Nov-2017.) |
15-Nov-2017 | 2pthfrgrarn 28433 | Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1 of [MertziosUnger] p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
FriendGrph | ||
15-Nov-2017 | hashgt12el2 28219 | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
15-Nov-2017 | hashgt12el 28218 | In a set with more than one element are two different elements. (Contributed by Alexander van der Vekens, 15-Nov-2017.) |
14-Nov-2017 | 3v3e3cycl 28411 | If and only if there is a 3-cycle in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 14-Nov-2017.) |
USGrph Cycles | ||
14-Nov-2017 | 3v3e3cycl2 28410 | If there are three (different) vertices in a graph which are mutually connected by edges, there is a 3-cycle in the graph. (Contributed by Alexander van der Vekens, 14-Nov-2017.) |
USGrph Cycles | ||
13-Nov-2017 | equsalihAUX7 29465 | One direction of equsalhNEW7 29466 with weaker hypothesis. TO DO: Delete if not used. (Contributed by NM, 13-Nov-2017.) |
13-Nov-2017 | constr3cycl 28407 | Construction of a 3-cycle from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |
USGrph Cycles | ||
13-Nov-2017 | constr3pth 28406 | Construction of a path from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |
USGrph Paths | ||
13-Nov-2017 | constr3trl 28405 | Construction of a trail from three given edges in a graph. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |
USGrph Trails | ||
13-Nov-2017 | constr3pthlem2 28402 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |
..^ | ||
13-Nov-2017 | constr3pthlem1 28401 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 13-Nov-2017.) |
..^ | ||
12-Nov-2017 | constr3trllem5 28400 | Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
USGrph ..^ | ||
12-Nov-2017 | constr3trllem2 28397 | Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
USGrph | ||
12-Nov-2017 | constr3lem5 28394 | Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
12-Nov-2017 | f1ocnvfvrneq 28189 | If the values of a one-to-one function for two arguments from the range of the function are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
12-Nov-2017 | f1veqaeq 28188 | If the values of the converse of a one-to-one function for two arguments are equal, the arguments themselves must be equal. (Contributed by Alexander van der Vekens, 12-Nov-2017.) |
12-Nov-2017 | equequ1 1667 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2017.) |
12-Nov-2017 | exiftru 1647 | A companion rule to ax-gen, valid only if an individual exists. Unlike ax-9 1644, it does not require equality on its interface. Some fundamental theorems of predicate logic can be proven from ax-gen 1536, ax-5 1547 and this theorem alone, not requiring ax-8 1661 or excessive distinct variable conditions. (Contributed by Wolf Lammen, 12-Nov-2017.) |
12-Nov-2017 | mpto2 1524 | Modus ponendo tollens 2, one of the "indemonstrables" in Stoic logic. Note that this uses exclusive-or . See rule 2 on [Lopez-Astorga] p. 12 , rule 4 on [Sanford] p. 39 and rule A4 in [Hitchcock] p. 5 . (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 12-Nov-2017.) |
11-Nov-2017 | constr3cycllem1 28404 | Lemma for constr3cycl 28407. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
11-Nov-2017 | constr3pthlem3 28403 | Lemma for constr3pth 28406. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
..^ | ||
11-Nov-2017 | constr3trllem4 28399 | Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
11-Nov-2017 | constr3trllem3 28398 | Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
11-Nov-2017 | constr3lem6 28395 | Lemma for constr3pthlem3 28403. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
11-Nov-2017 | 3cycl3dv 28388 | In a simple graph, the vertices of a 3-cycle are mutually different. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
USGrph | ||
11-Nov-2017 | disjpr2 28185 | The intersection of distinct pairs is disjoint, analogous to disjsn2 3707. (Contributed by Alexander van der Vekens, 11-Nov-2017.) |
11-Nov-2017 | itgsubnc 25013 | Choice-free analogue of itgsub 19196. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
11-Nov-2017 | iblsubnc 25012 | Choice-free analogue of iblsub 19192. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
11-Nov-2017 | itgaddnc 25011 | Choice-free analogue of itgadd 19195. (Contributed by Brendan Leahy, 11-Nov-2017.) |
MblFn | ||
11-Nov-2017 | mtp-or 1528 | Modus tollendo ponens (inclusive-or version), aka disjunctive syllogism. This is similar to mtp-xor 1526, one of the five original "indemonstrables" in Stoic logic. However, in Stoic logic this rule used exclusive-or, while the name modus tollendo ponens often refers to a variant of the rule that uses inclusive-or instead. The rule says, "if is not true, and or (or both) are true, then must be true." An alternative phrasing is, "Once you eliminate the impossible, whatever remains, no matter how improbable, must be the truth." -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign of the Four, ch. 6). (Contributed by David A. Wheeler, 3-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.) |
11-Nov-2017 | mtp-xor 1526 | Modus tollendo ponens (original exclusive-or version), aka disjunctive syllogism, one of the five "indemonstrables" in Stoic logic. The rule says, "if is not true, and either or (exclusively) are true, then must be true." Today the name "modus tollendo ponens" often refers to a variant, the inclusive-or version as defined in mtp-or 1528. See rule 3 on [Lopez-Astorga] p. 12 (note that the "or" is the same as mpto2 1524, that is, it is exclusive-or df-xor 1296), rule 3 of [Sanford] p. 39 (where it is not as clearly stated which kind of "or" is used but it appears to be in the same sense as mpto2 1524), and rule A5 in [Hitchcock] p. 5 (exclusive-or is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.) (Proof shortened by Wolf Lammen, 11-Nov-2017.) |
10-Nov-2017 | constr3trllem1 28396 | Lemma for constr3trl 28405. (Contributed by Alexander van der Vekens, 10-Nov-2017.) |
USGrph Word | ||
10-Nov-2017 | constr3lem4 28393 | Lemma for constr3trl 28405 etc. The proof could be much shorter if a theorem "fvprg" analogous to fvsng 5730, fvpr1 5738 and fvpr2 5739 was available. (Contributed by Alexander van der Vekens, 10-Nov-2017.) |
10-Nov-2017 | constr3lem2 28392 | Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.) |
10-Nov-2017 | constr3lem1 28391 | Lemma for constr3trl 28405 etc. (Contributed by Alexander van der Vekens, 10-Nov-2017.) |
10-Nov-2017 | hashtpg 28217 | The size of an unordered triple of three different elements. (Contributed by Alexander van der Vekens, 10-Nov-2017.) |
10-Nov-2017 | itgaddnclem2 25010 | Lemma for itgaddnc 25011; cf. itgaddlem2 19194. (Contributed by Brendan Leahy, 10-Nov-2017.) |
MblFn | ||
9-Nov-2017 | 4cycl4dv4e 28414 | If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
USGrph Cycles | ||
9-Nov-2017 | 4cycl4v4e 28412 | If there is a cycle of length 4 in a graph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
Cycles | ||
9-Nov-2017 | 3v3e3cycl1 28390 | If there is a cycle of length 3 in a graph, there are three (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
Cycles | ||
9-Nov-2017 | nvnencycllem 28389 | Lemma for 3v3e3cycl1 28390 and 4cycl4v4e 28412. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
Word | ||
9-Nov-2017 | usgrcyclnl2 28387 | In an undirected simple graph (with no loops!) there are no cycles with length 2 (consisting of two edges ). (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
USGrph Cycles | ||
9-Nov-2017 | fzo0to3tp 28210 | A half-open integer range from 0 to 3 is an unordered triple. (Contributed by Alexander van der Vekens, 9-Nov-2017.) |
..^ | ||
8-Nov-2017 | cyclispthon 28378 | A cycle is a path starting and ending at its first vertex. (Contributed by Alexander van der Vekens, 8-Nov-2017.) |
Cycles PathOn | ||
8-Nov-2017 | ispthon 28362 | Properties of a pair of functions to be a path between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) |
PathOn WalkOn Paths | ||
8-Nov-2017 | pthon 28361 | The set of paths between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 8-Nov-2017.) |
PathOn WalkOn Paths | ||
7-Nov-2017 | usgrcyclnl1 28386 | In an undirected simple graph (with no loops!) there are no cycles with length 1 (consisting of one edge ). (Contributed by Alexander van der Vekens, 7-Nov-2017.) |
USGrph Cycles | ||
7-Nov-2017 | cycliswlk 28377 | A cycle is a walk. (Contributed by Alexander van der Vekens, 7-Nov-2017.) |
Cycles Walks | ||
7-Nov-2017 | usgrnloop 28351 | In an undirected simple graph, each walk has no loops! (Contributed by Alexander van der Vekens, 7-Nov-2017.) |
USGrph Walks ..^ | ||
7-Nov-2017 | iblabsnc 25015 | Choice-free analogue of iblabs 19199. As with ibladdnc 25008, a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
7-Nov-2017 | iblabsnclem 25014 | Lemma for iblabsnc 25015; cf. iblabslem 19198. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
7-Nov-2017 | itgaddnclem1 25009 | Lemma for itgaddnc 25011; cf. itgaddlem1 19193. (Contributed by Brendan Leahy, 7-Nov-2017.) |
MblFn | ||
6-Nov-2017 | bi123imp0 28560 | Similar to 3imp 1145 except all implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi23imp1 28559 | Similar to 3imp 1145 except all but outermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi12imp3 28558 | Similar to 3imp 1145 except all but innermost implication are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi13imp2 28557 | Similar to 3imp 1145 except the outermost and innermost implications are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi13imp23 28556 | 3imp 1145 with outermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi23imp13 28555 | 3imp 1145 with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi33imp12 28554 | 3imp 1145 with innermost implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi123impia 28553 | 3impia 1148 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi13impia 28552 | 3impia 1148 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi123impib 28551 | 3impib 1149 with the implications of the hypothesis biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi13impib 28550 | 3impib 1149 with the outer implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi23impib 28549 | 3impib 1149 with the inner implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi3impa 28548 | Similar to 3impa 1146 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi3impb 28547 | Similar to 3impb 1147 with implication in hypothesis replaced by biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bi2imp 28546 | Importation inference similar to imp 418, except the both implications of the hypothesis are biconditionals. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | biimp 28545 | Importation inference similar to imp 418, except the outermost implication of the hypothesis is a biconditional. (Contributed by Alan Sare, 6-Nov-2017.) |
6-Nov-2017 | bddiblnc 25021 | Choice-free proof of bddibl 19210. (Contributed by Brendan Leahy, 2-Nov-2017.) (Revised by Brendan Leahy, 6-Nov-2017.) |
MblFn | ||
5-Nov-2017 | trlonwlkon 28342 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
TrailOn WalkOn | ||
5-Nov-2017 | trlonprop 28341 | A trail between two vertices is a walk between these vertices. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
TrailOn WalkOn Trails | ||
5-Nov-2017 | brabv 28193 | If two classes are in a relationship given by an ordered-pair class abstraction, the classes are sets. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
5-Nov-2017 | 0neqopab 28192 | The empty set is never an element in an ordered-pair class abstraction. (Contributed by Alexander van der Vekens, 5-Nov-2017.) |
4-Nov-2017 | trlon 28339 | The set of trails between two vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 4-Nov-2017.) |
TrailOn WalkOn Trails | ||
3-Nov-2017 | istrlon 28340 | Properties of a pair of functions to be a trail between two given vertices(in an undirected graph). (Contributed by Alexander van der Vekens, 3-Nov-2017.) |
TrailOn WalkOn Trails | ||
3-Nov-2017 | jaoi2 28176 | If one part of a disjunction is already true, the other part can be true only if the first part is false. (Contributed by Alexander van der Vekens, 3-Nov-2017.) |
2-Nov-2017 | wlkonwlk 28334 | A walk is a walk between its endpoints. (Contributed by Alexander van der Vekens, 2-Nov-2017.) |
Walks WalkOn | ||
2-Nov-2017 | iswlkon 28332 | Properties of a pair of functions to be a walk between two given vertices (in an undirected graph). (Contributed by Alexander van der Vekens, 2-Nov-2017.) |
WalkOn Walks | ||
2-Nov-2017 | cnicciblnc 25022 | Choice-free proof of cniccibl 19211. (Contributed by Brendan Leahy, 2-Nov-2017.) |
1-Nov-2017 | redwlk 28364 | A walk ending at the last but one vertex of the walk is a walk. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
Walks ..^ Walks ..^ | ||
1-Nov-2017 | redwlklem 28363 | Lemma for redwlk 28364. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
Walks ..^ | ||
1-Nov-2017 | wlkres 28331 | Restrictions of walks are sets. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
Walks | ||
1-Nov-2017 | fzossrbm1 28209 | Subset of a half open range. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
..^ ..^ | ||
1-Nov-2017 | opabbrex 28191 | A collection of ordered pairs with an extension of a binary relation is a set. (Contributed by Alexander van der Vekens, 1-Nov-2017.) |
1-Nov-2017 | ibladdnc 25008 | Choice-free analogue of itgadd 19195. A measurability hypothesis is necessitated by the loss of mbfadd 19032; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-Nov-2017.) |
MblFn | ||
31-Oct-2017 | pthdepisspth 28360 | A path with different start end end points is a simple path (in an undirected graph). (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
Paths SPaths | ||
31-Oct-2017 | wlkbprop 28333 | Basic properties of a walk. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
Walks | ||
31-Oct-2017 | injresinj 28215 | A function whose restriction is injective and the values of the remaining arguments are different from all other values is injective itself. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
..^ ..^ | ||
31-Oct-2017 | injresinjlem 28214 | Lemma for injresinj 28215. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
..^ ..^ | ||
31-Oct-2017 | elfznelfzo 28213 | A value in a finite set of sequential integers is a border value if it is not contained in the half-open integer range contained in the finite set of sequential integerss. (Contributed by Alexander van der Vekens, 31-Oct-2017.) |
..^ | ||
31-Oct-2017 | ibladdnclem 25007 | Lemma for ibladdnc 25008; cf ibladdlem 19190, whose fifth hypothesis is rendered unnecessary by the weakened hypotheses of itg2addnc 25005. (Contributed by Brendan Leahy, 31-Oct-2017.) |
MblFn | ||
31-Oct-2017 | itg2addnc 25005 | Alternate proof of itg2add 19130 using the "buffer zone" definition from the first lemma, in which every simple function in the set is divided into to by dividing its buffer by a third and finding the largest allowable function locked to a grid laid out in increments of the new, smaller buffer up to the original simple function. The measurability of this function follows from that of the augend, and subtracting it from the original simple function yields another simple function by i1fsub 19079, which is allowable by the fact that the grid must have a mark between one third and two thirds the original buffer. This has two advantages over the current approach: first, eliminating ax-cc 8077, and second, weakening the measurability hypothesis to only the augend. (Contributed by Brendan Leahy, 31-Oct-2017.) |
MblFn | ||
30-Oct-2017 | hbaew5AUX7 29619 | Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 30-Oct-2017.) |
30-Oct-2017 | hbaew4AUX7 29618 | Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 30-Oct-2017.) |
30-Oct-2017 | hbaew3AUX7 29499 | Weak version of hbae 1906 not requiring ax-7 1720. Has different distinct variable requirements from hbaewAUX7 29455. (Contributed by NM, 30-Oct-2017.) |
30-Oct-2017 | hbaew2AUX7 29456 | Weak version of hbae 1906 not requiring ax-7 1720. Different distinct variable requirements from hbaewAUX7 29455. (Contributed by NM, 30-Oct-2017.) |
30-Oct-2017 | cyclnspth 28376 | A (non trivial) cycle is not a simple path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles SPaths | ||
30-Oct-2017 | cycliscrct 28375 | A cycle is a circuit. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles Circuits | ||
30-Oct-2017 | cyclispth 28374 | A cycle is a path. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles Paths | ||
30-Oct-2017 | crctistrl 28373 | A circuit is a trail. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Circuits Trails | ||
30-Oct-2017 | 0cycl 28372 | A pair of an empty set (of edges) and a second set (of vertices) is a cycle if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles | ||
30-Oct-2017 | 0crct 28371 | A pair of an empty set (of edges) and a second set (of vertices) is a circuit if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Circuits | ||
30-Oct-2017 | iscycl 28370 | Properties of a pair of functions to be a cycle (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles Paths | ||
30-Oct-2017 | iscrct 28369 | Properties of a pair of functions to be a circuit (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Circuits Trails | ||
30-Oct-2017 | cycls 28368 | The set of cycles (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Cycles Paths | ||
30-Oct-2017 | crcts 28367 | The set of circuits (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Circuits Trails | ||
30-Oct-2017 | 0spth 28357 | A pair of an empty set (of edges) and a second set (of vertices) is a simple path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
SPaths | ||
30-Oct-2017 | 0pth 28356 | A pair of an empty set (of edges) and a second set (of vertices) is a path if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Paths | ||
30-Oct-2017 | 0trl 28344 | A pair of an empty set (of edges) and a second set (of vertices) is a trail if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Trails | ||
30-Oct-2017 | 0wlk 28343 | A pair of an empty set (of edges) and a second set (of vertices) is a walk if and only if the second set contains exactly one vertex (in an undirected graph). (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
Walks | ||
30-Oct-2017 | fzon 28212 | A half-open set of sequential integers is empty if the bounds are equal or reversed. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
..^ | ||
30-Oct-2017 | isprmpt2 28208 | Properties of a pair in an extended binary relation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
30-Oct-2017 | sprmpt2 28207 | The extension of a binary relation which is the value of an operation given in maps-to notation. (Contributed by Alexander van der Vekens, 30-Oct-2017.) |
29-Oct-2017 | hbaew0AUX7 29617 | Weak version of hbae 1906 not requiring ax-7 1720. (Contributed by NM, 29-Oct-2017.) |
29-Oct-2017 | ax12olem3aAUX7 29434 | Lemma for ax12o 1887. Show the equivalence of an intermediate equivalent to ax12o 1887 with the conjunction of ax-12 1878 and a variant with negated equalities. (Contributed by NM, 29-Oct-2017.) |
29-Oct-2017 | itg2addnclem2 25004 | Lemma for itg2addnc 25005. The function described is a simple function. (Contributed by Brendan Leahy, 29-Oct-2017.) |
MblFn | ||
28-Oct-2017 | sbhbwAUX7 29579 | Weak version of sbhb 2059 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | sb8ewAUX7 29566 | Weak version of sb8e 2046 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | sb8wAUX7 29565 | Weak version of sb8 2045 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | aevwAUX7 29497 | Weak version of aev 1944 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbvexwAUX7 29495 | Weak version of cbvex 1938 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbvalwwAUX7 29494 | Weak version of cbval 1937 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv3hwAUX7 29493 | Weak version of cbv3h 1936 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv3wAUX7 29492 | Weak version of cbv3 1935 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv2wAUX7 29491 | Weak version of cbv2 1934 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv2hwAUX7 29490 | Weak version of cbv2h 1933 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv1wAUX7 29489 | Weak version of cbv1 1932 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | cbv1hwAUX7 29488 | Weak version of cbv1h 1931 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
28-Oct-2017 | a7swAUX7 29422 | Weak version of a7s 1721 not requiring ax-7 1720. (Contributed by NM, 28-Oct-2017.) |
27-Oct-2017 | ax7w1hAUX7 29616 | Weak version of hbal 1722 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | sbcomwAUX7 29562 | Weak version of sbcom 2042 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | sbco3wAUX7 29561 | Weak version of sbco3 2041 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | sbco2dwAUX7 29560 | Weak version of sbco2d 2040 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | sbco2wAUX7 29559 | Weak version of sbco2 2039 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | nfsb4wAUX7 29552 | Weak version of nfsb4t 2033 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | nfsb4twAUX7 29551 | Weak version of nfsb4t 2033 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | sbequ5wAUX7 29533 | Weak version of sbequ5 1984 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | equs5bAUX7 29510 | Lemma used in proofs of substitution properties. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | drnf2wAUX7 29475 | Weak version of drnf2 1923 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |
27-Oct-2017 | drex2wAUX7 29474 | Weak version of drex2 1921 not requiring ax-7 1720. (Contributed by NM, 27-Oct-2017.) |