Home | Metamath
Proof Explorer Theorem List (p. 149 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ruclem3 14801* | Lemma for ruc 14811. The constructed interval [𝑋, 𝑌] always excludes 𝑀. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ (𝜑 → 𝐹:ℕ⟶ℝ) & ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, 〈(1st ‘𝑥), 𝑚〉, 〈((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)〉))) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝑀 ∈ ℝ) & ⊢ 𝑋 = (1st ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ 𝑌 = (2nd ‘(〈𝐴, 𝐵〉𝐷𝑀)) & ⊢ (𝜑 → 𝐴 < 𝐵) ⇒ ⊢ (𝜑 → (𝑀 < 𝑋 ∨ 𝑌 < 𝑀)) | ||
Theorem | ruclem4 14802* | Lemma for ruc 14811. 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 14803* | Lemma for ruc 14811. Domain and range 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 14804* | Lemma for ruc 14811. 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 14805* | Lemma for ruc 14811. 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 14806* | Lemma for ruc 14811. 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 14807* | Lemma for ruc 14811. 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 14808* | Lemma for ruc 14811. 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 14809* | Lemma for ruc 14811. 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 14810 | Lemma for ruc 14811. There is no function that maps ℕ onto ℝ. (Use nex 1722 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 14811 | 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 14799 through ruclem13 14810 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 14810 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable. For an alternate proof see rucALT 14798. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.) |
⊢ ℕ ≺ ℝ | ||
Theorem | resdomq 14812 | The set of rationals is strictly less equinumerous than the set of reals (ℝ strictly dominates ℚ). (Contributed by NM, 18-Dec-2004.) |
⊢ ℚ ≺ ℝ | ||
Theorem | aleph1re 14813 | There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.) |
⊢ (ℵ‘1𝑜) ≼ ℝ | ||
Theorem | aleph1irr 14814 | There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.) |
⊢ (ℵ‘1𝑜) ≼ (ℝ ∖ ℚ) | ||
Theorem | cnso 14815 | 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 | sqr2irrlem 14816 | Lemma for irrationality of square root of 2. 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.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → (√‘2) = (𝐴 / 𝐵)) ⇒ ⊢ (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ)) | ||
Theorem | sqrt2irr 14817 | The square root of 2 is irrational. See zsqrtelqelz 15304 for a generalization to all non-square integers. The proof's core is proven in sqr2irrlem 14816, 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 "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/. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
⊢ (√‘2) ∉ ℚ | ||
Theorem | sqrt2re 14818 | The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.) |
⊢ (√‘2) ∈ ℝ | ||
Theorem | nthruc 14819 | 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 14820 for a further refinement. (Contributed by NM, 12-Jan-2002.) |
⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ)) | ||
Theorem | nthruz 14820 | 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 14819. (Contributed by NM, 9-May-2004.) |
⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ) | ||
Syntax | cdvds 14821 | Extend the definition of a class to include the divides relation. See df-dvds 14822. |
class ∥ | ||
Definition | df-dvds 14822* | Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ∥ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)} | ||
Theorem | divides 14823* | Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 26705). As proven in dvdsval3 14825, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 14823 and dvdsval2 14824 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | dvdsval2 14824 | 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 14825 | 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 14826 | Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) | ||
Theorem | nndivdvds 14827 | Strong form of dvdsval2 14824 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ)) | ||
Theorem | nndivides 14828* | Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁)) | ||
Theorem | moddvds 14829 | Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵))) | ||
Theorem | dvds0lem 14830 | A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁) | ||
Theorem | dvds1lem 14831* | A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvds2lem 14832* | A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ)) & ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ)) & ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ) & ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁)) ⇒ ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁)) | ||
Theorem | iddvds 14833 | 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 14834 | 1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁) | ||
Theorem | dvds0 14835 | Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0) | ||
Theorem | negdvdsb 14836 | An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁)) | ||
Theorem | dvdsnegb 14837 | An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁)) | ||
Theorem | absdvdsb 14838 | An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁)) | ||
Theorem | dvdsabsb 14839 | An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (abs‘𝑁))) | ||
Theorem | 0dvds 14840 | 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 14841 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmul2 14842 | An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁)) | ||
Theorem | iddvdsexp 14843 | An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀↑𝑁)) | ||
Theorem | muldvds1 14844 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ 𝑁)) | ||
Theorem | muldvds2 14845 | If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁)) | ||
Theorem | dvdscmul 14846 | 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 14847 | Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾))) | ||
Theorem | dvdscmulr 14848 | Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | dvdsmulcr 14849 | Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁)) | ||
Theorem | summodnegmod 14850 | 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 14851 | 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 14852 | 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 14853 | If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁))) | ||
Theorem | dvds2sub 14854 | If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvds2subd 14855 | Natural deduction form of dvds2sub 14854. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) & ⊢ (𝜑 → 𝐾 ∥ 𝑁) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 − 𝑁)) | ||
Theorem | dvdstr 14856 | 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 14857 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑀 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | dvdsmultr1d 14858 | Natural deduction form of dvdsmultr1 14857. (Contributed by Stanislas Polu, 9-Mar-2020.) |
⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐾 ∥ 𝑀) ⇒ ⊢ (𝜑 → 𝐾 ∥ (𝑀 · 𝑁)) | ||
Theorem | dvdsmultr2 14859 | If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∥ 𝑁 → 𝐾 ∥ (𝑀 · 𝑁))) | ||
Theorem | ordvdsmul 14860 | 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 14861 | 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 14862 | 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 14863 | An integer divides another iff it divides their sum. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 + 𝑀))) | ||
Theorem | dvdssub 14864 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑀 − 𝑁))) | ||
Theorem | dvdssubr 14865 | An integer divides another iff it divides their difference. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (𝑁 − 𝑀))) | ||
Theorem | dvdsadd2b 14866 | Adding a multiple of the base does not affect divisibility. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | dvdsaddre2b 14867 | Adding a multiple of the base does not affect divisibility. Variant of dvdsadd2b 14866 only requiring 𝐵 to be a real number (not necessarily an integer). (Contributed by AV, 19-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ ∧ (𝐶 ∈ ℤ ∧ 𝐴 ∥ 𝐶)) → (𝐴 ∥ 𝐵 ↔ 𝐴 ∥ (𝐶 + 𝐵))) | ||
Theorem | fsumdvds 14868* | If every term in a sum is divisible by 𝑁, then so is the sum. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑁 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑁 ∥ Σ𝑘 ∈ 𝐴 𝐵) | ||
Theorem | dvdslelem 14869 | Lemma for dvdsle 14870. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑀 ∈ ℤ & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐾 ∈ ℤ ⇒ ⊢ (𝑁 < 𝑀 → (𝐾 · 𝑀) ≠ 𝑁) | ||
Theorem | dvdsle 14870 | The divisors of a positive integer are bounded by it. The proof does not use /. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 → 𝑀 ≤ 𝑁)) | ||
Theorem | dvdsleabs 14871 | 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 14872 | Transfer divisibility to an order constraint on absolute values. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 ∥ 𝑁 → (abs‘𝑀) ≤ (abs‘𝑁))) | ||
Theorem | dvdsabseq 14873 | 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 14874 | 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 14875 | 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 14876* | 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 14877* | 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 14878* | The set of divisors of a number is a subset of a finite set. (Contributed by Mario Carneiro, 22-Sep-2014.) |
⊢ (𝐴 ∈ ℕ → {𝑝 ∈ ℕ ∣ 𝑝 ∥ 𝐴} ⊆ (1...𝐴)) | ||
Theorem | dvds1 14879 | The only nonnegative integer that divides 1 is 1. (Contributed by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑀 ∈ ℕ0 → (𝑀 ∥ 1 ↔ 𝑀 = 1)) | ||
Theorem | alzdvds 14880* | Only 0 is divisible by all integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (∀𝑥 ∈ ℤ 𝑥 ∥ 𝑁 ↔ 𝑁 = 0)) | ||
Theorem | dvdsext 14881* | Poset extensionality for division. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑥 ∈ ℕ0 (𝐴 ∥ 𝑥 ↔ 𝐵 ∥ 𝑥))) | ||
Theorem | fzm1ndvds 14882 | No number between 1 and 𝑀 − 1 divides 𝑀. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (1...(𝑀 − 1))) → ¬ 𝑀 ∥ 𝑁) | ||
Theorem | fzo0dvdseq 14883 | 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 14884 | Two different elements of a half-open range are not congruent mod its length. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐴 ∈ (𝐶..^𝐷) ∧ 𝐵 ∈ (𝐶..^𝐷)) → ((𝐷 − 𝐶) ∥ (𝐴 − 𝐵) ↔ 𝐴 = 𝐵)) | ||
Theorem | addmodlteqALT 14885 | 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 12607 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 14886 | A positive integer divides any greater factorial. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝑁 ∈ (ℤ≥‘𝐾)) → 𝐾 ∥ (!‘𝑁)) | ||
Theorem | dvdsexp 14887 | A power divides a power with a greater exponent. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑀) ∥ (𝐴↑𝑁)) | ||
Theorem | dvdsmod 14888 | 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 14889 | If an integer is divisible by a positive integer, the product of this integer with another integer modulo the positive integer is 0. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑁 ∥ 𝐴 → ((𝐴 · 𝐵) mod 𝑁) = 0)) | ||
Theorem | 3dvds 14890* | 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 | 3dvdsOLD 14891* | Obsolete version of 3dvds 14890 as of 8-Sep-2021. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 17-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(0...𝑁)⟶ℤ) → (3 ∥ Σ𝑘 ∈ (0...𝑁)((𝐹‘𝑘) · (10↑𝑘)) ↔ 3 ∥ Σ𝑘 ∈ (0...𝑁)(𝐹‘𝑘))) | ||
Theorem | 3dvdsdec 14892 | 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 | 3dvdsdecOLD 14893 | Obsolete proof of 3dvdsdec 14892 as of 8-Sep-2021. (Contributed by AV, 14-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 ⇒ ⊢ (3 ∥ ;𝐴𝐵 ↔ 3 ∥ (𝐴 + 𝐵)) | ||
Theorem | 3dvds2dec 14894 | 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 | 3dvds2decOLD 14895 | Old version of 3dvds2dec 14894. Obsolete as of 1-Aug-2021. (Contributed by AV, 14-Jun-2021.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ 𝐴 ∈ ℕ0 & ⊢ 𝐵 ∈ ℕ0 & ⊢ 𝐶 ∈ ℕ0 ⇒ ⊢ (3 ∥ ;;𝐴𝐵𝐶 ↔ 3 ∥ ((𝐴 + 𝐵) + 𝐶)) | ||
Theorem | fprodfvdvdsd 14896* | A finite product of integers is divisible by any of its factors being function values. (Contributed by AV, 1-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵⟶ℤ) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∥ ∏𝑘 ∈ 𝐴 (𝐹‘𝑘)) | ||
Theorem | fproddvdsd 14897* | 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 14900. 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 14898) and ¬ 2 ∥ 𝑁 to say that "𝑁 is odd" (under the assumption that 𝑁 ∈ ℤ). The previously proven theorems about even and odd numbers, like zneo 11336, zeo 11339, zeo2 11340, etc. use different representations, which are equivalent with the representations using the divides relation, see evend2 14919 and oddp1d2 14920. The corresponding theorems are zeneo 14901, zeo3 14899 and zeo4 14900. | ||
Theorem | evenelz 14898 | An even number is an integer. This follows immediately from the reverse closure of the divides relation, see dvdszrcl 14826. (Contributed by AV, 22-Jun-2021.) |
⊢ (2 ∥ 𝑁 → 𝑁 ∈ ℤ) | ||
Theorem | zeo3 14899 | An integer is even or odd. With this representation of even and odd integers, this variant of zeo 11339 follows immediatly from the law of excluded middle, see exmidd 431. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) | ||
Theorem | zeo4 14900 | An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 11340 follows immediatly from the principle of double negation, see notnotb 303. (Contributed by AV, 17-Jun-2021.) |
⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |