|
|
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: |
| Date | Label | Description |
|---|---|---|
| Theorem | ||
| 10-Feb-2022 | ltmininf 10116 | Two ways of saying a number is less than the minimum of two others. (Contributed by Jim Kingdon, 10-Feb-2022.) |
| 10-Feb-2022 | maxltsup 10104 | Two ways of saying the maximum of two numbers is less than a third. (Contributed by Jim Kingdon, 10-Feb-2022.) |
| 9-Feb-2022 | maxleastlt 10101 | The maximum as a least upper bound, in terms of less than. (Contributed by Jim Kingdon, 9-Feb-2022.) |
| 6-Feb-2022 | unsnfidcel 6386 |
The |
| 6-Feb-2022 | unsnfidcex 6385 |
The |
| 5-Feb-2022 | funrnfi 6392 | The range of a finite relation is finite if its converse is a function. (Contributed by Jim Kingdon, 5-Feb-2022.) |
| 5-Feb-2022 | relcnvfi 6391 | If a relation is finite, its converse is as well. (Contributed by Jim Kingdon, 5-Feb-2022.) |
| 5-Feb-2022 | fundmfi 6389 | The domain of a finite function is finite. (Contributed by Jim Kingdon, 5-Feb-2022.) |
| 5-Feb-2022 | infiexmid 6362 | If the intersection of any finite set and any other set is finite, excluded middle follows. (Contributed by Jim Kingdon, 5-Feb-2022.) |
| 3-Feb-2022 | unsnfi 6384 | Adding a singleton to a finite set yields a finite set. (Contributed by Jim Kingdon, 3-Feb-2022.) |
| 3-Feb-2022 | domfiexmid 6363 | If any set dominated by a finite set is finite, excluded middle follows. (Contributed by Jim Kingdon, 3-Feb-2022.) |
| 3-Feb-2022 | ssfilem 6360 | Lemma for ssfiexmid 6361. (Contributed by Jim Kingdon, 3-Feb-2022.) |
| 1-Feb-2022 | maxclpr 10108 |
The maximum of two real numbers is one of those numbers if and only if
dichotomy ( |
| 31-Jan-2022 | znege1 10556 | The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.) |
| 31-Jan-2022 | maxleastb 10100 | Two ways of saying the maximum of two numbers is less than or equal to a third. (Contributed by Jim Kingdon, 31-Jan-2022.) |
| 30-Jan-2022 | max0addsup 10105 | The sum of the positive and negative part functions is the absolute value function over the reals. (Contributed by Jim Kingdon, 30-Jan-2022.) |
| 29-Jan-2022 | expcanlem 9643 | Lemma for expcan 9644. Proving the order in one direction. (Contributed by Jim Kingdon, 29-Jan-2022.) |
| 28-Jan-2022 | exfzdc 9249 | Decidability of the existence of an integer defined by a decidable proposition. (Contributed by Jim Kingdon, 28-Jan-2022.) |
| 25-Jan-2022 | 1nen2 6347 | One and two are not equinumerous. (Contributed by Jim Kingdon, 25-Jan-2022.) |
| 24-Jan-2022 | divmulasscomap 7784 | An associative/commutative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.) |
| 24-Jan-2022 | divmulassap 7783 | An associative law for division and multiplication. (Contributed by Jim Kingdon, 24-Jan-2022.) |
| 21-Jan-2022 | lcmmndc 10444 | Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.) |
| 20-Jan-2022 | infssuzcldc 10347 | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.) |
| 19-Jan-2022 | suprnubex 8031 | An upper bound is not less than the supremum of a nonempty bounded set of reals. (Contributed by Jim Kingdon, 19-Jan-2022.) |
| 19-Jan-2022 | suprlubex 8030 | The supremum of a nonempty bounded set of reals is the least upper bound. (Contributed by Jim Kingdon, 19-Jan-2022.) |
| 18-Jan-2022 | suprubex 8029 | A member of a nonempty bounded set of reals is less than or equal to the set's upper bound. (Contributed by Jim Kingdon, 18-Jan-2022.) |
| 17-Jan-2022 | zdvdsdc 10216 | Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.) |
| 17-Jan-2022 | suplub2ti 6414 | Bidirectional form of suplubti 6413. (Contributed by Jim Kingdon, 17-Jan-2022.) |
| 16-Jan-2022 | zssinfcl 10344 | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
| 16-Jan-2022 | supelti 6415 | Supremum membership in a set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
| 15-Jan-2022 | infsupneg 8684 | If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 8683. (Contributed by Jim Kingdon, 15-Jan-2022.) |
| 15-Jan-2022 | supinfneg 8683 | If a set of real numbers has a least upper bound, the set of the negation of those numbers has a greatest lower bound. For a theorem which is similar but only for the boundedness part, see ublbneg 8698. (Contributed by Jim Kingdon, 15-Jan-2022.) |
| 14-Jan-2022 | supminfex 8685 | A supremum is the negation of the infimum of that set's image under negation. (Contributed by Jim Kingdon, 14-Jan-2022.) |
| 14-Jan-2022 | infrenegsupex 8682 |
The infimum of a set of reals |
| 13-Jan-2022 | infssuzledc 10346 | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.) |
| 13-Jan-2022 | infssuzex 10345 | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
| 11-Jan-2022 | eucialg 10441 |
Euclid's Algorithm computes the greatest common divisor of two
nonnegative integers by repeatedly replacing the larger of them with
its remainder modulo the smaller until the remainder is 0. Theorem
1.15 in [ApostolNT] p. 20.
Upon halting, the 1st member of the final state |
| 11-Jan-2022 | eucialgcvga 10440 |
Once Euclid's Algorithm halts after |
| 11-Jan-2022 | ifcldadc 3378 | Conditional closure. (Contributed by Jim Kingdon, 11-Jan-2022.) |
| 9-Jan-2022 | bezoutlemsup 10398 |
Lemma for Bézout's identity. The number satisfying the
greatest common divisor condition is the supremum of divisors of
both |
| 9-Jan-2022 | bezoutlemle 10397 |
Lemma for Bézout's identity. The number satisfying the
greatest common divisor condition is the largest number which
divides both |
| 9-Jan-2022 | bezoutlemeu 10396 | Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
| 9-Jan-2022 | bezoutlemmo 10395 | Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
| 8-Jan-2022 | bezoutlembi 10394 | Lemma for Bézout's identity. Like bezoutlembz 10393 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
| 8-Jan-2022 | bezoutlembz 10393 | Lemma for Bézout's identity. Like bezoutlemaz 10392 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
| 8-Jan-2022 | bezoutlemaz 10392 | Lemma for Bézout's identity. Like bezoutlemzz 10391 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
| 8-Jan-2022 | bezoutlemzz 10391 | Lemma for Bézout's identity. Like bezoutlemex 10390 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
| 6-Jan-2022 | bezoutlemnewy 10385 |
Lemma for Bézout's identity. The is-bezout predicate holds for
|
| 3-Jan-2022 | bezoutlemex 10390 | Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.) |
| 3-Jan-2022 | bezoutlemstep 10386 | Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.) |
| 1-Jan-2022 | fvifdc 5217 | Move a conditional outside of a function. (Contributed by Jim Kingdon, 1-Jan-2022.) |
| 1-Jan-2022 | ifeq1dadc 3379 | Conditional equality. (Contributed by Jim Kingdon, 1-Jan-2022.) |
| 1-Jan-2022 | ifsbdc 3363 | Distribute a function over an if-clause. (Contributed by Jim Kingdon, 1-Jan-2022.) |
| 31-Dec-2021 | dfgcd3 10399 |
Alternate definition of the |
| 30-Dec-2021 | bezoutlemb 10389 |
Lemma for Bézout's identity. The is-bezout condition is
satisfied by |
| 30-Dec-2021 | bezoutlema 10388 |
Lemma for Bézout's identity. The is-bezout condition is
satisfied by |
| 30-Dec-2021 | bezoutlemmain 10387 | Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.) |
| 22-Dec-2021 | maxleast 10099 | The maximum of two reals is a least upper bound. Lemma 3.11 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 22-Dec-2021.) |
| 22-Dec-2021 | maxcl 10096 | The maximum of two real numbers is a real number. (Contributed by Jim Kingdon, 22-Dec-2021.) |
| 22-Dec-2021 | maxabslemval 10094 | Lemma for maxabs 10095. Value of the supremum. (Contributed by Jim Kingdon, 22-Dec-2021.) |
| 21-Dec-2021 | dfabsmax 10103 | Absolute value of a real number in terms of maximum. Definition 3.13 of [Geuvers], p. 11. (Contributed by BJ and Jim Kingdon, 21-Dec-2021.) |
| 21-Dec-2021 | maxleb 10102 |
Equivalence of |
| 21-Dec-2021 | maxle2 10098 | The maximum of two reals is no smaller than the second real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.) |
| 21-Dec-2021 | maxle1 10097 | The maximum of two reals is no smaller than the first real. Lemma 3.10 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.) |
| 21-Dec-2021 | maxabslemab 10092 | Lemma for maxabs 10095. A variation of maxleim 10091- that is, if we know which of two real numbers is larger, we know the maximum of the two. (Contributed by Jim Kingdon, 21-Dec-2021.) |
| 21-Dec-2021 | maxleim 10091 | Value of maximum when we know which number is larger. (Contributed by Jim Kingdon, 21-Dec-2021.) |
| 21-Dec-2021 | maxcom 10089 | The maximum of two reals is commutative. Lemma 3.9 of [Geuvers], p. 10. (Contributed by Jim Kingdon, 21-Dec-2021.) |
| 20-Dec-2021 | maxabs 10095 | Maximum of two real numbers in terms of absolute value. (Contributed by Jim Kingdon, 20-Dec-2021.) |
| 20-Dec-2021 | maxabslemlub 10093 |
Lemma for maxabs 10095. A least upper bound for |
| 20-Dec-2021 | maxabsle 10090 |
An upper bound for |
| 20-Dec-2021 | suprzclex 8445 | The supremum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 20-Dec-2021.) |
| 20-Dec-2021 | r19.12sn 3458 | Special case of r19.12 2466 where its converse holds. (Contributed by NM, 19-May-2008.) (Revised by Mario Carneiro, 23-Apr-2015.) (Revised by BJ, 20-Dec-2021.) |
| 19-Dec-2021 | infisoti 6445 | Image of an infimum under an isomorphism. (Contributed by Jim Kingdon, 19-Dec-2021.) |
| 19-Dec-2021 | infsnti 6443 | The infimum of a singleton. (Contributed by Jim Kingdon, 19-Dec-2021.) |
| 19-Dec-2021 | infeuti 6442 | An infimum is unique. (Contributed by Jim Kingdon, 19-Dec-2021.) |
| 18-Dec-2021 | infmoti 6441 |
Any class |
| 18-Dec-2021 | infminti 6440 | The smallest element of a set is its infimum. Note that the converse is not true; the infimum might not be an element of the set considered. (Contributed by Jim Kingdon, 18-Dec-2021.) |
| 18-Dec-2021 | infnlbti 6439 | A lower bound is not greater than the infimum. (Contributed by Jim Kingdon, 18-Dec-2021.) |
| 18-Dec-2021 | infglbti 6438 | An infimum is the greatest lower bound. See also infclti 6436 and inflbti 6437. (Contributed by Jim Kingdon, 18-Dec-2021.) |
| 18-Dec-2021 | inflbti 6437 | An infimum is a lower bound. See also infclti 6436 and infglbti 6438. (Contributed by Jim Kingdon, 18-Dec-2021.) |
| 17-Dec-2021 | infclti 6436 | An infimum belongs to its base class (closure law). See also inflbti 6437 and infglbti 6438. (Contributed by Jim Kingdon, 17-Dec-2021.) |
| 17-Dec-2021 | infvalti 6435 | Alternate expression for the infimum. (Contributed by Jim Kingdon, 17-Dec-2021.) |
| 17-Dec-2021 | cnvti 6432 | If a relation satisfies a condition corresponding to tightness of an apartness generated by an order, so does its converse. (Contributed by Jim Kingdon, 17-Dec-2021.) |
| 17-Dec-2021 | cnvinfex 6431 | Two ways of expressing existence of an infimum (one in terms of converse). (Contributed by Jim Kingdon, 17-Dec-2021.) |
| 16-Dec-2021 | eqinftid 6434 | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
| 16-Dec-2021 | eqinfti 6433 | Sufficient condition for an element to be equal to the infimum. (Contributed by Jim Kingdon, 16-Dec-2021.) |
| 13-Dec-2021 | orandc 880 | Disjunction in terms of conjunction (De Morgan's law), for decidable propositions. Compare Theorem *4.57 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 13-Dec-2021.) |
| 12-Dec-2021 | gcdsupex 10349 |
Existence of the supremum used in defining |
| 12-Dec-2021 | gcdmndc 10340 |
Decidablity lemma used in various proofs related to |
| 12-Dec-2021 | ddifstab 3104 | A class is equal to its double complement if and only if it is stable (that is, membership in it is a stable property). (Contributed by BJ, 12-Dec-2021.) |
| 11-Dec-2021 | gcdsupcl 10350 |
Closure of the supremum used in defining |
| 11-Dec-2021 | dvdsbnd 10348 | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
| 7-Dec-2021 | zsupcl 10343 |
Closure of supremum for decidable integer properties. The property
which defines the set we are taking the supremum of must (a) be true at
|
| 7-Dec-2021 | zsupcllemex 10342 | Lemma for zsupcl 10343. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
| 7-Dec-2021 | zsupcllemstep 10341 | Lemma for zsupcl 10343. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
| 5-Dec-2021 | divalglemqt 10319 |
Lemma for divalg 10324. The |
| 4-Dec-2021 | divalglemeuneg 10323 | Lemma for divalg 10324. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
| 4-Dec-2021 | divalglemeunn 10321 | Lemma for divalg 10324. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
| 4-Dec-2021 | divalglemnqt 10320 |
Lemma for divalg 10324. The |
| 2-Dec-2021 | rspc2gv 2712 | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.) |
| 30-Nov-2021 | divalglemex 10322 | Lemma for divalg 10324. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) |
| 30-Nov-2021 | divalglemnn 10318 | Lemma for divalg 10324. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) |
| 27-Nov-2021 | ioom 9269 | An open interval of extended reals is inhabited iff the lower argument is less than the upper argument. (Contributed by Jim Kingdon, 27-Nov-2021.) |
| 26-Nov-2021 | supisoti 6423 | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
| 26-Nov-2021 | isoti 6420 | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
| 26-Nov-2021 | isotilem 6419 | Lemma for isoti 6420. (Contributed by Jim Kingdon, 26-Nov-2021.) |
| 26-Nov-2021 | supsnti 6418 | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
| 24-Nov-2021 | supmaxti 6417 | The greatest element of a set is its supremum. Note that the converse is not true; the supremum might not be an element of the set considered. (Contributed by Jim Kingdon, 24-Nov-2021.) |
| 24-Nov-2021 | suplubti 6413 | A supremum is the least upper bound. See also supclti 6411 and supubti 6412. (Contributed by Jim Kingdon, 24-Nov-2021.) |
| 24-Nov-2021 | supubti 6412 |
A supremum is an upper bound. See also supclti 6411 and suplubti 6413.
This proof demonstrates how to expand an iota-based definition (df-iota 4887) using riotacl2 5501. (Contributed by Jim Kingdon, 24-Nov-2021.) |
| 24-Nov-2021 | supclti 6411 | A supremum belongs to its base class (closure law). See also supubti 6412 and suplubti 6413. (Contributed by Jim Kingdon, 24-Nov-2021.) |
| 24-Nov-2021 | eqsuptid 6410 | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
| 23-Nov-2021 | eqsupti 6409 | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
| 23-Nov-2021 | supval2ti 6408 | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
| 23-Nov-2021 | supeuti 6407 | A supremum is unique. Similar to Theorem I.26 of [Apostol] p. 24 (but for suprema in general). (Contributed by Jim Kingdon, 23-Nov-2021.) |
| 23-Nov-2021 | supmoti 6406 |
Any class |
| 17-Nov-2021 | sqne2sq 10555 | The square of a natural number can never be equal to two times the square of a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 17-Nov-2021 | 2sqpwodd 10554 | The greatest power of two dividing twice the square of an integer is an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 17-Nov-2021 | sqpweven 10553 | The greatest power of two dividing the square of an integer is an even power of two. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 17-Nov-2021 | oddpwdclemndvds 10549 | Lemma for oddpwdc 10552. A natural number is not divisible by one more than the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 17-Nov-2021 | oddpwdclemdvds 10548 | Lemma for oddpwdc 10552. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 17-Nov-2021 | pw2dvdseulemle 10545 | Lemma for pw2dvdseu 10546. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
| 16-Nov-2021 | oddpwdclemdc 10551 | Lemma for oddpwdc 10552. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.) |
| 16-Nov-2021 | oddpwdclemodd 10550 | Lemma for oddpwdc 10552. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.) |
| 16-Nov-2021 | oddpwdclemxy 10547 | Lemma for oddpwdc 10552. Another way of stating that decomposing a natural number into a power of two and an odd number is unique. (Contributed by Jim Kingdon, 16-Nov-2021.) |
| 16-Nov-2021 | pw2dvdseu 10546 | A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) |
| 14-Nov-2021 | pw2dvds 10544 | A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
| 14-Nov-2021 | pw2dvdslemn 10543 | Lemma for pw2dvds 10544. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
| 14-Nov-2021 | dvdsdc 10203 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
| 11-Nov-2021 | fz01or 10278 | An integer is in the integer range from zero to one iff it is either zero or one. (Contributed by Jim Kingdon, 11-Nov-2021.) |
| 11-Nov-2021 | muldivdirap 7795 | Distribution of division over addition with a multiplication. (Contributed by Jim Kingdon, 11-Nov-2021.) |
| 10-Nov-2021 | zeoxor 10268 | An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.) |
| 9-Nov-2021 | qlttri2 8726 | Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 9-Nov-2021.) |
| 8-Nov-2021 | dvdslelemd 10243 | Lemma for dvdsle 10244. (Contributed by Jim Kingdon, 8-Nov-2021.) |
| 8-Nov-2021 | qabsord 9962 | The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.) |
| 8-Nov-2021 | qabsor 9961 | The absolute value of a rational number is either that number or its negative. (Contributed by Jim Kingdon, 8-Nov-2021.) |
| 6-Nov-2021 | ibcval5 9690 |
Write out the top and bottom parts of the binomial coefficient
|
| 3-Nov-2021 | qavgle 9267 | The average of two rational numbers is less than or equal to at least one of them. (Contributed by Jim Kingdon, 3-Nov-2021.) |
| 31-Oct-2021 | nn0opth2d 9650 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 9649. (Contributed by Jim Kingdon, 31-Oct-2021.) |
| 31-Oct-2021 | nn0opthd 9649 |
An ordered pair theorem for nonnegative integers. Theorem 17.3 of
[Quine] p. 124. We can represent an
ordered pair of nonnegative
integers |
| 31-Oct-2021 | nn0opthlem2d 9648 | Lemma for nn0opth2 9651. (Contributed by Jim Kingdon, 31-Oct-2021.) |
| 31-Oct-2021 | nn0opthlem1d 9647 | A rather pretty lemma for nn0opth2 9651. (Contributed by Jim Kingdon, 31-Oct-2021.) |
| 31-Oct-2021 | nn0le2msqd 9646 | The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.) |
| 28-Oct-2021 | mulle0r 8022 | Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.) |
| 26-Oct-2021 | modqeqmodmin 9396 | A rational number equals the difference of the rational number and a modulus modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.) |
| 26-Oct-2021 | modqsubdir 9395 | Distribute the modulo operation over a subtraction. (Contributed by Jim Kingdon, 26-Oct-2021.) |
| 26-Oct-2021 | modqdi 9394 | Distribute multiplication over a modulo operation. (Contributed by Jim Kingdon, 26-Oct-2021.) |
| 26-Oct-2021 | modqaddmulmod 9393 | The sum of a rational number and the product of a second rational number modulo a modulus and an integer equals the sum of the rational number and the product of the other rational number and the integer modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.) |
| 26-Oct-2021 | modqmulmodr 9392 | The product of an integer and a rational number modulo a modulus equals the product of the integer and the rational number modulo the modulus. (Contributed by Jim Kingdon, 26-Oct-2021.) |
| 25-Oct-2021 | modqmulmod 9391 | The product of a rational number modulo a modulus and an integer equals the product of the rational number and the integer modulo the modulus. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | q2submod 9387 | If a number is between a modulus and twice the modulus, the first number modulo the modulus equals the first number minus the modulus. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | q2txmodxeq0 9386 | Two times a positive number modulo the number is zero. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | modqsubmodmod 9385 | The difference of a number modulo a modulus and another number modulo the same modulus equals the difference of the two numbers modulo the modulus. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | modqsubmod 9384 | The difference of a number modulo a modulus and another number equals the difference of the two numbers modulo the modulus. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | modqsub12d 9383 | Subtraction property of the modulo operation. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | modqadd12d 9382 | Additive property of the modulo operation. (Contributed by Jim Kingdon, 25-Oct-2021.) |
| 25-Oct-2021 | syldc 45 | Syllogism deduction. Commuted form of syld 44. (Contributed by BJ, 25-Oct-2021.) |
| 25-Oct-2021 | syl11 31 | A syllogism inference. Commuted form of an instance of syl 14. (Contributed by BJ, 25-Oct-2021.) |
| 24-Oct-2021 | ax-ddkcomp 10784 | Axiom of Dedekind completeness for Dedekind real numbers: every inhabited upper-bounded located set of reals has a real upper bound. Ideally, this axiom should be "proved" as "axddkcomp" for the real numbers constructed from IZF, and then the axiom ax-ddkcomp 10784 should be used in place of construction specific results. In particular, axcaucvg 7066 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
| 24-Oct-2021 | modqnegd 9381 | Negation property of the modulo operation. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 24-Oct-2021 | modqmul12d 9380 | Multiplication property of the modulo operation, see theorem 5.2(b) in [ApostolNT] p. 107. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 24-Oct-2021 | modqmul1 9379 |
Multiplication property of the modulo operation. Note that the
multiplier |
| 24-Oct-2021 | modqltm1p1mod 9378 | If a number modulo a modulus is less than the modulus decreased by 1, the first number increased by 1 modulo the modulus equals the first number modulo the modulus, increased by 1. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 24-Oct-2021 | modqm1p1mod0 9377 | If a number modulo a modulus equals the modulus decreased by 1, the first number increased by 1 modulo the modulus equals 0. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 24-Oct-2021 | modqadd2mod 9376 | The sum of a number modulo a modulus and another number equals the sum of the two numbers modulo the modulus. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 24-Oct-2021 | qnegmod 9371 | The negation of a number modulo a positive number is equal to the difference of the modulus and the number modulo the modulus. (Contributed by Jim Kingdon, 24-Oct-2021.) |
| 23-Oct-2021 | modqmuladdnn0 9370 | Implication of a decomposition of a nonnegative integer into a multiple of a modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.) |
| 23-Oct-2021 | modqmuladdim 9369 | Implication of a decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.) |
| 23-Oct-2021 | modqmuladd 9368 | Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.) |
| 23-Oct-2021 | mulqaddmodid 9366 | The sum of a positive rational number less than an upper bound and the product of an integer and the upper bound is the positive rational number modulo the upper bound. (Contributed by Jim Kingdon, 23-Oct-2021.) |
| 23-Oct-2021 | modqaddmod 9365 | The sum of a number modulo a modulus and another number equals the sum of the two numbers modulo the same modulus. (Contributed by Jim Kingdon, 23-Oct-2021.) |
| 22-Oct-2021 | modqaddabs 9364 | Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.) |
| 22-Oct-2021 | modqadd1 9363 | Addition property of the modulo operation. (Contributed by Jim Kingdon, 22-Oct-2021.) |
| 21-Oct-2021 | modqcyc2 9362 | The modulo operation is periodic. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqcyc 9361 | The modulo operation is periodic. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqabs2 9360 | Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqabs 9359 | Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | q1mod 9358 | Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | q0mod 9357 | Special case: 0 modulo a positive real number is 0. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqid2 9353 | Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqid0 9352 | A positive real number modulo itself is 0. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 21-Oct-2021 | modqid 9351 | Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
| 20-Oct-2021 | modqvalp1 9345 | The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Jim Kingdon, 20-Oct-2021.) |
| 20-Oct-2021 | onunsnss 6383 | Adding a singleton to create an ordinal. (Contributed by Jim Kingdon, 20-Oct-2021.) |
| 19-Oct-2021 | snon0 6387 |
An ordinal which is a singleton is |
| 18-Oct-2021 | qdencn 10785 |
The set of complex numbers whose real and imaginary parts are rational
is dense in the complex plane. This is a two dimensional analogue to
qdenre 10088 (and also would hold for |
| 18-Oct-2021 | modqmulnn 9344 | Move a positive integer in and out of a floor in the first argument of a modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | intqfrac 9341 | Break a number into its integer part and its fractional part. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | flqmod 9340 | The floor function expressed in terms of the modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | modqfrac 9339 | The fractional part of a number is the number modulo 1. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | modqdifz 9338 |
The modulo operation differs from |
| 18-Oct-2021 | modqdiffl 9337 |
The modulo operation differs from |
| 18-Oct-2021 | modqelico 9336 | Modular reduction produces a half-open interval. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | modqlt 9335 | The modulo operation is less than its second argument. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | modqge0 9334 | The modulo operation is nonnegative. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | negqmod0 9333 |
|
| 18-Oct-2021 | mulqmod0 9332 | The product of an integer and a positive rational number is 0 modulo the positive real number. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | flqdiv 9323 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 18-Oct-2021 | intqfrac2 9321 | Decompose a real into integer and fractional parts. (Contributed by Jim Kingdon, 18-Oct-2021.) |
| 17-Oct-2021 | modq0 9331 |
|
| 16-Oct-2021 | modqcld 9330 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) |
| 16-Oct-2021 | flqpmodeq 9329 | Partition of a division into its integer part and the remainder. (Contributed by Jim Kingdon, 16-Oct-2021.) |
| 16-Oct-2021 | modqcl 9328 | Closure law for the modulo operation. (Contributed by Jim Kingdon, 16-Oct-2021.) |
| 16-Oct-2021 | modqvalr 9327 | The value of the modulo operation (multiplication in reversed order). (Contributed by Jim Kingdon, 16-Oct-2021.) |
| 16-Oct-2021 | modqval 9326 |
The value of the modulo operation. The modulo congruence notation of
number theory, |
| 15-Oct-2021 | qdenre 10088 |
The rational numbers are dense in |
| 14-Oct-2021 | qbtwnrelemcalc 9264 |
Lemma for qbtwnre 9265. Calculations involved in showing the
constructed
rational number is less than |
| 13-Oct-2021 | rebtwn2z 9263 |
A real number can be bounded by integers above and below which are two
apart.
The proof starts by finding two integers which are less than and greater than the given real number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on weak linearity, and iterating until the range consists of integers which are two apart. (Contributed by Jim Kingdon, 13-Oct-2021.) |
| 13-Oct-2021 | rebtwn2zlemshrink 9262 | Lemma for rebtwn2z 9263. Shrinking the range around the given real number. (Contributed by Jim Kingdon, 13-Oct-2021.) |
| 13-Oct-2021 | rebtwn2zlemstep 9261 | Lemma for rebtwn2z 9263. Induction step. (Contributed by Jim Kingdon, 13-Oct-2021.) |
| 11-Oct-2021 | flqeqceilz 9320 | A rational number is an integer iff its floor equals its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | flqleceil 9319 | The floor of a rational number is less than or equal to its ceiling. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceilqidz 9318 | A rational number equals its ceiling iff it is an integer. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceilqle 9316 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceiqle 9315 | The ceiling of a real number is the smallest integer greater than or equal to it. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceilqm1lt 9314 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceiqm1l 9313 | One less than the ceiling of a real number is strictly less than that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceilqge 9312 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceiqge 9311 | The ceiling of a real number is greater than or equal to that number. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceilqcl 9310 | Closure of the ceiling function. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | ceiqcl 9309 | The ceiling function returns an integer (closure law). (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | qdceq 9256 | Equality of rationals is decidable. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 11-Oct-2021 | qltlen 8725 | Rational 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7730 which is a similar result for real numbers. (Contributed by Jim Kingdon, 11-Oct-2021.) |
| 10-Oct-2021 | ceilqval 9308 | The value of the ceiling function. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | flqmulnn0 9301 | Move a nonnegative integer in and out of a floor. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | flqzadd 9300 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | flqaddz 9299 | An integer can be moved in and out of the floor of a sum. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | flqge1nn 9296 | The floor of a number greater than or equal to 1 is a positive integer. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | flqge0nn0 9295 | The floor of a number greater than or equal to 0 is a nonnegative integer. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | 4ap0 8138 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 10-Oct-2021 | 3ap0 8135 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
| 9-Oct-2021 | flqbi2 9293 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 9-Oct-2021 | flqbi 9292 | A condition equivalent to floor. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 9-Oct-2021 | flqword2 9291 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 9-Oct-2021 | flqwordi 9290 | Ordering relationship for the greatest integer function. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 9-Oct-2021 | flqltnz 9289 | If A is not an integer, then the floor of A is less than A. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 9-Oct-2021 | flqidz 9288 | A rational number equals its floor iff it is an integer. (Contributed by Jim Kingdon, 9-Oct-2021.) |
| 8-Oct-2021 | flqidm 9287 | The floor function is idempotent. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqlt 9285 | The floor function value is less than the next integer. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqge 9284 | The floor function value is the greatest integer less than or equal to its argument. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qfracge0 9283 | The fractional part of a rational number is nonnegative. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qfraclt1 9282 | The fractional part of a rational number is less than one. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqltp1 9281 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqle 9280 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqcld 9279 | The floor (greatest integer) function is an integer (closure law). (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqlelt 9278 | A basic property of the floor (greatest integer) function. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | flqcl 9277 | The floor (greatest integer) function yields an integer when applied to a rational (closure law). It would presumably be possible to prove a similar result for some real numbers (for example, those apart from any integer), but not real numbers in general. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qbtwnz 9260 | There is a unique greatest integer less than or equal to a rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qbtwnzlemex 9259 |
Lemma for qbtwnz 9260. Existence of the integer.
The proof starts by finding two integers which are less than and greater than the given rational number. Then this range can be shrunk by choosing an integer in between the endpoints of the range and then deciding which half of the range to keep based on rational number trichotomy, and iterating until the range consists of two consecutive integers. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qbtwnzlemshrink 9258 | Lemma for qbtwnz 9260. Shrinking the range around the given rational number. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qbtwnzlemstep 9257 | Lemma for qbtwnz 9260. Induction step. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 8-Oct-2021 | qltnle 9255 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 8-Oct-2021.) |
| 7-Oct-2021 | qlelttric 9254 | Rational trichotomy. (Contributed by Jim Kingdon, 7-Oct-2021.) |
| 6-Oct-2021 | qletric 9253 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) |
| 6-Oct-2021 | qtri3or 9252 | Rational trichotomy. (Contributed by Jim Kingdon, 6-Oct-2021.) |
| 3-Oct-2021 | reg3exmid 4322 |
If any inhabited set satisfying df-wetr 4089 for |
| 3-Oct-2021 | reg3exmidlemwe 4321 |
Lemma for reg3exmid 4322. Our counterexample |
| 2-Oct-2021 | sqrt2irrap 10558 |
The square root of 2 is irrational. That is, for any rational number,
|
| 2-Oct-2021 | sqrt2irraplemnn 10557 | Lemma for sqrt2irrap 10558. The square root of 2 is apart from a positive rational expressed as a numerator and denominator. (Contributed by Jim Kingdon, 2-Oct-2021.) |
| 2-Oct-2021 | reg2exmid 4279 |
If any inhabited set has a minimal element (when expressed by |
| 2-Oct-2021 | reg2exmidlema 4277 |
Lemma for reg2exmid 4279. If |
| 30-Sep-2021 | fin0or 6370 | A finite set is either empty or inhabited. (Contributed by Jim Kingdon, 30-Sep-2021.) |
| 30-Sep-2021 | wessep 4320 | A subset of a set well-ordered by set membership is well-ordered by set membership. (Contributed by Jim Kingdon, 30-Sep-2021.) |
| 28-Sep-2021 | frind 4107 | Induction over a well-founded set. (Contributed by Jim Kingdon, 28-Sep-2021.) |
| 26-Sep-2021 | wetriext 4319 | A trichotomous well-order is extensional. (Contributed by Jim Kingdon, 26-Sep-2021.) |
| 25-Sep-2021 | nnwetri 6382 |
A natural number is well-ordered by |
| 23-Sep-2021 | wepo 4114 | A well-ordering is a partial ordering. (Contributed by Jim Kingdon, 23-Sep-2021.) |
| 23-Sep-2021 | df-wetr 4089 |
Define the well-ordering predicate. It is unusual to define
"well-ordering" in the absence of excluded middle, but we mean
an
ordering which is like the ordering which we have for ordinals (for
example, it does not entail trichotomy because ordinals don't have that
as seen at ordtriexmid 4265). Given excluded middle, well-ordering is
usually defined to require trichotomy (and the defintion of |
| 22-Sep-2021 | frforeq3 4102 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
| 22-Sep-2021 | frforeq2 4100 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
| 22-Sep-2021 | frforeq1 4098 | Equality theorem for the well-founded predicate. (Contributed by Jim Kingdon, 22-Sep-2021.) |
| 22-Sep-2021 | df-frfor 4086 |
Define the well-founded relation predicate where |
| 21-Sep-2021 | frirrg 4105 |
A well-founded relation is irreflexive. This is the case where |
| 21-Sep-2021 | df-frind 4087 |
Define the well-founded relation predicate. In the presence of excluded
middle, there are a variety of equivalent ways to define this. In our
case, this definition, in terms of an inductive principle, works better
than one along the lines of "there is an element which is minimal
when A
is ordered by R". Because |
| 17-Sep-2021 | ontr2exmid 4268 | An ordinal transitivity law which implies excluded middle. (Contributed by Jim Kingdon, 17-Sep-2021.) |
| 16-Sep-2021 | decrmac 8534 |
Perform a multiply-add of two numerals |
| 16-Sep-2021 | decrmanc 8533 |
Perform a multiply-add of two numerals |
| 16-Sep-2021 | nnsseleq 6102 | For natural numbers, inclusion is equivalent to membership or equality. (Contributed by Jim Kingdon, 16-Sep-2021.) |
| 15-Sep-2021 | fientri3 6381 | Trichotomy of dominance for finite sets. (Contributed by Jim Kingdon, 15-Sep-2021.) |
| 15-Sep-2021 | nntri2or2 6099 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-Sep-2021.) |
| 14-Sep-2021 | findcard2sd 6376 | Deduction form of finite set induction . (Contributed by Jim Kingdon, 14-Sep-2021.) |
| 13-Sep-2021 | php5fin 6366 | A finite set is not equinumerous to a set which adds one element. (Contributed by Jim Kingdon, 13-Sep-2021.) |
| 13-Sep-2021 | fiunsnnn 6365 | Adding one element to a finite set which is equinumerous to a natural number. (Contributed by Jim Kingdon, 13-Sep-2021.) |
| 12-Sep-2021 | fisbth 6367 | Schroeder-Bernstein Theorem for finite sets. (Contributed by Jim Kingdon, 12-Sep-2021.) |
| 11-Sep-2021 | diffisn 6377 | Subtracting a singleton from a finite set produces a finite set. (Contributed by Jim Kingdon, 11-Sep-2021.) |
| 10-Sep-2021 | fin0 6369 | A nonempty finite set has at least one element. (Contributed by Jim Kingdon, 10-Sep-2021.) |
| 9-Sep-2021 | fidifsnid 6356 | If we remove a single element from a finite set then put it back in, we end up with the original finite set. This strengthens difsnss 3531 from subset to equality when the set is finite. (Contributed by Jim Kingdon, 9-Sep-2021.) |
| 9-Sep-2021 | fidifsnen 6355 | All decrements of a finite set are equinumerous. (Contributed by Jim Kingdon, 9-Sep-2021.) |
| 8-Sep-2021 | 3dvdsdec 10264 |
A decimal number is divisible by three iff the sum of its two
"digits"
is divisible by three. The term "digits" in its narrow sense
is only
correct if |
| 8-Sep-2021 | 1lt10 8615 | 1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 2lt10 8614 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 3lt10 8613 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 4lt10 8612 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 5lt10 8611 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 6lt10 8610 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 7lt10 8609 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 8lt10 8608 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 9lt10 8607 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | decltdi 8515 | Comparing a digit to a decimal integer. (Contributed by AV, 8-Sep-2021.) |
| 8-Sep-2021 | decleh 8511 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | decle 8510 | Comparing two decimal integers (equal higher places). (Contributed by AV, 17-Aug-2021.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 3declth 8508 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
| 8-Sep-2021 | declth 8506 | Comparing two decimal integers (unequal higher places). (Contributed by AV, 8-Sep-2021.) |
| 8-Sep-2021 | le9lt10 8503 | A "decimal digit" (i.e. a nonnegative integer less than or equal to 9) is less then 10. (Contributed by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 10re 8495 | The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | 10pos 8493 | The number 10 is positive. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) |
| 8-Sep-2021 | diffifi 6378 | Subtracting one finite set from another produces a finite set. (Contributed by Jim Kingdon, 8-Sep-2021.) |
| 8-Sep-2021 | diffitest 6371 |
If subtracting any set from a finite set gives a finite set, any
proposition of the form |
| 6-Sep-2021 | 9t11e99 8606 | 9 times 11 equals 99. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 8t6e48 8595 | 8 times 6 equals 48. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 8t5e40 8594 | 8 times 5 equals 40. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 6t6e36 8584 | 6 times 6 equals 36. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 6t5e30 8583 | 6 times 5 equals 30. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 5t5e25 8579 | 5 times 5 equals 25. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 5t4e20 8578 | 5 times 4 equals 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 5t3e15 8577 | 5 times 3 equals 15. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 10m1e9 8572 | 10 - 1 = 9. (Contributed by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 10p10e20 8571 | 10 + 10 = 20. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 9p2e11 8563 | 9 + 2 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 8p3e11 8557 | 8 + 3 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 8p2e10 8556 | 8 + 2 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 7p4e11 8552 | 7 + 4 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 7p3e10 8551 | 7 + 3 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 6p5e11 8549 | 6 + 5 = 11. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 6p4e10 8548 | 6 + 4 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 5p5e10 8547 | 5 + 5 = 10. (Contributed by NM, 5-Feb-2007.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decmul10add 8545 | A multiplication of a number and a numeral expressed as addition with first summand as multiple of 10. (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decmul2c 8542 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decmul1c 8541 | The product of a numeral with a number (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decmul1 8540 | The product of a numeral with a number (no carry). (Contributed by AV, 22-Jul-2021.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decsubi 8539 |
Difference between a numeral |
| 6-Sep-2021 | decaddci2 8538 |
Add two numerals |
| 6-Sep-2021 | decaddc2 8532 |
Add two numerals |
| 6-Sep-2021 | decaddc 8531 |
Add two numerals |
| 6-Sep-2021 | decadd 8530 |
Add two numerals |
| 6-Sep-2021 | decma2c 8529 |
Perform a multiply-add of two numerals |
| 6-Sep-2021 | decmac 8528 |
Perform a multiply-add of two numerals |
| 6-Sep-2021 | decma 8527 |
Perform a multiply-add of two numerals |
| 6-Sep-2021 | dec10p 8519 | Ten plus an integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decsucc 8517 | The successor of a decimal integer (with carry). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | declti 8514 | Comparing a digit to a decimal integer. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 3decltc 8509 | Comparing two decimal integers with three "digits" (unequal higher places). (Contributed by AV, 15-Jun-2021.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decsuc 8507 | The successor of a decimal integer (no carry). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decltc 8505 | Comparing two decimal integers (unequal higher places). (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | declt 8504 | Comparing two decimal integers (equal higher places). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decnncl2 8500 | Closure for a decimal integer (zero units place). (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | dec0h 8498 | Add a zero in the higher places. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | dec0u 8497 | Add a zero in the units place. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | decnncl 8496 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 10nn0 8494 | 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | 10nn 8492 | 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | deccl 8491 | Closure for a numeral. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | deceq2 8482 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | deceq1 8481 | Equality theorem for the decimal constructor. (Contributed by Mario Carneiro, 17-Apr-2015.) (Revised by AV, 6-Sep-2021.) |
| 6-Sep-2021 | phpelm 6352 | Pigeonhole Principle. A natural number is not equinumerous to an element of itself. (Contributed by Jim Kingdon, 6-Sep-2021.) |
| 5-Sep-2021 | ex-gcd 10568 | Example for df-gcd 10339. (Contributed by AV, 5-Sep-2021.) |
| 5-Sep-2021 | fidceq 6354 |
Equality of members of a finite set is decidable. This may be
counterintuitive: cannot any two sets be elements of a finite set?
Well, to show, for example, that |
| 5-Sep-2021 | phplem4on 6353 | Equinumerosity of successors of an ordinal and a natural number implies equinumerosity of the originals. (Contributed by Jim Kingdon, 5-Sep-2021.) |
| 4-Sep-2021 | ex-bc 10566 | Example for df-bc 9675. (Contributed by AV, 4-Sep-2021.) |
| 4-Sep-2021 | ex-fac 10565 | Example for df-fac 9653. (Contributed by AV, 4-Sep-2021.) |
| 4-Sep-2021 | ex-ceil 10564 | Example for df-ceil 9275. (Contributed by AV, 4-Sep-2021.) |
| 4-Sep-2021 | 5t2e10 8576 | 5 times 2 equals 10. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 4-Sep-2021.) |
| 3-Sep-2021 | 0elsucexmid 4308 | If the successor of any ordinal class contains the empty set, excluded middle follows. (Contributed by Jim Kingdon, 3-Sep-2021.) |
| 1-Sep-2021 | php5dom 6349 | A natural number does not dominate its successor. (Contributed by Jim Kingdon, 1-Sep-2021.) |
| 1-Sep-2021 | phplem4dom 6348 | Dominance of successors implies dominance of the original natural numbers. (Contributed by Jim Kingdon, 1-Sep-2021.) |
| 1-Sep-2021 | snnen2oprc 6346 |
A singleton |
| 1-Sep-2021 | snnen2og 6345 |
A singleton |
| 1-Sep-2021 | phplem3g 6342 | A natural number is equinumerous to its successor minus any element of the successor. Version of phplem3 6340 with unnecessary hypotheses removed. (Contributed by Jim Kingdon, 1-Sep-2021.) |
| 31-Aug-2021 | nndifsnid 6103 | If we remove a single element from a natural number then put it back in, we end up with the original natural number. This strengthens difsnss 3531 from subset to equality but the proof relies on equality being decidable. (Contributed by Jim Kingdon, 31-Aug-2021.) |
| 30-Aug-2021 | carden2bex 6458 | If two numerable sets are equinumerous, then they have equal cardinalities. (Contributed by Jim Kingdon, 30-Aug-2021.) |
| 30-Aug-2021 | cardval3ex 6454 |
The value of |
| 30-Aug-2021 | cardcl 6450 | The cardinality of a well-orderable set is an ordinal. (Contributed by Jim Kingdon, 30-Aug-2021.) |
| 30-Aug-2021 | onintrab2im 4262 | An existence condition which implies an intersection is an ordinal number. (Contributed by Jim Kingdon, 30-Aug-2021.) |
| 30-Aug-2021 | onintonm 4261 | The intersection of an inhabited collection of ordinal numbers is an ordinal number. Compare Exercise 6 of [TakeutiZaring] p. 44. (Contributed by Mario Carneiro and Jim Kingdon, 30-Aug-2021.) |
| 29-Aug-2021 | onintexmid 4315 | If the intersection (infimum) of an inhabited class of ordinal numbers belongs to the class, excluded middle follows. The hypothesis would be provable given excluded middle. (Contributed by Mario Carneiro and Jim Kingdon, 29-Aug-2021.) |
| 29-Aug-2021 | ordtri2or2exmid 4314 | Ordinal trichotomy implies excluded middle. (Contributed by Jim Kingdon, 29-Aug-2021.) |
| 29-Aug-2021 | ordtri2or2exmidlem 4269 |
A set which is |
| 29-Aug-2021 | 2ordpr 4267 |
Version of 2on 6032 with the definition of |
| 25-Aug-2021 | nnap0d 8084 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.) |
| 24-Aug-2021 | climcaucn 10188 |
A converging sequence of complex numbers is a Cauchy sequence. This is
like climcau 10184 but adds the part that |
| 24-Aug-2021 | climcvg1nlem 10186 |
Lemma for climcvg1n 10187. We construct sequences of the real and
imaginary parts of each term of |
| 23-Aug-2021 | climcvg1n 10187 |
A Cauchy sequence of complex numbers converges, existence version.
The rate of convergence is fixed: all terms after the nth term must be
within |
| 23-Aug-2021 | climrecvg1n 10185 |
A Cauchy sequence of real numbers converges, existence version. The
rate of convergence is fixed: all terms after the nth term must be
within |
| 22-Aug-2021 | climserile 10183 | The partial sums of a converging infinite series with nonnegative terms are bounded by its limit. (Contributed by Jim Kingdon, 22-Aug-2021.) |
| 22-Aug-2021 | iserige0 10181 | The limit of an infinite series of nonnegative reals is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.) |
| 22-Aug-2021 | iserile 10180 | Comparison of the limits of two infinite series. (Contributed by Jim Kingdon, 22-Aug-2021.) |
| 22-Aug-2021 | serile 9474 | Comparison of partial sums of two infinite series of reals. (Contributed by Jim Kingdon, 22-Aug-2021.) |
| 22-Aug-2021 | serige0 9473 | A finite sum of nonnegative terms is nonnegative. (Contributed by Jim Kingdon, 22-Aug-2021.) |
| 21-Aug-2021 | divalgmodcl 10328 |
The result of the |
| 21-Aug-2021 | divalgmod 10327 |
The result of the |
| 21-Aug-2021 | clim2iser2 10176 | The limit of an infinite series with an initial segment added. (Contributed by Jim Kingdon, 21-Aug-2021.) |
| 21-Aug-2021 | iseqdistr 9470 | The distributive property for series. (Contributed by Jim Kingdon, 21-Aug-2021.) |
| 21-Aug-2021 | iseqhomo 9468 | Apply a homomorphism to a sequence. (Contributed by Jim Kingdon, 21-Aug-2021.) |
| 20-Aug-2021 | oddprmge3 10516 | An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 20-Aug-2021.) |
| 20-Aug-2021 | oddprmgt2 10515 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
| 20-Aug-2021 | clim2iser 10175 | The limit of an infinite series with an initial segment removed. (Contributed by Jim Kingdon, 20-Aug-2021.) |
| 20-Aug-2021 | iseqex 9433 | Existence of the sequence builder operation. (Contributed by Jim Kingdon, 20-Aug-2021.) |
| 20-Aug-2021 | frecex 6004 | Finite recursion produces a set. (Contributed by Jim Kingdon, 20-Aug-2021.) |
| 20-Aug-2021 | tfrfun 5978 | Transfinite recursion produces a function. (Contributed by Jim Kingdon, 20-Aug-2021.) |
| 19-Aug-2021 | modremain 10329 | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
| 19-Aug-2021 | iserclim0 10144 | The zero series converges to zero. (Contributed by Jim Kingdon, 19-Aug-2021.) |
| 19-Aug-2021 | shftval4g 9725 |
Value of a sequence shifted by |
| 19-Aug-2021 | iser0f 9472 | A zero-valued infinite series is equal to the constant zero function. (Contributed by Jim Kingdon, 19-Aug-2021.) |
| 19-Aug-2021 | iser0 9471 | The value of the partial sums in a zero-valued infinite series. (Contributed by Jim Kingdon, 19-Aug-2021.) |
| 19-Aug-2021 | ovexg 5559 | Evaluating a set operation at two sets gives a set. (Contributed by Jim Kingdon, 19-Aug-2021.) |
| 18-Aug-2021 | iseqid3s 9466 |
A sequence that consists of zeroes up to |
| 18-Aug-2021 | iseqid3 9465 |
A sequence that consists entirely of zeroes (or whatever the identity
|
| 18-Aug-2021 | iseqss 9446 |
Specifying a larger universe for |
| 17-Aug-2021 | iseqcaopr 9462 | The sum of two infinite series (generalized to an arbitrary commutative and associative operation). (Contributed by Jim Kingdon, 17-Aug-2021.) |
| 17-Aug-2021 | declei 8512 | Comparing a digit to a decimal integer. (Contributed by AV, 17-Aug-2021.) |
| 16-Aug-2021 | oddge22np1 10281 | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) |
| 16-Aug-2021 | iseqcaopr3 9460 | Lemma for iseqcaopr2 . (Contributed by Jim Kingdon, 16-Aug-2021.) |
| 16-Aug-2021 | iseq1p 9459 | Removing the first term from a sequence. (Contributed by Jim Kingdon, 16-Aug-2021.) |
| 16-Aug-2021 | iseqsplit 9458 | Split a sequence into two sequences. (Contributed by Jim Kingdon, 16-Aug-2021.) |
| 15-Aug-2021 | n2dvdsm1 10313 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
| 15-Aug-2021 | shftfibg 9708 |
Value of a fiber of the relation |
| 15-Aug-2021 | ovshftex 9707 | Existence of the result of applying shift. (Contributed by Jim Kingdon, 15-Aug-2021.) |
| 15-Aug-2021 | isermono 9457 | The partial sums in an infinite series of positive terms form a monotonic sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) |
| 15-Aug-2021 | iserf 9453 |
An infinite series of complex terms is a function from |
| 15-Aug-2021 | iseqshft2 9452 | Shifting the index set of a sequence. (Contributed by Jim Kingdon, 15-Aug-2021.) |
| 15-Aug-2021 | iseqfeq 9451 | Equality of sequences. (Contributed by Jim Kingdon, 15-Aug-2021.) |
| 13-Aug-2021 | absdivapd 10081 | Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | absrpclapd 10074 | The absolute value of a complex number apart from zero is a positive real. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | absdivapzi 10040 | Absolute value distributes over division. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | absgt0ap 9985 | The absolute value of a number apart from zero is positive. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | recvalap 9983 | Reciprocal expressed with a real denominator. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | sqap0 9542 | A number is apart from zero iff its square is apart from zero. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | leltapd 7737 | '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 13-Aug-2021 | leltap 7724 | '<_' implies 'less than' is 'apart'. (Contributed by Jim Kingdon, 13-Aug-2021.) |
| 12-Aug-2021 | evennn2n 10283 | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
| 12-Aug-2021 | evennn02n 10282 | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) |
| 12-Aug-2021 | abssubap0 9976 | If the absolute value of a complex number is less than a real, its difference from the real is apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | ltabs 9973 | A number which is less than its absolute value is negative. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | absext 9949 | Strong extensionality for absolute value. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | sq11ap 9639 | Analogue to sq11 9548 but for apartness. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | subap0d 7740 | Two numbers apart from each other have difference apart from zero. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | ltapd 7736 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | gtapd 7735 | 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | ltapi 7734 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | ltapii 7733 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | gtapii 7732 | 'Greater than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 12-Aug-2021 | ltap 7731 | 'Less than' implies apart. (Contributed by Jim Kingdon, 12-Aug-2021.) |
| 11-Aug-2021 | absexpzap 9966 | Absolute value of integer exponentiation. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | absdivap 9956 | Absolute value distributes over division. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | abs00ap 9948 | The absolute value of a number is apart from zero iff the number is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | absrpclap 9947 | The absolute value of a number apart from zero is a positive real. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | sqrt11ap 9924 | Analogue to sqrt11 9925 but for apartness. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | cjap0d 9835 | A number which is apart from zero has a complex conjugate which is apart from zero. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | ap0gt0d 7739 | A nonzero nonnegative number is positive. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 11-Aug-2021 | ap0gt0 7738 | A nonnegative number is apart from zero if and only if it is positive. (Contributed by Jim Kingdon, 11-Aug-2021.) |
| 10-Aug-2021 | rersqrtthlem 9916 | Lemma for resqrtth 9917. (Contributed by Jim Kingdon, 10-Aug-2021.) |
| 10-Aug-2021 | rersqreu 9914 | Existence and uniqueness for the real square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
| 10-Aug-2021 | rsqrmo 9913 | Uniqueness for the square root function. (Contributed by Jim Kingdon, 10-Aug-2021.) |
| 9-Aug-2021 | dvdsdivcl 10250 |
The complement of a divisor of |
| 9-Aug-2021 | resqrexlemoverl 9907 |
Lemma for resqrex 9912. Every term in the sequence is an
overestimate
compared with the limit |
| 8-Aug-2021 | isoddgcd1 10538 | The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
| 8-Aug-2021 | isevengcd2 10537 | The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.) |
| 8-Aug-2021 | gcdeq 10412 |
|
| 8-Aug-2021 | dfgcd2 10403 |
Alternate definition of the |
| 8-Aug-2021 | resqrexlemga 9909 |
Lemma for resqrex 9912. The sequence formed by squaring each term
of |
| 8-Aug-2021 | resqrexlemglsq 9908 |
Lemma for resqrex 9912. The sequence formed by squaring each term
of |
| 8-Aug-2021 | recvguniqlem 9880 | Lemma for recvguniq 9881. Some of the rearrangements of the expressions. (Contributed by Jim Kingdon, 8-Aug-2021.) |
| 8-Aug-2021 | ifcldcd 3381 | Membership (closure) of a conditional operator, deduction form. (Contributed by Jim Kingdon, 8-Aug-2021.) |
| 8-Aug-2021 | ifbothdc 3380 |
A wff |
| 7-Aug-2021 | divconjdvds 10249 |
If a nonzero integer |
| 7-Aug-2021 | dvdseq 10248 | If two nonnegative integers divide each other, they must be equal. (Contributed by Mario Carneiro, 30-May-2014.) (Proof shortened by AV, 7-Aug-2021.) |
| 7-Aug-2021 | dvdsabseq 10247 | If two integers divide each other, they must be equal, up to a difference in sign. Theorem 1.1(j) in [ApostolNT] p. 14. (Contributed by Mario Carneiro, 30-May-2014.) (Revised by AV, 7-Aug-2021.) |
| 7-Aug-2021 | resqrexlemsqa 9910 |
Lemma for resqrex 9912. The square of a limit is |
| 7-Aug-2021 | resqrexlemgt0 9906 | Lemma for resqrex 9912. A limit is nonnegative. (Contributed by Jim Kingdon, 7-Aug-2021.) |
| 7-Aug-2021 | recvguniq 9881 | Limits are unique. (Contributed by Jim Kingdon, 7-Aug-2021.) |
| 6-Aug-2021 | resqrexlemcvg 9905 | Lemma for resqrex 9912. The sequence has a limit. (Contributed by Jim Kingdon, 6-Aug-2021.) |
| 6-Aug-2021 | cvg1nlemcxze 9868 | Lemma for cvg1n 9872. Rearranging an expression related to the rate of convergence. (Contributed by Jim Kingdon, 6-Aug-2021.) |
| 4-Aug-2021 | coprmdvds1 10473 | If two positive integers are coprime, i.e. their greatest common divisor is 1, the only positive integer that divides both of them is 1. (Contributed by AV, 4-Aug-2021.) |
| 1-Aug-2021 | 3dvds2dec 10265 |
A decimal number is divisible by three iff the sum of its three
"digits"
is divisible by three. The term "digits" in its narrow sense
is only
correct if |
| 1-Aug-2021 | cvg1n 9872 |
Convergence of real sequences.
This is a version of caucvgre 9867 with a constant multiplier (Contributed by Jim Kingdon, 1-Aug-2021.) |
| 1-Aug-2021 | cvg1nlemres 9871 |
Lemma for cvg1n 9872. The original sequence |
| 1-Aug-2021 | cvg1nlemcau 9870 |
Lemma for cvg1n 9872. By selecting spaced out terms for the
modified
sequence |
| 1-Aug-2021 | cvg1nlemf 9869 |
Lemma for cvg1n 9872. The modified sequence |
| 1-Aug-2021 | 3dec 9642 | A "decimal constructor" which is used to build up "decimal integers" or "numeric terms" in base 10 with 3 "digits". (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| 1-Aug-2021 | sq10e99m1 9641 | The square of 10 is 99 plus 1. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| 1-Aug-2021 | sq10 9640 | The square of 10 is 100. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
| 1-Aug-2021 | dfdec10 8480 |
Version of the definition of the "decimal constructor" using ; |
| 1-Aug-2021 | 9p1e10 8479 | 9 + 1 = 10. (Contributed by Mario Carneiro, 18-Apr-2015.) (Revised by Stanislas Polu, 7-Apr-2020.) (Revised by AV, 1-Aug-2021.) |
| 1-Aug-2021 | df-dec 8478 |
Define the "decimal constructor", which is used to build up
"decimal
integers" or "numeric terms" in base |
| 31-Jul-2021 | resqrexlemnm 9904 | Lemma for resqrex 9912. The difference between two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 31-Jul-2021.) |
| 31-Jul-2021 | resqrexlemdecn 9898 | Lemma for resqrex 9912. The sequence is decreasing. (Contributed by Jim Kingdon, 31-Jul-2021.) |
| 30-Jul-2021 | resqrexlemnmsq 9903 | Lemma for resqrex 9912. The difference between the squares of two terms of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 30-Jul-2021.) |
| 30-Jul-2021 | decaddm10 8535 | The sum of two multiples of 10 is a multiple of 10. (Contributed by AV, 30-Jul-2021.) |
| 30-Jul-2021 | divmuldivapd 7918 | Multiplication of two ratios. (Contributed by Jim Kingdon, 30-Jul-2021.) |
| 30-Jul-2021 | muladd11r 7264 | A simple product of sums expansion. (Contributed by AV, 30-Jul-2021.) |
| 29-Jul-2021 | resqrexlemcalc3 9902 | Lemma for resqrex 9912. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
| 29-Jul-2021 | resqrexlemcalc2 9901 | Lemma for resqrex 9912. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
| 29-Jul-2021 | resqrexlemcalc1 9900 | Lemma for resqrex 9912. Some of the calculations involved in showing that the sequence converges. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
| 29-Jul-2021 | resqrexlemlo 9899 | Lemma for resqrex 9912. A (variable) lower bound for each term of the sequence. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
| 29-Jul-2021 | resqrexlemdec 9897 | Lemma for resqrex 9912. The sequence is decreasing. (Contributed by Mario Carneiro and Jim Kingdon, 29-Jul-2021.) |
| 28-Jul-2021 | resqrexlemp1rp 9892 | Lemma for resqrex 9912. Applying the recursion rule yields a positive real (expressed in a way that will help apply iseqf 9444 and similar theorems). (Contributed by Jim Kingdon, 28-Jul-2021.) |
| 28-Jul-2021 | resqrexlem1arp 9891 |
Lemma for resqrex 9912. |
| 28-Jul-2021 | rpap0d 8779 | A positive real is apart from zero. (Contributed by Jim Kingdon, 28-Jul-2021.) |
| 27-Jul-2021 | resqrexlemex 9911 | Lemma for resqrex 9912. Existence of square root given a sequence which converges to the square root. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
| 27-Jul-2021 | resqrexlemover 9896 | Lemma for resqrex 9912. Each element of the sequence is an overestimate. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
| 27-Jul-2021 | resqrexlemfp1 9895 | Lemma for resqrex 9912. Recursion rule. This sequence is the ancient method for computing square roots, often known as the babylonian method, although known to many ancient cultures. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
| 27-Jul-2021 | resqrexlemf1 9894 | Lemma for resqrex 9912. Initial value. Although this sequence converges to the square root with any positive initial value, this choice makes various steps in the proof of convergence easier. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
| 27-Jul-2021 | resqrexlemf 9893 | Lemma for resqrex 9912. The sequence is a function. (Contributed by Mario Carneiro and Jim Kingdon, 27-Jul-2021.) |
| 26-Jul-2021 | nndivides 10202 | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
| 25-Jul-2021 | summodnegmod 10226 | The sum of two integers modulo a positive integer equals zero iff the first of the two integers equals the negative of the other integer modulo the positive integer. (Contributed by AV, 25-Jul-2021.) |
| 24-Jul-2021 | dvdsnprmd 10507 | If a number is divisible by an integer greater than 1 and less then the number, the number is not prime. (Contributed by AV, 24-Jul-2021.) |
| 23-Jul-2021 | iseqf 9444 | Range of the recursive sequence builder. (Contributed by Jim Kingdon, 23-Jul-2021.) |
| 22-Jul-2021 | ialgrlemconst 10425 | Lemma for ialgr0 10426. Closure of a constant function, in a form suitable for theorems such as iseq1 9442 or iseqfn 9441. (Contributed by Jim Kingdon, 22-Jul-2021.) |
| 22-Jul-2021 | ialgrlem1st 10424 | Lemma for ialgr0 10426. Expressing algrflemg 5871 in a form suitable for theorems such as iseq1 9442 or iseqfn 9441. (Contributed by Jim Kingdon, 22-Jul-2021.) |
| 22-Jul-2021 | algrflemg 5871 | Lemma for algrf and related theorems. (Contributed by Jim Kingdon, 22-Jul-2021.) |
| 21-Jul-2021 | mod2eq0even 10277 | An integer is 0 modulo 2 iff it is even (i.e. divisible by 2), see example 2 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.) |
| 21-Jul-2021 | modmulconst 10227 | Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.) |
| 21-Jul-2021 | zmod1congr 9343 | Two arbitrary integers are congruent modulo 1, see example 4 in [ApostolNT] p. 107. (Contributed by AV, 21-Jul-2021.) |
| 20-Jul-2021 | caucvgrelemcau 9866 | Lemma for caucvgre 9867. Converting the Cauchy condition. (Contributed by Jim Kingdon, 20-Jul-2021.) |
| 20-Jul-2021 | caucvgrelemrec 9865 | Two ways to express a reciprocal. (Contributed by Jim Kingdon, 20-Jul-2021.) |
| 19-Jul-2021 | sqoddm1div8z 10286 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
| 19-Jul-2021 | mulsucdiv2z 10285 | An integer multiplied with its successor divided by 2 yields an integer, i.e. an integer multiplied with its successor is even. (Contributed by AV, 19-Jul-2021.) |
| 19-Jul-2021 | caucvgre 9867 |
Convergence of real sequences.
A Cauchy sequence (as defined here, which has a rate of convergence
built in) of real numbers converges to a real number. Specifically on
rate of convergence, all terms after the nth term must be within
(Contributed by Jim Kingdon, 19-Jul-2021.) |
| 19-Jul-2021 | sqoddm1div8 9625 | A squared odd number minus 1 divided by 8 is the odd number multiplied with its successor divided by 2. (Contributed by AV, 19-Jul-2021.) |
| 19-Jul-2021 | mulbinom2 9589 | The square of a binomial with factor. (Contributed by AV, 19-Jul-2021.) |
| 19-Jul-2021 | nzadd 8403 | The sum of a real number not being an integer and an integer is not an integer. Note that "not being an integer" in this case means "the negation of is an integer" rather than "is apart from any integer" (given excluded middle, those two would be equivalent). (Contributed by AV, 19-Jul-2021.) |
| 19-Jul-2021 | ax-caucvg 7096 |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7066.
A Cauchy sequence (as defined here, which has a rate convergence built
in) of real numbers converges to a real number. Specifically on rate of
convergence, all terms after the nth term must be within
This axiom should not be used directly; instead use caucvgre 9867 (which is
the same, but stated in terms of the |
| 18-Jul-2021 | mulnqpr 6767 | Multiplication of fractions embedded into positive reals. One can either multiply the fractions as fractions, or embed them into positive reals and multiply them as positive reals, and get the same result. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 18-Jul-2021 | mulnqprlemfu 6766 | Lemma for mulnqpr 6767. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 18-Jul-2021 | mulnqprlemfl 6765 | Lemma for mulnqpr 6767. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 18-Jul-2021 | mulnqprlemru 6764 | Lemma for mulnqpr 6767. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 18-Jul-2021 | mulnqprlemrl 6763 | Lemma for mulnqpr 6767. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 18-Jul-2021 | lt2mulnq 6595 | Ordering property of multiplication for positive fractions. (Contributed by Jim Kingdon, 18-Jul-2021.) |
| 17-Jul-2021 | recidpirqlemcalc 7025 | Lemma for recidpirq 7026. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
| 17-Jul-2021 | recidpipr 7024 | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
| 16-Jul-2021 | 2teven 10287 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
| 16-Jul-2021 | 2tp1odd 10284 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
| 15-Jul-2021 | mulp1mod1 9367 | The product of an integer and an integer greater than 1 increased by 1 is 1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021.) |
| 15-Jul-2021 | rereceu 7055 | The reciprocal from axprecex 7046 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
| 15-Jul-2021 | recidpirq 7026 |
A real number times its reciprocal is one, where reciprocal is expressed
with |
| 15-Jul-2021 | recnnre 7019 |
Embedding the reciprocal of a natural number into |
| 15-Jul-2021 | pitore 7018 |
Embedding from |
| 15-Jul-2021 | pitoregt0 7017 |
Embedding from |
| 14-Jul-2021 | m1modge3gt1 9373 | Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021.) |
| 14-Jul-2021 | m1modnnsub1 9372 | Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021.) |
| 14-Jul-2021 | adddivflid 9294 | The floor of a sum of an integer and a fraction is equal to the integer iff the denominator of the fraction is less than the numerator. (Contributed by AV, 14-Jul-2021.) |
| 14-Jul-2021 | nnindnn 7059 | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8055 designed for real number axioms which involve natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
| 14-Jul-2021 | peano5nnnn 7058 | Peano's inductive postulate. This is a counterpart to peano5nni 8042 designed for real number axioms which involve natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
| 14-Jul-2021 | peano2nnnn 7021 | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8051 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7066). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
| 14-Jul-2021 | peano1nnnn 7020 |
One is an element of |
| 14-Jul-2021 | addvalex 7012 |
Existence of a sum. This is dependent on how we define |
| 13-Jul-2021 | cncongrprm 10536 | Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021.) |
| 13-Jul-2021 | prmndvdsfaclt 10535 | A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.) |
| 13-Jul-2021 | cncongrcoprm 10488 | Corollary 1 of Cancellability of Congruences: Two products with a common factor are congruent modulo an integer being coprime to the common factor iff the other factors are congruent modulo the integer. (Contributed by AV, 13-Jul-2021.) |
| 13-Jul-2021 | cncongr 10487 | Cancellability of Congruences (see ProofWiki "Cancellability of Congruences, https://proofwiki.org/wiki/Cancellability_of_Congruences, 10-Jul-2021): Two products with a common factor are congruent modulo a positive integer iff the other factors are congruent modulo the integer divided by the greates common divisor of the integer and the common factor. See also Theorem 5.4 "Cancellation law" in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
| 13-Jul-2021 | cncongr1 10485 | One direction of the bicondition in cncongr 10487. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.) |
| 13-Jul-2021 | nntopi 7060 |
Mapping from |
| 13-Jul-2021 | ltrennb 7022 |
Ordering of natural numbers with |
| 12-Jul-2021 | divgcdcoprmex 10484 | Integers divided by gcd are coprime (see ProofWiki "Integers Divided by GCD are Coprime", 11-Jul-2021, https://proofwiki.org/wiki/Integers_Divided_by_GCD_are_Coprime): Any pair of integers, not both zero, can be reduced to a pair of coprime ones by dividing them by their gcd. (Contributed by AV, 12-Jul-2021.) |
| 12-Jul-2021 | divgcdcoprm0 10483 | Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.) |
| 12-Jul-2021 | ltrenn 7023 |
Ordering of natural numbers with |
| 11-Jul-2021 | cncongr2 10486 | The other direction of the bicondition in cncongr 10487. (Contributed by AV, 11-Jul-2021.) |
| 11-Jul-2021 | congr 10482 |
Definition of congruence by integer multiple (see ProofWiki "Congruence
(Number Theory)", 11-Jul-2021,
https://proofwiki.org/wiki/Definition:Congruence_(Number_Theory)):
An integer |
| 11-Jul-2021 | divgcdz 10363 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
| 11-Jul-2021 | zeqzmulgcd 10362 | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
| 11-Jul-2021 | recriota 7056 | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
| 11-Jul-2021 | elrealeu 6998 | The real number mapping in elreal 6997 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
| 10-Jul-2021 | coprmdvds 10474 | Euclid's Lemma (see ProofWiki "Euclid's Lemma", 10-Jul-2021, https://proofwiki.org/wiki/Euclid's_Lemma): If an integer divides the product of two integers and is coprime to one of them, then it divides the other. See also theorem 1.5 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by AV, 10-Jul-2021.) |
| 10-Jul-2021 | divgcdnnr 10367 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
| 10-Jul-2021 | divgcdnn 10366 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
| 10-Jul-2021 | gcd2n0cl 10361 |
Closure of the |
| 10-Jul-2021 | axcaucvglemres 7065 |
Lemma for axcaucvg 7066. Mapping the limit from |
| 10-Jul-2021 | axcaucvglemval 7063 |
Lemma for axcaucvg 7066. Value of sequence when mapping to |
| 10-Jul-2021 | axcaucvglemcl 7061 |
Lemma for axcaucvg 7066. Mapping to |
| 9-Jul-2021 | axcaucvglemcau 7064 |
Lemma for axcaucvg 7066. The result of mapping to |
| 9-Jul-2021 | axcaucvglemf 7062 |
Lemma for axcaucvg 7066. Mapping to |
| 8-Jul-2021 | fldiv4p1lem1div2 9307 | The floor of an integer equal to 3 or greater than 4, increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) |
| 8-Jul-2021 | divfl0 9298 | The floor of a fraction is 0 iff the denominator is less than the numerator. (Contributed by AV, 8-Jul-2021.) |
| 8-Jul-2021 | div4p1lem1div2 8284 | An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) |
| 8-Jul-2021 | axcaucvg 7066 |
Real number completeness axiom. A Cauchy sequence with a modulus of
convergence converges. This is basically Corollary 11.2.13 of [HoTT],
p. (varies). The HoTT book theorem has a modulus of convergence
(that is, a rate of convergence) specified by (11.2.9) in HoTT whereas
this theorem fixes the rate of convergence to say that all terms after
the nth term must be within
Because we are stating this axiom before we have introduced notations
for This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 7096. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
| 7-Jul-2021 | ltadd1sr 6953 | Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.) |
| 7-Jul-2021 | lteupri 6807 | The difference from ltexpri 6803 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.) |
| 7-Jul-2021 | sbcimdv 2879 | Substitution analogue of Theorem 19.20 of [Margaris] p. 90 (alim 1386). (Contributed by NM, 11-Nov-2005.) (Revised by NM, 17-Aug-2018.) (Proof shortened by JJ, 7-Jul-2021.) |
| 7-Jul-2021 | eqsbc3r 2874 | eqsbc3 2853 with setvar variable on right side of equals sign. (Contributed by Alan Sare, 24-Oct-2011.) (Proof shortened by JJ, 7-Jul-2021.) |
| 4-Jul-2021 | flodddiv4t2lthalf 10337 | The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.) |
| 4-Jul-2021 | flodddiv4lt 10336 | The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.) |
| 4-Jul-2021 | fldivndvdslt 10335 | The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.) |
| 4-Jul-2021 | 4dvdseven 10317 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
| 4-Jul-2021 | z4even 10316 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
| 4-Jul-2021 | caucvgsrlemasr 6966 | Lemma for caucvgsr 6978. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.) |
| 3-Jul-2021 | caucvgsrlemoffres 6976 | Lemma for caucvgsr 6978. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
| 3-Jul-2021 | caucvgsrlemoffgt1 6975 | Lemma for caucvgsr 6978. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
| 3-Jul-2021 | caucvgsrlemoffcau 6974 | Lemma for caucvgsr 6978. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
| 3-Jul-2021 | caucvgsrlemofff 6973 | Lemma for caucvgsr 6978. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
| 3-Jul-2021 | caucvgsrlemoffval 6972 | Lemma for caucvgsr 6978. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
| 2-Jul-2021 | caucvgsrlemcl 6965 | Lemma for caucvgsr 6978. Terms of the sequence from caucvgsrlemgt1 6971 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.) |
| 1-Jul-2021 | halfleoddlt 10294 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) |
| 1-Jul-2021 | zltaddlt1le 9028 | The sum of an integer and a real number between 0 and 1 is less than or equal to a second integer iff the sum is less than the second integer. (Contributed by AV, 1-Jul-2021.) |
| 1-Jul-2021 | addlelt 8839 | If the sum of a real number and a positive real number is less than or equal to a third real number, the first real number is less than the third real number. (Contributed by AV, 1-Jul-2021.) |
| 29-Jun-2021 | ltoddhalfle 10293 | An integer is less than half of an odd number iff it is less than or equal to the half of the predecessor of the odd number (which is an even number). (Contributed by AV, 29-Jun-2021.) |
| 29-Jun-2021 | ledivge1le 8803 | If a number is less than or equal to another number, the number divided by a positive number greater than or equal to one is less than or equal to the other number. (Contributed by AV, 29-Jun-2021.) |
| 29-Jun-2021 | divle1le 8802 | A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.) |
| 29-Jun-2021 | caucvgsrlemfv 6967 | Lemma for caucvgsr 6978. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) |
| 29-Jun-2021 | prsrriota 6964 | Mapping a restricted iota from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) |
| 29-Jun-2021 | prsrlt 6963 | Mapping from positive real ordering to signed real ordering. (Contributed by Jim Kingdon, 29-Jun-2021.) |
| 29-Jun-2021 | prsradd 6962 | Mapping from positive real addition to signed real addition. (Contributed by Jim Kingdon, 29-Jun-2021.) |
| 28-Jun-2021 | nnoddm1d2 10310 | A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
| 28-Jun-2021 | nn0oddm1d2 10309 | A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
| 28-Jun-2021 | nnehalf 10304 | The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.) |
| 28-Jun-2021 | nn0ehalf 10303 | The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.) |
| 26-Jun-2021 | m1expo 10300 | Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.) |
| 25-Jun-2021 | m1expe 10299 | Exponentiation of -1 by an even power. Variant of m1expeven 9523. (Contributed by AV, 25-Jun-2021.) |
| 25-Jun-2021 | caucvgsrlembound 6970 | Lemma for caucvgsr 6978. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.) |
| 25-Jun-2021 | prsrpos 6961 | Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.) |
| 25-Jun-2021 | prsrcl 6960 | Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.) |
| 25-Jun-2021 | srpospr 6959 | Mapping from a signed real greater than zero to a positive real. (Contributed by Jim Kingdon, 25-Jun-2021.) |
| 23-Jun-2021 | z2even 10314 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
| 23-Jun-2021 | z0even 10311 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
| 23-Jun-2021 | caucvgsrlemcau 6969 | Lemma for caucvgsr 6978. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) |
| 23-Jun-2021 | caucvgsrlemf 6968 | Lemma for caucvgsr 6978. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) |
| 22-Jun-2021 | oddm1d2 10292 | An integer is odd iff its predecessor divided by 2 is an integer. This is another representation of odd numbers without using the divides relation. (Contributed by AV, 18-Jun-2021.) (Proof shortened by AV, 22-Jun-2021.) |
| 22-Jun-2021 | oddp1d2 10290 | An integer is odd iff its successor divided by 2 is an integer. This is a representation of odd numbers without using the divides relation, see zeo 8452 and zeo2 8453. (Contributed by AV, 22-Jun-2021.) |
| 22-Jun-2021 | evend2 10289 | An integer is even iff its quotient with 2 is an integer. This is a representation of even numbers without using the divides relation, see zeo 8452 and zeo2 8453. (Contributed by AV, 22-Jun-2021.) |
| 22-Jun-2021 | zeneo 10270 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. This variant of zneo 8448 follows immediately from the fact that a contradiction implies anything, see pm2.21i 607. (Contributed by AV, 22-Jun-2021.) |
| 22-Jun-2021 | evenelz 10266 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 10200. (Contributed by AV, 22-Jun-2021.) |
| 22-Jun-2021 | caucvgsrlemgt1 6971 | Lemma for caucvgsr 6978. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.) |
| 20-Jun-2021 | m1exp1 10301 | Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.) |
| 20-Jun-2021 | caucvgsr 6978 |
A Cauchy sequence of signed reals with a modulus of convergence
converges to a signed real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies). The HoTT book
theorem has a modulus of
convergence (that is, a rate of convergence) specified by (11.2.9) in
HoTT whereas this theorem fixes the rate of convergence to say that
all terms after the nth term must be within This is similar to caucvgprpr 6902 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 6977). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 6973).
3. Since a signed real (element of 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 6971). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 6976). (Contributed by Jim Kingdon, 20-Jun-2021.) |
| 19-Jun-2021 | prm2orodd 10508 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
| 19-Jun-2021 | oddnn02np1 10280 | A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.) |
| 19-Jun-2021 | 2tnp1ge0ge0 9303 | Two times an integer plus one is not negative iff the integer is not negative. (Contributed by AV, 19-Jun-2021.) |
| 19-Jun-2021 | nn0ledivnn 8838 | Division of a nonnegative integer by a positive integer is less than or equal to the integer. (Contributed by AV, 19-Jun-2021.) |
| 19-Jun-2021 | nnledivrp 8837 | Division of a positive integer by a positive number is less than or equal to the integer iff the number is greater than or equal to 1. (Contributed by AV, 19-Jun-2021.) |
| 19-Jun-2021 | caucvgsrlembnd 6977 | Lemma for caucvgsr 6978. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.) |
| 19-Jun-2021 | caucvgprprlemclphr 6895 |
Lemma for caucvgprpr 6902. The putative limit is a positive real.
Like caucvgprprlemcl 6894 but without a distinct variable
constraint
between |
| 19-Jun-2021 | ltnqpr 6783 |
We can order fractions via |
| 17-Jun-2021 | flodddiv4 10334 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
| 17-Jun-2021 | zeo4 10269 | An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.) |
| 17-Jun-2021 | zeo3 10267 | An integer is even or odd. (Contributed by AV, 17-Jun-2021.) |
| 17-Jun-2021 | caucvgprprlemnbj 6883 | Lemma for caucvgprpr 6902. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.) |
| 16-Jun-2021 | caucvgprprlemexbt 6896 | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-Jun-2021.) |
| 16-Jun-2021 | prplnqu 6810 | Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.) |
| 15-Jun-2021 | 11multnc 8544 | The product of 11 (as numeral) with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| 15-Jun-2021 | decmulnc 8543 | The product of a numeral with a number (no carry). (Contributed by AV, 15-Jun-2021.) |
| 15-Jun-2021 | caucvgprprlemexb 6897 | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-Jun-2021.) |
| 5-Jun-2021 | caucvgprprlemaddq 6898 | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-Jun-2021.) |
| 5-Apr-2021 | simpl2im 378 | Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) |
| 27-Mar-2021 | notnotd 592 | Deduction associated with notnot 591 and notnoti 606. (Contributed by Jarvin Udandy, 2-Sep-2016.) Avoid biconditional. (Revised by Wolf Lammen, 27-Mar-2021.) |
| 20-Mar-2021 | addmodlteq 9400 | Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. (Contributed by AV, 20-Mar-2021.) |
| 20-Mar-2021 | subfzo0 9251 | The difference between two elements in a half-open range of nonnegative integers is greater than the negation of the upper bound and less than the upper bound of the range. (Contributed by AV, 20-Mar-2021.) |
| 19-Mar-2021 | modsumfzodifsn 9398 | The sum of a number within a half-open range of positive integers is an element of the corresponding open range of nonnegative integers with one excluded integer modulo the excluded integer. (Contributed by AV, 19-Mar-2021.) |
| 19-Mar-2021 | modfzo0difsn 9397 | For a number within a half-open range of nonnegative integers with one excluded integer there is a positive integer so that the number is equal to the sum of the positive integer and the excluded integer modulo the upper bound of the range. (Contributed by AV, 19-Mar-2021.) |
| 19-Mar-2021 | addmodidr 9375 | The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by AV, 19-Mar-2021.) |
| 19-Mar-2021 | ltaddnegr 7529 | Adding a negative number to another number decreases it. (Contributed by AV, 19-Mar-2021.) |
| 14-Mar-2021 | addmodlteqALT 10259 | Two nonnegative integers less than the modulus are equal iff the sums of these integer with another integer are equal modulo the modulus. Shorter proof of addmodlteq 9400 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| 14-Mar-2021 | modlteq 9399 | Two nonnegative integers less than the modulus are equal iff they are equal modulo the modulus. (Contributed by AV, 14-Mar-2021.) |
| 3-Mar-2021 | caucvgprprlemval 6878 | Lemma for caucvgprpr 6902. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.) |
| 28-Feb-2021 | n2dvds3 10315 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
| 27-Feb-2021 | recnnpr 6738 | The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.) |
| 12-Feb-2021 | caucvgprprlemnjltk 6881 | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
| 12-Feb-2021 | caucvgprprlemnkeqj 6880 | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
| 12-Feb-2021 | caucvgprprlemnkltj 6879 | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.) |
| 12-Feb-2021 | caucvgprprlemcbv 6877 | Lemma for caucvgprpr 6902. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.) |
| 9-Feb-2021 | min2inf 10114 | The minimum of two numbers is less than or equal to the second. (Contributed by Jim Kingdon, 9-Feb-2021.) |
| 8-Feb-2021 | min1inf 10113 | The minimum of two numbers is less than or equal to the first. (Contributed by Jim Kingdon, 8-Feb-2021.) |
| 8-Feb-2021 | minmax 10112 | Minimum expressed in terms of maximum. (Contributed by Jim Kingdon, 8-Feb-2021.) |
| 8-Feb-2021 | mincom 10111 | The minimum of two reals is commutative. (Contributed by Jim Kingdon, 8-Feb-2021.) |
| 8-Feb-2021 | caucvgprprlemloccalc 6874 | Lemma for caucvgprpr 6902. Rearranging some expressions for caucvgprprlemloc 6893. (Contributed by Jim Kingdon, 8-Feb-2021.) |
| 5-Feb-2021 | fvinim0ffz 9250 | The function values for the borders of a finite interval of integers, which is the domain of the function, are not in the image of the interior of the interval iff the intersection of the images of the interior and the borders is empty. (Contributed by Alexander van der Vekens, 31-Oct-2017.) (Revised by AV, 5-Feb-2021.) |
| 28-Jan-2021 | caucvgprprlemelu 6876 | Lemma for caucvgprpr 6902. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-Jan-2021.) |
| 21-Jan-2021 | caucvgprprlemell 6875 | Lemma for caucvgprpr 6902. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.) |
| 20-Jan-2021 | caucvgprprlemnkj 6882 | Lemma for caucvgprpr 6902. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.) |
| 17-Jan-2021 | addn0nid 7478 | Adding a nonzero number to a complex number does not yield the complex number. (Contributed by AV, 17-Jan-2021.) |
| 17-Jan-2021 | addid0 7477 |
If adding a number to a another number yields the other number, the added
number must be |
| 8-Jan-2021 | ltnqpri 6784 |
We can order fractions via |
| 29-Dec-2020 | caucvgprprlemmu 6885 | Lemma for caucvgprpr 6902. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
| 29-Dec-2020 | caucvgprprlemml 6884 | Lemma for caucvgprpr 6902. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemloc 6893 | Lemma for caucvgprpr 6902. The putative limit is located. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemdisj 6892 | Lemma for caucvgprpr 6902. The putative limit is disjoint. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemrnd 6891 | Lemma for caucvgprpr 6902. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemupu 6890 | Lemma for caucvgprpr 6902. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemopu 6889 | Lemma for caucvgprpr 6902. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemlol 6888 | Lemma for caucvgprpr 6902. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemopl 6887 | Lemma for caucvgprpr 6902. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 21-Dec-2020 | caucvgprprlemm 6886 | Lemma for caucvgprpr 6902. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.) |
| 29-Nov-2020 | nqpru 6742 |
Comparing a fraction to a real can be done by whether it is an element
of the upper cut, or by |
| 28-Nov-2020 | caucvgprprlemk 6873 | Lemma for caucvgprpr 6902. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.) |
| 25-Nov-2020 | caucvgprprlem2 6900 | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
| 25-Nov-2020 | caucvgprprlem1 6899 | Lemma for caucvgprpr 6902. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-2020.) |
| 25-Nov-2020 | archrecpr 6854 | Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.) |
| 21-Nov-2020 | caucvgprprlemlim 6901 | Lemma for caucvgprpr 6902. The putative limit is a limit. (Contributed by Jim Kingdon, 21-Nov-2020.) |
| 21-Nov-2020 | caucvgprprlemcl 6894 | Lemma for caucvgprpr 6902. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-2020.) |
| 17-Nov-2020 | pm3.2 137 | Join antecedents with conjunction. Theorem *3.2 of [WhiteheadRussell] p. 111. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Nov-2012.) (Proof shortened by Jia Ming, 17-Nov-2020.) |
| 14-Nov-2020 | caucvgprpr 6902 |
A Cauchy sequence of positive reals with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
This is similar to caucvgpr 6872 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 6852) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-Nov-2020.) |
| 27-Oct-2020 | bj-omssonALT 10758 | Alternate proof of bj-omsson 10757. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.) |
| 27-Oct-2020 | bj-omsson 10757 | Constructive proof of omsson 4353. See also bj-omssonALT 10758. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged. |
| 27-Oct-2020 | bj-nnelon 10754 | A natural number is an ordinal. Constructive proof of nnon 4350. Can also be proved from bj-omssonALT 10758. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
| 27-Oct-2020 | bj-nnord 10753 | A natural number is an ordinal. Constructive proof of nnord 4352. Can also be proved from bj-nnelon 10754 if the latter is proved from bj-omssonALT 10758. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) |
| 27-Oct-2020 | bj-axempty2 10685 | Axiom of the empty set from bounded separation, alternate version to bj-axempty 10684. (Contributed by BJ, 27-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3904 instead. (New usage is discouraged.) |
| 25-Oct-2020 | bj-indind 10727 |
If |
| 25-Oct-2020 | bj-axempty 10684 | Axiom of the empty set from bounded separation. It is provable from bounded separation since the intuitionistic FOL used in iset.mm assumes a non-empty universe. See axnul 3903. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3904 instead. (New usage is discouraged.) |
| 25-Oct-2020 | bj-axemptylem 10683 | Lemma for bj-axempty 10684 and bj-axempty2 10685. (Contributed by BJ, 25-Oct-2020.) (Proof modification is discouraged.) Use ax-nul 3904 instead. (New usage is discouraged.) |
| 23-Oct-2020 | caucvgprlemnkj 6856 | Lemma for caucvgpr 6872. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.) |
| 20-Oct-2020 | caucvgprlemupu 6862 | Lemma for caucvgpr 6872. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.) |
| 20-Oct-2020 | caucvgprlemopu 6861 | Lemma for caucvgpr 6872. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
| 20-Oct-2020 | caucvgprlemlol 6860 | Lemma for caucvgpr 6872. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.) |
| 20-Oct-2020 | caucvgprlemopl 6859 | Lemma for caucvgpr 6872. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.) |
| 18-Oct-2020 | caucvgprlemnbj 6857 | Lemma for caucvgpr 6872. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.) |
| 11-Oct-2020 | elexd 2612 | If a class is a member of another class, it is a set. (Contributed by Glauco Siliprandi, 11-Oct-2020.) |
| 9-Oct-2020 | caucvgprlemladdfu 6867 |
Lemma for caucvgpr 6872. Adding |
| 9-Oct-2020 | caucvgprlemk 6855 | Lemma for caucvgpr 6872. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.) |
| 8-Oct-2020 | caucvgprlemladdrl 6868 |
Lemma for caucvgpr 6872. Adding |
| 3-Oct-2020 | caucvgprlem2 6870 | Lemma for caucvgpr 6872. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
| 3-Oct-2020 | caucvgprlem1 6869 | Lemma for caucvgpr 6872. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.) |
| 3-Oct-2020 | ltnnnq 6613 |
Ordering of positive integers via |
| 1-Oct-2020 | caucvgprlemlim 6871 | Lemma for caucvgpr 6872. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.) |
| 27-Sep-2020 | caucvgprlemloc 6865 | Lemma for caucvgpr 6872. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.) |
| 27-Sep-2020 | caucvgprlemdisj 6864 | Lemma for caucvgpr 6872. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.) |
| 27-Sep-2020 | caucvgprlemrnd 6863 | Lemma for caucvgpr 6872. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.) |
| 27-Sep-2020 | caucvgprlemm 6858 | Lemma for caucvgpr 6872. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.) |
| 27-Sep-2020 | archrecnq 6853 | Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.) |
| 26-Sep-2020 | caucvgprlemcl 6866 | Lemma for caucvgpr 6872. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.) |
| 16-Sep-2020 | lcmass 10467 | Associative law for lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcmgcdlem 10459 |
Lemma for lcmgcd 10460 and lcmdvds 10461. Prove them for positive |
| 16-Sep-2020 | lcmledvds 10452 | A positive integer which both operands of the lcm operator divide bounds it. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcmcllem 10449 | Lemma for lcmn0cl 10450 and dvdslcm 10451. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcmn0val 10448 | The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcm0val 10447 | The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 10446 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcmcom 10446 | The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.) |
| 16-Sep-2020 | lcmval 10445 |
Value of the lcm operator. |
| 16-Sep-2020 | df-lcm 10443 |
Define the lcm operator. For example, |
| 4-Sep-2020 | dfinfre 8034 |
The infimum of a set of reals |
| 4-Sep-2020 | lbinfle 8028 | If a set of reals contains a lower bound, its infimum is less than or equal to all members of the set. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
| 4-Sep-2020 | lbinfcl 8027 | If a set of reals contains a lower bound, it contains its infimum. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
| 4-Sep-2020 | lbinf 8026 | If a set of reals contains a lower bound, the lower bound is its infimum. (Contributed by NM, 9-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
| 4-Sep-2020 | inf00 6444 | The infimum regarding an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
| 4-Sep-2020 | sup00 6416 | The supremum under an empty base set is always the empty set. (Contributed by AV, 4-Sep-2020.) |
| 2-Sep-2020 | nfinf 6430 | Hypothesis builder for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq123d 6429 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq3 6428 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq2 6427 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq1i 6426 | Equality inference for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq1d 6425 | Equality deduction for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | infeq1 6424 | Equality theorem for infimum. (Contributed by AV, 2-Sep-2020.) |
| 2-Sep-2020 | df-inf 6398 |
Define the infimum of class |
| 2-Sep-2020 | impel 274 | An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.) |
| 1-Sep-2020 | 2a1 25 | A double form of ax-1 5. Its associated inference is 2a1i 27. Its associated deduction is 2a1d 23. (Contributed by BJ, 10-Aug-2020.) (Proof shortened by Wolf Lammen, 1-Sep-2020.) |
| 27-Aug-2020 | 3lcm2e6 10539 | The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.) |
| 27-Aug-2020 | 6lcm4e12 10469 | The least common multiple of six and four is twelve. (Contributed by AV, 27-Aug-2020.) |
| 27-Aug-2020 | 3lcm2e6woprm 10468 | The least common multiple of three and two is six. This proof does not use the property of 2 and 3 being prime. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 27-Aug-2020.) |
| 27-Aug-2020 | lcmgcdnn 10464 | The product of two positive integers' least common multiple and greatest common divisor is the product of the two integers. (Contributed by AV, 27-Aug-2020.) |
| 27-Aug-2020 | 6gcd4e2 10384 |
The greatest common divisor of six and four is two. To calculate this
gcd, a simple form of Euclid's algorithm is used:
|
| 26-Aug-2020 | sqrt0rlem 9889 | Lemma for sqrt0 9890. (Contributed by Jim Kingdon, 26-Aug-2020.) |
| 23-Aug-2020 | lcm1 10463 | The lcm of an integer and 1 is the absolute value of the integer. (Contributed by AV, 23-Aug-2020.) |
| 23-Aug-2020 | sqrtrval 9886 | Value of square root function. (Contributed by Jim Kingdon, 23-Aug-2020.) |
| 23-Aug-2020 | df-rsqrt 9884 |
Define a function whose value is the square root of a nonnegative real
number.
Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root. (Contributed by Jim Kingdon, 23-Aug-2020.) |
| 19-Aug-2020 | addnqpr 6751 | Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| 19-Aug-2020 | addnqprlemfu 6750 | Lemma for addnqpr 6751. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| 19-Aug-2020 | addnqprlemfl 6749 | Lemma for addnqpr 6751. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| 19-Aug-2020 | addnqprlemru 6748 | Lemma for addnqpr 6751. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| 19-Aug-2020 | addnqprlemrl 6747 | Lemma for addnqpr 6751. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.) |
| 15-Aug-2020 | prmdvdsfz 10520 | Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020.) |
| 15-Aug-2020 | caucvgprlemcanl 6834 | Lemma for cauappcvgprlemladdrl 6847. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.) |
| 10-Aug-2020 | 2a1d 23 | Deduction introducing two antecedents. Two applications of a1d 22. Deduction associated with 2a1 25 and 2a1i 27. (Contributed by BJ, 10-Aug-2020.) |
| 9-Aug-2020 | ncoprmgcdgt1b 10472 | Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is greater than 1. (Contributed by AV, 9-Aug-2020.) |
| 9-Aug-2020 | ncoprmgcdne1b 10471 | Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is not 1. (Contributed by AV, 9-Aug-2020.) |
| 9-Aug-2020 | coprmgcdb 10470 | Two positive integers are coprime, i.e. the only positive integer that divides both of them is 1, iff their greatest common divisor is 1. (Contributed by AV, 9-Aug-2020.) |
| 9-Aug-2020 | nndvdslegcd 10357 |
A positive integer which divides both positive operands of the |
| 9-Aug-2020 | negfi 10110 | The negation of a finite set of real numbers is finite. (Contributed by AV, 9-Aug-2020.) |
| 9-Aug-2020 | negf1o 7486 | Negation is an isomorphism of a subset of the real numbers to the negated elements of the subset. (Contributed by AV, 9-Aug-2020.) |
| 4-Aug-2020 | cauappcvgprlemupu 6839 | Lemma for cauappcvgpr 6852. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| 4-Aug-2020 | cauappcvgprlemopu 6838 | Lemma for cauappcvgpr 6852. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| 4-Aug-2020 | cauappcvgprlemlol 6837 | Lemma for cauappcvgpr 6852. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| 4-Aug-2020 | cauappcvgprlemopl 6836 | Lemma for cauappcvgpr 6852. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.) |
| 22-Jul-2020 | prmex 10495 | The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.) |
| 22-Jul-2020 | prmssnn 10494 | The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.) |
| 18-Jul-2020 | cauappcvgprlemloc 6842 | Lemma for cauappcvgpr 6852. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| 18-Jul-2020 | cauappcvgprlemdisj 6841 | Lemma for cauappcvgpr 6852. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| 18-Jul-2020 | cauappcvgprlemrnd 6840 | Lemma for cauappcvgpr 6852. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| 18-Jul-2020 | cauappcvgprlemm 6835 | Lemma for cauappcvgpr 6852. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.) |
| 11-Jul-2020 | cauappcvgprlemladdrl 6847 | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| 11-Jul-2020 | cauappcvgprlemladdru 6846 | Lemma for cauappcvgprlemladd 6848. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| 11-Jul-2020 | cauappcvgprlemladdfl 6845 | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| 11-Jul-2020 | cauappcvgprlemladdfu 6844 | Lemma for cauappcvgprlemladd 6848. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.) |
| 8-Jul-2020 | nqprl 6741 |
Comparing a fraction to a real can be done by whether it is an element
of the lower cut, or by |
| 5-Jul-2020 | addmodid 9374 | The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by Alexander van der Vekens, 30-Oct-2018.) (Proof shortened by AV, 5-Jul-2020.) |
| 1-Jul-2020 | gcdzeq 10411 |
A positive integer |
| 29-Jun-2020 | rspcda 2706 | Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 29-Jun-2020.) |
| 26-Jun-2020 | zeo5 10288 | An integer is either even or odd, version of zeo3 10267 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.) |
| 25-Jun-2020 | even2n 10273 | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
| 24-Jun-2020 | nqprlu 6737 | The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.) |
| 23-Jun-2020 | cauappcvgprlem2 6850 | Lemma for cauappcvgpr 6852. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
| 23-Jun-2020 | cauappcvgprlem1 6849 | Lemma for cauappcvgpr 6852. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.) |
| 23-Jun-2020 | cauappcvgprlemladd 6848 |
Lemma for cauappcvgpr 6852. This takes |
| 21-Jun-2020 | rspcdva 2707 | Restricted specialization, using implicit substitution. (Contributed by Thierry Arnoux, 21-Jun-2020.) |
| 20-Jun-2020 | cauappcvgprlemlim 6851 | Lemma for cauappcvgpr 6852. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.) |
| 20-Jun-2020 | cauappcvgprlemcl 6843 | Lemma for cauappcvgpr 6852. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.) |
| 19-Jun-2020 | cauappcvgpr 6852 |
A Cauchy approximation has a limit. A Cauchy approximation, here
This proof (including its lemmas) is similar to the proofs of caucvgpr 6872 and caucvgprpr 6902 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.) |
| 18-Jun-2020 | caucvgpr 6872 |
A Cauchy sequence of positive fractions with a modulus of convergence
converges to a positive real. This is basically Corollary 11.2.13 of
[HoTT], p. (varies) (one key difference
being that this is for
positive reals rather than signed reals). Also, the HoTT book theorem
has a modulus of convergence (that is, a rate of convergence)
specified by (11.2.9) in HoTT whereas this theorem fixes the rate of
convergence to say that all terms after the nth term must be within
This proof (including its lemmas) is similar to the proofs of cauappcvgpr 6852 and caucvgprpr 6902. Reading cauappcvgpr 6852 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.) |
| 15-Jun-2020 | imdivapd 9862 | Imaginary part of a division. Related to remul2 9760. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| 15-Jun-2020 | redivapd 9861 | Real part of a division. Related to remul2 9760. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| 15-Jun-2020 | cjdivapd 9855 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| 15-Jun-2020 | riotaexg 5492 | Restricted iota is a set. (Contributed by Jim Kingdon, 15-Jun-2020.) |
| 14-Jun-2020 | cjdivapi 9822 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | cjdivap 9796 | Complex conjugate distributes over division. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | cjap0 9794 | A number is apart from zero iff its complex conjugate is apart from zero. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | cjap 9793 | Complex conjugate and apartness. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | imdivap 9768 | Imaginary part of a division. Related to immul2 9767. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | redivap 9761 | Real part of a division. Related to remul2 9760. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 14-Jun-2020 | mulreap 9751 | A product with a real multiplier apart from zero is real iff the multiplicand is real. (Contributed by Jim Kingdon, 14-Jun-2020.) |
| 13-Jun-2020 | sqgt0apd 9633 | The square of a real apart from zero is positive. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| 13-Jun-2020 | reexpclzapd 9630 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| 13-Jun-2020 | expdivapd 9619 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| 13-Jun-2020 | sqdivapd 9618 | Distribution of square over division. (Contributed by Jim Kingdon, 13-Jun-2020.) |
| 12-Jun-2020 | expsubapd 9616 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | expm1apd 9615 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | expp1zapd 9614 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | exprecapd 9613 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | expnegapd 9612 | Value of a complex number raised to a negative power. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | expap0d 9611 | Nonnegative integer exponentiation is nonzero if its mantissa is nonzero. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | expclzapd 9610 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | sqrecapd 9609 | Square of reciprocal. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | sqgt0api 9561 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 12-Jun-2020 | sqdivapi 9559 | Distribution of square over division. (Contributed by Jim Kingdon, 12-Jun-2020.) |
| 11-Jun-2020 | sqgt0ap 9544 | The square of a nonzero real is positive. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | sqdivap 9540 | Distribution of square over division. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | expdivap 9527 | Nonnegative integer exponentiation of a quotient. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | expm1ap 9526 | Value of a complex number raised to an integer power minus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | expp1zap 9525 | Value of a nonzero complex number raised to an integer power plus one. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | expsubap 9524 | Exponent subtraction law for nonnegative integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 11-Jun-2020 | expmulzap 9522 | Product of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 11-Jun-2020.) |
| 10-Jun-2020 | expaddzap 9520 | Sum of exponents law for integer exponentiation. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | expaddzaplem 9519 | Lemma for expaddzap 9520. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | exprecap 9517 | Nonnegative integer exponentiation of a reciprocal. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | mulexpzap 9516 | Integer exponentiation of a product. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | expap0i 9508 | Integer exponentiation is apart from zero if its mantissa is apart from zero. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | expap0 9506 | Positive integer exponentiation is apart from zero iff its mantissa is apart from zero. That it is easier to prove this first, and then prove expeq0 9507 in terms of it, rather than the other way around, is perhaps an illustration of the maxim "In constructive analysis, the apartness is more basic [ than ] equality." ([Geuvers], p. 1). (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 10-Jun-2020 | mvllmulapd 7921 | Move LHS left multiplication to RHS. (Contributed by Jim Kingdon, 10-Jun-2020.) |
| 9-Jun-2020 | expclzap 9501 | Closure law for integer exponentiation. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| 9-Jun-2020 | expclzaplem 9500 | Closure law for integer exponentiation. Lemma for expclzap 9501 and expap0i 9508. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| 9-Jun-2020 | reexpclzap 9496 | Closure of exponentiation of reals. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| 9-Jun-2020 | neg1ap0 8148 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
| 8-Jun-2020 | expcl2lemap 9488 | Lemma for proving integer exponentiation closure laws. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| 8-Jun-2020 | expn1ap0 9486 | A number to the negative one power is the reciprocal. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| 8-Jun-2020 | expineg2 9485 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| 8-Jun-2020 | expnegap0 9484 | Value of a complex number raised to a negative integer power. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| 8-Jun-2020 | expinnval 9479 | Value of exponentiation to positive integer powers. (Contributed by Jim Kingdon, 8-Jun-2020.) |
| 7-Jun-2020 | zob 10291 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
| 7-Jun-2020 | expival 9478 | Value of exponentiation to integer powers. (Contributed by Jim Kingdon, 7-Jun-2020.) |
| 7-Jun-2020 | expivallem 9477 | Lemma for expival 9478. If we take a complex number apart from zero and raise it to a positive integer power, the result is apart from zero. (Contributed by Jim Kingdon, 7-Jun-2020.) |
| 7-Jun-2020 | df-iexp 9476 |
Define exponentiation to nonnegative integer powers. This definition is
not meant to be used directly; instead, exp0 9480
and expp1 9483 provide the
standard recursive definition. The up-arrow notation is used by Donald
Knuth for iterated exponentiation (Science 194, 1235-1242, 1976)
and
is convenient for us since we don't have superscripts. 10-Jun-2005: The
definition was extended to include zero exponents, so that |
| 7-Jun-2020 | halfge0 8247 | One-half is not negative. (Contributed by AV, 7-Jun-2020.) |
| 4-Jun-2020 | nn0ob 10308 | Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.) |
| 4-Jun-2020 | iseqfveq 9450 | Equality of sequences. (Contributed by Jim Kingdon, 4-Jun-2020.) |
| 3-Jun-2020 | iseqfeq2 9449 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| 3-Jun-2020 | iseqfveq2 9448 | Equality of sequences. (Contributed by Jim Kingdon, 3-Jun-2020.) |
| 2-Jun-2020 | nn0o 10307 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.) |
| 2-Jun-2020 | nno 10306 | An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.) |
| 2-Jun-2020 | nn0o1gt2 10305 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) |
| 2-Jun-2020 | 3halfnz 8444 | Three halves is not an integer. (Contributed by AV, 2-Jun-2020.) |
| 1-Jun-2020 | iseqcl 9443 | Closure properties of the recursive sequence builder. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| 1-Jun-2020 | fzdcel 9059 | Decidability of membership in a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| 1-Jun-2020 | fztri3or 9058 | Trichotomy in terms of a finite interval of integers. (Contributed by Jim Kingdon, 1-Jun-2020.) |
| 1-Jun-2020 | zdclt 8425 |
Integer |
| 31-May-2020 | iseqp1 9445 | Value of the sequence builder function at a successor. (Contributed by Jim Kingdon, 31-May-2020.) |
| 31-May-2020 | iseq1 9442 | Value of the sequence builder function at its initial value. (Contributed by Jim Kingdon, 31-May-2020.) |
| 31-May-2020 | iseqovex 9439 | Closure of a function used in proving sequence builder theorems. This can be thought of as a lemma for the small number of sequence builder theorems which need it. (Contributed by Jim Kingdon, 31-May-2020.) |
| 31-May-2020 | frecuzrdgcl 9415 |
Closure law for the recursive definition generator on upper
integers. See comment in frec2uz0d 9401 for the description of |
| 30-May-2020 | nn0enne 10302 | A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.) |
| 30-May-2020 | iseqfn 9441 | The sequence builder function is a function. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | iseqval 9440 | Value of the sequence builder function. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | nfiseq 9438 | Hypothesis builder for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | iseqeq4 9437 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | iseqeq3 9436 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | iseqeq2 9435 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | iseqeq1 9434 | Equality theorem for the sequence builder operation. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | nffrec 6005 | Bound-variable hypothesis builder for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | freceq2 6003 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| 30-May-2020 | freceq1 6002 | Equality theorem for the finite recursive definition generator. (Contributed by Jim Kingdon, 30-May-2020.) |
| 29-May-2020 | df-iseq 9432 |
Define a general-purpose operation that builds a recursive sequence
(i.e. a function on the positive integers
The first operand in the parentheses is the operation that is applied to
the previous value and the value of the input sequence (second operand).
The operand to the left of the parenthesis is the integer to start from.
For example, for the operation
Internally, the frec function generates as its values a set of
ordered pairs starting at (Contributed by Jim Kingdon, 29-May-2020.) |
| 28-May-2020 | frecuzrdgsuc 9417 |
Successor value of a recursive definition generator on upper
integers. See comment in frec2uz0d 9401 for the description of |
| 27-May-2020 | frecuzrdg0 9416 |
Initial value of a recursive definition generator on upper integers.
See comment in frec2uz0d 9401 for the description of |
| 27-May-2020 | frecuzrdgrrn 9410 |
The function |
| 27-May-2020 | dffun5r 4934 | A way of proving a relation is a function, analogous to mo2r 1993. (Contributed by Jim Kingdon, 27-May-2020.) |
| 26-May-2020 | frecuzrdgfn 9414 |
The recursive definition generator on upper integers is a function.
See comment in frec2uz0d 9401 for the description of |
| 26-May-2020 | frecuzrdglem 9413 | A helper lemma for the value of a recursive definition generator on upper integers. (Contributed by Jim Kingdon, 26-May-2020.) |
| 26-May-2020 | frecuzrdgrom 9412 |
The function |
| 25-May-2020 | divlt1lt 8801 | A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.) |
| 25-May-2020 | freccl 6016 | Closure for finite recursion. (Contributed by Jim Kingdon, 25-May-2020.) |
| 24-May-2020 | mod2eq1n2dvds 10279 | An integer is 1 modulo 2 iff it is odd (i.e. not divisible by 2), see example 3 in [ApostolNT] p. 107. (Contributed by AV, 24-May-2020.) |
| 24-May-2020 | frec2uzrdg 9411 |
A helper lemma for the value of a recursive definition generator on
upper integers (typically either |
| 24-May-2020 | eluz2gt1 8689 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
| 24-May-2020 | xp1d2m1eqxm1d2 8283 | A complex number increased by 1, then divided by 2, then decreased by 1 equals the complex number decreased by 1 and then divided by 2. (Contributed by AV, 24-May-2020.) |
| 21-May-2020 | fzofig 9424 | Half-open integer sets are finite. (Contributed by Jim Kingdon, 21-May-2020.) |
| 21-May-2020 | fzfigd 9423 | Deduction form of fzfig 9422. (Contributed by Jim Kingdon, 21-May-2020.) |
| 19-May-2020 | fzfig 9422 | A finite interval of integers is finite. (Contributed by Jim Kingdon, 19-May-2020.) |
| 19-May-2020 | frechashgf1o 9421 |
|
| 19-May-2020 | ssfiexmid 6361 | If any subset of a finite set is finite, excluded middle follows. One direction of Theorem 2.1 of [Bauer], p. 485. (Contributed by Jim Kingdon, 19-May-2020.) |
| 19-May-2020 | enm 6317 | A set equinumerous to an inhabited set is inhabited. (Contributed by Jim Kingdon, 19-May-2020.) |
| 18-May-2020 | frecfzen2 9420 | The cardinality of a finite set of sequential integers with arbitrary endpoints. (Contributed by Jim Kingdon, 18-May-2020.) |
| 18-May-2020 | frecfzennn 9419 | The cardinality of a finite set of sequential integers. (See frec2uz0d 9401 for a description of the hypothesis.) (Contributed by Jim Kingdon, 18-May-2020.) |
| 17-May-2020 | frec2uzisod 9409 |
|
| 17-May-2020 | frec2uzf1od 9408 |
|
| 17-May-2020 | frec2uzrand 9407 |
Range of |
| 16-May-2020 | frec2uzlt2d 9406 |
The mapping |
| 16-May-2020 | frec2uzltd 9405 |
Less-than relation for |
| 16-May-2020 | frec2uzuzd 9404 |
The value |
| 16-May-2020 | frec2uzsucd 9403 |
The value of |
| 16-May-2020 | frec2uzzd 9402 |
The value of |
| 16-May-2020 | frec2uz0d 9401 |
The mapping |
| 15-May-2020 | nntri3 6098 | A trichotomy law for natural numbers. (Contributed by Jim Kingdon, 15-May-2020.) |
| 14-May-2020 | rdgifnon2 5990 | The recursive definition generator is a function on ordinal numbers. (Contributed by Jim Kingdon, 14-May-2020.) |
| 14-May-2020 | rdgtfr 5984 | The recursion rule for the recursive definition generator is defined everywhere. (Contributed by Jim Kingdon, 14-May-2020.) |
| 13-May-2020 | frecfnom 6009 | The function generated by finite recursive definition generation is a function on omega. (Contributed by Jim Kingdon, 13-May-2020.) |
| 13-May-2020 | frecabex 6007 | The class abstraction from df-frec 6001 exists. This is a lemma for other finite recursion proofs. (Contributed by Jim Kingdon, 13-May-2020.) |
| 8-May-2020 | tfr0 5960 | Transfinite recursion at the empty set. (Contributed by Jim Kingdon, 8-May-2020.) |
| 7-May-2020 | frec0g 6006 | The initial value resulting from finite recursive definition generation. (Contributed by Jim Kingdon, 7-May-2020.) |
| 3-May-2020 | dcned 2251 | Decidable equality implies decidable negated equality. (Contributed by Jim Kingdon, 3-May-2020.) |
| 2-May-2020 | ax-arch 7095 |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7057.
This axiom should not be used directly; instead use arch 8285
(which is the
same, but stated in terms of |
| 30-Apr-2020 | ltexnqi 6599 | Ordering on positive fractions in terms of existence of sum. (Contributed by Jim Kingdon, 30-Apr-2020.) |
| 26-Apr-2020 | pitonnlem1p1 7014 | Lemma for pitonn 7016. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
| 26-Apr-2020 | addnqpr1 6752 | Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6751. (Contributed by Jim Kingdon, 26-Apr-2020.) |
| 26-Apr-2020 | addpinq1 6654 | Addition of one to the numerator of a fraction whose denominator is one. (Contributed by Jim Kingdon, 26-Apr-2020.) |
| 26-Apr-2020 | nnnq 6612 | The canonical embedding of positive integers into positive fractions. (Contributed by Jim Kingdon, 26-Apr-2020.) |
| 24-Apr-2020 | pitonnlem2 7015 | Lemma for pitonn 7016. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
| 24-Apr-2020 | pitonnlem1 7013 | Lemma for pitonn 7016. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
| 23-Apr-2020 | archsr 6958 |
For any signed real, there is an integer that is greater than it. This
is also known as the "archimedean property". The expression
|
| 23-Apr-2020 | nnprlu 6743 | The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
| 22-Apr-2020 | axarch 7057 |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7095. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
| 22-Apr-2020 | pitonn 7016 |
Mapping from |
| 22-Apr-2020 | archpr 6833 |
For any positive real, there is an integer that is greater than it.
This is also known as the "archimedean property". The integer
|
| 20-Apr-2020 | fzo0m 9200 | A half-open integer range based at 0 is inhabited precisely if the upper bound is a positive integer. (Contributed by Jim Kingdon, 20-Apr-2020.) |
| 20-Apr-2020 | fzom 9173 | A half-open integer interval is inhabited iff it contains its left endpoint. (Contributed by Jim Kingdon, 20-Apr-2020.) |
| 18-Apr-2020 | eluzdc 8697 | Membership of an integer in an upper set of integers is decidable. (Contributed by Jim Kingdon, 18-Apr-2020.) |
| 17-Apr-2020 | zlelttric 8396 | Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.) |
| 16-Apr-2020 | fznlem 9060 | A finite set of sequential integers is empty if the bounds are reversed. (Contributed by Jim Kingdon, 16-Apr-2020.) |
| 15-Apr-2020 | fzm 9057 | Properties of a finite interval of integers which is inhabited. (Contributed by Jim Kingdon, 15-Apr-2020.) |
| 15-Apr-2020 | xpdom3m 6331 | A set is dominated by its Cartesian product with an inhabited set. Exercise 6 of [Suppes] p. 98. (Contributed by Jim Kingdon, 15-Apr-2020.) |
| 13-Apr-2020 | snfig 6314 | A singleton is finite. (Contributed by Jim Kingdon, 13-Apr-2020.) |
| 13-Apr-2020 | en1bg 6303 | A set is equinumerous to ordinal one iff it is a singleton. (Contributed by Jim Kingdon, 13-Apr-2020.) |
| 10-Apr-2020 | negm 8700 | The image under negation of an inhabited set of reals is inhabited. (Contributed by Jim Kingdon, 10-Apr-2020.) |
| 8-Apr-2020 | zleloe 8398 | Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.) |
| 7-Apr-2020 | zdcle 8424 |
Integer |
| 5-Apr-2020 | faccld 9663 | Closure of the factorial function, deduction version of faccl 9662. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| 5-Apr-2020 | divge1 8800 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
| 4-Apr-2020 | ioorebasg 8998 | Open intervals are elements of the set of all open intervals. (Contributed by Jim Kingdon, 4-Apr-2020.) |
| 30-Mar-2020 | icc0r 8949 | An empty closed interval of extended reals. (Contributed by Jim Kingdon, 30-Mar-2020.) |
| 30-Mar-2020 | ubioog 8937 | An open interval does not contain its right endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) |
| 30-Mar-2020 | lbioog 8936 | An open interval does not contain its left endpoint. (Contributed by Jim Kingdon, 30-Mar-2020.) |
| 29-Mar-2020 | iooidg 8932 | An open interval with identical lower and upper bounds is empty. (Contributed by Jim Kingdon, 29-Mar-2020.) |
| 27-Mar-2020 | zletric 8395 | Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.) |
| 26-Mar-2020 | 4z 8381 | 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
| 25-Mar-2020 | elfzmlbm 9142 | Subtracting the lower bound of a finite set of sequential integers from an element of this set. (Contributed by Alexander van der Vekens, 29-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| 25-Mar-2020 | elfz0add 9134 | An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| 25-Mar-2020 | 2eluzge0 8663 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
| 23-Mar-2020 | rpnegap 8766 | Either a real apart from zero or its negation is a positive real, but not both. (Contributed by Jim Kingdon, 23-Mar-2020.) |
| 23-Mar-2020 | reapltxor 7689 | Real apartness in terms of less than (exclusive-or version). (Contributed by Jim Kingdon, 23-Mar-2020.) |
| 22-Mar-2020 | rpcnap0 8754 | A positive real is a complex number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
| 22-Mar-2020 | rpreap0 8752 | A positive real is a real number apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
| 22-Mar-2020 | rpap0 8750 | A positive real is apart from zero. (Contributed by Jim Kingdon, 22-Mar-2020.) |
| 20-Mar-2020 | qapne 8724 | Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 20-Mar-2020.) |
| 20-Mar-2020 | divap1d 7888 | If two complex numbers are apart, their quotient is apart from one. (Contributed by Jim Kingdon, 20-Mar-2020.) |
| 20-Mar-2020 | apmul1 7876 | Multiplication of both sides of complex apartness by a complex number apart from zero. (Contributed by Jim Kingdon, 20-Mar-2020.) |
| 19-Mar-2020 | divfnzn 8706 |
Division restricted to |
| 19-Mar-2020 | div2negapd 7892 | Quotient of two negatives. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | divneg2apd 7891 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | divnegapd 7890 | Move negative sign inside of a division. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | divap0bd 7889 | A ratio is zero iff the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | diveqap0ad 7887 | A fraction of complex numbers is zero iff its numerator is. Deduction form of diveqap0 7770. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | diveqap1ad 7886 | The quotient of two complex numbers is one iff they are equal. Deduction form of diveqap1 7793. Generalization of diveqap1d 7885. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | diveqap1d 7885 | Equality in terms of unit ratio. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 19-Mar-2020 | diveqap0d 7884 | If a ratio is zero, the numerator is zero. (Contributed by Jim Kingdon, 19-Mar-2020.) |
| 15-Mar-2020 | nneoor 8449 | A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.) |
| 14-Mar-2020 | zltlen 8426 | Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7730 which is a similar result for real numbers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | zdceq 8423 | Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | zapne 8422 | Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | zltnle 8397 | 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | ztri3or 8394 | Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | ztri3or0 8393 | Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.) |
| 14-Mar-2020 | zaddcllemneg 8390 |
Lemma for zaddcl 8391. Special case in which |
| 14-Mar-2020 | zaddcllempos 8388 |
Lemma for zaddcl 8391. Special case in which |
| 14-Mar-2020 | dcne 2256 |
Decidable equality expressed in terms of |
| 9-Mar-2020 | dvdsmultr1d 10234 | Natural deduction form of dvdsmultr1 10233. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| 9-Mar-2020 | dvds2subd 10231 | Natural deduction form of dvds2sub 10230. (Contributed by Stanislas Polu, 9-Mar-2020.) |
| 9-Mar-2020 | 2muliap0 8255 |
|
| 9-Mar-2020 | iap0 8254 |
The imaginary unit |
| 9-Mar-2020 | 2ap0 8132 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | 1ne0 8107 |
|
| 9-Mar-2020 | redivclapi 7867 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | redivclapzi 7866 | Closure law for division of reals. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | rerecclapi 7865 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | rerecclapzi 7864 | Closure law for reciprocal. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divdivdivapi 7863 | Division of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divadddivapi 7862 | Addition of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divmul13api 7861 | Swap denominators of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divmuldivapi 7860 | Multiplication of two ratios. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | div11api 7859 | One-to-one relationship for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | div23api 7858 | A commutative/associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divdirapi 7857 | Distribution of division over addition. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 9-Mar-2020 | divassapi 7856 | An associative law for division. (Contributed by Jim Kingdon, 9-Mar-2020.) |
| 8-Mar-2020 | nnap0 8068 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
| 8-Mar-2020 | divdivap2d 7909 | Division by a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) |
| 8-Mar-2020 | divdivap1d 7908 | Division into a fraction. (Contributed by Jim Kingdon, 8-Mar-2020.) |
| 8-Mar-2020 | dmdcanap2d 7907 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) |
| 8-Mar-2020 | dmdcanapd 7906 | Cancellation law for division and multiplication. (Contributed by Jim Kingdon, 8-Mar-2020.) |
| Copyright terms: Public domain | W3C HTML validation [external] |