Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 22-Apr-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (13-Apr-2017) See equidK for a discussion of the recent theorems in my mathbox. -NM
(24-Mar-2017) Alan Sare updated his completeusersproof program.
(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.
(28-Dec-2016) David A. Wheeler is putting together a page on Metamath (specifically set.mm) conventions. Comments are welcome on the Google Group thread.
(24-Dec-2016) Mario Carneiro introduced the abbreviation "F/ x ph" (symbols: turned F, x, phi) in df-nf to represent the "effectively not free" idiom "A. x ( ph -> A. x ph )". Theorem nf2 shows a version without nested quantifiers.
(22-Dec-2016) Naip Moro has developed a Metamath database for G. Spencer-Brown's Laws of Form. You can follow the Google Group discussion here.
(20-Dec-2016) In metamath program version 0.137, 'verify markup *' now checks that ax-XXX $a matches axXXX $p when the latter exists, per the discussion at https://groups.google.com/d/msg/metamath/Vtz3CKGmXnI/Fxq3j1I_EQAJ.
(24-Nov-2016) Mingl Yuan has kindly provided a mirror site in Beijing, China. He has also provided an rsync server; type "rsync cn.metamath.org::" in a bash shell to check its status (it should return "metamath metamath").
(14-Aug-2016) All HTML pages on this site should now be mobile-friendly and pass the Mobile-Friendly Test. If you find one that does not, let me know.
(14-Aug-2016) Daniel Whalen wrote a paper describing the use of using deep learning to prove 14% of test theorems taken from set.mm: Holophrasm: a neural Automated Theorem Prover for higher-order logic. The associated program is called Holophrasm.
(14-Aug-2016) David A. Wheeler created a video called Metamath Proof Explorer: A Modern Principia Mathematica
(12-Aug-2016) A Gitter chat room has been created for Metamath.
(9-Aug-2016) Mario Carneiro wrote a Metamath proof verifier in the Scala language as part of the ongoing Metamath -> MMT import project
(9-Aug-2016) David A. Wheeler created a GitHub project called metamath-test (last execution run) to check that different verifiers both pass good databases and detect errors in defective ones.
(4-Aug-2016) Mario gave two presentations at CICM 2016.
(17-Jul-2016) Thierry Arnoux has written EMetamath, a Metamath plugin for the Eclipse IDE.
(16-Jul-2016) Mario recovered Chris Capel's collapsible proof demo.
(13-Jul-2016) FL sent me an updated version of PDF (LaTeX source) developed with Lamport's pf2 package. See the 23-Apr-2012 entry below.
(12-Jul-2016) David A. Wheeler produced a new video for mmj2 called "Creating functions in Metamath". It shows a more efficient approach than his previous recent video "Creating functions in Metamath" (old) but it can be of interest to see both approaches.
(10-Jul-2016) Metamath program version 0.132 changes the command 'show restricted' to 'show discouraged' and adds a new command, 'set discouragement'. See the mmnotes.txt entry of 11-May-2016 (updated 10-Jul-2016).
(12-Jun-2016) Dan Getz has written Metamath.jl, a Metamath proof verifier written in the Julia language. Older news...
Color key: | Metamath Proof Explorer | Hilbert Space Explorer | User Mathboxes |
Date | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Theorem | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
21-Apr-2017 | ax12olem24K 27879 | Lemma for ax12o 1663. Construct an intermediate equivalent to ax-12 1633 from two instances of ax-12 1633. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that and are bundled. THIS IS AS FAR AS I WAS ABLE TO GET using only Tarski's schemes; I couldn't find a way to prove ax12olem25 1659 through ax12olem27 1661 without making and distinct. (Contributed by NM, 21-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
20-Apr-2017 | ax12olem22K 27875 | Lemma for ax12o 1663. Negate the equalities in ax-12 1633, shown as the hypothesis. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that and are bundled. (Contributed by NM, 20-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
20-Apr-2017 | equextvK 27874 | An extensionality-like property for equality. Similar to equveli 1880. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that and are bundled. (Contributed by NM, 20-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
20-Apr-2017 | equvinvK 27861 | Similar to equvini 1879. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). Note that and are bundled. (Contributed by NM, 20-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem23aK 27877 | Lemma for ax12o 1663. Show one direction of the equivalence of an intermediate equivalent to ax-12o 1664 with the conjunction of ax-12 1633 and a variant with negated equalities. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem21K 27872 | Lemma for ax12o 1663. Similar to equvin 1999 but with a negated equality. Uses only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem20K 27870 | Lemma for ax12o 1663. Weak version of 19.12 1766, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem19K 27868 | Lemma for ax12o 1663. Weak version of nfex 1733, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem18K 27866 | Lemma for ax12o 1663. Weak version of hbim1 1810, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem17K 27864 | Lemma for ax12o 1663. Weak version of 19.21 1771, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12olem16K 27862 | Lemma for ax12o 1663. Weak version of equsalh 1851, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem15K 27859 | Lemma for ax12o 1663. Weak version of exlimih 1782, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem14K 27857 | Lemma for ax12o 1663. Weak version of 19.23 1777, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem13K 27855 | Lemma for ax12o 1663. Weak version of 19.9 1762, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem12K 27853 | Lemma for ax12o 1663. Weak version of 19.9t 1761, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem11K 27851 | Lemma for ax12o 1663. Weak version of hbim 1723, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem10K 27848 | Lemma for ax12o 1663. Weak version of hbnt 1717, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem9K 27847 | Lemma for ax12o 1663. Weak version of ax6o 1696, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem8K 27845 | Lemma for ax12o 1663 and ax10 1677. Weak version of a4ime 1868 with distinct variables, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem7K 27843 | Lemma for ax12o 1663 and ax10 1677. Weak version of hbimd 1809, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem6K 27841 | Lemma for ax12o 1663 and ax10 1677. Weak version of hbn 1722, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem5K 27839 | Lemma for ax12o 1663 and ax10 1677. Weak version of hba1 1718, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem4K 27837 | Lemma for ax12o 1663. Weak version of 19.8a 1758, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax12o10lem3K 27836 | Lemma for ax12o 1663 and ax10 1677. Weak version of ax4 1691, using only Tarski's FOL axiom schemes (see description for equidK 27792). (Contributed by NM, 19-Apr-2017.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax11wflemK 27822 | Verson of ax11wlemK 27823 without distinct variables. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | hbalwK 27820 | Weak version of hbal 1567. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. Unlike hbal 1567, this theorem requires that and be distinct i.e. are not bundled. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | hbe1wK 27818 | Weak version of hbe1 1565. See comments for ax6wK 27816. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax6wfK 27815 | Weak version of ax-6 1534 from which we can prove any ax-6 1534 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | cbvexvK 27814 | Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | cbvaliK 27810 | Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | ax4wfK 27806 | Weak version of ax-4 1692. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 9 of [KalishMontague] p. 86. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | a4imK 27804 | Specialization. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 8 of [KalishMontague] p. 87. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | albidK 27802 | Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Apr-2017 | alimdK 27800 | Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 19-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
14-Apr-2017 | ax11wdemoK 27826 | Example of an application of ax11wK 27824 that results in an instance of ax-11 1624 for a contrived formula with mixed free and bound variables, , in place of . The proof illustrates bound variable renaming with cbvalvK 27813 to obtain fresh variables to avoid distinct variable clashes. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 14-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax12dgen4K 27831 | Degenerate instance of ax-12 1633 where bundled variables , , and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax12dgen3K 27830 | Degenerate instance of ax-12 1633 where bundled variables and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax12dgen2K 27829 | Degenerate instance of ax-12 1633 where bundled variables and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax12dgen1K 27828 | Degenerate instance of ax-12 1633 where bundled variables and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax11dgenK 27825 | Degenerate instance of ax-11 1624 where bundled variables and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Apr-2017 | ax7dgenK 27821 | Degenerate instance of ax-7 1535 where bundled variables and have a common substitution. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 13-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
11-Apr-2017 | albidvK 27803 | Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 11-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
11-Apr-2017 | alimdvK 27801 | Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 11-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | ax12wK 27827 | Weak version (principal instance) of ax-12 1633 not involving bundling. Uses only Tarski's predicate calculus axiom schemes. The proof is trivial but is included to complete the set ax6wK 27816, ax7wK 27819, and ax11wK 27824. See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | ax11wK 27824 | Weak version of ax-11 1624 from which we can prove any ax-7 1535 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. An instance of the first hypothesis will normally require that and be distinct (unless does not occur in ). See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | ax11wlemK 27823 | Lemma for weak version of ax-11 1624. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. In some cases, this lemma may lead to shorter proofs than ax11wK 27824. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | ax7wK 27819 | Weak version of ax-7 1535 from which we can prove any ax-7 1535 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. Unlike ax-7 1535, this theorem requires that and be distinct i.e. are not bundled. See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | 19.8vK 27809 | Version of 19.8a 1758 and its converse when does not occur in . Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
10-Apr-2017 | ax4vK 27808 | Version of ax-4 1692 when does not occur in . This provides the other direction of ax-17 1628. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 10-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | hba1wK 27817 | Weak version of hba1 1718. See comments for ax6wK 27816. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | ax6wK 27816 | Weak version of ax-6 1534 from which we can prove any ax-6 1534 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. See the description in the comment of equidK 27792. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | cbvalvK 27813 | Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | cbvalK 27812 | Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | cbvalivK 27811 | Change bound variable. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 7 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | ax4wK 27807 | Weak version of ax-4 1692. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 9 of [KalishMontague] p. 86. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | a4imvK 27805 | Specialization. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 8 of [KalishMontague] p. 87. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | albiiK 27799 | Add universal quantifier to both sides of an equivalence. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Part of Lemma 5 of [KalishMontague] p. 86. (The other parts are just notbii 289 and imbi12i 318.) (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | alimiK 27798 | Add universal quantifier to both sides of an implication. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | elequ2K 27797 | An equality for the membership predicate. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | elequ1K 27796 | An equality law for the membership predicate. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | equequ2K 27795 | An equality law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | equequ1K 27794 | An equality law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | equcomiK 27793 | Commutative law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 3 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Apr-2017 | equidK 27792 |
(Theorems equidK 27792 through ax12dgen4K 27831 are part of a study of our
non-Tarski predicate calculus axiom schemes. We are using this theorem
as a placeholder to describe this study.)
The orginal axiom schemes of Tarski's predicate calculus are ax-5 1533, ax-8 1623, ax-9v 1632, ax-13 1625, ax-14 1626, and ax-17 1628 (see http://us.metamath.org/mpegif/mmset.html#compare) and are shown as axiom schemes B4 through B8 in [KalishMontague] p. 81. These are shown to be logically complete by Theorem 1 of [KalishMontague] p. 85. The axiom system of set.mm includes the additional axiom schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633, which are not part of Tarski's axiom schemes. They are used (and we conjecture are required) to make our system "metalogically complete" i.e. able to prove directly all possible schemes with wff and set metavariables, bundled or not, whose object-language instances are valid. (ax-11 1624 has been proved to be required; see http://us.metamath.org/award2003.html#9a. Metalogical independence of the other three are open problems.) (There arem additional predicate calculus axiom schemes included in set.mm such as ax-4 1692, but they can all be proved as theorems from the above.) Terminology: Two set (individual) metavariables are "bundled" in an axiom or theorem scheme when there is no distinct variable constraint ($d) imposed on them. (The term "bundled" is due to Raph Levien.) For example, the and in ax-9 1684 are bundled, but they are not in ax-9v 1632. We also say that a scheme is bundled when it has at least one pair of bundled set metavariables. If distinct variable conditions are added to all set metavariable pairs in a bundled scheme, we call that the "principal" instance of the bundled scheme. For example, ax-9v 1632 is the principal instance of ax-9 1684. Whenever a common variable is substituted for two or more bundled variables in an axiom or theorem scheme, we call the substitution instance "degenerate". For example, the instance of ax-9 1684 is degenerate. An advantage of bundling is ease of use since there are fewer distinct variable restrictions ($d) to be concerned with. There is also a small economy in being able to state principal and degenerate instances simultaneously. A disadvantage is that bundling may present difficulties in translations to other proof languages, which typically lack the concept (in part because their variables often represent the variables of the object language rather than metavariables ranging over them). Because Tarski's axiom schemes are logically complete, they can be used to prove any object-language instance of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633. "Translating" this to Metamath, it means that Tarksi's axioms can prove any substitution instance of ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633 in which (1) there are no wff metavariables and (2) all set metavariables are mutually distinct i.e. are not bundled. In effect this is mimicking the object language by pretending that each set metavariable is an object-language variable. (There may also be specific instances with wff metavariables and/or bundling that are directly provable from Tarski's axiom schemes, but it isn't guaranteed. Whether all of them are possible is part of the still open metalogical independence problem for our additional axiom schemes.) It can be useful to see how this can be done, both to show that our additional schemes are valid metatheorems of Tarski's system and to be able to translate object language instances of our proofs into proofs that would work with a system using only Tarski's original schemes. In addition, it may (or may not) provide insight into the conjectured metalogical independence of our additional schemes. Past work showed that instances of ax-11o 1940 meeting condition (1) can be proved without invoking that axiom scheme (see comments in ax-11 1624). However, it was somewhat awkward to use, involving an inductive argument with auxiliary theorems ax11eq 2105, ax11el 2106, ax11indn 2108, ax11indi 2109, and ax11inda 2113. It also used axiom schemes other than Tarski's. The new theorem schemes ax6wK 27816, ax7wK 27819, ax11wK 27824, and ax12wK 27827 are derived using only Tarski's axiom schemes, showing that Tarski's schemes can be used to derive all substitution instances of ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 meeting conditions (1) and (2). (The "K" suffix stands for Kalish/Montague, whose paper was a source for some of the proofs. I may change these names in the future since our practice has been to reserve upper case for special cases such as the ALT or OLD suffixes.) Each hypothesis of ax6wK 27816, ax7wK 27819, and ax11wK 27824 is of the form where is an auxiliary or "dummy" wff metavariable in which doesn't occur. We can show by induction on formula length that the hypotheses can be eliminated in all cases meeting conditions (1) and (2). The example ax11wdemoK 27826 illustrates the techniques (equality theorems and bound variable renaming) used to achieve this. We also show the degenerate instances for axioms with bundled variables in ax7dgenK 27821, ax11dgenK 27825, ax12dgen1K 27828, ax12dgen2K 27829, ax12dgen3K 27830, and ax12dgen4K 27831. (Their proofs are trivial but we include them to be thorough.) Combining the principal and degenerate cases outside of Metamath, we show that the bundled schemes ax-6 1534, ax-7 1535, ax-11 1624, and ax-12 1633 are schemes of Tarski's system, meaning that all object language instances they generate are theorems of Tarski's system. It is interesting that Tarski's system bundles set metavariables in ax-8 1623, ax-13 1625, and ax-14 1626; indeed, a degenerate instance of ax-8 1623 appears to be indispensable for the proof of equidK 27792. Perhaps his general philosophy was that bundling is acceptable for free variables. But he also used the bundled scheme ax-9 1684 in an older system, so it seems the main purpose of his later ax-9v 1632 was just to show that the weaker unbundled form is sufficient rather than an aesthetic objection to bundled free and bound variables. The case of ax-4 1692 is curious: originally an axiom of Tarski's system, it was proved redundant by Lemma 9 of [KalishMontague] p. 86. However, the proof is by induction on formula length, and the compact scheme form apparently cannot be proved directly from Tarski's other axioms. The best we can do seems to be ax4wK 27807, again requiring substitution instances of that meet conditions (1) and (2) above. Note that our direct proof ax4 1691 requires ax-11 1624, which is not part of Tarski's system. (End of study description.) Identity law for equality. Does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633. Lemma 2 of [KalishMontague] p. 85. (Contributed by NM, 9-Apr-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthm 19878 | The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA PB and PC PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to . The result is proven by using chordthmlem5 19877 twice to show that PA PB and PC PD both equal BQ^{2} PQ^{2}. This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem5 19877 | If P is on the segment AB and AQ = BQ, then PA PB = BQ^{2} PQ^{2}. This follows from two uses of chordthmlem3 19875 to show that PQ^{2} = QM^{2} PM^{2} and BQ^{2} = QM^{2} BM^{2}, so BQ^{2} PQ^{2} = (QM^{2} BM^{2}) (QM^{2} PM^{2}) = BM^{2} PM^{2}, which equals PA PB by chordthmlem4 19876. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem4 19876 | If P is on the segment AB and M is the midpoint of AB, then PA PB = BM^{2} PM^{2}. If all lengths are reexpressed as fractions of AB, this reduces to the identity ^{2} ^{2}. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem3 19875 | If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then PQ^{2} = QM^{2} PM^{2}. This follows from chordthmlem2 19874 and the Pythagorean theorem (pythag 19859) in the case where P and Q are unequal to M. If either P or Q equals M, the result is trivial. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem2 19874 | If M is the midpoint of AB, AQ = BQ, and P is on the line AB, then QMP is a right angle. This is proven by reduction to the special case chordthmlem 19873, where P = B, and using angrtmuld 19850 to observe that QMP is right iff QMB is. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | chordthmlem 19873 | If M is the midpoint of AB and AQ = BQ, then QMB is a right angle. The proof uses ssscongptld 19866 to observe that, since AMQ and BMQ have equal sides, the angles QMB and QMA must be equal. Since they are supplementary, both must be right. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvd 19872 | The angle ABC is iff B is a nontrivial convex combination of A and C, i.e., iff B is in the interior of the segment AC. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpined 19871 | If the angle at ABC is , then A is not equal to C. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvdlem2 19870 | Equivalence used in angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angpieqvdlem 19869 | Equivalence used in the proof of angpieqvd 19872. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | affineequiv2 19868 | Equivalence between two ways of expressing as an affine combination of and . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | affineequiv 19867 | Equivalence between two ways of expressing as an affine combination of and . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | ssscongptld 19866 |
If two triangles have equal sides, one angle in one triangle has the
same cosine as the corresponding angle in the other triangle. This is a
partial form of the SSS congruence theorem.
This theorem is proven by using lawcos 19858 on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angrtmuld 19850 | Perpendicularity of two vectors does not change under rescaling the second. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosangneg2d 19849 | The cosine of the angle between and is the negative of that between and . If A, B and C are collinear points, this implies that the cosines of DBA and DBC sum to zero, i.e., that DBA and DBC are supplementary. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angrteqvd 19848 | Two vectors are at a right angle iff their quotient is purely imaginary. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angcld 19847 | The (signed) angle between two vectors is in . Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | angvald 19846 | The (signed) angle between two vectors is the argument of their quotient. Deduction form of angval 19843. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosarg0d 19795 | The cosine of the argument is zero precisely on the imaginary axis. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosargd 19794 | The cosine of the argument is the quotient of the real part and the absolute value. Compare to efiarg 19793. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logimclad 19762 | The imaginary part of the logarithm is in . Alternate form of logimcld 19761. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logimcld 19761 | The imaginary part of the logarithm is in . Deduction form of logimcl 19759. Compare logimclad 19762. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | logcld 19760 | The logarithm of a nonzero complex number is a complex number. Deduction form of logcl 19758. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negpitopissre 19734 | is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | coseq0negpitopi 19703 | Location of the zeroes of cosine in . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | coseq00topi 19702 | Location of the zeroes of cosine in . (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | cosneghalfpi 19670 | The cosine of is zero. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | halfpire 19667 | is real. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | abs00bd 11653 | If a complex number is zero, its absolute value is zero. Converse of abs00d 11805. One-way deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | abs00ad 11652 | A complex number is zero iff its absolute value is zero. Deduction form of abs00 11651. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | sq0id 11075 | If a number is zero, its square is zero. Deduction form of sq0i 11074. Converse of sqeq0d 11122. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | unitssre 10659 | is a subset of the reals. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | xov1plusxeqvd 10658 | A complex number is positive real iff is in . Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | rehalfcli 9839 | Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | div2subd 9466 | Swap subtrahend and minuend inside the numerator and denominator of a fraction. Deduction form of div2sub 9465. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq1bd 9464 | If two complex numbers are equal, their quotient is one. One-way deduction form of diveq1 9334. Converse of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | dmdcan2d 9446 | Cancellation law for division and multiplication. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | divne1d 9427 | If two complex numbers are unequal, their quotient is not one. Contrapositive of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq0ad 9426 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveq0 9314. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | diveq1ad 9425 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveq1 9334. Generalization of diveq1d 9424. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | eqnegad 9362 | If a complex number equals its own negative, it is zero. One-way deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | eqnegd 9361 | A complex number equals its negative iff it is zero. Deduction form of eqneg 9360. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulne0bbd 9302 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulne0bad 9301 | A factor of a nonzero complex number is nonzero. Partial converse of mulne0d 9300 and consequence of mulne0bd 9299. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulcan2ad 9284 | Cancellation of a nonzero factor on the right in an equation. One-way deduction form of mulcan2d 9282. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | mulcanad 9283 | Cancellation of a nonzero factor on the left in an equation. One-way deduction form of mulcand 9281. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | lt0ne0d 9218 | Something less than zero is not zero. Deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subeq0bd 9089 | If two complex numbers are equal, their difference is zero. Consequence of subeq0ad 9047. Converse of subeq0d 9045. Contrapositive of subne0ad 9048. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subneintr2d 9083 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subcan2ad 9082 | Cancellation law for subtraction. Deduction form of subcan2 8952. Generalization of subcan2d 9079. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subneintrd 9081 | Introducing subtraction on both sides of a statement of nonequality. Contrapositive of subcand 9078. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subcanad 9080 | Cancellation law for subtraction. Deduction form of subcan 8982. Generalization of subcand 9078. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subne0ad 9048 | If the difference of two complex numbers is nonzero, they are unequal. Converse of subne0d 9046. Contrapositive of subeq0bd 9089. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | subeq0ad 9047 | The difference of two complex numbers is zero iff they are equal. Deduction form of subeq0 8953. Generalization of subeq0d 9045. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negned 9034 | If two complex numbers are unequal, so are their negatives. Contrapositive of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | neg11ad 9033 | The negatives of two complex numbers are equal iff they are equal. Deduction form of neg11 8978. Generalization of neg11d 9049. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negcon1ad 9032 | Contraposition law for unary minus. One-way deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | negcon1d 9031 | Contraposition law for unary minus. Deduction form of negcon1 8979. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addneintr2d 8900 | Introducing a term on the right-hand side of a sum in a negated equality. Contrapositive of addcan2ad 8898. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addneintrd 8899 | Introducing a term on the left-hand side of a sum in a negated equality. Contrapositive of addcanad 8897. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addcan2ad 8898 | Cancelling a term on the right-hand side of a sum in an equality. Consequence of addcan2d 8896. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | addcanad 8897 | Cancelling a term on the left-hand side of a sum in an equality. Consequence of addcand 8895. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | rexri 8764 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | pm2.21ddne 2486 | A contradiction implies anything. Equality/inequality deduction form. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
28-Feb-2017 | neneqad 2482 | If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2428. One-way deduction form of df-ne 2414. (Contributed by David Moews, 28-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-natded9.20-2 20663 | A more efficient proof of Theorem 9.20 of [Laboreo] p. 45. Compare with ex-natded9.20 20662. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-natded9.20 20662 |
Theorem 9.20 of [Laboreo] p. 43, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof is ex-natded9.20-2 20663. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
19-Feb-2017 | ex-natded5.5 20655 |
Theorem 5.5 of [Laboreo] p. 18, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof is mtod 170; a proof without context is shown in mto 169. (Proof modification is discouraged.) (Contributed by David A. Wheeler, 19-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbidd-misc 26878 | An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbidd 26877 | An identity theorem for substitution. See sbid 1895. See Remark 9.1 in [Megill] p. 447 (p. 15 of the preprint). (Contributed by DAW, 18-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | ex-natded9.26 20664 |
Theorem 9.26 of [Laboreo] p. 45, translated line by line using an
interpretation of natural deduction in Metamath. This proof has some
additional complications due to the fact that Metamath's existential
elimination rule does not change bound variables, so we need to verify
that is bound in the conclusion.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). Note that in the original proof, has explicit parameters. In Metamath, these parameters are always implicit, and the parameters upon which a wff variable can depend are recorded in the "allowed substitution hints" below. A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded9.26-2 20665. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) (Revised by David A. Wheeler, 18-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
18-Feb-2017 | sbcid 2937 | An identity theorem for substitution. See sbid 1895. (Contributed by Mario Carneiro, 18-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
13-Feb-2017 | 19.8ad 26876 | If a wff is true, it is true for at least one instance. Deductive form of 19.8a 1758. (Contributed by DAW, 13-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | resolution 26954 | Resolution rule. This is the primary inference rule in some automated theorem provers such as prover9. The resolution rule can be traced back to Davis and Putnam (1960). (Contributed by David A. Wheeler, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded9.26-2 20665 | A more efficient proof of Theorem 9.26 of [Laboreo] p. 45. Compare with ex-natded9.26 20664. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.13-2 20661 | A more efficient proof of Theorem 5.13 of [Laboreo] p. 20. Compare with ex-natded5.13 20660. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.13 20660 |
Theorem 5.13 of [Laboreo] p. 20, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.13-2 20661.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.8-2 20659 | A more efficient proof of Theorem 5.8 of [Laboreo] p. 20. For a longer line-by-line translation, see ex-natded5.8 20658. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.8 20658 |
Theorem 5.8 of [Laboreo] p. 20, translated line by line using the
usual translation of natural deduction (ND) in the
Metamath Proof Explorer (MPE) notation.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows
(the leading "..." shows an embedded ND hypothesis, beginning with
the initial assumption of the ND hypothesis):
The original used Latin letters; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. To add an assumption, the antecedent is modified to include it (typically by using adantr 453; simpr 449 is useful when you want to depend directly on the new assumption). Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.8-2 20659. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.7-2 20657 | A more efficient proof of Theorem 5.7 of [Laboreo] p. 19. Compare with ex-natded5.7 20656. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.7 20656 |
Theorem 5.7 of [Laboreo] p. 19, translated line by line using the
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.7-2 20657.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.3i 20654 | The same as ex-natded5.3 20652 and ex-natded5.3-2 20653 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.3-2 20653 | A more efficient proof of Theorem 5.3 of [Laboreo] p. 16. Compare with ex-natded5.3 20652 and ex-natded5.3i 20654. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.3 20652 |
Theorem 5.3 of [Laboreo] p. 16, translated line by line using an
interpretation of natural deduction in Metamath.
A much more efficient proof, using more of Metamath and MPE's
capabilities, is shown in ex-natded5.3-2 20653.
A proof without context is shown in ex-natded5.3i 20654.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.2i 20651 | The same as ex-natded5.2 20649 and ex-natded5.2-2 20650 but with no context. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.2-2 20650 | A more efficient proof of Theorem 5.2 of [Laboreo] p. 15. Compare with ex-natded5.2 20649 and ex-natded5.2i 20651. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | ex-natded5.2 20649 |
Theorem 5.2 of [Laboreo] p. 15, translated line by line using the
interpretation of natural deduction in Metamath.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
The original proof, which uses Fitch style, was written as follows:
The original used Latin letters for predicates; we have replaced them with Greek letters to follow Metamath naming conventions and so that it is easier to follow the Metamath translation. The Metamath line-for-line translation of this natural deduction approach precedes every line with an antecedent including and uses the Metamath equivalents of the natural deduction rules. Below is the final metamath proof (which reorders some steps). A much more efficient proof, using more of Metamath and MPE's capabilities, is shown in ex-natded5.2-2 20650. A proof without context is shown in ex-natded5.2i 20651. (Proof modification is discouraged.) (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | a4esbcd 3003 | form of a4sbc 2933. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | a4sbcd 2934 | Specialization: if a formula is true for all sets, it is true for any class which is a set. Similar to Theorem 6.11 of [Quine] p. 44. See also stdpc4 1896 and ra4sbc 2999. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | sbceq1dd 2927 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | sbceq1d 2926 | Equality theorem for class substitution. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | exlimdd 1933 | Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.21fal 1331 | If a wff and its negation are provable, then falsum is provable. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | efald 1330 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | inegd 1329 | Negation introduction rule from natural deduction. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | dfnot 1328 | Given falsum, we can define the negation of a wff as the statement that a contradiction follows from assuming . (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | falimd 1326 | implies anything. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.18da 432 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.01da 431 | Deduction based on reductio ad absurdum. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | exmidd 407 | Law of excluded middle in a context. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
9-Feb-2017 | pm2.21dd 101 | A contradiction implies anything. Deduction from pm2.21 102. (Contributed by Mario Carneiro, 9-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
8-Feb-2017 | notnotrd 107 | Deduction converting double-negation into the original wff, aka the double negation rule. A translation of natural deduction rule -C, => ; see natded 4. THis is definition NNC in [Pfenning] p. 17. This rule is valid in classical logic (which MPE uses), but not intuitionistic logic. (Contributed by DAW, 8-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
5-Feb-2017 | eelT 27238 | An elimination deduction. (Contributed by Alan Sare, 5-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3impdirp1 27281 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3impdir 1243 is ~? uun3132 and is in set.mm. 3impdirp1 27281 is ~? uun3132p1. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2221p2 27280 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2221p1 27279 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p4 27277 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p3 27276 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p2 27275 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123p1 27274 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun123 27273 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3anidm12p2 27272 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | 3anidm12p1 27271 | A deduction unionizing a non-unionized collection of virtual hypotheses. 3anidm12 1244 denotes the deduction which would have been named uun112 if it did not pre-exist in set.mm. This second permutation's name is based on this pre-existing name. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun111 27270 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p5 27269 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p4 27268 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p3 27267 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p2 27266 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12p1 27265 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT12 27264 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11p2 27263 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11p1 27262 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT11 27261 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1p2 27260 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1p1 27259 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunTT1 27258 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2131p1 27257 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun2131 27256 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | anabss7p1 27252 | A deduction unionizing a non-unionized collection of virtual hypotheses. This would have been named uun221 if the 0th permutation did not exist in set.mm as anabss7 797. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun132p1 27251 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun132 27250 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun121p1 27249 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uun121 27248 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | uunT1p1 27246 | A deduction unionizing a non-unionized collection of virtual hypotheses. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT0 27240 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0cT 27239 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTT 27236 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel00cT 27235 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0T1 27180 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT01 27179 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTT1 27178 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT12 27176 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT11 27173 | A elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelTTT 27171 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eelT00 27170 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel0TT 27169 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | eel000cT 27168 | An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | sbtT 27029 | A substitution into a theorem remains true. sbt 1905 with the existence of no virtual hypotheses for the hypothesis expressed as the empty virtual hypothesis collection. (Contributed by Alan Sare, 4-Feb-2017.) (Proof modification is discouraged.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
4-Feb-2017 | natded 4 |
Here are typical natural deduction (ND) rules in the style of Gentzen
and Jaśkowski, along with MPE translations of them.
This also shows the recommended theorems when you find yourself
needing these rules (the recommendations encourage a slightly
different proof style that works more naturally with metamath).
A decent list of the standard rules of natural deduction can be
found beginning with definition /\I in [Pfenning] p. 18.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
Many more citations could be added.
Note that MPE uses classical logic, not intuitionist logic. As is conventional, the "I" rules are introduction rules, "E" rules are elimination rules, the "C" rules are conversion rules, and represents the set of (current) hypotheses. We use wff variable names beginning with to provide a closer representation of the Metamath equivalents (which typically use the antedent to represent the context ). Most of this information was developed by Mario Carneiro and posted on 3-Feb-2017. For more information, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. For annotated examples where some traditional ND rules are directly applied in MPE, see ex-natded5.2 20649, ex-natded5.3 20652, ex-natded5.5 20655, ex-natded5.7 20656, ex-natded5.8 20658, ex-natded5.13 20660, ex-natded9.20 20662, and ex-natded9.26 20664. (Contributed by DAW, 4-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
31-Jan-2017 | 2p2ne5 26953 | Prove that . In George Orwell's "1984", Part One, Chapter Seven, the protagonist Winston notes that, "In the end the Party would announce that two and two made five, and you would have to believe it." http://www.sparknotes.com/lit/1984/section4.rhtml. More generally, the phrase has come to represent an obviously false dogma one may be required to believe. See the Wikipedia article for more about this: https://en.wikipedia.org/wiki/2_%2B_2_%3D_5. Unsurprisingly, we can easily prove that this claim is false. (Contributed by David A. Wheeler, 31-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
31-Jan-2017 | 5m4e1 26952 | Prove that 5 - 4 = 1. (Contributed by David A. Wheeler, 31-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | yoniso 13903 | If the codomain is recoverable from a hom-set, then the Yoneda embedding is injective on objects, and hence is an isomorphism from into a full subcategory of a presheaf category. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat CatCat FuncCat ↾_{s} _{f} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | fullres2c 13657 | Condition for a full functor to also be a full functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} Full Full | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | fthres2c 13649 | Condition for a faithful functor to also be a faithful functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} Faith Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
30-Jan-2017 | funcres2c 13619 | Condition for a functor to also be a functor into the restriction. (Contributed by Mario Carneiro, 30-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
↾_{s} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonffth 13902 | The Yoneda Lemma. The Yoneda embedding, the curried Hom functor, is full and faithful, and hence is a representation of the category as a full subcategory of the category of presheaves on . (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat _{f} Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yoneda 13901 | The Yoneda Lemma. There is a natural isomorphism between the functors and , where is the natural transformations from Yon to , and is the evaluation functor. Here we need two universes to state the claim: the smaller universe is used for forming the functor category ^{op} , which itself does not (necessarily) live in but instead is an element of the larger universe . (If is a Grothendieck universe, then it will be closed under this "presheaf" operation, and so we can set in this case.) (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonffthlem 13900 | Lemma for yonffth 13902. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Inv Full Faith | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedainv 13899 | The Yoneda Lemma with explicit inverse. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Inv | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem3b 13897 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat Nat comp comp | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem22 13896 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4c 13895 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} Nat | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4b 13894 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos _{func} _{F} ⟨,⟩_{F} _{F} _{f} _{f} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
29-Jan-2017 | yonedalem4a 13893 | Lemma for yoneda 13901. (Contributed by Mario Carneiro, 29-Jan-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Yon oppCat FuncCat Hom_{F} _{c} FuncCat eval_{F} _{func} tpos |