Home | Intuitionistic Logic Explorer Theorem List (p. 120 of 142) | < 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 | zsupcllemex 11901* | Lemma for zsupcl 11902. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒)) & ⊢ (𝜑 → 𝜒) & ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓) & ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) | ||
Theorem | zsupcl 11902* | 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 11903* | The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.) |
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦))) & ⊢ (𝜑 → 𝐵 ⊆ ℤ) & ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ) ⇒ ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵) | ||
Theorem | infssuzex 11904* | Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓} & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦))) | ||
Theorem | infssuzledc 11905* | 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 11906* | 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 | suprzubdc 11907* | The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) | ||
Theorem | nninfdcex 11908* | A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑦 𝑦 ∈ 𝐴) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) | ||
Theorem | zsupssdc 11909* | An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧))) | ||
Theorem | suprzcl2dc 11910* | The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7895.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.) |
⊢ (𝜑 → 𝐴 ⊆ ℤ) & ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴) & ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) & ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) ⇒ ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴) | ||
Theorem | dvdsbnd 11911* | There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴) | ||
Theorem | gcdsupex 11912* | Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.) |
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧))) | ||
Theorem | gcdsupcl 11913* | Closure of the supremum used in defining gcd. A lemma for gcdval 11914 and gcdn0cl 11917. (Contributed by Jim Kingdon, 11-Dec-2021.) |
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈ ℕ) | ||
Theorem | gcdval 11914* | 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 11915 | 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 11916* | 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 11917 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcddvds 11918 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) | ||
Theorem | dvdslegcd 11919 | 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 11920 | 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 11921 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcdnncl 11922 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcdcld 11923 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcd2n0cl 11924 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | zeqzmulgcd 11925* | 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 11926 | 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 11927 | 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 11928 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | gcdcomd 11929 | The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | divgcdnn 11930 | 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 11931 | 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 11932 | 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 11933 | 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 11934 | 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 11935 | 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 11936 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁) | ||
Theorem | gcdneg 11937 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | neggcd 11938 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | gcdaddm 11939 | 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 11940 | 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 11941 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁)) | ||
Theorem | gcd1 11942 | 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 11943 | 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 11944 | 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 11945 | 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 11946 | 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 11947 | 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 11948 | 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 11949 | 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 11950 | 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 11951* | 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 11952* | 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 11953* | 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 11954* | Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐴. (Contributed by Jim Kingdon, 30-Dec-2021.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜃 → [𝐴 / 𝑟]𝜑) | ||
Theorem | bezoutlemb 11955* | Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐵. (Contributed by Jim Kingdon, 30-Dec-2021.) |
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡))) & ⊢ (𝜃 → 𝐴 ∈ ℕ0) & ⊢ (𝜃 → 𝐵 ∈ ℕ0) ⇒ ⊢ (𝜃 → [𝐵 / 𝑟]𝜑) | ||
Theorem | bezoutlemex 11956* | 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 11957* | Lemma for Bézout's identity. Like bezoutlemex 11956 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 11958* | Lemma for Bézout's identity. Like bezoutlemzz 11957 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 11959* | Lemma for Bézout's identity. Like bezoutlemaz 11958 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 11960* | Lemma for Bézout's identity. Like bezoutlembz 11959 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 11961* | 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 11962* | 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 11963* | 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 11964* | 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 11965* | Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)))) | ||
Theorem | bezout 11966* |
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 11967 | 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 11968 | Biconditional form of dvdsgcd 11967. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁))) | ||
Theorem | dfgcd2 11969* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) | ||
Theorem | gcdass 11970 | 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 11971 | 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 𝑁))) | ||
Theorem | absmulgcd 11972 | Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) gcd (𝐾 · 𝑁)) = (abs‘(𝐾 · (𝑀 gcd 𝑁)))) | ||
Theorem | mulgcdr 11973 | Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0) → ((𝐴 · 𝐶) gcd (𝐵 · 𝐶)) = ((𝐴 gcd 𝐵) · 𝐶)) | ||
Theorem | gcddiv 11974 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶))) | ||
Theorem | gcdmultiple 11975 | The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdmultiplez 11976 | Extend gcdmultiple 11975 so 𝑁 can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdzeq 11977 | A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 11978. (Contributed by AV, 1-Jul-2020.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵)) | ||
Theorem | gcdeq 11978 | 𝐴 is equal to its gcd with 𝐵 if and only if 𝐴 divides 𝐵. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by AV, 8-Aug-2021.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵)) | ||
Theorem | dvdssqim 11979 | Unidirectional form of dvdssq 11986. (Contributed by Scott Fenton, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | dvdsmulgcd 11980 | Relationship between the order of an element and that of a multiple. (a divisibility equivalent). (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) | ||
Theorem | rpmulgcd 11981 | If 𝐾 and 𝑀 are relatively prime, then the GCD of 𝐾 and 𝑀 · 𝑁 is the GCD of 𝐾 and 𝑁. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐾 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝐾 gcd 𝑀) = 1) → (𝐾 gcd (𝑀 · 𝑁)) = (𝐾 gcd 𝑁)) | ||
Theorem | rplpwr 11982 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd 𝐵) = 1)) | ||
Theorem | rppwr 11983 | If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | sqgcd 11984 | Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) = ((𝑀↑2) gcd (𝑁↑2))) | ||
Theorem | dvdssqlem 11985 | Lemma for dvdssq 11986. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | dvdssq 11986 | Two numbers are divisible iff their squares are. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | bezoutr 11987 | Partial converse to bezout 11966. Existence of a linear combination does not set the GCD, but it does upper bound it. (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) → (𝐴 gcd 𝐵) ∥ ((𝐴 · 𝑋) + (𝐵 · 𝑌))) | ||
Theorem | bezoutr1 11988 | Converse of bezout 11966 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 1 → (𝐴 gcd 𝐵) = 1)) | ||
Theorem | nnmindc 11989* | An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.) |
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴) | ||
Theorem | nnminle 11990* | The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 11989. (Contributed by Jim Kingdon, 26-Sep-2024.) |
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵) | ||
Theorem | nnwodc 11991* | Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.) |
⊢ ((𝐴 ⊆ ℕ ∧ ∃𝑤 𝑤 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | uzwodc 11992* | Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.) |
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘) | ||
Theorem | nnwofdc 11993* | Well-ordering principle: any inhabited decidable set of positive integers has a least element. This version allows 𝑥 and 𝑦 to be present in 𝐴 as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.) |
⊢ Ⅎ𝑥𝐴 & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ ∃𝑧 𝑧 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) | ||
Theorem | nnwosdc 11994* | Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.) |
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((∃𝑥 ∈ ℕ 𝜑 ∧ ∀𝑥 ∈ ℕ DECID 𝜑) → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦))) | ||
Theorem | nn0seqcvgd 11995* | A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝜑 → 𝐹:ℕ0⟶ℕ0) & ⊢ (𝜑 → 𝑁 = (𝐹‘0)) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘))) ⇒ ⊢ (𝜑 → (𝐹‘𝑁) = 0) | ||
Theorem | ialgrlem1st 11996 | Lemma for ialgr0 11998. Expressing algrflemg 6209 in a form suitable for theorems such as seq3-1 10416 or seqf 10417. (Contributed by Jim Kingdon, 22-Jul-2021.) |
⊢ (𝜑 → 𝐹:𝑆⟶𝑆) ⇒ ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝐹 ∘ 1st )𝑦) ∈ 𝑆) | ||
Theorem | ialgrlemconst 11997 | Lemma for ialgr0 11998. Closure of a constant function, in a form suitable for theorems such as seq3-1 10416 or seqf 10417. (Contributed by Jim Kingdon, 22-Jul-2021.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑍 × {𝐴})‘𝑥) ∈ 𝑆) | ||
Theorem | ialgr0 11998 | The value of the algorithm iterator 𝑅 at 0 is the initial state 𝐴. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) ⇒ ⊢ (𝜑 → (𝑅‘𝑀) = 𝐴) | ||
Theorem | algrf 11999 |
An algorithm is a step function 𝐹:𝑆⟶𝑆 on a state space 𝑆.
An algorithm acts on an initial state 𝐴 ∈ 𝑆 by iteratively applying
𝐹 to give 𝐴, (𝐹‘𝐴), (𝐹‘(𝐹‘𝐴)) and so
on. An algorithm is said to halt if a fixed point of 𝐹 is
reached
after a finite number of iterations.
The algorithm iterator 𝑅:ℕ0⟶𝑆 "runs" the algorithm 𝐹 so that (𝑅‘𝑘) is the state after 𝑘 iterations of 𝐹 on the initial state 𝐴. Domain and codomain of the algorithm iterator 𝑅. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) ⇒ ⊢ (𝜑 → 𝑅:𝑍⟶𝑆) | ||
Theorem | algrp1 12000 | The value of the algorithm iterator 𝑅 at (𝐾 + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐹:𝑆⟶𝑆) ⇒ ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝑅‘(𝐾 + 1)) = (𝐹‘(𝑅‘𝐾))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |