Metamath Proof Explorer Most Recent Proofs |
||
Mirrors > Home > MPE Home > Th. List > Recent | Other > MM 100 |
The original proofs of theorems with recently shortened proofs can often be found by appending "OLD" to the theorem name, for example 19.43OLD for 19.43.
Other links Email: Norm Megill. Mailing list: Metamath Google Group Updated 18-Aug-2017 . Syndication: RSS feed (courtesy of Dan Getz). Related wikis: Wikiproofs (JHilbert) (Recent Changes); Ghilbert site; Ghilbert Google Group.
Recent news items (7-Aug-2017) Mario Carneiro added a new proof to the 100 theorem list, Principle of Inclusion/Exclusion incexc, bringing the Metamath total to 65.
(1-Jul-2017) Glauco Siliprandi added a new proof to the 100 theorem list, Stirling's Formula stirling, bringing the Metamath total to 64. Related theorems include 2 versions of Wallis' formula for π (wallispi and wallispi2).
(7-May-2017) Thierry Arnoux added a new proof to the 100 theorem list, Betrand's Ballot Problem ballotth, bringing the Metamath total to 63.
(20-Apr-2017) Glauco Siliprandi added a new proof in the supplementary list on the 100 theorem list, Stone-Weierstrass Theorem stowei.
(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 | ||
13-Aug-2017 | spnfw 1642 | Weak version of ax-4 2077. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) (Proof shortened by Wolf Lammen, 13-Aug-2017.) |
12-Aug-2017 | ax12b 1656 | Two equivalent ways of expressing ax-12 1867. See the comment for ax-12 1867. (Contributed by NM, 2-May-2017.) (Proof shortened by Wolf Lammen, 12-Aug-2017.) |
7-Aug-2017 | incexc2 12291 | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | incexc 12290 | The inclusion/exclusion principle for counting the elements of a finite union of finite sets. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | incexclem 12289 | Lemma for incexc 12290. (Contributed by Mario Carneiro, 7-Aug-2017.) |
7-Aug-2017 | spimw 1640 | Specialization. Lemma 8 of [KalishMontague] p. 87. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 19-Apr-2017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
7-Aug-2017 | spimfw 1628 | Specialization, with additional weakening to allow bundling of and . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-1017.) (Proof shortened by Wolf Lammen, 7-Aug-2017.) |
6-Aug-2017 | hashun3 11360 | The size of the union of finite sets is the sum of their sizes minus the size of the intersection. (Contributed by Mario Carneiro, 6-Aug-2017.) |
5-Aug-2017 | speimfw 1627 | Specialization, with additional weakening to allow bundling of and . Uses only Tarski's FOL axiom schemes. (Contributed by NM, 23-Apr-2017.) (Proof shortened by Wolf Lammen, 5-Aug-2017.) |
4-Aug-2017 | equequ2 1650 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2017.) |
3-Aug-2017 | a9ev 1639 | At least one individual exists. Weaker version of a9e 1892. When possible, use of this theorem rather than a9e 1892 is preferred since its derivation from axioms is much shorter. (Contributed by NM, 3-Aug-2017.) |
2-Aug-2017 | ralbinrald 27350 | Elemination of a restricted universal quantification under certain conditions. (Contributed by Alexander van der Vekens, 2-Aug-2017.) |
2-Aug-2017 | 19.2 1672 | Theorem 19.2 of [Margaris] p. 89. Note: This proof is very different from Margaris' because we only have Tarski's FOL axiom schemes available at this point. See the later 19.2g 1781 for a more conventional proof. (Contributed by NM, 2-Aug-2017.) |
1-Aug-2017 | dvelimfALT2 1736 | Proof of dvelimh 1940 without using ax-12 1867. (Contributed by Andrew Salmon, 21-Jul-2011.) (Revised by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.21h 1732 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.9v 1664 | Special case of Theorem 19.9 of [Margaris] p. 89. (Contributed by NM, 28-May-1995.) (Revised by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.3v 1663 | Special case of Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | 19.8w 1660 | Weak version of 19.8a 1719. Uses only Tarski's FOL axiom schemes. (Contributed by NM, 1-Aug-2017.) |
1-Aug-2017 | spnfwOLD 1659 | Weak version of ax-4 2077. Uses only Tarski's FOL axiom schemes. Obsolete version of spnfw 1642 as of 13-Aug-2017. (Contributed by NM, 1-Aug-2017.) (New usage is discouraged.) |
28-Jul-2017 | tz6.12-afv 27412 | Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27, , analogous to tz6.12-1 5504, but it is required for A to be a set. (Contributed by Alexander van der Vekens, 28-Jul-2017.) |
' | ||
25-Jul-2017 | funressnfv 27364 | A restriction to a singleton with a function value is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | funcoressn 27363 | A composition restricted to a singleton is a function under certain conditions. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | fnresfnco 27362 | Composition of two functions, similar to fnco 5317. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
25-Jul-2017 | funresfunco 27361 | Composition of two functions, generalization of funco 5257. (Contributed by Alexander van der Vekens, 25-Jul-2017.) |
23-Jul-2017 | afvco2 27414 | Value of a function composition, analogous to fvco2 5555. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
' '' | ||
23-Jul-2017 | dmfcoafv 27413 | Domains of a function composition, analogous to dmfco 5554. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
' | ||
23-Jul-2017 | csbafv12g 27377 | Move class substitution in and out of a function value, analogous to csbfv12g 5495, with a direct proof proposed by Mario Carneiro, analogous to csbovg 5850. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
' ' | ||
23-Jul-2017 | sbcfun 27358 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | csbdmg 27353 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | sbcrel 27352 | Distribute proper substitution through the domain of a class. (Contributed by Alexander van der Vekens, 23-Jul-2017.) |
23-Jul-2017 | sbcss 3565 | Distribute proper substitution through a subclass relation. (Contributed by Alan Sare, 22-Jul-2012.) (Proof shortened by Alexander van der Vekens, 23-Jul-2017.) |
22-Jul-2017 | logbid1 27527 | General logarithm when base and arg match (Contributed by David A. Wheeler, 22-Jul-2017.) |
logb | ||
22-Jul-2017 | logeq0im1 27523 | if then (Contributed by David A. Wheeler, 22-Jul-2017.) |
22-Jul-2017 | eldiftp 27522 | Membership in a set with three elements removed. Similar to eldifsn 3750 and eldifpr 27521. (Contributed by David A. Wheeler, 22-Jul-2017.) |
22-Jul-2017 | afvres 27411 | The value of a restricted function, analogous to fvres 5502. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
' ' | ||
22-Jul-2017 | afveq2 27375 | Equality theorem for function value, analogous to fveq1 5484. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
' ' | ||
22-Jul-2017 | afveq1 27374 | Equality theorem for function value, analogous to fveq1 5484. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
' ' | ||
22-Jul-2017 | dfafv2 27372 | Alternative definition of ' using directly. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
' def@ | ||
22-Jul-2017 | dfdfat2 27369 | Alternate definition of the predicate "defined at" not using the predicate. (Contributed by Alexander van der Vekens, 22-Jul-2017.) |
def@ | ||
18-Jul-2017 | eldifpr 27521 | Membership in a set with two elements removed. Similar to eldifsn 3750 and eldiftp 27522. (Contributed by Mario Carneiro, 18-Jul-2017.) |
17-Jul-2017 | logbcl 27526 | General logarithm closure. (Contributed by David A. Wheeler, 17-Jul-2017.) |
logb | ||
17-Jul-2017 | logccne0ALT 27525 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19950, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) |
17-Jul-2017 | logccne0 27524 | log isn't 0 if argument isn't 0 or 1. Unlike logne0 19950, this handles complex numbers. (Contributed by David A. Wheeler, 17-Jul-2017.) |
16-Jul-2017 | logb2aval 27520 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used in the 2-argument form logb (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) |
logb | ||
16-Jul-2017 | logbval 27519 | Define the value of the logb function, the logarithm generalized to an arbitrary base, when used as infix. Most Metamath statements select variables in order of their use, but to make the order clearer we use "B" for base and "X" for the other operand here. Proof is similar to modval 10969. (Contributed by David A. Wheeler, 21-Jan-2017.) (Revised by David A. Wheeler, 16-Jul-2017.) |
logb | ||
16-Jul-2017 | prmz 12756 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
14-Jul-2017 | df-log_ 27529 | Define the log_ operator. This is the logarithm generalized to an arbitrary base. It can be used as log_ for "log base B of X". This formulation suggested by Mario Carneiro. (Contributed by David A. Wheeler, 14-Jul-2017.) |
log_ | ||
2-Jul-2017 | eldmressnsn 27357 | The element of the domain of a restriction to a singleton is the element of the singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | dmressnsn 27356 | The domain of a restriction to a singleton is a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | eldmressn 27355 | Element of the domain of a restriction to a singleton. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | 2reu8 27349 | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu8 2231. Curiously, we can put on either of the internal conjuncts but not both. We can also commute using 2reu7 27348. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | 2reu7 27348 | Two equivalent expressions for double restricted existential uniqueness, analogous to 2eu7 2230. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | reuan 27337 | Introduction of a conjunct into restricted uniqueness quantifier, analogous to euan 2201. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | 2ralbiim 27331 | Split a biconditional and distribute 2 quantifiers, analogous to 2albiim 1600 and ralbiim 2681. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | cbvrex2 27330 | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvrex2v 2774. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | cbvral2 27329 | Change bound variables of double restricted universal quantification, using implicit substitution, analogous to cbvral2v 2773. (Contributed by Alexander van der Vekens, 2-Jul-2017.) |
2-Jul-2017 | climreeq 27138 | If is a real function, then converges to with respect to the standard topology on the reals if and only if it converges to with respect to the standard topology on complex numbers. In the theorem, is defined to be convergence w.r.t. the standard topology on the reals and then represents the statement " converges to , with respect to the standard topology on the reals". Notice that there is no need for the hypothesis that is a real number. (Contributed by Glauco Siliprandi, 2-Jul-2017.) |
1-Jul-2017 | 2reu4 27347 | Definition of double restricted existential uniqueness ("exactly one and exactly one "), analogous to 2eu4 2227. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
1-Jul-2017 | 2reu4a 27346 | Definition of double restricted existential uniqueness ("exactly one and exactly one "), analogous to 2eu4 2227 with the additional requirement that the restricting classes are not empty (which is not necessary as shown in 2reu4 27347). (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
1-Jul-2017 | 2rexrsb 27328 | An equivalent expression for double restricted existence, analogous to 2exsb 2074. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
1-Jul-2017 | 2rexsb 27327 | An equivalent expression for double restricted existence, analogous to rexsb 27325. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
1-Jul-2017 | rexrsb 27326 | An equivalent expression for restricted existence, analogous to exsb 2072. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
1-Jul-2017 | rexsb 27325 | An equivalent expression for restricted existence, analogous to exsb 2072. (Contributed by Alexander van der Vekens, 1-Jul-2017.) |
30-Jun-2017 | stirlinglem1 27222 | A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
30-Jun-2017 | wallispi2lem2 27220 | Two expressions are proven to be equal, and this is used to complete the proof of the second version of Wallis' formula for π . (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
30-Jun-2017 | wallispi2lem1 27219 | An intermediate step between the first version of the Wallis' formula for π and the second version of Wallis' formula. This second version will then be used to prove Stirling's approximation formula for the factorial. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
30-Jun-2017 | wallispilem5 27217 | The sequence converges to 1. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
30-Jun-2017 | wallispilem4 27216 | maps to explicit expression for the ratio of two consecutive values of (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
30-Jun-2017 | mulc1cncfg 27120 | A version of mulc1cncf 18403 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 30-Jun-2017.) |
29-Jun-2017 | 2reu3 27345 | Double restricted existential uniqueness, analogous to 2eu3 2226. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
29-Jun-2017 | 2reu2 27344 | Double restricted existential uniqueness, analogous to 2eu2 2225. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
29-Jun-2017 | raaan2 27332 | Rearrange restricted quantifiers with two different restricting classes, analogous to raaan 3562. It is necessary that either both restricting classes are empty or both are not empty. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
29-Jun-2017 | r19.32 27324 | Theorem 19.32 of [Margaris] p. 90 with restricted quantifiers, analogous to r19.32v 2687. (Contributed by Alexander van der Vekens, 29-Jun-2017.) |
29-Jun-2017 | stirlingr 27238 | Stirling's approximation formula for factorial: here convergence is expressed with respect to the standard topology on the reals. The main theorem stirling 27237 is proven for convergence in the topology of complex numbers. The variable is used to denote convergence with respect to the standard topology on the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirling 27237 | Stirling's approximation formula for factorial. The proof follows two major steps: first it is proven that and factorial are asymptotically equivalent, up to an unknown constant. Then, using Wallis' formula for π it is proven that the unknown constant is the square root of π and then the exact Stirling's formula is established. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem15 27236 | The Stirling's formula is proven using a number of local definitions. The main theorem stirling 27237 will use this final lemma, but it will not expose the local definitions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem14 27235 | The sequence converges to a positive real. This proves that the Stirling's formula converges to the factorial, up to a constant. In another theorem, using Wallis' formula for π& , such constant is exactly determined, thus proving the Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem13 27234 | is decreasing and has a lower bound, then it converges. Since is , in another theorem it is proven that converges also. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem12 27233 | The sequence is bounded below. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem11 27232 | is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem10 27231 | A bound for any B(N)-B(N + 1) that will allow to find a lower bound for the whole sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem9 27230 | is expressed as a limit of a series. This result will be used both to prove that is decreasing and to prove that is bounded (below). It will follow that converges in the reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem8 27229 | If converges to , then converges to C^2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem7 27228 | Algebraic manipulation of the formula for J(n) (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem6 27227 | A series that converges to log (N+1)/N (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem5 27226 | If is between and , then a series (without alternating negative and positive terms) is given that converges to log (1+T)/(1-T) . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem4 27225 | Algebraic manipulation of n ) - ( B . It will be used in other theorems to show that is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem3 27224 | Long but simple algebraic transformations are applied to show that , the Wallis formula for π , can be expressed in terms of , the Stirling's approximation formula for the factorial, up to a constant factor. This will allow (in a later theorem) to determine the right constant factor to be put into the , in order to get the exact Stirling's formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | stirlinglem2 27223 | maps to positive reals. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | wallispi2 27221 | An alternative version of Wallis' formula for π ; this second formula uses factorials and it is later used to proof Stirling's approximation formula. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | wallispi 27218 | Wallis' formula for π : Wallis' product converges to π / 2 . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | wallispilem3 27215 | I maps to real values (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | wallispilem2 27214 | A first set of properties for the sequence that will be used in the proof of the Wallis product formula (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | wallispilem1 27213 | is monotone: increasing the exponent, the integral decreases. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | itgsinexp 27148 |
A recursive formula for the integral of sin^N on the interval (0,π) .
(Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | itgsinexplem1 27147 | Integration by parts is applied to integrate sin^(N+1) (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | iblioosinexp 27146 | sin^n on an open integral is integrable (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | itgsin0pi 27145 | Calculation of the integral for sine on the (0,π) interval (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | ibliccsinexp 27144 | sin^n on a closed interval is integrable. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | itgsin0pilem1 27143 | Calculation of the integral for sine on the (0,π) interval (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | volioo 27142 | The measure of an open interval. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | ioovolcl 27141 | An open real interval has finite volume. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | dvcosre 27140 | The real derivative of the cosine (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | dvsinexp 27139 | The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climdivf 27137 | Limit of the ratio of two converging sequences. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climinff 27136 | A version of climinf 27131 using bound-variable hypotheses instead of distinct variable conditions (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climneg 27135 | Complex limit of the negative of a sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climrecf 27134 | A version of climrec 27128 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climsuse 27133 | A subsequence of a converging sequence , converges to the same limit. is the strictly increasing and it is used to index the subsequence (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climsuselem1 27132 | The subsequence index has the expected properties: it belongs to the same upper integers as the original index, and it is always larger or equal than the original index. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climinf 27131 | A bounded monotonic non increasing sequence converges to the infimum of its range. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climexp 27130 | The limit of natural powers, is the natural power of the limit. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climmulf 27129 | A version of climmul 12100 using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | climrec 27128 | Limit of the reciprocal of a converging sequence. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | isumneg 27127 | Negation of a converging sum. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | clim1fr1 27126 | A class of sequences of fractions that converge to 1 (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | expcnfg 27125 | If is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf 27122. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | m1expeven 27124 | Exponentiation of negative one to an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | eluzelcn 27123 | A member of a set of upper integers is a complex number. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | expcncf 27122 | The power function on complex numbers, for fixed exponent N, is continuous. Similar to expcn 18370. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | infrglb 27121 | The infimum of a non-empty bounded set of reals is the greatest lower bound. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | mulcncf 27119 | The multiplication of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | rrpsscn 27118 | The positive reals are a subset of the complex numbers. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | fmptdf 27117 | A version of fmptd 5645 using bound-variable hypothesis instead of a distinct variable condition for . (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
29-Jun-2017 | cncfmptss 27116 | A continuous complex function restricted to a subset is continuous, using "map to" notation. (Contributed by Glauco Siliprandi, 29-Jun-2017.) |
25-Jun-2017 | 2reu1 27343 | Double restricted existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one, analogous to 2eu1 2224. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
25-Jun-2017 | 2rexreu 27342 | Double restricted existential uniqueness implies double restricted uniqueness quantification, analogous to 2exeu 2221. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
25-Jun-2017 | 2rmoswap 27341 | A condition allowing swap of restricted "at most one" and restricted existential quantifiers, analogous to 2moswap 2219. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
25-Jun-2017 | 2reu2rex 27340 | Double restricted existential uniqueness, analogous to 2eu2ex 2218. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
25-Jun-2017 | rmoanim 27336 | Introduction of a conjunct into restricted "at most one" quantifier, analogous to moanim 2200. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
25-Jun-2017 | reuimrmo 27335 | Restricted uniqueness implies restricted "at most one" through implication, analogous to euimmo 2193. (Contributed by Alexander van der Vekens, 25-Jun-2017.) |
24-Jun-2017 | 2reurmo 27339 | Double restricted quantification with restricted existential uniqueness and restricted "at most one.", analogous to 2eumo 2217. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
24-Jun-2017 | 2reurex 27338 | Double restricted quantification with existential uniqueness, analogous to 2euex 2216. (Contributed by Alexander van der Vekens, 24-Jun-2017.) |
17-Jun-2017 | 2reu5a 27334 | Double restricted existential uniqueness in terms of restricted existence and restricted "at most one." (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoimi 27333 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | idomsubgmo 26913 | The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Revised by NM, 17-Jun-2017.) |
mulGrp ↾_{s} Unit IDomn SubGrp | ||
17-Jun-2017 | hilbert1.2 24185 | There is at most one line through any two distinct points. Hilbert's axiom I.2 for geometry. (Contributed by Scott Fenton, 29-Oct-2013.) (Revised by NM, 17-Jun-2017.) |
LinesEE | ||
17-Jun-2017 | cvmliftmo 23219 | A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
CovMap 𝑛Locally | ||
17-Jun-2017 | ply1divmo 19515 | Uniqueness of a quotient in a polynomial division. For polynomials such that and the leading coefficient of is not a zero divisor, there is at most one polynomial which satisfies where the degree of is less than the degree of . (Contributed by Stefan O'Rear, 26-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
Poly_{1} deg_{1} coe_{1} RLReg | ||
17-Jun-2017 | 2ndcdisj2 17177 | Any disjoint collection of open sets in a second-countable space is countable. (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | 2ndcdisj 17176 | Any disjoint family of open sets in a second-countable space is countable. (The sets are required to be nonempty because otherwise there could be many empty sets in the family.) (Contributed by Mario Carneiro, 21-Mar-2015.) (Proof shortened by Mario Carneiro, 9-Apr-2015.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | lspextmo 15807 | A linear function is completely determined (or overdetermined) by its values on a spanning subset. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by NM, 17-Jun-2017.) |
LMHom | ||
17-Jun-2017 | mgmidmo 14364 | A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | sqrmo 11731 | Uniqueness for the square root function. (Contributed by Mario Carneiro, 9-Jul-2013.) (Revised by NM, 17-Jun-2017.) |
17-Jun-2017 | rmorabex 4232 | Restricted "at most one" existence implies a restricted class abstraction exists. (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | dfdisj2 3996 | Alternate definition for disjoint classes. (Contributed by NM, 17-Jun-2017.) |
Disj | ||
17-Jun-2017 | rmo2i 3078 | Condition implying restricted "at most one." (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | rmo2 3077 | Alternate definition of restricted "at most one." Note that is not equivalent to (in analogy to reu6 2955); to see this, let be the empty set. However, one direction of this pattern holds; see rmo2i 3078. (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | 2reu5 2974 | Double restricted existential uniqueness in terms of restricted existential quantification and restricted universal quantification, analogous to 2eu5 2228 and reu3 2956. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | 2reu5lem3 2973 | Lemma for 2reu5 2974. This lemma is interesting in its own right, showing that existential restriction in the last conjunct (the "at most one" part) is optional; compare rmo2 3077. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | 2reu5lem2 2972 | Lemma for 2reu5 2974. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | 2reu5lem1 2971 | Lemma for 2reu5 2974. Note that does not mean "there is exactly one in and exactly one in such that holds;" see comment for 2eu5 2228. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | 2rmorex 2970 | Double restricted quantification with "at most one," analogous to 2moex 2215. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoimi2 2967 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoimia 2966 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoim 2965 | Restricted "at most one" is preserved through implication (note wff reversal). (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmov 2805 | A uniqueness quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | cbvrmov 2768 | Change the bound variable of a restricted uniqueness quantifier using implicit substitution. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | nrexrmo 2758 | Nonexistence implies restricted "at most one". (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | rmoeqd 2748 | Equality deduction for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoeq1 2740 | Equality theorem for restricted uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | rmoeq1f 2736 | Equality theorem for restricted uniqueness quantifier, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
17-Jun-2017 | nfrmod 2714 | Deduction version of nfrmo 2716. (Contributed by NM, 17-Jun-2017.) |
17-Jun-2017 | sb8mo 2163 | Variable substitution in uniqueness quantifier. (Contributed by Alexander van der Vekens, 17-Jun-2017.) |
16-Jun-2017 | spwmo 14329 | A poset has at most one supremum. (Contributed by NM, 13-May-2008.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | poslubmo 14244 | Least upper bounds in a poset are unique if they exist. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | brdom7disj 8151 | An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 29-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | brdom4 8150 | An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | iunmapdisj 7645 | The union is a disjoint union. (Contributed by Mario Carneiro, 17-May-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | moriotass 6329 | Restriction of a unique element to a smaller class. (Contributed by NM, 19-Feb-2006.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | dffun9 5248 | Alternate definition of a function. (Contributed by NM, 28-Mar-2007.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | reuxfr2 4557 | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 14-Nov-2004.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | reuxfr2d 4556 | Transfer existential uniqueness from a variable to another variable contained in expression . (Contributed by NM, 16-Jan-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | somo 4347 | A totally ordered set has at most one minimal element. (Contributed by Mario Carneiro, 24-Jun-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | df-disj 3995 | A collection of classes is disjoint when for each element , it is in for at most one . (Contributed by Mario Carneiro, 14-Nov-2016.) (Revised by NM, 16-Jun-2017.) |
Disj | ||
16-Jun-2017 | rmoi 3081 | Consequence of "at most one", using implicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | rmob 3080 | Consequence of "at most one", using implicit substitution. (Contributed by NM, 2-Jan-2015.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo3 3079 | Restricted "at most one" using explicit substitution. (Contributed by NM, 4-Nov-2012.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | 2reuswap 2968 | A condition allowing swap of uniqueness and existential quantifiers. (Contributed by Thierry Arnoux, 7-Apr-2017.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | rmoan 2964 | Restricted "at most one" still holds when a conjunct is added. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo4 2959 | Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | cbvrmo 2764 | Change the bound variable of restricted "at most one" using implicit substitution. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmo5 2757 | Restricted "at most one" in term of uniqueness. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | reurmo 2756 | Restricted existential uniqueness implies restricted "at most one." (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | reu5 2754 | Restricted uniqueness in terms of "at most one." (Contributed by NM, 23-May-1999.) (Revised by NM, 16-Jun-2017.) |
16-Jun-2017 | mormo 2753 | Unrestricted "at most one" implies restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobii 2732 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobiia 2731 | Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobidv 2730 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobidva 2729 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | rmobida 2728 | Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | nfrmo 2716 | Bound-variable hypothesis builder for restricted uniqueness. (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | nfrmo1 2712 | is not free in . (Contributed by NM, 16-Jun-2017.) |
16-Jun-2017 | df-rmo 2552 | Define restricted "at most one". (Contributed by NM, 16-Jun-2017.) |
1-Jun-2017 | afvelrnb0 27403 | A member of a function's range is a value of the function, only one direction of implication of fvelrnb 5531. (Contributed by Alexander van der Vekens, 1-Jun-2017.) |
' | ||
1-Jun-2017 | dmmpt2g 27354 | Domain of a class given by the "maps to" notation, closed form of dmmpt2 6155. (Contributed by Alexander van der Vekens, 1-Jun-2017.) |
26-May-2017 | ndmaovdistr 27446 | Any operation is distributive outside its domain. In contrast to ndmaovdistr 27446 where it is required that the operation's domain doesn't contain the empty set ( ), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(( (()) )) (( (()) (()) )) | ||
26-May-2017 | ndmaovass 27445 | Any operation is associative outside its domain. In contrast to ndmaovass 27445 where it is required that the operation's domain doesn't contain the empty set ( ), no additional assumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(( (()) )) (( (()) )) | ||
26-May-2017 | ndmaovcom 27444 | Any operation is commutative outside its domain, analogous to ndmovcom 5968. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | ndmaovrcl 27443 | Reverse closure law, in contrast to ndmovrcl 5967 where it is required that the operation's domain doesn't contain the empty set ( ), no additional asumption is required. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | ndmaovcl 27442 | The "closure" of an operation outside its domain, when the operation's value is a set in contrast to ndmovcl 5966 where it is required that the domain contains the empty set ( ). (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) (()) | ||
26-May-2017 | aoprssdm 27441 | Domain of closure of an operation. In contrast to oprssdm 5963, no additional property for S ( ) is required! (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovmpt4g 27440 | Value of a function given by the "maps to" notation, analogous to ovmpt4g 5931. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | faovcl 27439 | Closure law for an operation, analogous to fovcl 5910. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | ffnaov 27438 | An operation maps to a class to which all values belong, analogous to ffnov 5909. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | fnotaovb 27437 | Equivalence of operation value and ordered triple membership, analogous to fnopfvb 5525. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | rspceaov 27436 | A frequently used special case of rspc2ev 2893 for operation values, analogous to rspceov 5854. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | aovov0bi 27435 | The operation's value on an ordered pair is the empty set if and only if the alternative value of the operation on this ordered pair is either the empty set or the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | aov0nbovbi 27434 | The operation's value on an ordered pair is an element of a set if and only if the alternative value of the operation on this ordered pair is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovovn0oveq 27433 | If the operation's value at an argument is not the empty set, it equals the value of the alternative operation at this argument. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aov0ov0 27432 | If the alternative value of the operation on an ordered pair is the empty set, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovvoveq 27431 | The alternative value of the operation on an ordered pair equals the operation's value on this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | aovnuoveq 27430 | The alternative value of the operation on an ordered pair equals the operation's value at this ordered pair. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | aovpcov0 27429 | If the alternative value of the operation on an ordered pair is the universal class, the operation's value at this ordered pair is the empty set. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovrcl 27428 | Reverse closure for an operation value, analogous to afvvv 27385. In contrast to ovrcl 5849, elementhood of the operation's value in a set is required, not containing an element. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovprc 27427 | The value of an operation when the one of the arguments is a proper class, analogous to ovprc 5846. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovvfunressn 27426 | If the operation value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | nfunsnaov 27425 | If the restriction of a class to a singleton is not a function, its operation value is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovvdm 27424 | If the operation value of a class for an ordered pair is a set, the ordered pair is contained in the domain of the class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | ndmaovg 27423 | The value of an operation outside its domain, analogous to ndmovg 5964. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | ndmaov 27422 | The value of an operation outside its domain, analogous to ndmafv 27380. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aovnfundmuv 27421 | If an ordered pair is not in the domain of a class or the class is not a function restricted to the ordered pair, then the operation value for this pair is the universal class. (Contributed by Alexander van der Vekens, 26-May-2017.) |
def@ (()) | ||
26-May-2017 | aovfundmoveq 27420 | If a class is a function restricted to an ordered pair of its domain, then the value of the operation on this pair is equal for both definitions. (Contributed by Alexander van der Vekens, 26-May-2017.) |
def@ (()) | ||
26-May-2017 | csbaovg 27419 | Move class substitution in and out of an operation. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (( )) | ||
26-May-2017 | nfaov 27418 | Bound-variable hypothesis builder for operation value, analogous to nfov 5842. To prove a deduction version of this analogous to nfovd 5841 is not quickly possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of alternative operation values is based on are not available (see nfafv 27376). (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) | ||
26-May-2017 | aoveq123d 27417 | Equality deduction for operation value, analogous to oveq123d 5840. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) (()) | ||
26-May-2017 | df-aov 27416 | Define the value of an operation. In contrast to df-ov 5822, the alternative definition for a function value ( see df-afv 27371) is used. By this, the value of the operation applied to two arguments is the universal class if the operation is not defined for these two arguments. There are still no restrictions of any kind on what those class expressions may be, although only certain kinds of class expressions - a binary operation and its arguments and - will be useful for proving meaningful theorems. (Contributed by Alexander van der Vekens, 26-May-2017.) |
(()) ' | ||
26-May-2017 | afvnfundmuv 27379 | If a set is not in the domain of a class or the class is not a function restricted to the set, then the function value for this set is the universe. (Contributed by Alexander van der Vekens, 26-May-2017.) |
def@ ' | ||
26-May-2017 | nfafv 27376 | Bound-variable hypothesis builder for function value, analogous to nffv 5492. To prove a deduction version of this analogous to nffvd 5494 is not easily possible because a deduction version of nfdfat 27368 cannot be shown easily. (Contributed by Alexander van der Vekens, 26-May-2017.) |
' | ||
26-May-2017 | afveq12d 27373 | Equality deduction for function value, analogous to fveq12d 5491. (Contributed by Alexander van der Vekens, 26-May-2017.) |
' ' | ||
26-May-2017 | nfdfat 27368 | Bound-variable hypothesis builder for "defined at". To prove a deduction version of this theorem is not easily possible because many deduction versions for bound-variable hypothesis builder for constructs the definition of "defined at" is based on are not available (e.g. for Fun/Rel, dom, C_, etc.). (Contributed by Alexander van der Vekens, 26-May-2017.) |
def@ | ||
26-May-2017 | dfateq12d 27367 | Equality deduction for "defined at". (Contributed by Alexander van der Vekens, 26-May-2017.) |
def@ def@ | ||
26-May-2017 | fveqvfvv 27360 | If a function's value at an argument is the universal class (which can never be the case because of fvex 5499), the function's value at this argument is any set (especially the empty set). In short "If a function's value is a proper class, it is a set", which sounds strange/contradictory, but which is a consequence of that a contradiction implies anything ( see pm2.21i 125). (Contributed by Alexander van der Vekens, 26-May-2017.) |
26-May-2017 | fvfundmfvn0 27359 | If a class' value at an argument is not the empty set, the argument is contained in the domain of the class, and the class restricted to the argument is a function. (Contributed by Alexander van der Vekens, 26-May-2017.) |
26-May-2017 | nvelim 27351 | If a class is the universal class it doesn't belong to any class, generalisation of nvel 4154. (Contributed by Alexander van der Vekens, 26-May-2017.) |
25-May-2017 | ffnafv 27410 | A function maps to a class to which all values belong, analogous to ffnfv 5646. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | fafvelrn 27409 | A function's value belongs to its codomain, analogous to ffvelrn 5624. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | fnafvelrn 27408 | A function's value belongs to its range, analogous to fnfvelrn 5623. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvelrn 27407 | A function's value belongs to its range, analogous to fvelrn 5622. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvelima 27406 | Function value in an image, analogous to fvelima 5535. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | dfaimafn2 27405 | Alternate definition of the image of a function as an indexed union of singletons of function values, analogous to dfimafn2 5533. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | dfaimafn 27404 | Alternate definition of the image of a function, analogous to dfimafn 5532. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvelrnb 27402 | A member of a function's range is a value of the function, analogous to fvelrnb 5531 with the additional requirement that the member must be a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | fnrnafv 27401 | The range of a function expressed as a collection of the function's values, analogous to fnrnfv 5530. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | dfafn5b 27400 | Representation of a function in terms of its values, analogous to dffn5 5529 (only if it is assumed that the function value for each x is a set). (Contributed by Alexander van der Vekens, 25-May-2017.) |
' ' | ||
25-May-2017 | dfafn5a 27399 | Representation of a function in terms of its values, analogous to dffn5 5529 (only one direction of implication!). (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | funbrafv2b 27398 | Function value in terms of a binary relation, analogous to funbrfv2b 5528. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | funbrafv 27397 | The second argument of a binary relation on a function is the function's value, analogous to funbrfv 5522. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | funopafvb 27396 | Equivalence of function value and ordered pair membership, analogous to funopfvb 5527. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | funbrafvb 27395 | Equivalence of function value and binary relation, analogous to funbrfvb 5526. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | fnopafvb 27394 | Equivalence of function value and ordered pair membership, analogous to fnopfvb 5525. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | fnbrafvb 27393 | Equivalence of function value and binary relation, analogous to fnbrfvb 5524. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvfv0bi 27392 | The function's value at an argument is the empty set if and only if the value of the alternative function at this argument is either the empty set or the universe. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' ' | ||
25-May-2017 | afv0nbfvbi 27391 | The function's value at an argument is an element of a set if and only if the value of the alternative function at this argument is an element of that set, if the set does not contain the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvfvn0fveq 27390 | If the function's value at an argument is not the empty set, it equals the value of the alternative function at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afv0fv0 27389 | If the value of the alternative function at an argument is the empty set, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvvfveq 27388 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' ' | ||
25-May-2017 | afvnufveq 27387 | The value of the alternative function at a set as argument equals the function's value at this argument. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' ' | ||
25-May-2017 | afvpcfv0 27386 | If the value of the alternative function at an argument is the universe, the function's value at this argument is the empty set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvvv 27385 | If a function's value at an argument is a set, the argument is also a set. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvprc 27384 | A function's value at a proper class is the universe, compare with fvprc 5482. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvvfunressn 27383 | If the function value of a class for an argument is a set, the class restricted to the singleton of the argument is a function. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | nfunsnafv 27382 | If the restriction of a class to a singleton is not a function, its value is the universe, compare with nfunsn 5519 (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvvdm 27381 | If the function value of a class for an argument is a set, the argument is contained in the domain of the class. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | ndmafv 27380 | The value of a class outside its domain is the universe, compare with ndmfv 5513. (Contributed by Alexander van der Vekens, 25-May-2017.) |
' | ||
25-May-2017 | afvfundmfveq 27378 | If a class is a function restricted to a member of its domain, then the function value for this member is equal for both definitions. (Contributed by Alexander van der Vekens, 25-May-2017.) |
def@ ' | ||
25-May-2017 | df-afv 27371 | Alternative definition of the value of a function, ', also known as function application. In contrast to ' (see df-fv 5229 and ndmfv 5513), ' if F is not defined for A! (Contributed by Alexander van der Vekens, 25-May-2017.) |
' def@ | ||
25-May-2017 | df-dfat 27366 | Definition of the predicate that determines if some class is defined as function for an argument or, in other words, if the function value for some class for an argument is defined. We say that is defined at if a is a function restricted to the member of its domain. (Contributed by Alexander van der Vekens, 25-May-2017.) |
def@ | ||
18-May-2017 | fsnunfv 5681 | Recover the added point from a point-added function. (Contributed by Stefan O'Rear, 28-Feb-2015.) (Revised by NM, 18-May-2017.) |
5-May-2017 | ballotlemsima 23067 | The image by of an interval before the first pick. (Contributed by Thierry Arnoux, 5-May-2017.) |
2-May-2017 | addeq0 23036 | Two complex which add up to zero are each other's negatives. (Contributed by Thierry Arnoux, 2-May-2017.) |
2-May-2017 | fzsplit3 23023 | Split a finite interval of integers into two parts. (Contributed by Thierry Arnoux, 2-May-2017.) |
2-May-2017 | ax12bOLD 1657 | Obsolete version of ax12b 1656 as of 12-Aug-2017. (Contributed by NM, 2-May-2017.) (New usage is discouraged.) |
1-May-2017 | lvecdim 15904 | The dimension theorem for vector spaces: any two bases of the same vector space are equinumerous. Proven by using lssacsex 15891 and lbsacsbs 15903 to show that being a basis for a vector space is equivalent to being a basis for the associated algebraic closure system, and then using acsexdimd 14280. (Contributed by David Moews, 1-May-2017.) |
LBasis | ||
1-May-2017 | lbsacsbs 15903 | Being a basis in a vector space is equivalent to being a basis in the associated algebraic closure system. Equivalent to islbs2 15901. (Contributed by David Moews, 1-May-2017.) |
mrCls mrInd LBasis | ||
1-May-2017 | lssacsex 15891 | In a vector space, subspaces form an algebraic closure system whose closure operator has the exchange property. Strengthening of lssacs 15718 by lspsolv 15890. (Contributed by David Moews, 1-May-2017.) |
mrCls ACS | ||
1-May-2017 | acsexdimd 14280 | In an algebraic closure system whose closure operator has the exchange property, if two independent sets have equal closure, they are equinumerous. See mreexfidimd 13546 for the finite case and acsinfdimd 14279 for the infinite case. This is a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsinfdimd 14279 | In an algebraic closure system, if two independent sets have equal closure and one is infinite, then they are equinumerous. This is proven by using acsdomd 14278 twice with acsinfd 14277. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsdomd 14278 | In an algebraic closure system, if and have the same closure and is infinite independent, then dominates . This follows from applying acsinfd 14277 and then applying unirnfdomd 8184 to the map given in acsmap2d 14276. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsinfd 14277 | In an algebraic closure system, if and have the same closure and is infinite independent, then is infinite. This follows from applying unirnffid 7142 to the map given in acsmap2d 14276. See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsmap2d 14276 | In an algebraic closure system, if and have the same closure and is independent, then there is a map from into the set of finite subsets of such that equals the union of . This is proven by taking the map from acsmapd 14275 and observing that, since and have the same closure, the closure of must contain . Since is independent, by mrissmrcd 13536, must equal . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsmapd 14275 | In an algebraic closure system, if is contained in the closure of , there is a map from into the set of finite subsets of such that the closure of contains . This is proven by applying acsficl2d 14273 to each element of . See Section II.5 in [Cohn] p. 81 to 82. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsfiindd 14274 | In an algebraic closure system, a set is independent if and only if all its finite subsets are independent. Part of Proposition 4.1.3 in [FaureFrolicher] p. 83. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls mrInd | ||
1-May-2017 | acsficl2d 14273 | In an algebraic closure system, an element is in the closure of a set if and only if it is in the closure of a finite subset. Alternate form of acsficl 14268. Deduction form. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsficld 14272 | In an algebraic closure system, the closure of a set is the union of the closures of its finite subsets. Deduction form of acsficl 14268. (Contributed by David Moews, 1-May-2017.) |
ACS mrCls | ||
1-May-2017 | acsmred 13552 | An algebraic closure system is also a Moore system. Deduction form of acsmre 13548. (Contributed by David Moews, 1-May-2017.) |
ACS Moore | ||
1-May-2017 | mreexfidimd 13546 | In a Moore system whose closure operator has the exchange property, if two independent sets have equal closure and one is finite, then they are equinumerous. Proven by using mreexdomd 13545 twice. This implies a special case of Theorem 4.2.2 in [FaureFrolicher] p. 87. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexdomd 13545 | In a Moore system whose closure operator has the exchange property, if is independent and contained in the closure of , and either or is finite, then dominates . This is an immediate consequence of mreexexd 13544. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexd 13544 | Exchange-type theorem. In a Moore system whose closure operator has the exchange property, if and are disjoint from , is independent, is contained in the closure of , and either or is finite, then there is a subset of equinumerous to such that is independent. This implies the case of Proposition 4.2.1 in [FaureFrolicher] p. 86 where either or is finite. The theorem is proven by induction using mreexexlem3d 13542 for the base case and mreexexlem4d 13543 for the induction step. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd | ||
1-May-2017 | mreexexlem4d 13543 | Induction step of the induction in mreexexd 13544. (Contributed by David Moews, 1-May-2017.) |
Moore mrCls mrInd |