![]() |
Metamath
Proof Explorer Theorem List (p. 163 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ruclem3 16201* | Lemma for ruc 16211. The constructed interval [π, π] always excludes π. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) & β’ (π β π΄ < π΅) β β’ (π β (π < π β¨ π < π)) | ||
Theorem | ruclem4 16202* | Lemma for ruc 16211. Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) β β’ (π β (πΊβ0) = β¨0, 1β©) | ||
Theorem | ruclem6 16203* | Lemma for ruc 16211. Domain and codomain of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) β β’ (π β πΊ:β0βΆ(β Γ β)) | ||
Theorem | ruclem7 16204* | Lemma for ruc 16211. Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) β β’ ((π β§ π β β0) β (πΊβ(π + 1)) = ((πΊβπ)π·(πΉβ(π + 1)))) | ||
Theorem | ruclem8 16205* | Lemma for ruc 16211. The intervals of the πΊ sequence are all nonempty. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) β β’ ((π β§ π β β0) β (1st β(πΊβπ)) < (2nd β(πΊβπ))) | ||
Theorem | ruclem9 16206* | Lemma for ruc 16211. The first components of the πΊ sequence are increasing, and the second components are decreasing. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) & β’ (π β π β β0) & β’ (π β π β (β€β₯βπ)) β β’ (π β ((1st β(πΊβπ)) β€ (1st β(πΊβπ)) β§ (2nd β(πΊβπ)) β€ (2nd β(πΊβπ)))) | ||
Theorem | ruclem10 16207* | Lemma for ruc 16211. Every first component of the πΊ sequence is less than every second component. That is, the sequences form a chain a1 < a2 <... < b2 < b1, where ai are the first components and bi are the second components. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) & β’ (π β π β β0) & β’ (π β π β β0) β β’ (π β (1st β(πΊβπ)) < (2nd β(πΊβπ))) | ||
Theorem | ruclem11 16208* | Lemma for ruc 16211. Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) β β’ (π β (ran (1st β πΊ) β β β§ ran (1st β πΊ) β β β§ βπ§ β ran (1st β πΊ)π§ β€ 1)) | ||
Theorem | ruclem12 16209* | Lemma for ruc 16211. The supremum of the increasing sequence 1st β πΊ is a real number that is not in the range of πΉ. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ πΆ = ({β¨0, β¨0, 1β©β©} βͺ πΉ) & β’ πΊ = seq0(π·, πΆ) & β’ π = sup(ran (1st β πΊ), β, < ) β β’ (π β π β (β β ran πΉ)) | ||
Theorem | ruclem13 16210 | Lemma for ruc 16211. There is no function that maps β onto β. (Use nex 1795 if you want this in the form Β¬ βππ:ββontoββ.) (Contributed by NM, 14-Oct-2004.) (Proof shortened by Fan Zheng, 6-Jun-2016.) |
β’ Β¬ πΉ:ββontoββ | ||
Theorem | ruc 16211 | The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 16199 through ruclem13 16210 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 16210 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 16210. For an alternate proof see rucALT 16198. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.) |
β’ β βΊ β | ||
Theorem | resdomq 16212 | The set of rationals is strictly less equinumerous than the set of reals (β strictly dominates β). (Contributed by NM, 18-Dec-2004.) |
β’ β βΊ β | ||
Theorem | aleph1re 16213 | There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ β | ||
Theorem | aleph1irr 16214 | There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ (β β β) | ||
Theorem | cnso 16215 | The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014.) |
β’ βπ₯ π₯ Or β | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Theorem | sqrt2irrlem 16216 | Lemma for sqrt2irr 16217. This is the core of the proof: if π΄ / π΅ = β(2), then π΄ and π΅ are even, so π΄ / 2 and π΅ / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). This is Metamath 100 proof #1. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) (Proof shortened by JV, 4-Jan-2022.) |
β’ (π β π΄ β β€) & β’ (π β π΅ β β) & β’ (π β (ββ2) = (π΄ / π΅)) β β’ (π β ((π΄ / 2) β β€ β§ (π΅ / 2) β β)) | ||
Theorem | sqrt2irr 16217 | The square root of 2 is irrational. See zsqrtelqelz 16721 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 16216, which shows that if π΄ / π΅ = β(2), then π΄ and π΅ are even, so π΄ / 2 and π΅ / 2 are smaller representatives, which is absurd. An older version of this proof was included in The Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ 16216. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ (ββ2) β β | ||
Theorem | sqrt2re 16218 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
β’ (ββ2) β β | ||
Theorem | sqrt2irr0 16219 | The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022.) |
β’ (ββ2) β (β β β) | ||
Theorem | nthruc 16220 | The sequence β, β€, β, β, and β forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to β€ but not β, one-half belongs to β but not β€, the square root of 2 belongs to β but not β, and finally that the imaginary number i belongs to β but not β. See nthruz 16221 for a further refinement. (Contributed by NM, 12-Jan-2002.) |
β’ ((β β β€ β§ β€ β β) β§ (β β β β§ β β β)) | ||
Theorem | nthruz 16221 | The sequence β, β0, and β€ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to β0 but not β and minus one belongs to β€ but not β0. This theorem refines the chain of proper subsets nthruc 16220. (Contributed by NM, 9-May-2004.) |
β’ (β β β0 β§ β0 β β€) | ||
Syntax | cdvds 16222 | Extend the definition of a class to include the divides relation. See df-dvds 16223. |
class β₯ | ||
Definition | df-dvds 16223* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ β₯ = {β¨π₯, π¦β© β£ ((π₯ β β€ β§ π¦ β β€) β§ βπ β β€ (π Β· π₯) = π¦)} | ||
Theorem | divides 16224* | Define the divides relation. π β₯ π means π divides into π with no remainder. For example, 3 β₯ 6 (ex-dvds 30253). As proven in dvdsval3 16226, π β₯ π β (π mod π) = 0. See divides 16224 and dvdsval2 16225 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β βπ β β€ (π Β· π) = π)) | ||
Theorem | dvdsval2 16225 | One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.) |
β’ ((π β β€ β§ π β 0 β§ π β β€) β (π β₯ π β (π / π) β β€)) | ||
Theorem | dvdsval3 16226 | 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.) |
β’ ((π β β β§ π β β€) β (π β₯ π β (π mod π) = 0)) | ||
Theorem | dvdszrcl 16227 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ (π β₯ π β (π β β€ β§ π β β€)) | ||
Theorem | dvdsmod0 16228 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
β’ ((π β β β§ π β₯ π) β (π mod π) = 0) | ||
Theorem | p1modz1 16229 | 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 16230 | 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 16744). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
β’ ((π β β β§ π΅ β β β§ π β₯ π΄) β ((π΄βπ΅) mod π) = (π΄ mod π)) | ||
Theorem | nndivdvds 16231 | Strong form of dvdsval2 16225 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΅ β₯ π΄ β (π΄ / π΅) β β)) | ||
Theorem | nndivides 16232* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
β’ ((π β β β§ π β β) β (π β₯ π β βπ β β (π Β· π) = π)) | ||
Theorem | moddvds 16233 | Two ways to say π΄β‘π΅ (mod π), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ π΅ β β€) β ((π΄ mod π) = (π΅ mod π) β π β₯ (π΄ β π΅))) | ||
Theorem | modm1div 16234 | 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 16235 | A lemma to assist theorems of β₯ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ (πΎ Β· π) = π) β π β₯ π) | ||
Theorem | dvds1lem 16236* | A lemma to assist theorems of β₯ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (π½ β β€ β§ πΎ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ π₯ β β€) β π β β€) & β’ ((π β§ π₯ β β€) β ((π₯ Β· π½) = πΎ β (π Β· π) = π)) β β’ (π β (π½ β₯ πΎ β π β₯ π)) | ||
Theorem | dvds2lem 16237* | A lemma to assist theorems of β₯ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (πΌ β β€ β§ π½ β β€)) & β’ (π β (πΎ β β€ β§ πΏ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β π β β€) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β (((π₯ Β· πΌ) = π½ β§ (π¦ Β· πΎ) = πΏ) β (π Β· π) = π)) β β’ (π β ((πΌ β₯ π½ β§ πΎ β₯ πΏ) β π β₯ π)) | ||
Theorem | iddvds 16238 | 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 16239 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β 1 β₯ π) | ||
Theorem | dvds0 16240 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β π β₯ 0) | ||
Theorem | negdvdsb 16241 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β -π β₯ π)) | ||
Theorem | dvdsnegb 16242 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ -π)) | ||
Theorem | absdvdsb 16243 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ π)) | ||
Theorem | dvdsabsb 16244 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (absβπ))) | ||
Theorem | 0dvds 16245 | Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β (0 β₯ π β π = 0)) | ||
Theorem | dvdsmul1 16246 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | dvdsmul2 16247 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | iddvdsexp 16248 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β β€ β§ π β β) β π β₯ (πβπ)) | ||
Theorem | muldvds1 16249 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β πΎ β₯ π)) | ||
Theorem | muldvds2 16250 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β π β₯ π)) | ||
Theorem | dvdscmul 16251 | 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 16252 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (π β₯ π β (π Β· πΎ) β₯ (π Β· πΎ))) | ||
Theorem | dvdscmulr 16253 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ (πΎ β β€ β§ πΎ β 0)) β ((πΎ Β· π) β₯ (πΎ Β· π) β π β₯ π)) | ||
Theorem | dvdsmulcr 16254 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ (πΎ β β€ β§ πΎ β 0)) β ((π Β· πΎ) β₯ (π Β· πΎ) β π β₯ π)) | ||
Theorem | summodnegmod 16255 | 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 16256 | 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 16257 | 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 16258 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π + π))) | ||
Theorem | dvds2sub 16259 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π β π))) | ||
Theorem | dvds2addd 16260 | Deduction form of dvds2add 16258. (Contributed by SN, 21-Aug-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π + π)) | ||
Theorem | dvds2subd 16261 | Deduction form of dvds2sub 16259. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π β π)) | ||
Theorem | dvdstr 16262 | 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 | dvdstrd 16263 | The divides relation is transitive, a deduction version of dvdstr 16262. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β π β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | dvdsmultr1 16264 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β₯ π β πΎ β₯ (π Β· π))) | ||
Theorem | dvdsmultr1d 16265 | Deduction form of dvdsmultr1 16264. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π Β· π)) | ||
Theorem | dvdsmultr2 16266 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β₯ π β πΎ β₯ (π Β· π))) | ||
Theorem | dvdsmultr2d 16267 | Deduction form of dvdsmultr2 16266. (Contributed by SN, 23-Aug-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π Β· π)) | ||
Theorem | ordvdsmul 16268 | 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 16269 | 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 16270 | 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 16271 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π + π))) | ||
Theorem | dvdssub 16272 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π β π))) | ||
Theorem | dvdssubr 16273 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π β π))) | ||
Theorem | dvdsadd2b 16274 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ (πΆ β β€ β§ π΄ β₯ πΆ)) β (π΄ β₯ π΅ β π΄ β₯ (πΆ + π΅))) | ||
Theorem | dvdsaddre2b 16275 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 16274 only requiring π΅ to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β β§ (πΆ β β€ β§ π΄ β₯ πΆ)) β (π΄ β₯ π΅ β π΄ β₯ (πΆ + π΅))) | ||
Theorem | fsumdvds 16276* | If every term in a sum is divisible by π, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
β’ (π β π΄ β Fin) & β’ (π β π β β€) & β’ ((π β§ π β π΄) β π΅ β β€) & β’ ((π β§ π β π΄) β π β₯ π΅) β β’ (π β π β₯ Ξ£π β π΄ π΅) | ||
Theorem | dvdslelem 16277 | Lemma for dvdsle 16278. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π β β & β’ πΎ β β€ β β’ (π < π β (πΎ Β· π) β π) | ||
Theorem | dvdsle 16278 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β) β (π β₯ π β π β€ π)) | ||
Theorem | dvdsleabs 16279 | 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 16280 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π β₯ π β (absβπ) β€ (absβπ))) | ||
Theorem | dvdsabseq 16281 | 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 16282 | 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 16283 | 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 16284* | 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 16285* | 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 16286* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ (π΄ β β β {π β β β£ π β₯ π΄} β (1...π΄)) | ||
Theorem | dvds1 16287 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
β’ (π β β0 β (π β₯ 1 β π = 1)) | ||
Theorem | alzdvds 16288* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β (βπ₯ β β€ π₯ β₯ π β π = 0)) | ||
Theorem | dvdsext 16289* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ = π΅ β βπ₯ β β0 (π΄ β₯ π₯ β π΅ β₯ π₯))) | ||
Theorem | fzm1ndvds 16290 | No number between 1 and π β 1 divides π. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ ((π β β β§ π β (1...(π β 1))) β Β¬ π β₯ π) | ||
Theorem | fzo0dvdseq 16291 | 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 16292 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΄ β (πΆ..^π·) β§ π΅ β (πΆ..^π·)) β ((π· β πΆ) β₯ (π΄ β π΅) β π΄ = π΅)) | ||
Theorem | addmodlteqALT 16293 | 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 13935 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 16294 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ ((πΎ β β β§ π β (β€β₯βπΎ)) β πΎ β₯ (!βπ)) | ||
Theorem | dvdsexp2im 16295 | If an integer divides another integer, then it also divides any of its powers. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β) β (πΎ β₯ π β πΎ β₯ (πβπ))) | ||
Theorem | dvdsexp 16296 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π΄ β β€ β§ π β β0 β§ π β (β€β₯βπ)) β (π΄βπ) β₯ (π΄βπ)) | ||
Theorem | dvdsmod 16297 | 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 16298 | 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.) (Proof shortened by AV, 18-Mar-2022.) |
β’ ((π β β β§ π΄ β β€ β§ π΅ β β€) β (π β₯ π΄ β ((π΄ Β· π΅) mod π) = 0)) | ||
Theorem | 3dvds 16299* | A rule for divisibility by 3 of a number written in base 10. This is Metamath 100 proof #85. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Revised by AV, 8-Sep-2021.) |
β’ ((π β β0 β§ πΉ:(0...π)βΆβ€) β (3 β₯ Ξ£π β (0...π)((πΉβπ) Β· (;10βπ)) β 3 β₯ Ξ£π β (0...π)(πΉβπ))) | ||
Theorem | 3dvdsdec 16300 | 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 β₯ (π΄ + π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |