![]() |
Metamath
Proof Explorer Theorem List (p. 163 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rucALT 16201 | Alternate proof of ruc 16214. This proof is a simple corollary of rpnnen 16198, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable 16198, see ruc 16214. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β βΊ β | ||
Theorem | ruclem1 16202* | Lemma for ruc 16214 (the reals are uncountable). Substitutions for the function π·. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Fan Zheng, 6-Jun-2016.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) β β’ (π β ((β¨π΄, π΅β©π·π) β (β Γ β) β§ π = if(((π΄ + π΅) / 2) < π, π΄, ((((π΄ + π΅) / 2) + π΅) / 2)) β§ π = if(((π΄ + π΅) / 2) < π, ((π΄ + π΅) / 2), π΅))) | ||
Theorem | ruclem2 16203* | Lemma for ruc 16214. Ordering property for the input to π·. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) & β’ (π β π΄ < π΅) β β’ (π β (π΄ β€ π β§ π < π β§ π β€ π΅)) | ||
Theorem | ruclem3 16204* | Lemma for ruc 16214. The constructed interval [π, π] always excludes π. (Contributed by Mario Carneiro, 28-May-2014.) |
β’ (π β πΉ:ββΆβ) & β’ (π β π· = (π₯ β (β Γ β), π¦ β β β¦ β¦(((1st βπ₯) + (2nd βπ₯)) / 2) / πβ¦if(π < π¦, β¨(1st βπ₯), πβ©, β¨((π + (2nd βπ₯)) / 2), (2nd βπ₯)β©))) & β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β π β β) & β’ π = (1st β(β¨π΄, π΅β©π·π)) & β’ π = (2nd β(β¨π΄, π΅β©π·π)) & β’ (π β π΄ < π΅) β β’ (π β (π < π β¨ π < π)) | ||
Theorem | ruclem4 16205* | Lemma for ruc 16214. 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 16206* | Lemma for ruc 16214. 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 16207* | Lemma for ruc 16214. 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 16208* | Lemma for ruc 16214. 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 16209* | Lemma for ruc 16214. 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 16210* | Lemma for ruc 16214. 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 16211* | Lemma for ruc 16214. 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 16212* | Lemma for ruc 16214. 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 16213 | Lemma for ruc 16214. There is no function that maps β onto β. (Use nex 1794 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 16214 | 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 16202 through ruclem13 16213 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 16213 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 16213. For an alternate proof see rucALT 16201. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.) |
β’ β βΊ β | ||
Theorem | resdomq 16215 | The set of rationals is strictly less equinumerous than the set of reals (β strictly dominates β). (Contributed by NM, 18-Dec-2004.) |
β’ β βΊ β | ||
Theorem | aleph1re 16216 | There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ β | ||
Theorem | aleph1irr 16217 | There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.) |
β’ (β΅β1o) βΌ (β β β) | ||
Theorem | cnso 16218 | 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 16219 | Lemma for sqrt2irr 16220. 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 16220 | The square root of 2 is irrational. See zsqrtelqelz 16724 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 16219, 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/ 16219. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ (ββ2) β β | ||
Theorem | sqrt2re 16221 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
β’ (ββ2) β β | ||
Theorem | sqrt2irr0 16222 | The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022.) |
β’ (ββ2) β (β β β) | ||
Theorem | nthruc 16223 | 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 16224 for a further refinement. (Contributed by NM, 12-Jan-2002.) |
β’ ((β β β€ β§ β€ β β) β§ (β β β β§ β β β)) | ||
Theorem | nthruz 16224 | 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 16223. (Contributed by NM, 9-May-2004.) |
β’ (β β β0 β§ β0 β β€) | ||
Syntax | cdvds 16225 | Extend the definition of a class to include the divides relation. See df-dvds 16226. |
class β₯ | ||
Definition | df-dvds 16226* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ β₯ = {β¨π₯, π¦β© β£ ((π₯ β β€ β§ π¦ β β€) β§ βπ β β€ (π Β· π₯) = π¦)} | ||
Theorem | divides 16227* | Define the divides relation. π β₯ π means π divides into π with no remainder. For example, 3 β₯ 6 (ex-dvds 30305). As proven in dvdsval3 16229, π β₯ π β (π mod π) = 0. See divides 16227 and dvdsval2 16228 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β βπ β β€ (π Β· π) = π)) | ||
Theorem | dvdsval2 16228 | 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 16229 | 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 16230 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ (π β₯ π β (π β β€ β§ π β β€)) | ||
Theorem | dvdsmod0 16231 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
β’ ((π β β β§ π β₯ π) β (π mod π) = 0) | ||
Theorem | p1modz1 16232 | 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 16233 | 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 16747). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
β’ ((π β β β§ π΅ β β β§ π β₯ π΄) β ((π΄βπ΅) mod π) = (π΄ mod π)) | ||
Theorem | nndivdvds 16234 | Strong form of dvdsval2 16228 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β β§ π΅ β β) β (π΅ β₯ π΄ β (π΄ / π΅) β β)) | ||
Theorem | nndivides 16235* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
β’ ((π β β β§ π β β) β (π β₯ π β βπ β β (π Β· π) = π)) | ||
Theorem | moddvds 16236 | Two ways to say π΄β‘π΅ (mod π), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
β’ ((π β β β§ π΄ β β€ β§ π΅ β β€) β ((π΄ mod π) = (π΅ mod π) β π β₯ (π΄ β π΅))) | ||
Theorem | modm1div 16237 | 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 16238 | A lemma to assist theorems of β₯ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (((πΎ β β€ β§ π β β€ β§ π β β€) β§ (πΎ Β· π) = π) β π β₯ π) | ||
Theorem | dvds1lem 16239* | A lemma to assist theorems of β₯ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (π½ β β€ β§ πΎ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ π₯ β β€) β π β β€) & β’ ((π β§ π₯ β β€) β ((π₯ Β· π½) = πΎ β (π Β· π) = π)) β β’ (π β (π½ β₯ πΎ β π β₯ π)) | ||
Theorem | dvds2lem 16240* | A lemma to assist theorems of β₯ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β (πΌ β β€ β§ π½ β β€)) & β’ (π β (πΎ β β€ β§ πΏ β β€)) & β’ (π β (π β β€ β§ π β β€)) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β π β β€) & β’ ((π β§ (π₯ β β€ β§ π¦ β β€)) β (((π₯ Β· πΌ) = π½ β§ (π¦ Β· πΎ) = πΏ) β (π Β· π) = π)) β β’ (π β ((πΌ β₯ π½ β§ πΎ β₯ πΏ) β π β₯ π)) | ||
Theorem | iddvds 16241 | 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 16242 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β 1 β₯ π) | ||
Theorem | dvds0 16243 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β π β₯ 0) | ||
Theorem | negdvdsb 16244 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β -π β₯ π)) | ||
Theorem | dvdsnegb 16245 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ -π)) | ||
Theorem | absdvdsb 16246 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β (absβπ) β₯ π)) | ||
Theorem | dvdsabsb 16247 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (absβπ))) | ||
Theorem | 0dvds 16248 | 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 16249 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | dvdsmul2 16250 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β π β₯ (π Β· π)) | ||
Theorem | iddvdsexp 16251 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
β’ ((π β β€ β§ π β β) β π β₯ (πβπ)) | ||
Theorem | muldvds1 16252 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β πΎ β₯ π)) | ||
Theorem | muldvds2 16253 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ Β· π) β₯ π β π β₯ π)) | ||
Theorem | dvdscmul 16254 | 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 16255 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ πΎ β β€) β (π β₯ π β (π Β· πΎ) β₯ (π Β· πΎ))) | ||
Theorem | dvdscmulr 16256 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ (πΎ β β€ β§ πΎ β 0)) β ((πΎ Β· π) β₯ (πΎ Β· π) β π β₯ π)) | ||
Theorem | dvdsmulcr 16257 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β€ β§ (πΎ β β€ β§ πΎ β 0)) β ((π Β· πΎ) β₯ (π Β· πΎ) β π β₯ π)) | ||
Theorem | summodnegmod 16258 | 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 16259 | 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 16260 | 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 16261 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π + π))) | ||
Theorem | dvds2sub 16262 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β ((πΎ β₯ π β§ πΎ β₯ π) β πΎ β₯ (π β π))) | ||
Theorem | dvds2addd 16263 | Deduction form of dvds2add 16261. (Contributed by SN, 21-Aug-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π + π)) | ||
Theorem | dvds2subd 16264 | Deduction form of dvds2sub 16262. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π β π)) | ||
Theorem | dvdstr 16265 | 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 16266 | The divides relation is transitive, a deduction version of dvdstr 16265. (Contributed by metakunt, 12-May-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) & β’ (π β π β₯ π) β β’ (π β πΎ β₯ π) | ||
Theorem | dvdsmultr1 16267 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β₯ π β πΎ β₯ (π Β· π))) | ||
Theorem | dvdsmultr1d 16268 | Deduction form of dvdsmultr1 16267. (Contributed by Stanislas Polu, 9-Mar-2020.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π Β· π)) | ||
Theorem | dvdsmultr2 16269 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
β’ ((πΎ β β€ β§ π β β€ β§ π β β€) β (πΎ β₯ π β πΎ β₯ (π Β· π))) | ||
Theorem | dvdsmultr2d 16270 | Deduction form of dvdsmultr2 16269. (Contributed by SN, 23-Aug-2024.) |
β’ (π β πΎ β β€) & β’ (π β π β β€) & β’ (π β π β β€) & β’ (π β πΎ β₯ π) β β’ (π β πΎ β₯ (π Β· π)) | ||
Theorem | ordvdsmul 16271 | 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 16272 | 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 16273 | 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 16274 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π + π))) | ||
Theorem | dvdssub 16275 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π β π))) | ||
Theorem | dvdssubr 16276 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
β’ ((π β β€ β§ π β β€) β (π β₯ π β π β₯ (π β π))) | ||
Theorem | dvdsadd2b 16277 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ (πΆ β β€ β§ π΄ β₯ πΆ)) β (π΄ β₯ π΅ β π΄ β₯ (πΆ + π΅))) | ||
Theorem | dvdsaddre2b 16278 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 16277 only requiring π΅ to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
β’ ((π΄ β β€ β§ π΅ β β β§ (πΆ β β€ β§ π΄ β₯ πΆ)) β (π΄ β₯ π΅ β π΄ β₯ (πΆ + π΅))) | ||
Theorem | fsumdvds 16279* | If every term in a sum is divisible by π, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
β’ (π β π΄ β Fin) & β’ (π β π β β€) & β’ ((π β§ π β π΄) β π΅ β β€) & β’ ((π β§ π β π΄) β π β₯ π΅) β β’ (π β π β₯ Ξ£π β π΄ π΅) | ||
Theorem | dvdslelem 16280 | Lemma for dvdsle 16281. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ π β β€ & β’ π β β & β’ πΎ β β€ β β’ (π < π β (πΎ Β· π) β π) | ||
Theorem | dvdsle 16281 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ ((π β β€ β§ π β β) β (π β₯ π β π β€ π)) | ||
Theorem | dvdsleabs 16282 | 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 16283 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π β β€ β§ π β β€ β§ π β 0) β (π β₯ π β (absβπ) β€ (absβπ))) | ||
Theorem | dvdsabseq 16284 | 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 16285 | 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 16286 | 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 16287* | 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 16288* | 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 16289* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
β’ (π΄ β β β {π β β β£ π β₯ π΄} β (1...π΄)) | ||
Theorem | dvds1 16290 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
β’ (π β β0 β (π β₯ 1 β π = 1)) | ||
Theorem | alzdvds 16291* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
β’ (π β β€ β (βπ₯ β β€ π₯ β₯ π β π = 0)) | ||
Theorem | dvdsext 16292* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΄ β β0 β§ π΅ β β0) β (π΄ = π΅ β βπ₯ β β0 (π΄ β₯ π₯ β π΅ β₯ π₯))) | ||
Theorem | fzm1ndvds 16293 | No number between 1 and π β 1 divides π. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ ((π β β β§ π β (1...(π β 1))) β Β¬ π β₯ π) | ||
Theorem | fzo0dvdseq 16294 | 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 16295 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ ((π΄ β (πΆ..^π·) β§ π΅ β (πΆ..^π·)) β ((π· β πΆ) β₯ (π΄ β π΅) β π΄ = π΅)) | ||
Theorem | addmodlteqALT 16296 | 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 13938 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 16297 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
β’ ((πΎ β β β§ π β (β€β₯βπΎ)) β πΎ β₯ (!βπ)) | ||
Theorem | dvdsexp2im 16298 | 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 16299 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
β’ ((π΄ β β€ β§ π β β0 β§ π β (β€β₯βπ)) β (π΄βπ) β₯ (π΄βπ)) | ||
Theorem | dvdsmod 16300 | 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 π) β π β₯ πΎ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |