![]() |
Metamath
Proof Explorer Theorem List (p. 164 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dvds1lem 16301* | A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvds2lem 16302* | A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ)) & ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁)) | ||
Theorem | iddvds 16303 | 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 16304 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁) | ||
Theorem | dvds0 16305 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) | ||
Theorem | negdvdsb 16306 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁)) | ||
Theorem | dvdsnegb 16307 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁)) | ||
Theorem | absdvdsb 16308 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) | ||
Theorem | dvdsabsb 16309 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (abs‘𝑁))) | ||
Theorem | 0dvds 16310 | 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 16311 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmul2 16312 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁)) | ||
Theorem | iddvdsexp 16313 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀↑𝑁)) | ||
Theorem | muldvds1 16314 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ 𝑁)) | ||
Theorem | muldvds2 16315 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvdscmul 16316 | 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 16317 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾))) | ||
Theorem | dvdscmulr 16318 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | dvdsmulcr 16319 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | summodnegmod 16320 | 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 16321 | 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 16322 | 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 16323 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁))) | ||
Theorem | dvds2sub 16324 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvds2addd 16325 | Deduction form of dvds2add 16323. (Contributed by SN, 21-Aug-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 + 𝑁)) | ||
Theorem | dvds2subd 16326 | Deduction form of dvds2sub 16324. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 − 𝑁)) | ||
Theorem | dvdstr 16327 | 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 16328 | The divides relation is transitive, a deduction version of dvdstr 16327. (Contributed by metakunt, 12-May-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ 𝑁) | ||
Theorem | dvdsmultr1 16329 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | dvdsmultr1d 16330 | Deduction form of dvdsmultr1 16329. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmultr2 16331 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | dvdsmultr2d 16332 | Deduction form of dvdsmultr2 16331. (Contributed by SN, 23-Aug-2024.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁)) | ||
Theorem | ordvdsmul 16333 | 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 16334 | 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 16335 | 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 16336 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 + 𝑀))) | ||
Theorem | dvdssub 16337 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvdssubr 16338 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 − 𝑀))) | ||
Theorem | dvdsadd2b 16339 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | dvdsaddre2b 16340 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 16339 only requiring 𝐵 to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | fsumdvds 16341* | If every term in a sum is divisible by 𝑁, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑁 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑁 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | dvdslelem 16342 | Lemma for dvdsle 16343. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 < 𝑀 → (𝐾 · 𝑀) ≠ 𝑁) | ||
Theorem | dvdsle 16343 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁)) | ||
Theorem | dvdsleabs 16344 | 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 16345 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁))) | ||
Theorem | dvdsabseq 16346 | 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 16347 | 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 16348 | 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 16349* | 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 16350* | 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 16351* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | ||
Theorem | dvds1 16352 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1)) | ||
Theorem | alzdvds 16353* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0)) | ||
Theorem | dvdsext 16354* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥))) | ||
Theorem | fzm1ndvds 16355 | No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁) | ||
Theorem | fzo0dvdseq 16356 | 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 16357 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | addmodlteqALT 16358 | 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 13983 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 16359 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁)) | ||
Theorem | dvdsexp2im 16360 | 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 16361 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁)) | ||
Theorem | dvdsmod 16362 | 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 16363 | 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 16364* | 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 16365 | 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 16366 | 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 16367* | A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵⟶ℤ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∥ ∏𝑘 ∈ 𝐴 (𝐹‘𝑘)) | ||
Theorem | fproddvdsd 16368* | 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 16371. 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 16369) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 12698, zeo 12701, zeo2 12702, etc. use different representations, which are equivalent to the representations using the divides relation, see evend2 16390 and oddp1d2 16391. The corresponding theorems are zeneo 16372, zeo3 16370 and zeo4 16371. | ||
Theorem | evenelz 16369 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 16291. (Contributed by AV, 22-Jun-2021.) |
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ) | ||
Theorem | zeo3 16370 | An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12701 follows immediately from the law of excluded middle, see exmidd 895. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) | ||
Theorem | zeo4 16371 | An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12702 follows immediately from the principle of double negation, see notnotb 315. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) | ||
Theorem | zeneo 16372 | 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 12698 follows immediately from the fact that a contradiction implies anything, see pm2.21i 119. (Contributed by AV, 22-Jun-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((2 ∥ 𝐴 ∧ ¬ 2 ∥ 𝐵) → 𝐴 ≠ 𝐵)) | ||
Theorem | odd2np1lem 16373* | Lemma for odd2np1 16374. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) | ||
Theorem | odd2np1 16374* | 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 16375* | An integer is even iff it is twice another integer. (Contributed by AV, 25-Jun-2020.) |
⊢ (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (2 · 𝑛) = 𝑁) | ||
Theorem | oddm1even 16376 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 − 1))) | ||
Theorem | oddp1even 16377 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ 2 ∥ (𝑁 + 1))) | ||
Theorem | oexpneg 16378 | 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 16379 | 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 16380 | 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 16381* | 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 16382* | 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 16383* | 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 16384* | A positive integer is even iff it is twice another positive integer. (Contributed by AV, 12-Aug-2021.) |
⊢ (𝑁 ∈ ℕ → (2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (2 · 𝑛) = 𝑁)) | ||
Theorem | 2tp1odd 16385 | A number which is twice an integer increased by 1 is odd. (Contributed by AV, 16-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = ((2 · 𝐴) + 1)) → ¬ 2 ∥ 𝐵) | ||
Theorem | mulsucdiv2z 16386 | 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 16387 | A squared odd number minus 1 divided by 8 is an integer. (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (((𝑁↑2) − 1) / 8) ∈ ℤ) | ||
Theorem | 2teven 16388 | A number which is twice an integer is even. (Contributed by AV, 16-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 = (2 · 𝐴)) → 2 ∥ 𝐵) | ||
Theorem | zeo5 16389 | An integer is either even or odd, version of zeo3 16370 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ 2 ∥ (𝑁 + 1))) | ||
Theorem | evend2 16390 | 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 12701 and zeo2 12702. (Contributed by AV, 22-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ (𝑁 / 2) ∈ ℤ)) | ||
Theorem | oddp1d2 16391 | 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 12701 and zeo2 12702. (Contributed by AV, 22-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℤ)) | ||
Theorem | zob 16392 | Alternate characterizations of an odd number. (Contributed by AV, 7-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (((𝑁 + 1) / 2) ∈ ℤ ↔ ((𝑁 − 1) / 2) ∈ ℤ)) | ||
Theorem | oddm1d2 16393 | 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 16394 | 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))) | ||
Theorem | halfleoddlt 16395 | An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀)) | ||
Theorem | opoe 16396 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵)) | ||
Theorem | omoe 16397 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵)) | ||
Theorem | opeo 16398 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 + 𝐵)) | ||
Theorem | omeo 16399 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 − 𝐵)) | ||
Theorem | z0even 16400 | 2 divides 0. That means 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 0 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |