Home | Intuitionistic Logic Explorer Theorem List (p. 115 of 132) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cos12dec 11401 | Cosine is decreasing from one to two. (Contributed by Mario Carneiro and Jim Kingdon, 6-Mar-2024.) |
Theorem | absefi 11402 | The absolute value of the exponential of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.) |
Theorem | absef 11403 | The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.) |
Theorem | absefib 11404 | A complex number is real iff the exponential of its product with has absolute value one. (Contributed by NM, 21-Aug-2008.) |
Theorem | efieq1re 11405 | A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.) |
Theorem | demoivre 11406 | De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 11407 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.) |
Theorem | demoivreALT 11407 | Alternate proof of demoivre 11406. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Syntax | ctau 11408 | Extend class notation to include the constant tau, = 6.28318.... |
Definition | df-tau 11409 | Define the circle constant tau, = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including , a three-legged variant of , or . Note the difference between this constant and the formula variable . Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.) |
inf | ||
Theorem | eirraplem 11410* | Lemma for eirrap 11411. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 5-Jan-2022.) |
# | ||
Theorem | eirrap 11411 | is irrational. That is, for any rational number, is apart from it. In the absence of excluded middle, we can distinguish between this and saying that is not rational, which is eirr 11412. (Contributed by Jim Kingdon, 6-Jan-2023.) |
# | ||
Theorem | eirr 11412 | is not rational. In the absence of excluded middle, we can distinguish between this and saying that is irrational in the sense of being apart from any rational number, which is eirrap 11411. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Jim Kingdon, 6-Jan-2023.) |
Theorem | egt2lt3 11413 | Euler's constant = 2.71828... is bounded by 2 and 3. (Contributed by NM, 28-Nov-2008.) (Revised by Jim Kingdon, 7-Jan-2023.) |
Theorem | epos 11414 | Euler's constant is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.) |
Theorem | epr 11415 | Euler's constant is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.) |
Theorem | ene0 11416 | is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.) |
Theorem | eap0 11417 | is apart from 0. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
Theorem | ene1 11418 | is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.) |
Theorem | eap1 11419 | is apart from 1. (Contributed by Jim Kingdon, 7-Jan-2023.) |
# | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Syntax | cdvds 11420 | Extend the definition of a class to include the divides relation. See df-dvds 11421. |
Definition | df-dvds 11421* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | divides 11422* | Define the divides relation. means divides into with no remainder. For example, (ex-dvds 12869). As proven in dvdsval3 11424, . See divides 11422 and dvdsval2 11423 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsval2 11423 | One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.) |
Theorem | dvdsval3 11424 | One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.) |
Theorem | dvdszrcl 11425 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Theorem | nndivdvds 11426 | Strong form of dvdsval2 11423 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
Theorem | nndivides 11427* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
Theorem | dvdsdc 11428 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
DECID | ||
Theorem | moddvds 11429 | Two ways to say (mod ), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
Theorem | dvds0lem 11430 | A lemma to assist theorems of with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds1lem 11431* | A lemma to assist theorems of with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2lem 11432* | A lemma to assist theorems of with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | iddvds 11433 | An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | 1dvds 11434 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds0 11435 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | negdvdsb 11436 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsnegb 11437 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | absdvdsb 11438 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsabsb 11439 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | 0dvds 11440 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | zdvdsdc 11441 | Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.) |
DECID | ||
Theorem | dvdsmul1 11442 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmul2 11443 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | iddvdsexp 11444 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | muldvds1 11445 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | muldvds2 11446 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdscmul 11447 | Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmulc 11448 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdscmulr 11449 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmulcr 11450 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | summodnegmod 11451 | 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.) |
Theorem | modmulconst 11452 | Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.) |
Theorem | dvds2ln 11453 | If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in [ApostolNT] p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2add 11454 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2sub 11455 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvds2subd 11456 | Natural deduction form of dvds2sub 11455. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | dvdstr 11457 | The divides relation is transitive. Theorem 1.1(b) in [ApostolNT] p. 14 (transitive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsmultr1 11458 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | dvdsmultr1d 11459 | Natural deduction form of dvdsmultr1 11458. (Contributed by Stanislas Polu, 9-Mar-2020.) |
Theorem | dvdsmultr2 11460 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | ordvdsmul 11461 | If an integer divides either of two others, it divides their product. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 17-Jul-2014.) |
Theorem | dvdssub2 11462 | If an integer divides a difference, then it divides one term iff it divides the other. (Contributed by Mario Carneiro, 13-Jul-2014.) |
Theorem | dvdsadd 11463 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 13-Jul-2014.) |
Theorem | dvdsaddr 11464 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdssub 11465 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdssubr 11466 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
Theorem | dvdsadd2b 11467 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
Theorem | dvdslelemd 11468 | Lemma for dvdsle 11469. (Contributed by Jim Kingdon, 8-Nov-2021.) |
Theorem | dvdsle 11469 | The divisors of a positive integer are bounded by it. The proof does not use . (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsleabs 11470 | The divisors of a nonzero integer are bounded by its absolute value. Theorem 1.1(i) in [ApostolNT] p. 14 (comparison property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
Theorem | dvdsleabs2 11471 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
Theorem | dvdsabseq 11472 | 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.) |
Theorem | dvdseq 11473 | 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.) |
Theorem | divconjdvds 11474 | If a nonzero integer divides another integer , the other integer divided by the nonzero integer (i.e. the divisor conjugate of to ) divides the other integer . Theorem 1.1(k) in [ApostolNT] p. 14. (Contributed by AV, 7-Aug-2021.) |
Theorem | dvdsdivcl 11475* | The complement of a divisor of is also a divisor of . (Contributed by Mario Carneiro, 2-Jul-2015.) (Proof shortened by AV, 9-Aug-2021.) |
Theorem | dvdsflip 11476* | An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.) |
Theorem | dvdsssfz1 11477* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
Theorem | dvds1 11478 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
Theorem | alzdvds 11479* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | dvdsext 11480* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Theorem | fzm1ndvds 11481 | No number between and divides . (Contributed by Mario Carneiro, 24-Jan-2015.) |
Theorem | fzo0dvdseq 11482 | Zero is the only one of the first nonnegative integers that is divisible by . (Contributed by Stefan O'Rear, 6-Sep-2015.) |
..^ | ||
Theorem | fzocongeq 11483 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
..^ ..^ | ||
Theorem | addmodlteqALT 11484 | 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 10139 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
..^ ..^ | ||
Theorem | dvdsfac 11485 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
Theorem | dvdsexp 11486 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
Theorem | dvdsmod 11487 | Any number whose mod base is divisible by a divisor of the base is also divisible by . This means that primes will also be relatively prime to the base when reduced for any base. (Contributed by Mario Carneiro, 13-Mar-2014.) |
Theorem | mulmoddvds 11488 | If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
Theorem | 3dvdsdec 11489 | 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 and actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers and , especially if is itself a decimal number, e.g. ;. (Contributed by AV, 14-Jun-2021.) (Revised by AV, 8-Sep-2021.) |
; | ||
Theorem | 3dvds2dec 11490 | 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 , and actually are digits (i.e. nonnegative integers less than 10). However, this theorem holds for arbitrary nonnegative integers , and . (Contributed by AV, 14-Jun-2021.) (Revised by AV, 1-Aug-2021.) |
;; | ||
The set of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 11494. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom to say that " is even" (which implies , see evenelz 11491) and to say that " is odd" (under the assumption that ). The previously proven theorems about even and odd numbers, like zneo 9120, zeo 9124, zeo2 9125, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 11513 and oddp1d2 11514. The corresponding theorems are zeneo 11495, zeo3 11492 and zeo4 11494. | ||
Theorem | evenelz 11491 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 11425. (Contributed by AV, 22-Jun-2021.) |
Theorem | zeo3 11492 | An integer is even or odd. (Contributed by AV, 17-Jun-2021.) |
Theorem | zeoxor 11493 | An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.) |
Theorem | zeo4 11494 | An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.) |
Theorem | zeneo 11495 | 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 9120 follows immediately from the fact that a contradiction implies anything, see pm2.21i 620. (Contributed by AV, 22-Jun-2021.) |
Theorem | odd2np1lem 11496* | Lemma for odd2np1 11497. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | odd2np1 11497* | An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
Theorem | even2n 11498* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
Theorem | oddm1even 11499 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
Theorem | oddp1even 11500 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |