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.) |
12-Dec-2019 | distrlem1prl 6415 | Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.) |
12-Dec-2019 | ltdcnq 6250 | Less-than for positive fractions is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) |
DECID | ||
12-Dec-2019 | ltdcpi 6177 | Less-than for positive integers is decidable. (Contributed by Jim Kingdon, 12-Dec-2019.) |
DECID | ||
11-Dec-2019 | mulassprg 6414 | Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | mulcomprg 6413 | Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | addassprg 6412 | Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | addcomprg 6411 | Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | genpassg 6375 | Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | genpassu 6374 | Associativity of upper cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | genpassl 6373 | Associativity of lower cuts. Lemma for genpassg 6375. (Contributed by Jim Kingdon, 11-Dec-2019.) |
11-Dec-2019 | preqlu 6320 | Two reals are equal if and only if their lower and upper cuts are. (Contributed by Jim Kingdon, 11-Dec-2019.) |
10-Dec-2019 | mullocprlem 6408 | Calculations for mullocpr 6409. (Contributed by Jim Kingdon, 10-Dec-2019.) |
10-Dec-2019 | mulnqpru 6407 | Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) |
10-Dec-2019 | mulnqprl 6406 | Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.) |
9-Dec-2019 | prmuloclemcalc 6403 | Calculations for prmuloc 6404. (Contributed by Jim Kingdon, 9-Dec-2019.) |
9-Dec-2019 | appdiv0nq 6402 | Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6401 in which is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.) |
9-Dec-2019 | ltmnqi 6256 | Ordering property of multiplication for positive fractions. One direction of ltmnqg 6254. (Contributed by Jim Kingdon, 9-Dec-2019.) |
9-Dec-2019 | ltanqi 6255 | Ordering property of addition for positive fractions. One direction of ltanqg 6253. (Contributed by Jim Kingdon, 9-Dec-2019.) |
8-Dec-2019 | bj-nn0sucALT 7335 | Alternate proof of bj-nn0suc 7321, also constructive but from ax-inf2 7333, hence requiring ax-bdsetind 7325. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
8-Dec-2019 | bj-omex2 7334 | Using bounded set induction and the strong axiom of infinity, is a set, that is, we recover ax-infvn 7302 (see bj-2inf 7299 for the equivalence of the latter with bj-omex 7303). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) (New usage is discouraged.) |
8-Dec-2019 | bj-inf2vn2 7332 | A sufficient condition for to be a set; unbounded version of bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
8-Dec-2019 | bj-inf2vn 7331 | A sufficient condition for to be a set. See bj-inf2vn2 7332 for the unbounded version from full set induction. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
8-Dec-2019 | bj-inf2vnlem4 7330 | Lemma for bj-inf2vn2 7332. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
8-Dec-2019 | bj-inf2vnlem3 7329 | Lemma for bj-inf2vn 7331. (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED Ind | ||
8-Dec-2019 | bj-inf2vnlem2 7328 | Lemma for bj-inf2vnlem3 7329 and bj-inf2vnlem4 7330. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
8-Dec-2019 | bj-inf2vnlem1 7327 | Lemma for bj-inf2vn 7331. Remark: unoptimized proof (have to use more deduction style). (Contributed by BJ, 8-Dec-2019.) (Proof modification is discouraged.) |
Ind | ||
8-Dec-2019 | bj-bdcel 7203 | Boundedness of a membership formula. (Contributed by BJ, 8-Dec-2019.) |
BOUNDED BOUNDED | ||
8-Dec-2019 | bj-ex 7148 | Existential generalization. (Contributed by BJ, 8-Dec-2019.) Proof modification is discouraged because there are shorter proofs, but using less basic results (like exlimiv 1467 and 19.9ht 1510 or 19.23ht 1363). (Proof modification is discouraged.) |
8-Dec-2019 | mullocpr 6409 | Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both and are positive, not just ). (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | prmuloc 6404 | Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | appdivnq 6401 | Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where and are positive, as well as ). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | nqprlu 6395 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | nqprloc 6394 | A cut produced from a rational is located. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | nqprdisj 6393 | A cut produced from a rational is disjoint. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | nqprrnd 6392 | A cut produced from a rational is rounded. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | nqprm 6391 | A cut produced from a rational is inhabited. Lemma for nqprlu 6395. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | mpvlu 6388 | Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
8-Dec-2019 | plpvlu 6387 | Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.) |
7-Dec-2019 | addlocprlemeqgt 6381 | Lemma for addlocpr 6385. This is a step used in both the and cases. (Contributed by Jim Kingdon, 7-Dec-2019.) |
7-Dec-2019 | addnqprulem 6377 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
7-Dec-2019 | addnqprllem 6376 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.) |
7-Dec-2019 | lt2addnq 6257 | Ordering property of addition for positive fractions. (Contributed by Jim Kingdon, 7-Dec-2019.) |
6-Dec-2019 | addlocprlem 6384 | Lemma for addlocpr 6385. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.) |
6-Dec-2019 | addlocprlemgt 6383 | Lemma for addlocpr 6385. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
6-Dec-2019 | addlocprlemeq 6382 | Lemma for addlocpr 6385. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
6-Dec-2019 | addlocprlemlt 6380 | Lemma for addlocpr 6385. The case. (Contributed by Jim Kingdon, 6-Dec-2019.) |
5-Dec-2019 | addlocpr 6385 | Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6351 to both and , and uses nqtri3or 6249 rather than prloc 6339 to decide whether is too big to be in the lower cut of (and deduce that if it is, then must be in the upper cut). What the two proofs have in common is that they take the difference between and to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.) |
5-Dec-2019 | addnqpru 6379 | Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) |
5-Dec-2019 | addnqprl 6378 | Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.) |
5-Dec-2019 | genpmu 6367 | The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.) |
5-Dec-2019 | genpelxp 6359 | Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.) |
3-Dec-2019 | addassnq0lemcl 6310 | A natural number closure law. Lemma for addassnq0 6311. (Contributed by Jim Kingdon, 3-Dec-2019.) |
3-Dec-2019 | nndir 5980 | Distributive law for natural numbers (right-distributivity). (Contributed by Jim Kingdon, 3-Dec-2019.) |
1-Dec-2019 | nnanq0 6307 | Addition of non-negative fractions with a common denominator. You can add two fractions with the same denominator by adding their numerators and keeping the same denominator. (Contributed by Jim Kingdon, 1-Dec-2019.) |
~_{Q0} ~_{Q0} +_{Q0} ~_{Q0} | ||
1-Dec-2019 | archnqq 6268 | For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Jim Kingdon, 1-Dec-2019.) |
30-Nov-2019 | bj-2inf 7299 | Two formulations of the axiom of infinity (see ax-infvn 7302 and bj-omex 7303) . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind Ind | ||
30-Nov-2019 | bj-om 7298 | A set is equal to if and only if it is the smallest inductive set. (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind Ind | ||
30-Nov-2019 | bj-ssom 7297 | A characterization of subclasses of . (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind | ||
30-Nov-2019 | bj-omssind 7296 | is included in all the inductive sets (but for the moment, we cannot prove that it is included in all the inductive classes). (Contributed by BJ, 30-Nov-2019.) (Proof modification is discouraged.) |
Ind | ||
30-Nov-2019 | bj-omind 7295 | is an inductive class. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
30-Nov-2019 | bj-dfom 7294 | Alternate definition of , as the intersection of all the inductive sets. Proposal: make this the definition. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
30-Nov-2019 | bj-indint 7293 | The property of being an inductive class is closed under intersections. (Contributed by BJ, 30-Nov-2019.) |
Ind Ind | ||
30-Nov-2019 | bj-bdind 7292 | Boundedness of the formula "the setvar is an inductive class". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED Ind | ||
30-Nov-2019 | bj-indeq 7291 | Equality property for Ind. (Contributed by BJ, 30-Nov-2019.) |
Ind Ind | ||
30-Nov-2019 | bj-indsuc 7290 | A direct consequence of the definition of Ind. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
30-Nov-2019 | df-bj-ind 7289 | Define the property of being an inductive class. (Contributed by BJ, 30-Nov-2019.) |
Ind | ||
30-Nov-2019 | bj-bdsucel 7248 | Boundedness of the formula "the successor of the setvar belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
30-Nov-2019 | bj-bd0el 7234 | Boundedness of the formula "the empty set belongs to the setvar ". (Contributed by BJ, 30-Nov-2019.) |
BOUNDED | ||
30-Nov-2019 | bj-sseq 7177 | If two converse inclusions are characterized each by a formula, then equality is characterized by the conjunction of these formulas. (Contributed by BJ, 30-Nov-2019.) |
30-Nov-2019 | nqpnq0nq 6302 | A positive fraction plus a non-negative fraction is a positive fraction. (Contributed by Jim Kingdon, 30-Nov-2019.) |
Q_{0} +_{Q0} | ||
30-Nov-2019 | mulclnq0 6301 | Closure of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 30-Nov-2019.) |
Q_{0} Q_{0} ·_{Q0} Q_{0} | ||
30-Nov-2019 | prarloclemarch 6269 | A version of the Archimedean property. This variation is "stronger" than archnqq 6268 in the sense that we provide an integer which is larger than a given rational even after being multiplied by a second rational . (Contributed by Jim Kingdon, 30-Nov-2019.) |
29-Nov-2019 | bj-elssuniab 7176 | Version of elssuni 3578 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) |
29-Nov-2019 | bj-intabssel1 7175 | Version of intss1 3600 using a class abstraction and implicit substitution. Closed form of intmin3 3612. (Contributed by BJ, 29-Nov-2019.) |
29-Nov-2019 | bj-intabssel 7174 | Version of intss1 3600 using a class abstraction and explicit substitution. (Contributed by BJ, 29-Nov-2019.) |
29-Nov-2019 | nq02m 6313 | Multiply a non-negative fraction by two. (Contributed by Jim Kingdon, 29-Nov-2019.) |
Q_{0} ~_{Q0} ·_{Q0} +_{Q0} | ||
29-Nov-2019 | distnq0r 6312 | Multiplication of non-negative fractions is distributive. Version of distrnq0 6308 with the multiplications commuted. (Contributed by Jim Kingdon, 29-Nov-2019.) |
Q_{0} Q_{0} Q_{0} +_{Q0} ·_{Q0} ·_{Q0} +_{Q0} ·_{Q0} | ||
29-Nov-2019 | addassnq0 6311 | Addition of non-negaative fractions is associative. (Contributed by Jim Kingdon, 29-Nov-2019.) |
Q_{0} Q_{0} Q_{0} +_{Q0} +_{Q0} +_{Q0} +_{Q0} | ||
29-Nov-2019 | addclnq0 6300 | Closure of addition on non-negative fractions. (Contributed by Jim Kingdon, 29-Nov-2019.) |
Q_{0} Q_{0} +_{Q0} Q_{0} | ||
29-Nov-2019 | mulcanenq0ec 6294 | Lemma for distributive law: cancellation of common factor. (Contributed by Jim Kingdon, 29-Nov-2019.) |
~_{Q0} ~_{Q0} | ||
28-Nov-2019 | ax-bdsetind 7325 | Axiom of bounded set induction. (Contributed by BJ, 28-Nov-2019.) |
BOUNDED | ||
28-Nov-2019 | bj-peano4 7316 | Remove from peano4 4243 dependency on ax-setind 4200. Therefore, it only requires core constructive axioms (albeit more of them). (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
28-Nov-2019 | bj-nnen2lp 7315 |
A version of en2lp 4212 for natural numbers, which does not require
ax-setind 4200.
Note: using this theorem and bj-nnelirr 7314, one can remove dependency on ax-setind 4200 from nntri2 5984 and nndcel 5987; one can actually remove more dependencies from these. (Contributed by BJ, 28-Nov-2019.) (Proof modification is discouraged.) |
27-Nov-2019 | mulcomnq0 6309 | Multiplication of non-negative fractions is commutative. (Contributed by Jim Kingdon, 27-Nov-2019.) |
Q_{0} Q_{0} ·_{Q0} ·_{Q0} | ||
27-Nov-2019 | distrnq0 6308 | Multiplication of non-negative fractions is distributive. (Contributed by Jim Kingdon, 27-Nov-2019.) |
Q_{0} Q_{0} Q_{0} ·_{Q0} +_{Q0} ·_{Q0} +_{Q0} ·_{Q0} | ||
25-Nov-2019 | prcunqu 6333 | An upper cut is closed upwards under the positive fractions. (Contributed by Jim Kingdon, 25-Nov-2019.) |
25-Nov-2019 | prarloclemarch2 6270 | Like prarloclemarch 6269 but the integer must be at least two, and there is also added to the right hand side. These details follow straightforwardly but are chosen to be helpful in the proof of prarloc 6351. (Contributed by Jim Kingdon, 25-Nov-2019.) |
25-Nov-2019 | subhalfnqq 6265 | There is a number which is less than half of any positive fraction. The case where is one is Lemma 11.4 of [BauerTaylor], p. 50, and they use the word "approximate half" for such a number (since there may be constructions, for some structures other than the rationals themselves, which rely on such an approximate half but do not require division by two as seen at halfnqq 6261). (Contributed by Jim Kingdon, 25-Nov-2019.) |
24-Nov-2019 | bj-nnelirr 7314 | A natural number does not belong to itself. Version of elirr 4204 for natural numbers, which does not require ax-setind 4200. (Contributed by BJ, 24-Nov-2019.) (Proof modification is discouraged.) |
24-Nov-2019 | bdcriota 7249 | A class given by a restricted definition binder is bounded, under the given hypotheses. (Contributed by BJ, 24-Nov-2019.) |
BOUNDED BOUNDED | ||
24-Nov-2019 | nq0nn 6291 | Decomposition of a non-negative fraction into numerator and denominator. (Contributed by Jim Kingdon, 24-Nov-2019.) |
Q_{0} ~_{Q0} | ||
24-Nov-2019 | enq0eceq 6286 | Equivalence class equality of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 24-Nov-2019.) |
~_{Q0} ~_{Q0} | ||
24-Nov-2019 | dfplq0qs 6279 | Addition on non-negative fractions. This definition is similar to df-plq0 6276 but expands Q_{0} (Contributed by Jim Kingdon, 24-Nov-2019.) |
+_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} | ||
23-Nov-2019 | addnq0mo 6296 | There is at most one result from adding non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.) |
~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} | ||
23-Nov-2019 | nnnq0lem1 6295 | Decomposing non-negative fractions into natural numbers. Lemma for addnnnq0 6298 and mulnnnq0 6299. (Contributed by Jim Kingdon, 23-Nov-2019.) |
~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} | ||
23-Nov-2019 | addcmpblnq0 6292 | Lemma showing compatibility of addition on non-negative fractions. (Contributed by Jim Kingdon, 23-Nov-2019.) |
~_{Q0} | ||
23-Nov-2019 | ee8anv 1788 | Rearrange existential quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.) |
23-Nov-2019 | 19.42vvvv 1768 | Theorem 19.42 of [Margaris] p. 90 with 4 quantifiers. (Contributed by Jim Kingdon, 23-Nov-2019.) |
22-Nov-2019 | bdsetindis 7326 | Axiom of bounded set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
22-Nov-2019 | setindis 7324 | Axiom of set induction using implicit substitutions. (Contributed by BJ, 22-Nov-2019.) |
22-Nov-2019 | setindf 7323 | Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) |
22-Nov-2019 | setindft 7322 | Axiom of set-induction with a DV condition replaced with a non-freeness hypothesis (Contributed by BJ, 22-Nov-2019.) |
22-Nov-2019 | bj-nntrans2 7313 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
22-Nov-2019 | bj-nntrans 7312 | A natural number is a transitive set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
22-Nov-2019 | bdfind 7307 | Bounded induction (principle of induction when is assumed to be bounded), proved from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See findset 7306 for a proof when is assumed to be a set. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
22-Nov-2019 | findset 7306 | Bounded induction (principle of induction when is assumed to be a set) allowing a proof from basic constructive axioms. See find 4245 for a nonconstructive proof of the general case. See bdfind 7307 for a proof when is assumed to be bounded. (Contributed by BJ, 22-Nov-2019.) (Proof modification is discouraged.) |
22-Nov-2019 | cbvrald 7173 | Rule used to change bound variables, using implicit substitution. (Contributed by BJ, 22-Nov-2019.) |
22-Nov-2019 | addnnnq0 6298 | Addition of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 22-Nov-2019.) |
~_{Q0} +_{Q0} ~_{Q0} ~_{Q0} | ||
22-Nov-2019 | dfmq0qs 6278 | Multiplication on non-negative fractions. This definition is similar to df-mq0 6277 but expands Q_{0} (Contributed by Jim Kingdon, 22-Nov-2019.) |
·_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} | ||
21-Nov-2019 | bj-findes 7338 | Principle of induction, using explicit substitutions. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. From this version, it is easy to prove findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
21-Nov-2019 | bj-findisg 7337 | Version of bj-findis 7336 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-findis 7336 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
21-Nov-2019 | bj-bdfindes 7310 | Bounded induction (principle of induction for bounded formulas), using explicit substitutions. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. From this version, it is easy to prove the bounded version of findes 4249. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
21-Nov-2019 | bj-bdfindisg 7309 | Version of bj-bdfindis 7308 using a class term in the consequent. Constructive proof (from CZF). See the comment of bj-bdfindis 7308 for explanations. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
21-Nov-2019 | bj-bdfindis 7308 | Bounded induction (principle of induction for bounded formulas), using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See finds 4246 for a proof of full induction in IZF. From this version, it is easy to prove bounded versions of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
21-Nov-2019 | bdeqsuc 7247 | Boundedness of the formula expressing that a setvar is equal to the successor of another. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
21-Nov-2019 | bdop 7241 | The ordered pair of two setvars is a bounded class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
21-Nov-2019 | bdeq0 7233 | Boundedness of the formula expressing that a setvar is equal to the empty class. (Contributed by BJ, 21-Nov-2019.) |
BOUNDED | ||
21-Nov-2019 | bj-rspg 7172 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | bj-rspgt 7171 | Restricted specialization, generalized. Weakens a hypothesis of rspccv 2626 and seems to have a shorter proof. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabg2 7170 | One implication of elabg 2661. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elab2a 7169 | One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elab1 7168 | One implication of elab 2660. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabf2 7167 | One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabf1 7166 | One implication of elabf 2659. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabgf2 7165 | One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabgf1 7164 | One implication of elabgf 2658. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabgft1 7163 | One implication of elabgf 2658, in closed form. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | elabgf0 7162 | Lemma for elabgf 2658. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | bj-vtoclgf 7161 | Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | bj-vtoclgft 7160 | Weakening two hypotheses of vtoclgf 2585. (Contributed by BJ, 21-Nov-2019.) |
21-Nov-2019 | bj-exlimmpi 7156 | Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
21-Nov-2019 | bj-exlimmp 7155 | Lemma for bj-vtoclgf 7161. (Contributed by BJ, 21-Nov-2019.) (Proof modification is discouraged.) |
20-Nov-2019 | mulnq0mo 6297 | There is at most one result from multiplying non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.) |
~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} ~_{Q0} | ||
20-Nov-2019 | mulcmpblnq0 6293 | Lemma showing compatibility of multiplication on non-negative fractions. (Contributed by Jim Kingdon, 20-Nov-2019.) |
~_{Q0} | ||
19-Nov-2019 | bj-nn0suc 7321 | Proof of (biconditional form of) nn0suc 4250 from the core axioms of CZF. See also bj-nn0sucALT 7335. As a characterization of the elements of , this could be labeled "elom". (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
19-Nov-2019 | bj-nn0suc0 7311 | Constructive proof of a variant of nn0suc 4250. For a constructive proof of nn0suc 4250, see bj-nn0suc 7321. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
19-Nov-2019 | speano5 7305 | Version of peano5 4244 when is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
19-Nov-2019 | bdpeano5 7304 | Bounded version of peano5 4244. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
19-Nov-2019 | peano5set 7301 | Version of peano5 4244 when is assumed to be a set, allowing a proof from the core axioms of CZF. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
19-Nov-2019 | bj-inex 7269 | The intersection of two sets is a set, from bounded separation. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
19-Nov-2019 | bdrabexg 7268 | Bounded version of rabexg 3870. (Contributed by BJ, 19-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
19-Nov-2019 | bds 7217 | Boundedness of a formula resulting from implicit substitution in a bounded formula. Note that the proof does not use ax-bdsb 7188; therefore, using implicit instead of explicit substitution when boundedness is important, one might avoid using ax-bdsb 7188. (Contributed by BJ, 19-Nov-2019.) |
BOUNDED BOUNDED | ||
19-Nov-2019 | mulnnnq0 6299 | Multiplication of non-negative fractions in terms of natural numbers. (Contributed by Jim Kingdon, 19-Nov-2019.) |
~_{Q0} ·_{Q0} ~_{Q0} ~_{Q0} | ||
18-Nov-2019 | bj-peano2 7300 | Constructive proof of peano2 4241. Temporary note: another possibility is to simply replace sucexg 4170 with bj-sucexg 7284 in the proof of peano2 4241. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-intnexr 7271 | vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-intexr 7270 | vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-vnex 7260 | vnex 3860 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-nvel 7259 | nvel 3859 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-vprc 7258 | vprc 3858 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | bj-nalset 7257 | nalset 3857 from bounded separation. (Contributed by BJ, 18-Nov-2019.) (Proof modification is discouraged.) |
18-Nov-2019 | nqnq0 6290 | A positive fraction is a non-negative fraction. (Contributed by Jim Kingdon, 18-Nov-2019.) |
Q_{0} | ||
18-Nov-2019 | nq0ex 6289 | The class of positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.) |
Q_{0} | ||
18-Nov-2019 | enq0ex 6288 | The equivalence relation for positive fractions exists. (Contributed by Jim Kingdon, 18-Nov-2019.) |
~_{Q0} | ||
14-Nov-2019 | ax-inf2 7333 | Another axiom of infinity in a constructive setting (see ax-infvn 7302). (Contributed by BJ, 14-Nov-2019.) (New usage is discouraged.) |
14-Nov-2019 | bj-omex 7303 | Proof of omex 4239 from ax-infvn 7302. (Contributed by BJ, 14-Nov-2019.) (Proof modification is discouraged.) |
14-Nov-2019 | ax-infvn 7302 | Axiom of infinity in a constructive setting. This asserts the existence of the special set we want (the set of natural numbers), instead of the existence of a set with some properties (ax-iinf 4234) from which one then proves (omex 4239) using full separation that the wanted set exists. "vn" is for "Von Neumann". (Contributed by BJ, 14-Nov-2019.) |
Ind Ind | ||
14-Nov-2019 | enq0tr 6283 | The equivalence relation for non-negative fractions is transitive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.) |
~_{Q0} ~_{Q0} ~_{Q0} | ||
14-Nov-2019 | enq0ref 6282 | The equivalence relation for non-negative fractions is reflexive. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.) |
~_{Q0} | ||
14-Nov-2019 | enq0sym 6281 | The equivalence relation for non-negative fractions is symmetric. Lemma for enq0er 6284. (Contributed by Jim Kingdon, 14-Nov-2019.) |
~_{Q0} ~_{Q0} | ||
13-Nov-2019 | bj-sucex 7285 | sucex 4171 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bj-sucexg 7284 | sucexg 4170 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bj-unexg 7283 | unexg 4124 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bdunexb 7282 | Bounded version of unexb 4123. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED BOUNDED | ||
13-Nov-2019 | bj-unex 7281 | unex 4122 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bj-uniexg 7280 | uniexg 4121 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bj-uniex 7279 | uniex 4120 from bounded separation. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
13-Nov-2019 | bdssexd 7267 | Bounded version of ssexd 3867. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdssexg 7266 | Bounded version of ssexg 3866. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdssexi 7265 | Bounded version of ssexi 3865. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdssex 7264 | Bounded version of ssex 3864. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdinex1g 7263 | Bounded version of inex1g 3863. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdinex2 7262 | Bounded version of inex2 3862. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdinex1 7261 | Bounded version of inex1 3861. (Contributed by BJ, 13-Nov-2019.) (Proof modification is discouraged.) |
BOUNDED | ||
13-Nov-2019 | bdzfauscl 7255 | Closed form of the version of zfauscl 3847 for bounded formulas using bounded separation. (Contributed by BJ, 13-Nov-2019.) |
BOUNDED | ||
12-Nov-2019 | enq0er 6284 | The equivalence relation for non-negative fractions is an equivalence relation. (Contributed by Jim Kingdon, 12-Nov-2019.) |
~_{Q0} | ||
12-Nov-2019 | enq0enq 6280 | Equivalence on positive fractions in terms of equivalence on non-negative fractions. (Contributed by Jim Kingdon, 12-Nov-2019.) |
~_{Q0} | ||
10-Nov-2019 | prarloclemup 6343 | Contracting the upper side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.) |
+_{Q0} ~_{Q0} ·_{Q0} +_{Q0} ~_{Q0} ·_{Q0} | ||
10-Nov-2019 | prarloclemlo 6342 | Contracting the lower side of an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.) |
+_{Q0} ~_{Q0} ·_{Q0} +_{Q0} ~_{Q0} ·_{Q0} | ||
10-Nov-2019 | prarloclemlt 6341 | Two possible ways of contracting an interval which straddles a Dedekind cut. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 10-Nov-2019.) |
10-Nov-2019 | nqnq0m 6304 | Multiplication of positive fractions is equal with or ·_{Q0}. (Contributed by Jim Kingdon, 10-Nov-2019.) |
·_{Q0} | ||
10-Nov-2019 | nqnq0a 6303 | Addition of positive fractions is equal with or +_{Q0}. (Contributed by Jim Kingdon, 10-Nov-2019.) |
+_{Q0} | ||
10-Nov-2019 | nqnq0pi 6287 | A non-negative fraction is a positive fraction if its numerator and denominator are positive integers. (Contributed by Jim Kingdon, 10-Nov-2019.) |
~_{Q0} | ||
10-Nov-2019 | nnppipi 6196 | A natural number plus a positive integer is a positive integer. (Contributed by Jim Kingdon, 10-Nov-2019.) |
9-Nov-2019 | prarloclem3step 6344 | Induction step for prarloclem3 6345. (Contributed by Jim Kingdon, 9-Nov-2019.) |
+_{Q0} ~_{Q0} ·_{Q0} +_{Q0} ~_{Q0} ·_{Q0} | ||
8-Nov-2019 | genpcuu 6369 | Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.) |
7-Nov-2019 | genppreclu 6363 | Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.) |
7-Nov-2019 | prnminu 6337 | An upper cut has no smallest member. (Contributed by Jim Kingdon, 7-Nov-2019.) |
5-Nov-2019 | prarloclemn 6347 | Subtracting two from a positive integer. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 5-Nov-2019.) |
5-Nov-2019 | nq0a0 6306 | Addition with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.) |
Q_{0} +_{Q0} 0_{Q0} | ||
5-Nov-2019 | nq0m0r 6305 | Multiplication with zero for non-negative fractions. (Contributed by Jim Kingdon, 5-Nov-2019.) |
Q_{0} 0_{Q0} ·_{Q0} 0_{Q0} | ||
5-Nov-2019 | df-0nq0 6275 | Define non-negative fraction constant 0. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. (Contributed by Jim Kingdon, 5-Nov-2019.) |
0_{Q0} ~_{Q0} | ||
4-Nov-2019 | prarloclem5 6348 | A substitution of zero for and minus two for . Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.) |
+_{Q0} ~_{Q0} ·_{Q0} | ||
4-Nov-2019 | prarloclem4 6346 | A slight rearrangement of prarloclem3 6345. Lemma for prarloc 6351. (Contributed by Jim Kingdon, 4-Nov-2019.) |
+_{Q0} ~_{Q0} ·_{Q0} +_{Q0} ~_{Q0} ·_{Q0} |