Home | Metamath
Proof Explorer Theorem List (p. 159 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sadcl 15801 | The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0) | ||
Theorem | sadcom 15802 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴)) | ||
Theorem | saddisjlem 15803* | Lemma for sadadd 15806. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) | ||
Theorem | saddisj 15804 | The sum of disjoint sequences is the union of the sequences. (In this case, there are no carried bits.) (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) ⇒ ⊢ (𝜑 → (𝐴 sadd 𝐵) = (𝐴 ∪ 𝐵)) | ||
Theorem | sadaddlem 15805* | Lemma for sadadd 15806. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ (bits‘𝐴), 𝑚 ∈ (bits‘𝐵), ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ 𝐾 = ◡(bits ↾ ℕ0) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((bits‘𝐴) sadd (bits‘𝐵)) ∩ (0..^𝑁)) = (bits‘((𝐴 + 𝐵) mod (2↑𝑁)))) | ||
Theorem | sadadd 15806 |
For sequences that correspond to valid integers, the adder sequence
function produces the sequence for the sum. This is effectively a proof
of the correctness of the ripple carry adder, implemented with logic
gates corresponding to df-had 1585 and df-cad 1599.
It is interesting to consider in what sense the sadd function can be said to be "adding" things outside the range of the bits function, that is, when adding sequences that are not eventually constant and so do not denote any integer. The correct interpretation is that the sequences are representations of 2-adic integers, which have a natural ring structure. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((bits‘𝐴) sadd (bits‘𝐵)) = (bits‘(𝐴 + 𝐵))) | ||
Theorem | sadid1 15807 | The adder sequence function has a left identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (𝐴 sadd ∅) = 𝐴) | ||
Theorem | sadid2 15808 | The adder sequence function has a right identity, the empty set, which is the representation of the integer zero. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (∅ sadd 𝐴) = 𝐴) | ||
Theorem | sadasslem 15809 | Lemma for sadass 15810. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝐶 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) | ||
Theorem | sadass 15810 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶))) | ||
Theorem | sadeq 15811 | Any element of a sequence sum only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 sadd 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) sadd (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) | ||
Theorem | bitsres 15812 | Restrict the bits of a number to an upper integer set. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((bits‘𝐴) ∩ (ℤ≥‘𝑁)) = (bits‘((⌊‘(𝐴 / (2↑𝑁))) · (2↑𝑁)))) | ||
Theorem | bitsuz 15813 | The bits of a number are all at least 𝑁 iff the number is divisible by 2↑𝑁. (Contributed by Mario Carneiro, 21-Sep-2016.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((2↑𝑁) ∥ 𝐴 ↔ (bits‘𝐴) ⊆ (ℤ≥‘𝑁))) | ||
Theorem | bitsshft 15814* | Shifting a bit sequence to the left (toward the more significant bits) causes the number to be multiplied by a power of two. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → {𝑛 ∈ ℕ0 ∣ (𝑛 − 𝑁) ∈ (bits‘𝐴)} = (bits‘(𝐴 · (2↑𝑁)))) | ||
Definition | df-smu 15815* | Define the multiplication of two bit sequences, using repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ smul = (𝑥 ∈ 𝒫 ℕ0, 𝑦 ∈ 𝒫 ℕ0 ↦ {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝑥 ∧ (𝑛 − 𝑚) ∈ 𝑦)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))‘(𝑘 + 1))}) | ||
Theorem | smufval 15816* | The multiplication of two bit sequences as repeated sequence addition. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → (𝐴 smul 𝐵) = {𝑘 ∈ ℕ0 ∣ 𝑘 ∈ (𝑃‘(𝑘 + 1))}) | ||
Theorem | smupf 15817* | The sequence of partial sums of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → 𝑃:ℕ0⟶𝒫 ℕ0) | ||
Theorem | smup0 15818* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → (𝑃‘0) = ∅) | ||
Theorem | smupp1 15819* | The initial element of the partial sum sequence. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑃‘(𝑁 + 1)) = ((𝑃‘𝑁) sadd {𝑛 ∈ ℕ0 ∣ (𝑁 ∈ 𝐴 ∧ (𝑛 − 𝑁) ∈ 𝐵)})) | ||
Theorem | smuval 15820* | Define the addition of two bit sequences, using df-had 1585 and df-cad 1599 bit operations. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘(𝑁 + 1)))) | ||
Theorem | smuval2 15821* | The partial sum sequence stabilizes at 𝑁 after the 𝑁 + 1-th element of the sequence; this stable value is the value of the sequence multiplication. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘(𝑁 + 1))) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 smul 𝐵) ↔ 𝑁 ∈ (𝑃‘𝑀))) | ||
Theorem | smupvallem 15822* | If 𝐴 only has elements less than 𝑁, then all elements of the partial sum sequence past 𝑁 already equal the final value. (Contributed by Mario Carneiro, 20-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝐴 ⊆ (0..^𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁)) ⇒ ⊢ (𝜑 → (𝑃‘𝑀) = (𝐴 smul 𝐵)) | ||
Theorem | smucl 15823 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 smul 𝐵) ⊆ ℕ0) | ||
Theorem | smu01lem 15824* | Lemma for smu01 15825 and smu02 15826. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0)) → ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 smul 𝐵) = ∅) | ||
Theorem | smu01 15825 | Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (𝐴 smul ∅) = ∅) | ||
Theorem | smu02 15826 | Multiplication of a sequence by 0 on the left. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (∅ smul 𝐴) = ∅) | ||
Theorem | smupval 15827* | Rewrite the elements of the partial sum sequence in terms of sequence multiplication. (Contributed by Mario Carneiro, 20-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑃‘𝑁) = ((𝐴 ∩ (0..^𝑁)) smul 𝐵)) | ||
Theorem | smup1 15828* | Rewrite smupp1 15819 using only smul instead of the internal recursive function 𝑃. (Contributed by Mario Carneiro, 20-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 ∩ (0..^(𝑁 + 1))) smul 𝐵) = (((𝐴 ∩ (0..^𝑁)) smul 𝐵) sadd {𝑛 ∈ ℕ0 ∣ (𝑁 ∈ 𝐴 ∧ (𝑛 − 𝑁) ∈ 𝐵)})) | ||
Theorem | smueqlem 15829* | Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ 𝑃 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ 𝐵)})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ 𝑄 = seq0((𝑝 ∈ 𝒫 ℕ0, 𝑚 ∈ ℕ0 ↦ (𝑝 sadd {𝑛 ∈ ℕ0 ∣ (𝑚 ∈ 𝐴 ∧ (𝑛 − 𝑚) ∈ (𝐵 ∩ (0..^𝑁)))})), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) ⇒ ⊢ (𝜑 → ((𝐴 smul 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) smul (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) | ||
Theorem | smueq 15830 | Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐴 smul 𝐵) ∩ (0..^𝑁)) = (((𝐴 ∩ (0..^𝑁)) smul (𝐵 ∩ (0..^𝑁))) ∩ (0..^𝑁))) | ||
Theorem | smumullem 15831 | Lemma for smumul 15832. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) | ||
Theorem | smumul 15832 |
For sequences that correspond to valid integers, the sequence
multiplication function produces the sequence for the product. This is
effectively a proof of the correctness of the multiplication process,
implemented in terms of logic gates for df-sad 15790, whose correctness is
verified in sadadd 15806.
Outside this range, the sequences cannot be representing integers, but the smul function still "works". This extended function is best interpreted in terms of the ring structure of the 2-adic integers. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((bits‘𝐴) smul (bits‘𝐵)) = (bits‘(𝐴 · 𝐵))) | ||
Syntax | cgcd 15833 | Extend the definition of a class to include the greatest common divisor operator. |
class gcd | ||
Definition | df-gcd 15834* | Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 28164). For an alternate definition, based on the definition in [ApostolNT] p. 15, see dfgcd2 15884. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) | ||
Theorem | gcdval 15835* | 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 15836 | 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 15837* | 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 | gcdcllem1 15838* | Lemma for gcdn0cl 15841, gcddvds 15842 and dvdslegcd 15843. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ 𝐴 𝑧 ∥ 𝑛} ⇒ ⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑛 ∈ 𝐴 𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | gcdcllem2 15839* | Lemma for gcdn0cl 15841, gcddvds 15842 and dvdslegcd 15843. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} & ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆) | ||
Theorem | gcdcllem3 15840* | Lemma for gcdn0cl 15841, gcddvds 15842 and dvdslegcd 15843. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} & ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} ⇒ ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < )))) | ||
Theorem | gcdn0cl 15841 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcddvds 15842 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) | ||
Theorem | dvdslegcd 15843 | 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 15844 | 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 15845 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcdnncl 15846 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcdcld 15847 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcd2n0cl 15848 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | zeqzmulgcd 15849* | 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 15850 | 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 15851 | 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 15852 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | divgcdnn 15853 | 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 15854 | 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 15855 | 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 15856 | 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 15857 | 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 15858 | 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 15859 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁) | ||
Theorem | gcdneg 15860 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | neggcd 15861 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | gcdaddmlem 15862 | Lemma for gcdaddm 15863. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ 𝐾 ∈ ℤ & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑁 ∈ ℤ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) | ||
Theorem | gcdaddm 15863 | 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 15864 | 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 15865 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁)) | ||
Theorem | gcd1 15866 | 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 15867 | 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 15868 | 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 15869 | 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 15870 | 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 15871 | 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 15872 | 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 | gcdmultiplez 15873 | The GCD of a multiple of an integer is the integer itself. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by AV, 12-Jan-2023.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdmultiple 15874 | The GCD of a multiple of a positive integer is the positive integer itself. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by AV, 12-Jan-2023.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | dvdsgcdidd 15875 | 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 15876 | 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 | bezoutlem1 15877* | Lemma for bezout 15881. (Contributed by Mario Carneiro, 15-Mar-2014.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) | ||
Theorem | bezoutlem2 15878* | Lemma for bezout 15881. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | bezoutlem3 15879* | Lemma for bezout 15881. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶)) | ||
Theorem | bezoutlem4 15880* | Lemma for bezout 15881. (Contributed by Mario Carneiro, 22-Feb-2014.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀) | ||
Theorem | bezout 15881* | Bézout's identity: For any integers 𝐴 and 𝐵, there are integers 𝑥, 𝑦 such that (𝐴 gcd 𝐵) = 𝐴 · 𝑥 + 𝐵 · 𝑦. This is Metamath 100 proof #60. (Contributed by Mario Carneiro, 22-Feb-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦))) | ||
Theorem | dvdsgcd 15882 | 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 15883 | Biconditional form of dvdsgcd 15882. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁))) | ||
Theorem | dfgcd2 15884* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) | ||
Theorem | gcdass 15885 | 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 15886 | 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 15887 | 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 15888 | 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 15889 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶))) | ||
Theorem | gcdmultipleOLD 15890 | Obsolete proof of gcdmultiple 15874 as of 12-Jan-2024. 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.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdmultiplezOLD 15891 | Obsolete proof of gcdmultiplez 15873 as of 12-Jan-2024. Extend gcdmultiple 15874 so 𝑁 can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdzeq 15892 | A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 15893. (Contributed by AV, 1-Jul-2020.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵)) | ||
Theorem | gcdeq 15893 | 𝐴 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 15894 | Unidirectional form of dvdssq 15901. (Contributed by Scott Fenton, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | dvdsmulgcd 15895 | A divisibility equivalent for odmulg 18614. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) | ||
Theorem | rpmulgcd 15896 | 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 15897 | 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 15898 | 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 15899 | 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 15900 | Lemma for dvdssq 15901. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |