Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
17-Jan-2020 | addcom 6737 | Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.) |
17-Jan-2020 | ax-addcom 6584 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6558. Proofs should normally use addcom 6737 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
17-Jan-2020 | axaddcom 6558 |
Addition commutes. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 6584 be used later.
Instead, use addcom 6737.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) |
16-Jan-2020 | addid1 6738 | is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.) |
16-Jan-2020 | ax-0id 6592 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 6566.
Proofs should normally use addid1 6738 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
16-Jan-2020 | ax0id 6566 |
is an identity element
for real addition. Axiom for real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-0id 6592.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.) |
15-Jan-2020 | axltwlin 6682 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6597 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
15-Jan-2020 | axltirr 6681 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6596 with ordering on the extended reals. New proofs should use ltnr 6689 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
14-Jan-2020 | 2pwuninelg 5816 | The power set of the power set of the union of a set does not belong to the set. This theorem provides a way of constructing a new set that doesn't belong to a given set. (Contributed by Jim Kingdon, 14-Jan-2020.) |
13-Jan-2020 | 1re 6622 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
13-Jan-2020 | ax-1re 6578 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6552. Proofs should use 1re 6622 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
13-Jan-2020 | ax1re 6552 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 6578.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6577 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
12-Jan-2020 | ax-pre-ltwlin 6597 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6571. (Contributed by Jim Kingdon, 12-Jan-2020.) |
12-Jan-2020 | ax-pre-ltirr 6596 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.) |
12-Jan-2020 | ax-precex 6594 |
Existence of reciprocal of positive real number. Axiom for real and
complex numbers, justified by theorem axprecex 6568.
In treatments which assume excluded middle, the condition is generally replaced by . (Contributed by Jim Kingdon, 12-Jan-2020.) |
12-Jan-2020 | ax-0lt1 6590 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6564. Proofs should normally use 0lt1 6728 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
12-Jan-2020 | axpre-ltwlin 6571 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 6597. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
12-Jan-2020 | axpre-ltirr 6570 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 6596. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
12-Jan-2020 | axprecex 6568 |
Existence of reciprocal of positive real number. Axiom for real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-precex 6594.
In treatments which assume excluded middle, the condition is generally replaced by . (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
12-Jan-2020 | ax0lt1 6564 |
0 is less than 1. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-0lt1 6590.
The version of this axiom in the Metamath Proof Explorer reads ; here we change it to . The proof of from in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
8-Jan-2020 | ecidg 6077 | A set is equal to its converse epsilon coset. (Note: converse epsilon is not an equivalence relation.) (Contributed by Jim Kingdon, 8-Jan-2020.) |
5-Jan-2020 | 1idsr 6509 | 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.) |
4-Jan-2020 | distrsrg 6500 | Multiplication of signed reals is distributive. (Contributed by Jim Kingdon, 4-Jan-2020.) |
3-Jan-2020 | mulasssrg 6499 | Multiplication of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.) |
3-Jan-2020 | mulcomsrg 6498 | Multiplication of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.) |
3-Jan-2020 | addasssrg 6497 | Addition of signed reals is associative. (Contributed by Jim Kingdon, 3-Jan-2020.) |
3-Jan-2020 | addcomsrg 6496 | Addition of signed reals is commutative. (Contributed by Jim Kingdon, 3-Jan-2020.) |
3-Jan-2020 | caovlem2d 5612 | Rearrangement of expression involving multiplication () and addition (). (Contributed by Jim Kingdon, 3-Jan-2020.) |
2-Jan-2020 | bj-d0clsepcl 7287 | Δ_{0}-classical logic and separation implies classical logic. (Contributed by BJ, 2-Jan-2020.) (Proof modification is discouraged.) |
2-Jan-2020 | ax-bj-d0cl 7286 | Axiom for Δ_{0}-classical logic. (Contributed by BJ, 2-Jan-2020.) |
BOUNDED | ||
1-Jan-2020 | mulcmpblnrlemg 6481 | Lemma used in lemma showing compatibility of multiplication. (Contributed by Jim Kingdon, 1-Jan-2020.) |
31-Dec-2019 | eceq1d 6049 | Equality theorem for equivalence class (deduction form). (Contributed by Jim Kingdon, 31-Dec-2019.) |
30-Dec-2019 | mulsrmo 6485 | There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) |
30-Dec-2019 | addsrmo 6484 | There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.) |
30-Dec-2019 | prsrlem1 6483 | Decomposing signed reals into positive reals. Lemma for addsrpr 6486 and mulsrpr 6487. (Contributed by Jim Kingdon, 30-Dec-2019.) |
29-Dec-2019 | bj-omelon 7320 | The set is an ordinal. Constructive proof of omelon 4254. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
29-Dec-2019 | bj-omord 7319 | The set is an ordinal. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
29-Dec-2019 | bj-omtrans2 7318 | The set is transitive. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
29-Dec-2019 | bj-omtrans 7317 |
The set is
transitive. A natural number is included in
.
The idea is to use bounded induction with the formula . This formula, in a logic with terms, is bounded. So in our logic without terms, we need to temporarily replace it with and then deduce the original claim. (Contributed by BJ, 29-Dec-2019.) (Proof modification is discouraged.) |
29-Dec-2019 | ltrnqg 6271 | Ordering property of reciprocal for positive fractions. For a simplified version of the forward implication, see ltrnqi 6272. (Contributed by Jim Kingdon, 29-Dec-2019.) |
29-Dec-2019 | rec1nq 6248 | Reciprocal of positive fraction one. (Contributed by Jim Kingdon, 29-Dec-2019.) |
28-Dec-2019 | recexprlemupu 6456 | The upper cut of is upper. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | recexprlemopu 6455 | The upper cut of is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | recexprlemlol 6454 | The lower cut of is lower. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | recexprlemopl 6453 | The lower cut of is open. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | prmuloc2 6405 | Positive reals are multiplicatively located. This is a variation of prmuloc 6404 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio , there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | 1pru 6400 | The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) |
28-Dec-2019 | 1prl 6399 | The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.) |
27-Dec-2019 | recexprlemex 6465 | is the reciprocal of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemss1u 6464 | The upper cut of is a subset of the upper cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemss1l 6463 | The lower cut of is a subset of the lower cut of one. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlem1ssu 6462 | The upper cut of one is a subset of the upper cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlem1ssl 6461 | The lower cut of one is a subset of the lower cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlempr 6460 | is a positive real. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemloc 6459 | is located. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemdisj 6458 | is disjoint. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemrnd 6457 | is rounded. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemm 6452 | is inhabited. Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemelu 6451 | Membership in the upper cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
27-Dec-2019 | recexprlemell 6450 | Membership in the lower cut of . Lemma for recexpr 6466. (Contributed by Jim Kingdon, 27-Dec-2019.) |
26-Dec-2019 | ltaprg 6449 | Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. Part of Definition 11.2.7(vi) of [HoTT]], p. (varies). (Contributed by Jim Kingdon, 26-Dec-2019.) |
26-Dec-2019 | prarloc2 6352 | A Dedekind cut is arithmetically located. This is a variation of prarloc 6351 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance , there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.) |
25-Dec-2019 | addcanprlemu 6446 | Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.) |
25-Dec-2019 | addcanprleml 6445 | Lemma for addcanprg 6447. (Contributed by Jim Kingdon, 25-Dec-2019.) |
24-Dec-2019 | addcanprg 6447 | Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.) |
23-Dec-2019 | ltprordil 6422 | If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.) |
22-Dec-2019 | bj-findis 7336 | Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7308 for a bounded version not requiring ax-setind 4200. See finds 4246 for a proof in IZF. From this version, it is easy to prove of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.) |
21-Dec-2019 | ltexprlemupu 6435 | The upper cut of our constructed difference is upper. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
21-Dec-2019 | ltexprlemopu 6434 | The upper cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
21-Dec-2019 | ltexprlemlol 6433 | The lower cut of our constructed difference is lower. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
21-Dec-2019 | ltexprlemopl 6432 | The lower cut of our constructed difference is open. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
21-Dec-2019 | ltexprlemelu 6430 | Element in upper cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
21-Dec-2019 | ltexprlemell 6429 | Element in lower cut of the constructed difference. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 21-Dec-2019.) |
17-Dec-2019 | ltexprlemru 6443 | Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemfu 6442 | Lemma for ltexpri 6444. One direction of our result for upper cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemrl 6441 | Lemma for ltexpri 6444. Reverse directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemfl 6440 | Lemma for ltexpri 6444. One directon of our result for lower cuts. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlempr 6439 | Our constructed difference is a positive real. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemloc 6438 | Our constructed difference is located. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemdisj 6437 | Our constructed difference is disjoint. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemrnd 6436 | Our constructed difference is rounded. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.) |
17-Dec-2019 | ltexprlemm 6431 | Our constructed difference is inhabited. Lemma for ltexpri 6444. (Contributed by Jim Kingdon, 17-Dec-2019.) |
16-Dec-2019 | bj-sbime 7159 | A strengthening of sbie 1652 (same proof). (Contributed by BJ, 16-Dec-2019.) |
16-Dec-2019 | bj-sbimeh 7158 | A strengthening of sbieh 1651 (same proof). (Contributed by BJ, 16-Dec-2019.) |
16-Dec-2019 | bj-sbimedh 7157 | A strengthening of sbiedh 1648 (same proof). (Contributed by BJ, 16-Dec-2019.) |
16-Dec-2019 | ltsopr 6427 | Positive real 'less than' is a weak linear order (in the sense of df-iso 4004). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.) |
15-Dec-2019 | ltpopr 6426 | Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6427. (Contributed by Jim Kingdon, 15-Dec-2019.) |
15-Dec-2019 | ltdfpr 6354 | More convenient form of df-iltp 6318. (Contributed by Jim Kingdon, 15-Dec-2019.) |
15-Dec-2019 | prdisj 6340 | A Dedekind cut is disjoint. (Contributed by Jim Kingdon, 15-Dec-2019.) |
13-Dec-2019 | 1idpru 6424 | Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.) |
13-Dec-2019 | 1idprl 6423 | Lemma for 1idpr 6425. (Contributed by Jim Kingdon, 13-Dec-2019.) |
13-Dec-2019 | gtnqex 6397 | The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
13-Dec-2019 | ltnqex 6396 | The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.) |
13-Dec-2019 | sotritrieq 4032 | A trichotomy relationship, given a trichotomous order. (Contributed by Jim Kingdon, 13-Dec-2019.) |
12-Dec-2019 | distrprg 6421 | Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | distrlem5pru 6420 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | distrlem5prl 6419 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | distrlem4pru 6418 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | distrlem4prl 6417 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | distrlem1pru 6416 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
Copyright terms: Public domain | W3C HTML validation [external] |