![]() |
Intuitionistic Logic Explorer Theorem List (p. 119 of 150) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvdszrcl 11801 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข (๐ โฅ ๐ โ (๐ โ โค โง ๐ โ โค)) | ||
Theorem | dvdsmod0 11802 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
โข ((๐ โ โ โง ๐ โฅ ๐) โ (๐ mod ๐) = 0) | ||
Theorem | p1modz1 11803 | If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.) |
โข ((๐ โฅ ๐ด โง 1 < ๐) โ ((๐ด + 1) mod ๐) = 1) | ||
Theorem | dvdsmodexp 11804 | If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 12236). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
โข ((๐ โ โ โง ๐ต โ โ โง ๐ โฅ ๐ด) โ ((๐ดโ๐ต) mod ๐) = (๐ด mod ๐)) | ||
Theorem | nndivdvds 11805 | Strong form of dvdsval2 11799 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ต โฅ ๐ด โ (๐ด / ๐ต) โ โ)) | ||
Theorem | nndivides 11806* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
โข ((๐ โ โ โง ๐ โ โ) โ (๐ โฅ ๐ โ โ๐ โ โ (๐ ยท ๐) = ๐)) | ||
Theorem | dvdsdc 11807 | Divisibility is decidable. (Contributed by Jim Kingdon, 14-Nov-2021.) |
โข ((๐ โ โ โง ๐ โ โค) โ DECID ๐ โฅ ๐) | ||
Theorem | moddvds 11808 | Two ways to say ๐ดโก๐ต (mod ๐), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ๐ โฅ (๐ด โ ๐ต))) | ||
Theorem | modm1div 11809 | An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.) |
โข ((๐ โ (โคโฅโ2) โง ๐ด โ โค) โ ((๐ด mod ๐) = 1 โ ๐ โฅ (๐ด โ 1))) | ||
Theorem | dvds0lem 11810 | A lemma to assist theorems of โฅ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โง (๐พ ยท ๐) = ๐) โ ๐ โฅ ๐) | ||
Theorem | dvds1lem 11811* | A lemma to assist theorems of โฅ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ (๐ฝ โ โค โง ๐พ โ โค)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข ((๐ โง ๐ฅ โ โค) โ ๐ โ โค) & โข ((๐ โง ๐ฅ โ โค) โ ((๐ฅ ยท ๐ฝ) = ๐พ โ (๐ ยท ๐) = ๐)) โ โข (๐ โ (๐ฝ โฅ ๐พ โ ๐ โฅ ๐)) | ||
Theorem | dvds2lem 11812* | A lemma to assist theorems of โฅ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ (๐ผ โ โค โง ๐ฝ โ โค)) & โข (๐ โ (๐พ โ โค โง ๐ฟ โ โค)) & โข (๐ โ (๐ โ โค โง ๐ โ โค)) & โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ ๐ โ โค) & โข ((๐ โง (๐ฅ โ โค โง ๐ฆ โ โค)) โ (((๐ฅ ยท ๐ผ) = ๐ฝ โง (๐ฆ ยท ๐พ) = ๐ฟ) โ (๐ ยท ๐) = ๐)) โ โข (๐ โ ((๐ผ โฅ ๐ฝ โง ๐พ โฅ ๐ฟ) โ ๐ โฅ ๐)) | ||
Theorem | iddvds 11813 | 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 11814 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ 1 โฅ ๐) | ||
Theorem | dvds0 11815 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ ๐ โฅ 0) | ||
Theorem | negdvdsb 11816 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ -๐ โฅ ๐)) | ||
Theorem | dvdsnegb 11817 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ -๐)) | ||
Theorem | absdvdsb 11818 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ (absโ๐) โฅ ๐)) | ||
Theorem | dvdsabsb 11819 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (absโ๐))) | ||
Theorem | 0dvds 11820 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ (0 โฅ ๐ โ ๐ = 0)) | ||
Theorem | zdvdsdc 11821 | Divisibility of integers is decidable. (Contributed by Jim Kingdon, 17-Jan-2022.) |
โข ((๐ โ โค โง ๐ โ โค) โ DECID ๐ โฅ ๐) | ||
Theorem | dvdsmul1 11822 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) | ||
Theorem | dvdsmul2 11823 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ ๐ โฅ (๐ ยท ๐)) | ||
Theorem | iddvdsexp 11824 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
โข ((๐ โ โค โง ๐ โ โ) โ ๐ โฅ (๐โ๐)) | ||
Theorem | muldvds1 11825 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐พ โฅ ๐)) | ||
Theorem | muldvds2 11826 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ ยท ๐) โฅ ๐ โ ๐ โฅ ๐)) | ||
Theorem | dvdscmul 11827 | 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 11828 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐พ โ โค) โ (๐ โฅ ๐ โ (๐ ยท ๐พ) โฅ (๐ ยท ๐พ))) | ||
Theorem | dvdscmulr 11829 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐พ ยท ๐) โฅ (๐พ ยท ๐) โ ๐ โฅ ๐)) | ||
Theorem | dvdsmulcr 11830 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค โง (๐พ โ โค โง ๐พ โ 0)) โ ((๐ ยท ๐พ) โฅ (๐ ยท ๐พ) โ ๐ โฅ ๐)) | ||
Theorem | summodnegmod 11831 | 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.) |
โข ((๐ด โ โค โง ๐ต โ โค โง ๐ โ โ) โ (((๐ด + ๐ต) mod ๐) = 0 โ (๐ด mod ๐) = (-๐ต mod ๐))) | ||
Theorem | modmulconst 11832 | Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.) |
โข (((๐ด โ โค โง ๐ต โ โค โง ๐ถ โ โ) โง ๐ โ โ) โ ((๐ด mod ๐) = (๐ต mod ๐) โ ((๐ถ ยท ๐ด) mod (๐ถ ยท ๐)) = ((๐ถ ยท ๐ต) mod (๐ถ ยท ๐)))) | ||
Theorem | dvds2ln 11833 | 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 11834 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ + ๐))) | ||
Theorem | dvds2sub 11835 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ ((๐พ โฅ ๐ โง ๐พ โฅ ๐) โ ๐พ โฅ (๐ โ ๐))) | ||
Theorem | dvds2subd 11836 | Deduction form of dvds2sub 11835. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ โ ๐)) | ||
Theorem | dvdstr 11837 | 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 | dvds2addd 11838 | Deduction form of dvds2add 11834. (Contributed by SN, 21-Aug-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ + ๐)) | ||
Theorem | dvdstrd 11839 | The divides relation is transitive, a deduction version of dvdstr 11837. (Contributed by metakunt, 12-May-2024.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) & โข (๐ โ ๐ โฅ ๐) โ โข (๐ โ ๐พ โฅ ๐) | ||
Theorem | dvdsmultr1 11840 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | dvdsmultr1d 11841 | Natural deduction form of dvdsmultr1 11840. (Contributed by Stanislas Polu, 9-Mar-2020.) |
โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐พ โฅ ๐) โ โข (๐ โ ๐พ โฅ (๐ ยท ๐)) | ||
Theorem | dvdsmultr2 11842 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข ((๐พ โ โค โง ๐ โ โค โง ๐ โ โค) โ (๐พ โฅ ๐ โ ๐พ โฅ (๐ ยท ๐))) | ||
Theorem | ordvdsmul 11843 | 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 11844 | 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 11845 | 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 11846 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ + ๐))) | ||
Theorem | dvdssub 11847 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ โ ๐))) | ||
Theorem | dvdssubr 11848 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โค) โ (๐ โฅ ๐ โ ๐ โฅ (๐ โ ๐))) | ||
Theorem | dvdsadd2b 11849 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
โข ((๐ด โ โค โง ๐ต โ โค โง (๐ถ โ โค โง ๐ด โฅ ๐ถ)) โ (๐ด โฅ ๐ต โ ๐ด โฅ (๐ถ + ๐ต))) | ||
Theorem | dvdsaddre2b 11850 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 11849 only requiring ๐ต to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต โ โ โง (๐ถ โ โค โง ๐ด โฅ ๐ถ)) โ (๐ด โฅ ๐ต โ ๐ด โฅ (๐ถ + ๐ต))) | ||
Theorem | dvdslelemd 11851 | Lemma for dvdsle 11852. (Contributed by Jim Kingdon, 8-Nov-2021.) |
โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐พ โ โค) & โข (๐ โ ๐ < ๐) โ โข (๐ โ (๐พ ยท ๐) โ ๐) | ||
Theorem | dvdsle 11852 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข ((๐ โ โค โง ๐ โ โ) โ (๐ โฅ ๐ โ ๐ โค ๐)) | ||
Theorem | dvdsleabs 11853 | 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.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โฅ ๐ โ ๐ โค (absโ๐))) | ||
Theorem | dvdsleabs2 11854 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
โข ((๐ โ โค โง ๐ โ โค โง ๐ โ 0) โ (๐ โฅ ๐ โ (absโ๐) โค (absโ๐))) | ||
Theorem | dvdsabseq 11855 | 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.) |
โข ((๐ โฅ ๐ โง ๐ โฅ ๐) โ (absโ๐) = (absโ๐)) | ||
Theorem | dvdseq 11856 | 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.) |
โข (((๐ โ โ0 โง ๐ โ โ0) โง (๐ โฅ ๐ โง ๐ โฅ ๐)) โ ๐ = ๐) | ||
Theorem | divconjdvds 11857 | 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.) |
โข ((๐ โฅ ๐ โง ๐ โ 0) โ (๐ / ๐) โฅ ๐) | ||
Theorem | dvdsdivcl 11858* | 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 11859* | An involution of the divisors of a number. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by Mario Carneiro, 13-May-2016.) |
โข ๐ด = {๐ฅ โ โ โฃ ๐ฅ โฅ ๐} & โข ๐น = (๐ฆ โ ๐ด โฆ (๐ / ๐ฆ)) โ โข (๐ โ โ โ ๐น:๐ดโ1-1-ontoโ๐ด) | ||
Theorem | dvdsssfz1 11860* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
โข (๐ด โ โ โ {๐ โ โ โฃ ๐ โฅ ๐ด} โ (1...๐ด)) | ||
Theorem | dvds1 11861 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
โข (๐ โ โ0 โ (๐ โฅ 1 โ ๐ = 1)) | ||
Theorem | alzdvds 11862* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ โ โค โ (โ๐ฅ โ โค ๐ฅ โฅ ๐ โ ๐ = 0)) | ||
Theorem | dvdsext 11863* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ โ0 โง ๐ต โ โ0) โ (๐ด = ๐ต โ โ๐ฅ โ โ0 (๐ด โฅ ๐ฅ โ ๐ต โฅ ๐ฅ))) | ||
Theorem | fzm1ndvds 11864 | No number between 1 and ๐ โ 1 divides ๐. (Contributed by Mario Carneiro, 24-Jan-2015.) |
โข ((๐ โ โ โง ๐ โ (1...(๐ โ 1))) โ ยฌ ๐ โฅ ๐) | ||
Theorem | fzo0dvdseq 11865 | Zero is the only one of the first ๐ด nonnegative integers that is divisible by ๐ด. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข (๐ต โ (0..^๐ด) โ (๐ด โฅ ๐ต โ ๐ต = 0)) | ||
Theorem | fzocongeq 11866 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ((๐ด โ (๐ถ..^๐ท) โง ๐ต โ (๐ถ..^๐ท)) โ ((๐ท โ ๐ถ) โฅ (๐ด โ ๐ต) โ ๐ด = ๐ต)) | ||
Theorem | addmodlteqALT 11867 | 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 10400 based on the "divides" relation. (Contributed by AV, 14-Mar-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ((๐ผ โ (0..^๐) โง ๐ฝ โ (0..^๐) โง ๐ โ โค) โ (((๐ผ + ๐) mod ๐) = ((๐ฝ + ๐) mod ๐) โ ๐ผ = ๐ฝ)) | ||
Theorem | dvdsfac 11868 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
โข ((๐พ โ โ โง ๐ โ (โคโฅโ๐พ)) โ ๐พ โฅ (!โ๐)) | ||
Theorem | dvdsexp 11869 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
โข ((๐ด โ โค โง ๐ โ โ0 โง ๐ โ (โคโฅโ๐)) โ (๐ดโ๐) โฅ (๐ดโ๐)) | ||
Theorem | dvdsmod 11870 | 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 mod ๐ for any base. (Contributed by Mario Carneiro, 13-Mar-2014.) |
โข (((๐ โ โ โง ๐ โ โ โง ๐พ โ โค) โง ๐ โฅ ๐) โ (๐ โฅ (๐พ mod ๐) โ ๐ โฅ ๐พ)) | ||
Theorem | mulmoddvds 11871 | 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.) |
โข ((๐ โ โ โง ๐ด โ โค โง ๐ต โ โค) โ (๐ โฅ ๐ด โ ((๐ด ยท ๐ต) mod ๐) = 0)) | ||
Theorem | 3dvdsdec 11872 | 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.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 โ โข (3 โฅ ;๐ด๐ต โ 3 โฅ (๐ด + ๐ต)) | ||
Theorem | 3dvds2dec 11873 | 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.) |
โข ๐ด โ โ0 & โข ๐ต โ โ0 & โข ๐ถ โ โ0 โ โข (3 โฅ ;;๐ด๐ต๐ถ โ 3 โฅ ((๐ด + ๐ต) + ๐ถ)) | ||
The set โค of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 11877. Instead of defining new class variables Even and Odd to represent these sets, we use the idiom 2 โฅ ๐ to say that "๐ is even" (which implies ๐ โ โค, see evenelz 11874) and ยฌ 2 โฅ ๐ to say that "๐ is odd" (under the assumption that ๐ โ โค). The previously proven theorems about even and odd numbers, like zneo 9356, zeo 9360, zeo2 9361, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 11896 and oddp1d2 11897. The corresponding theorems are zeneo 11878, zeo3 11875 and zeo4 11877. | ||
Theorem | evenelz 11874 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 11801. (Contributed by AV, 22-Jun-2021.) |
โข (2 โฅ ๐ โ ๐ โ โค) | ||
Theorem | zeo3 11875 | An integer is even or odd. (Contributed by AV, 17-Jun-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โจ ยฌ 2 โฅ ๐)) | ||
Theorem | zeoxor 11876 | An integer is even or odd but not both. (Contributed by Jim Kingdon, 10-Nov-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โป ยฌ 2 โฅ ๐)) | ||
Theorem | zeo4 11877 | An integer is even or odd but not both. (Contributed by AV, 17-Jun-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โ ยฌ ยฌ 2 โฅ ๐)) | ||
Theorem | zeneo 11878 | 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 9356 follows immediately from the fact that a contradiction implies anything, see pm2.21i 646. (Contributed by AV, 22-Jun-2021.) |
โข ((๐ด โ โค โง ๐ต โ โค) โ ((2 โฅ ๐ด โง ยฌ 2 โฅ ๐ต) โ ๐ด โ ๐ต)) | ||
Theorem | odd2np1lem 11879* | Lemma for odd2np1 11880. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
โข (๐ โ โ0 โ (โ๐ โ โค ((2 ยท ๐) + 1) = ๐ โจ โ๐ โ โค (๐ ยท 2) = ๐)) | ||
Theorem | odd2np1 11880* | 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.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ โ๐ โ โค ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | even2n 11881* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
โข (2 โฅ ๐ โ โ๐ โ โค (2 ยท ๐) = ๐) | ||
Theorem | oddm1even 11882 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ โ 1))) | ||
Theorem | oddp1even 11883 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ 2 โฅ (๐ + 1))) | ||
Theorem | oexpneg 11884 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) |
โข ((๐ด โ โ โง ๐ โ โ โง ยฌ 2 โฅ ๐) โ (-๐ดโ๐) = -(๐ดโ๐)) | ||
Theorem | mod2eq0even 11885 | 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.) |
โข (๐ โ โค โ ((๐ mod 2) = 0 โ 2 โฅ ๐)) | ||
Theorem | mod2eq1n2dvds 11886 | 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.) |
โข (๐ โ โค โ ((๐ mod 2) = 1 โ ยฌ 2 โฅ ๐)) | ||
Theorem | oddnn02np1 11887* | A nonnegative integer is odd iff it is one plus twice another nonnegative integer. (Contributed by AV, 19-Jun-2021.) |
โข (๐ โ โ0 โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ0 ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | oddge22np1 11888* | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) |
โข (๐ โ (โคโฅโ2) โ (ยฌ 2 โฅ ๐ โ โ๐ โ โ ((2 ยท ๐) + 1) = ๐)) | ||
Theorem | evennn02n 11889* | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) |
โข (๐ โ โ0 โ (2 โฅ ๐ โ โ๐ โ โ0 (2 ยท ๐) = ๐)) | ||
Theorem | evennn2n 11890* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
โข (๐ โ โ โ (2 โฅ ๐ โ โ๐ โ โ (2 ยท ๐) = ๐)) | ||
Theorem | 2tp1odd 11891 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต = ((2 ยท ๐ด) + 1)) โ ยฌ 2 โฅ ๐ต) | ||
Theorem | mulsucdiv2z 11892 | 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.) |
โข (๐ โ โค โ ((๐ ยท (๐ + 1)) / 2) โ โค) | ||
Theorem | sqoddm1div8z 11893 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐) โ (((๐โ2) โ 1) / 8) โ โค) | ||
Theorem | 2teven 11894 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
โข ((๐ด โ โค โง ๐ต = (2 ยท ๐ด)) โ 2 โฅ ๐ต) | ||
Theorem | zeo5 11895 | An integer is either even or odd, version of zeo3 11875 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020.) |
โข (๐ โ โค โ (2 โฅ ๐ โจ 2 โฅ (๐ + 1))) | ||
Theorem | evend2 11896 | 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 9360 and zeo2 9361. (Contributed by AV, 22-Jun-2021.) |
โข (๐ โ โค โ (2 โฅ ๐ โ (๐ / 2) โ โค)) | ||
Theorem | oddp1d2 11897 | 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 9360 and zeo2 9361. (Contributed by AV, 22-Jun-2021.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ ((๐ + 1) / 2) โ โค)) | ||
Theorem | zob 11898 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
โข (๐ โ โค โ (((๐ + 1) / 2) โ โค โ ((๐ โ 1) / 2) โ โค)) | ||
Theorem | oddm1d2 11899 | 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.) |
โข (๐ โ โค โ (ยฌ 2 โฅ ๐ โ ((๐ โ 1) / 2) โ โค)) | ||
Theorem | ltoddhalfle 11900 | 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.) |
โข ((๐ โ โค โง ยฌ 2 โฅ ๐ โง ๐ โ โค) โ (๐ < (๐ / 2) โ ๐ โค ((๐ โ 1) / 2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |