Home | Metamath
Proof Explorer Theorem List (p. 157 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory. | ||
Theorem | sqrt2irrlem 15601 | Lemma for sqrt2irr 15602. 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 15602 | The square root of 2 is irrational. See zsqrtelqelz 16098 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 15601, 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/ 15601. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ (√‘2) ∉ ℚ | ||
Theorem | sqrt2re 15603 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
⊢ (√‘2) ∈ ℝ | ||
Theorem | sqrt2irr0 15604 | The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022.) |
⊢ (√‘2) ∈ (ℝ ∖ ℚ) | ||
Theorem | nthruc 15605 | 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 15606 for a further refinement. (Contributed by NM, 12-Jan-2002.) |
⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ)) | ||
Theorem | nthruz 15606 | 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 15605. (Contributed by NM, 9-May-2004.) |
⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ) | ||
Syntax | cdvds 15607 | Extend the definition of a class to include the divides relation. See df-dvds 15608. |
class ∥ | ||
Definition | df-dvds 15608* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ∥ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} | ||
Theorem | divides 15609* | Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 28235). As proven in dvdsval3 15611, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 15609 and dvdsval2 15610 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | dvdsval2 15610 | 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 15611 | 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 15612 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) | ||
Theorem | dvdsmod0 15613 | If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁) → (𝑁 mod 𝑀) = 0) | ||
Theorem | p1modz1 15614 | 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 15615 | 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 16121). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴) → ((𝐴↑𝐵) mod 𝑁) = (𝐴 mod 𝑁)) | ||
Theorem | nndivdvds 15616 | Strong form of dvdsval2 15610 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ)) | ||
Theorem | nndivides 15617* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | moddvds 15618 | Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
Theorem | modm1div 15619 | A number greater than 1 divides an integer minus 1 iff the integer modulo the number is 1. (Contributed by AV, 30-May-2023.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑁) = 1 ↔ 𝑁 ∥ (𝐴 − 1))) | ||
Theorem | dvds0lem 15620 | A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁) | ||
Theorem | dvds1lem 15621* | A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvds2lem 15622* | A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ)) & ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁)) | ||
Theorem | iddvds 15623 | 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 15624 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁) | ||
Theorem | dvds0 15625 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) | ||
Theorem | negdvdsb 15626 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁)) | ||
Theorem | dvdsnegb 15627 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁)) | ||
Theorem | absdvdsb 15628 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) | ||
Theorem | dvdsabsb 15629 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (abs‘𝑁))) | ||
Theorem | 0dvds 15630 | 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 15631 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmul2 15632 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁)) | ||
Theorem | iddvdsexp 15633 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀↑𝑁)) | ||
Theorem | muldvds1 15634 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ 𝑁)) | ||
Theorem | muldvds2 15635 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvdscmul 15636 | 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 15637 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾))) | ||
Theorem | dvdscmulr 15638 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | dvdsmulcr 15639 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | summodnegmod 15640 | 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 15641 | 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 15642 | 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 15643 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁))) | ||
Theorem | dvds2sub 15644 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvds2subd 15645 | Natural deduction form of dvds2sub 15644. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 − 𝑁)) | ||
Theorem | dvdstr 15646 | 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 15647 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | dvdsmultr1d 15648 | Natural deduction form of dvdsmultr1 15647. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmultr2 15649 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | ordvdsmul 15650 | 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 15651 | 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 15652 | 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 15653 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 + 𝑀))) | ||
Theorem | dvdssub 15654 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvdssubr 15655 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 − 𝑀))) | ||
Theorem | dvdsadd2b 15656 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | dvdsaddre2b 15657 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 15656 only requiring 𝐵 to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | fsumdvds 15658* | If every term in a sum is divisible by 𝑁, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑁 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑁 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | dvdslelem 15659 | Lemma for dvdsle 15660. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 < 𝑀 → (𝐾 · 𝑀) ≠ 𝑁) | ||
Theorem | dvdsle 15660 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁)) | ||
Theorem | dvdsleabs 15661 | 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 15662 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁))) | ||
Theorem | dvdsabseq 15663 | 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 15664 | 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 15665 | 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 15666* | 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 15667* | 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 15668* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | ||
Theorem | dvds1 15669 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1)) | ||
Theorem | alzdvds 15670* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0)) | ||
Theorem | dvdsext 15671* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥))) | ||
Theorem | fzm1ndvds 15672 | No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁) | ||
Theorem | fzo0dvdseq 15673 | 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 15674 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | addmodlteqALT 15675 | 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 13315 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 15676 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁)) | ||
Theorem | dvdsexp 15677 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁)) | ||
Theorem | dvdsmod 15678 | 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 15679 | 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 15680* | 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 15681 | 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 15682 | 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 ∥ ((𝐴 + 𝐵) + 𝐶)) | ||
Theorem | fprodfvdvdsd 15683* | A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵⟶ℤ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∥ ∏𝑘 ∈ 𝐴 (𝐹‘𝑘)) | ||
Theorem | fproddvdsd 15684* | A finite product of integers is divisible by any of its factors. (Contributed by AV, 14-Aug-2020.) (Proof shortened by AV, 2-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℤ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ∥ ∏𝑘 ∈ 𝐴 𝑘) | ||
The set ℤ of integers can be partitioned into the set of even numbers and the set of odd numbers, see zeo4 15687. 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 15685) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 12066, zeo 12069, zeo2 12070, etc. use different representations, which are equivalent to the representations using the divides relation, see evend2 15706 and oddp1d2 15707. The corresponding theorems are zeneo 15688, zeo3 15686 and zeo4 15687. | ||
Theorem | evenelz 15685 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 15612. (Contributed by AV, 22-Jun-2021.) |
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ) | ||
Theorem | zeo3 15686 | An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12069 follows immediately from the law of excluded middle, see exmidd 892. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) | ||
Theorem | zeo4 15687 | An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12070 follows immediately from the principle of double negation, see notnotb 317. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) | ||
Theorem | zeneo 15688 | 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 12066 follows immediately from the fact that a contradiction implies anything, see pm2.21i 119. (Contributed by AV, 22-Jun-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵)) | ||
Theorem | odd2np1lem 15689* | Lemma for odd2np1 15690. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) | ||
Theorem | odd2np1 15690* | 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 15691* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁) | ||
Theorem | oddm1even 15692 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1))) | ||
Theorem | oddp1even 15693 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) | ||
Theorem | oexpneg 15694 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) | ||
Theorem | mod2eq0even 15695 | 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 15696 | 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.) (Proof shortened by AV, 5-Jul-2020.) |
⊢ (𝑁 ∈ ℤ → ((𝑁 mod 2) = 1 ↔ ¬ 2 ∥ 𝑁)) | ||
Theorem | oddnn02np1 15697* | 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 15698* | An integer greater than one is odd iff it is one plus twice a positive integer. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 9-Jul-2022.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ ((2 · 𝑛) + 1) = 𝑁)) | ||
Theorem | evennn02n 15699* | A nonnegative integer is even iff it is twice another nonnegative integer. (Contributed by AV, 12-Aug-2021.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ (𝑁 ∈ ℕ0 → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ0 (2 · 𝑛) = 𝑁)) | ||
Theorem | evennn2n 15700* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |