Home | Intuitionistic Logic Explorer Theorem List (p. 119 of 137) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nnoddm1d2 11801 | A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝑁 ∈ ℕ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℕ)) | ||
Theorem | z0even 11802 | 0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 0 | ||
Theorem | n2dvds1 11803 | 2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ ¬ 2 ∥ 1 | ||
Theorem | n2dvdsm1 11804 | 2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.) |
⊢ ¬ 2 ∥ -1 | ||
Theorem | z2even 11805 | 2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.) |
⊢ 2 ∥ 2 | ||
Theorem | n2dvds3 11806 | 2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.) |
⊢ ¬ 2 ∥ 3 | ||
Theorem | z4even 11807 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.) |
⊢ 2 ∥ 4 | ||
Theorem | 4dvdseven 11808 | An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.) |
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁) | ||
Theorem | divalglemnn 11809* | Lemma for divalg 11815. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalglemqt 11810 | Lemma for divalg 11815. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.) |
⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 𝑄 = 𝑇) & ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → 𝑅 = 𝑆) | ||
Theorem | divalglemnqt 11811 | Lemma for divalg 11815. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.) |
⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ ℤ) & ⊢ (𝜑 → 𝑆 ∈ ℤ) & ⊢ (𝜑 → 𝑄 ∈ ℤ) & ⊢ (𝜑 → 𝑇 ∈ ℤ) & ⊢ (𝜑 → 0 ≤ 𝑆) & ⊢ (𝜑 → 𝑅 < 𝐷) & ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆)) ⇒ ⊢ (𝜑 → ¬ 𝑄 < 𝑇) | ||
Theorem | divalglemeunn 11812* | Lemma for divalg 11815. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalglemex 11813* | Lemma for divalg 11815. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalglemeuneg 11814* | Lemma for divalg 11815. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalg 11815* | The division algorithm (theorem). Dividing an integer 𝑁 by a nonzero integer 𝐷 produces a (unique) quotient 𝑞 and a unique remainder 0 ≤ 𝑟 < (abs‘𝐷). Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟))) | ||
Theorem | divalgb 11816* | Express the division algorithm as stated in divalg 11815 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟)))) | ||
Theorem | divalg2 11817* | The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟))) | ||
Theorem | divalgmod 11818 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 11817 and divalgb 11816). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))) | ||
Theorem | divalgmodcl 11819 | The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 11818. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))) | ||
Theorem | modremain 11820* | The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁)) | ||
Theorem | ndvdssub 11821 | Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 − 1, 𝑁 − 2... 𝑁 − (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾))) | ||
Theorem | ndvdsadd 11822 | Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 + 1, 𝑁 + 2... 𝑁 + (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 𝐾))) | ||
Theorem | ndvdsp1 11823 | Special case of ndvdsadd 11822. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1))) | ||
Theorem | ndvdsi 11824 | A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝑄 ∈ ℕ0 & ⊢ 𝑅 ∈ ℕ & ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵 & ⊢ 𝑅 < 𝐴 ⇒ ⊢ ¬ 𝐴 ∥ 𝐵 | ||
Theorem | flodddiv4 11825 | The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2))) | ||
Theorem | fldivndvdslt 11826 | The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.) |
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐿 ≠ 0) ∧ ¬ 𝐿 ∥ 𝐾) → (⌊‘(𝐾 / 𝐿)) < (𝐾 / 𝐿)) | ||
Theorem | flodddiv4lt 11827 | The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (⌊‘(𝑁 / 4)) < (𝑁 / 4)) | ||
Theorem | flodddiv4t2lthalf 11828 | The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.) |
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2)) | ||
Syntax | cgcd 11829 | Extend the definition of a class to include the greatest common divisor operator. |
class gcd | ||
Definition | df-gcd 11830* | Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 13318). (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) | ||
Theorem | gcdmndc 11831 | Decidablity lemma used in various proofs related to gcd. (Contributed by Jim Kingdon, 12-Dec-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0)) | ||
Theorem | zsupcllemstep 11832* | Lemma for zsupcl 11834. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.) |
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓) ⇒ ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))))) | ||
Theorem | zsupcllemex 11833* | Lemma for zsupcl 11834. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) | ||
Theorem | zsupcl 11834* | Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at 𝑀 (which corresponds to the nonempty condition of classical supremum theorems), (b) decidable at each value after 𝑀, and (c) be false after 𝑗 (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → sup({𝑛 ∈ ℤ ∣ 𝜓}, ℝ, < ) ∈ (ℤ≥‘𝑀)) | ||
Theorem | zssinfcl 11835* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ ℤ) & ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ) ⇒ ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵) | ||
Theorem | infssuzex 11836* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓} & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) | ||
Theorem | infssuzledc 11837* | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓} & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → inf(𝑆, ℝ, < ) ≤ 𝐴) | ||
Theorem | infssuzcldc 11838* | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓} & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆) | ||
Theorem | nninfdcex 11839* | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | dvdsbnd 11840* | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴) | ||
Theorem | gcdsupex 11841* | Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.) |
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧))) | ||
Theorem | gcdsupcl 11842* | Closure of the supremum used in defining gcd. A lemma for gcdval 11843 and gcdn0cl 11846. (Contributed by Jim Kingdon, 11-Dec-2021.) |
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈ ℕ) | ||
Theorem | gcdval 11843* | The value of the gcd operator. (𝑀 gcd 𝑁) is the greatest common divisor of 𝑀 and 𝑁. If 𝑀 and 𝑁 are both 0, the result is defined conventionally as 0. (Contributed by Paul Chapman, 21-Mar-2011.) (Revised by Mario Carneiro, 10-Nov-2013.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = if((𝑀 = 0 ∧ 𝑁 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < ))) | ||
Theorem | gcd0val 11844 | The value, by convention, of the gcd operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (0 gcd 0) = 0 | ||
Theorem | gcdn0val 11845* | The value of the gcd operator when at least one operand is nonzero. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) = sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑀 ∧ 𝑛 ∥ 𝑁)}, ℝ, < )) | ||
Theorem | gcdn0cl 11846 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcddvds 11847 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) | ||
Theorem | dvdslegcd 11848 | An integer which divides both operands of the gcd operator is bounded by it. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ (𝑀 gcd 𝑁))) | ||
Theorem | nndvdslegcd 11849 | A positive integer which divides both positive operands of the gcd operator is bounded by it. (Contributed by AV, 9-Aug-2020.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ (𝑀 gcd 𝑁))) | ||
Theorem | gcdcl 11850 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcdnncl 11851 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcdcld 11852 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcd2n0cl 11853 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | zeqzmulgcd 11854* | An integer is the product of an integer and the gcd of it and another integer. (Contributed by AV, 11-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑛 ∈ ℤ 𝐴 = (𝑛 · (𝐴 gcd 𝐵))) | ||
Theorem | divgcdz 11855 | An integer divided by the gcd of it and a nonzero integer is an integer. (Contributed by AV, 11-Jul-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℤ) | ||
Theorem | gcdf 11856 | Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 16-Nov-2013.) |
⊢ gcd :(ℤ × ℤ)⟶ℕ0 | ||
Theorem | gcdcom 11857 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | gcdcomd 11858 | The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | divgcdnn 11859 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ) | ||
Theorem | divgcdnnr 11860 | A positive integer divided by the gcd of it and another integer is a positive integer. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → (𝐴 / (𝐵 gcd 𝐴)) ∈ ℕ) | ||
Theorem | gcdeq0 11861 | The gcd of two integers is zero iff they are both zero. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) = 0 ↔ (𝑀 = 0 ∧ 𝑁 = 0))) | ||
Theorem | gcdn0gt0 11862 | The gcd of two integers is positive (nonzero) iff they are not both zero. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (¬ (𝑀 = 0 ∧ 𝑁 = 0) ↔ 0 < (𝑀 gcd 𝑁))) | ||
Theorem | gcd0id 11863 | The gcd of 0 and an integer is the integer's absolute value. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (0 gcd 𝑁) = (abs‘𝑁)) | ||
Theorem | gcdid0 11864 | The gcd of an integer and 0 is the integer's absolute value. Theorem 1.4(d)2 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 0) = (abs‘𝑁)) | ||
Theorem | nn0gcdid0 11865 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁) | ||
Theorem | gcdneg 11866 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | neggcd 11867 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | gcdaddm 11868 | Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + (𝐾 · 𝑀)))) | ||
Theorem | gcdadd 11869 | The GCD of two numbers is the same as the GCD of the left and their sum. (Contributed by Scott Fenton, 20-Apr-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑀 gcd (𝑁 + 𝑀))) | ||
Theorem | gcdid 11870 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁)) | ||
Theorem | gcd1 11871 | The gcd of a number with 1 is 1. Theorem 1.4(d)1 in [ApostolNT] p. 16. (Contributed by Mario Carneiro, 19-Feb-2014.) |
⊢ (𝑀 ∈ ℤ → (𝑀 gcd 1) = 1) | ||
Theorem | gcdabs 11872 | The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) gcd (abs‘𝑁)) = (𝑀 gcd 𝑁)) | ||
Theorem | gcdabs1 11873 | gcd of the absolute value of the first operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → ((abs‘𝑁) gcd 𝑀) = (𝑁 gcd 𝑀)) | ||
Theorem | gcdabs2 11874 | gcd of the absolute value of the second operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑁 gcd (abs‘𝑀)) = (𝑁 gcd 𝑀)) | ||
Theorem | modgcd 11875 | The gcd remains unchanged if one operand is replaced with its remainder modulo the other. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((𝑀 mod 𝑁) gcd 𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | 1gcd 11876 | The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (𝑀 ∈ ℤ → (1 gcd 𝑀) = 1) | ||
Theorem | gcdmultipled 11877 | The greatest common divisor of a nonnegative integer 𝑀 and a multiple of it is 𝑀 itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd (𝑁 · 𝑀)) = 𝑀) | ||
Theorem | dvdsgcdidd 11878 | The greatest common divisor of a positive integer and another integer it divides is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∥ 𝑁) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) = 𝑀) | ||
Theorem | 6gcd4e2 11879 | The greatest common divisor of six and four is two. To calculate this gcd, a simple form of Euclid's algorithm is used: (6 gcd 4) = ((4 + 2) gcd 4) = (2 gcd 4) and (2 gcd 4) = (2 gcd (2 + 2)) = (2 gcd 2) = 2. (Contributed by AV, 27-Aug-2020.) |
⊢ (6 gcd 4) = 2 | ||
Theorem | bezoutlemnewy 11880* | Lemma for Bézout's identity. The is-bezout predicate holds for (𝑦 mod 𝑊). (Contributed by Jim Kingdon, 6-Jan-2022.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) & ⊢ (𝜃 → 𝑊 ∈ ℕ) & ⊢ (𝜃 → [𝑦 / 𝑟]𝜑) & ⊢ (𝜃 → 𝑦 ∈ ℕ0) & ⊢ (𝜃 → [𝑊 / 𝑟]𝜑) ⇒ ⊢ (𝜃 → [(𝑦 mod 𝑊) / 𝑟]𝜑) | ||
Theorem | bezoutlemstep 11881* | Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) & ⊢ (𝜃 → 𝑊 ∈ ℕ) & ⊢ (𝜃 → [𝑦 / 𝑟]𝜑) & ⊢ (𝜃 → 𝑦 ∈ ℕ0) & ⊢ (𝜃 → [𝑊 / 𝑟]𝜑) & ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦))) & ⊢ ((𝜃 ∧ [(𝑦 mod 𝑊) / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑊) / 𝑥][𝑊 / 𝑦]𝜓 ∧ 𝜑)) & ⊢ Ⅎ𝑥𝜃 & ⊢ Ⅎ𝑟𝜃 ⇒ ⊢ (𝜃 → ∃𝑟 ∈ ℕ0 ([𝑊 / 𝑥]𝜓 ∧ 𝜑)) | ||
Theorem | bezoutlemmain 11882* | Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑)))) | ||
Theorem | bezoutlema 11883* | Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐴. (Contributed by Jim Kingdon, 30-Dec-2021.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜃 → [𝐴 / 𝑟]𝜑) | ||
Theorem | bezoutlemb 11884* | Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐵. (Contributed by Jim Kingdon, 30-Dec-2021.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜃 → [𝐵 / 𝑟]𝜑) | ||
Theorem | bezoutlemex 11885* | Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | ||
Theorem | bezoutlemzz 11886* | Lemma for Bézout's identity. Like bezoutlemex 11885 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | ||
Theorem | bezoutlemaz 11887* | Lemma for Bézout's identity. Like bezoutlemzz 11886 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | ||
Theorem | bezoutlembz 11888* | Lemma for Bézout's identity. Like bezoutlemaz 11887 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | ||
Theorem | bezoutlembi 11889* | Lemma for Bézout's identity. Like bezoutlembz 11888 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))) | ||
Theorem | bezoutlemmo 11890* | Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) & ⊢ (𝜑 → 𝐸 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐸 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) ⇒ ⊢ (𝜑 → 𝐷 = 𝐸) | ||
Theorem | bezoutlemeu 11891* | Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) ⇒ ⊢ (𝜑 → ∃!𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) | ||
Theorem | bezoutlemle 11892* | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) → 𝑧 ≤ 𝐷)) | ||
Theorem | bezoutlemsup 11893* | Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵))) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → 𝐷 = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)}, ℝ, < )) | ||
Theorem | dfgcd3 11894* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) | ||
Theorem | bezout 11895* |
Bézout's identity: For any integers 𝐴 and 𝐵, there are
integers 𝑥, 𝑦 such that (𝐴 gcd 𝐵) = 𝐴 · 𝑥 + 𝐵 · 𝑦. This
is Metamath 100 proof #60.
The proof is constructive, in the sense that it applies the Extended Euclidian Algorithm to constuct a number which can be shown to be (𝐴 gcd 𝐵) and which satisfies the rest of the theorem. In the presence of excluded middle, it is common to prove Bézout's identity by taking the smallest number which satisfies the Bézout condition, and showing it is the greatest common divisor. But we do not have the ability to show that number exists other than by providing a way to determine it. (Contributed by Mario Carneiro, 22-Feb-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | ||
Theorem | dvdsgcd 11896 | An integer which divides each of two others also divides their gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 30-May-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 gcd 𝑁))) | ||
Theorem | dvdsgcdb 11897 | Biconditional form of dvdsgcd 11896. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁))) | ||
Theorem | dfgcd2 11898* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) | ||
Theorem | gcdass 11899 | Associative law for gcd operator. Theorem 1.4(b) in [ApostolNT] p. 16. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((𝑁 gcd 𝑀) gcd 𝑃) = (𝑁 gcd (𝑀 gcd 𝑃))) | ||
Theorem | mulgcd 11900 | Distribute multiplication by a nonnegative integer over gcd. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
⊢ ((𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) gcd (𝐾 · 𝑁)) = (𝐾 · (𝑀 gcd 𝑁))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |