Intuitionistic Logic Explorer Most Recent Proofs |
||
Mirrors > Home > ILE Home > Th. List > Recent | MPE Most Recent Other > MM 100 |
See the MPE Most Recent Proofs page for news and some useful links.
Color key: | Intuitionistic Logic Explorer | User Mathboxes |
Date | Label | Description |
---|---|---|
Theorem | ||
5-Dec-2021 | divalglemqt 10231 | Lemma for divalg 10236. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.) |
4-Dec-2021 | divalglemeuneg 10235 | Lemma for divalg 10236. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
4-Dec-2021 | divalglemeunn 10233 | Lemma for divalg 10236. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
4-Dec-2021 | divalglemnqt 10232 | Lemma for divalg 10236. The case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.) |
2-Dec-2021 | rspc2gv 2684 | Restricted specialization with two quantifiers, using implicit substitution. (Contributed by BJ, 2-Dec-2021.) |
30-Nov-2021 | divalglemex 10234 | Lemma for divalg 10236. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) |
30-Nov-2021 | divalglemnn 10230 | Lemma for divalg 10236. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) |
27-Nov-2021 | ioom 9217 | 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 6414 | Image of a supremum under an isomorphism. (Contributed by Jim Kingdon, 26-Nov-2021.) |
26-Nov-2021 | isoti 6411 | An isomorphism preserves tightness. (Contributed by Jim Kingdon, 26-Nov-2021.) |
26-Nov-2021 | isotilem 6410 | Lemma for isoti 6411. (Contributed by Jim Kingdon, 26-Nov-2021.) |
26-Nov-2021 | supsnti 6409 | The supremum of a singleton. (Contributed by Jim Kingdon, 26-Nov-2021.) |
24-Nov-2021 | supmaxti 6408 | 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 6406 | A supremum is the least upper bound. See also supclti 6404 and supubti 6405. (Contributed by Jim Kingdon, 24-Nov-2021.) |
24-Nov-2021 | supubti 6405 |
A supremum is an upper bound. See also supclti 6404 and suplubti 6406.
This proof demonstrates how to expand an iota-based definition (df-iota 4895) using riotacl2 5509. (Contributed by Jim Kingdon, 24-Nov-2021.) |
24-Nov-2021 | supclti 6404 | A supremum belongs to its base class (closure law). See also supubti 6405 and suplubti 6406. (Contributed by Jim Kingdon, 24-Nov-2021.) |
24-Nov-2021 | eqsuptid 6403 | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 24-Nov-2021.) |
23-Nov-2021 | eqsupti 6402 | Sufficient condition for an element to be equal to the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
23-Nov-2021 | supval2ti 6401 | Alternate expression for the supremum. (Contributed by Jim Kingdon, 23-Nov-2021.) |
23-Nov-2021 | supeuti 6400 | 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 6399 | Any class has at most one supremum in (where is interpreted as 'less than'). The hypothesis is satisfied by real numbers (see lttri3 7157) or other orders which correspond to tight apartnesses. (Contributed by Jim Kingdon, 23-Nov-2021.) |
17-Nov-2021 | oddpwdclemndvds 10259 | Lemma for oddpwdc 10262. 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 10258 | Lemma for oddpwdc 10262. 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 10255 | Lemma for pw2dvdseu 10256. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.) |
16-Nov-2021 | oddpwdclemdc 10261 | Lemma for oddpwdc 10262. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.) |
16-Nov-2021 | oddpwdclemodd 10260 | Lemma for oddpwdc 10262. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.) |
16-Nov-2021 | oddpwdclemxy 10257 | Lemma for oddpwdc 10262. 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 10256 | A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.) |
14-Nov-2021 | pw2dvds 10254 | A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.) |
14-Nov-2021 | pw2dvdslemn 10253 | Lemma for pw2dvds 10254. 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 10116 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
DECID | ||
11-Nov-2021 | fz01or 10190 | 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 7758 | Distribution of division over addition with a multiplication. (Contributed by Jim Kingdon, 11-Nov-2021.) |
# | ||
10-Nov-2021 | zeoxor 10180 | An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.) |
9-Nov-2021 | qlttri2 8673 | Apartness is equivalent to not equal for rationals. (Contributed by Jim Kingdon, 9-Nov-2021.) |
8-Nov-2021 | dvdslelemd 10155 | Lemma for dvdsle 10156. (Contributed by Jim Kingdon, 8-Nov-2021.) |
8-Nov-2021 | qabsord 9903 | 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 9902 | 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 9631 | Write out the top and bottom parts of the binomial coefficient explicitly. In this form, it is valid even for , although it is no longer valid for nonpositive . (Contributed by Jim Kingdon, 6-Nov-2021.) |
3-Nov-2021 | qavgle 9215 | 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 9591 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. See comments for nn0opthd 9590. (Contributed by Jim Kingdon, 31-Oct-2021.) |
31-Oct-2021 | nn0opthd 9590 | An ordered pair theorem for nonnegative integers. Theorem 17.3 of [Quine] p. 124. We can represent an ordered pair of nonnegative integers and by . If two such ordered pairs are equal, their first elements are equal and their second elements are equal. Contrast this ordered pair representation with the standard one df-op 3412 that works for any set. (Contributed by Jim Kingdon, 31-Oct-2021.) |
31-Oct-2021 | nn0opthlem2d 9589 | Lemma for nn0opth2 9592. (Contributed by Jim Kingdon, 31-Oct-2021.) |
31-Oct-2021 | nn0opthlem1d 9588 | A rather pretty lemma for nn0opth2 9592. (Contributed by Jim Kingdon, 31-Oct-2021.) |
31-Oct-2021 | nn0le2msqd 9587 | The square function on nonnegative integers is monotonic. (Contributed by Jim Kingdon, 31-Oct-2021.) |
28-Oct-2021 | mulle0r 7985 | Multiplying a nonnegative number by a nonpositive number yields a nonpositive number. (Contributed by Jim Kingdon, 28-Oct-2021.) |
26-Oct-2021 | modqeqmodmin 9344 | 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 9343 | Distribute the modulo operation over a subtraction. (Contributed by Jim Kingdon, 26-Oct-2021.) |
26-Oct-2021 | modqdi 9342 | Distribute multiplication over a modulo operation. (Contributed by Jim Kingdon, 26-Oct-2021.) |
26-Oct-2021 | modqaddmulmod 9341 | 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 9340 | 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 9339 | 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 9335 | 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 9334 | Two times a positive number modulo the number is zero. (Contributed by Jim Kingdon, 25-Oct-2021.) |
25-Oct-2021 | modqsubmodmod 9333 | 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 9332 | 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 9331 | Subtraction property of the modulo operation. (Contributed by Jim Kingdon, 25-Oct-2021.) |
25-Oct-2021 | modqadd12d 9330 | Additive property of the modulo operation. (Contributed by Jim Kingdon, 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 10501 | 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 10501 should be used in place of construction specific results. In particular, axcaucvg 7032 should be proved from it. (Contributed by BJ, 24-Oct-2021.) |
24-Oct-2021 | modqnegd 9329 | Negation property of the modulo operation. (Contributed by Jim Kingdon, 24-Oct-2021.) |
24-Oct-2021 | modqmul12d 9328 | 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 9327 | Multiplication property of the modulo operation. Note that the multiplier must be an integer. (Contributed by Jim Kingdon, 24-Oct-2021.) |
24-Oct-2021 | modqltm1p1mod 9326 | 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 9325 | 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 9324 | 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 9319 | 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 9318 | 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 9317 | 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 9316 | Decomposition of an integer into a multiple of a modulus and a remainder. (Contributed by Jim Kingdon, 23-Oct-2021.) |
23-Oct-2021 | mulqaddmodid 9314 | 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 9313 | 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 9312 | Absorption law for modulo. (Contributed by Jim Kingdon, 22-Oct-2021.) |
22-Oct-2021 | modqadd1 9311 | Addition property of the modulo operation. (Contributed by Jim Kingdon, 22-Oct-2021.) |
21-Oct-2021 | modqcyc2 9310 | The modulo operation is periodic. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqcyc 9309 | The modulo operation is periodic. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqabs2 9308 | Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqabs 9307 | Absorption law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | q1mod 9306 | Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | q0mod 9305 | Special case: 0 modulo a positive real number is 0. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqid2 9301 | Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqid0 9300 | A positive real number modulo itself is 0. (Contributed by Jim Kingdon, 21-Oct-2021.) |
21-Oct-2021 | modqid 9299 | Identity law for modulo. (Contributed by Jim Kingdon, 21-Oct-2021.) |
20-Oct-2021 | modqvalp1 9293 | The value of the modulo operation (expressed with sum of denominator and nominator). (Contributed by Jim Kingdon, 20-Oct-2021.) |
20-Oct-2021 | onunsnss 6386 | 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 . (Contributed by Jim Kingdon, 19-Oct-2021.) |
18-Oct-2021 | qdencn 10511 | 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 10029 (and also would hold for with the usual metric; this is not about complex numbers in particular). (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqmulnn 9292 | 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 9289 | Break a number into its integer part and its fractional part. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | flqmod 9288 | The floor function expressed in terms of the modulo operation. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqfrac 9287 | The fractional part of a number is the number modulo 1. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqdifz 9286 | The modulo operation differs from by an integer multiple of . (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqdiffl 9285 | The modulo operation differs from by an integer multiple of . (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqelico 9284 | Modular reduction produces a half-open interval. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqlt 9283 | The modulo operation is less than its second argument. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | modqge0 9282 | The modulo operation is nonnegative. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | negqmod0 9281 | is divisible by iff its negative is. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | mulqmod0 9280 | 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 9271 | Cancellation of the embedded floor of a real divided by an integer. (Contributed by Jim Kingdon, 18-Oct-2021.) |
18-Oct-2021 | intqfrac2 9269 | Decompose a real into integer and fractional parts. (Contributed by Jim Kingdon, 18-Oct-2021.) |
Copyright terms: Public domain | W3C HTML validation [external] |