![]() |
Metamath
Proof Explorer Theorem List (p. 157 of 437) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-28364) |
![]() (28365-29889) |
![]() (29890-43671) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sadcom 15601 | The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴)) | ||
Theorem | saddisjlem 15602* | Lemma for sadadd 15605. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅) & ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1)))) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵))) | ||
Theorem | saddisj 15603 | 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 15604* | Lemma for sadadd 15605. (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 15605 |
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 1652 and df-cad 1665.
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 15606 | 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 15607 | 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 15608 | Lemma for sadass 15609. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ (𝜑 → 𝐶 ⊆ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁))) | ||
Theorem | sadass 15609 | Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶))) | ||
Theorem | sadeq 15610 | 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 15611 | 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 15612 | 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 15613* | 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 15614* | 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 15615* | 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 15616* | 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 15617* | 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 15618* | 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 15619* | Define the addition of two bit sequences, using df-had 1652 and df-cad 1665 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 15620* | 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 15621* | 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 15622 | The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 smul 𝐵) ⊆ ℕ0) | ||
Theorem | smu01lem 15623* | Lemma for smu01 15624 and smu02 15625. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ (𝜑 → 𝐴 ⊆ ℕ0) & ⊢ (𝜑 → 𝐵 ⊆ ℕ0) & ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0)) → ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵)) ⇒ ⊢ (𝜑 → (𝐴 smul 𝐵) = ∅) | ||
Theorem | smu01 15624 | Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (𝐴 smul ∅) = ∅) | ||
Theorem | smu02 15625 | Multiplication of a sequence by 0 on the left. (Contributed by Mario Carneiro, 9-Sep-2016.) |
⊢ (𝐴 ⊆ ℕ0 → (∅ smul 𝐴) = ∅) | ||
Theorem | smupval 15626* | 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 15627* | Rewrite smupp1 15618 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 15628* | 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 15629 | 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 15630 | Lemma for smumul 15631. (Contributed by Mario Carneiro, 22-Sep-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵))) | ||
Theorem | smumul 15631 |
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 15589, whose correctness is
verified in sadadd 15605.
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 15632 | Extend the definition of a class to include the greatest common divisor operator. |
class gcd | ||
Definition | df-gcd 15633* | Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 27906). For an alternate definition, based on the definition in [ApostolNT] p. 15, see dfgcd2 15679. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < ))) | ||
Theorem | gcdval 15634* | 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 15635 | 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 15636* | 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 15637* | Lemma for gcdn0cl 15640, gcddvds 15641 and dvdslegcd 15642. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ 𝐴 𝑧 ∥ 𝑛} ⇒ ⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑛 ∈ 𝐴 𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥)) | ||
Theorem | gcdcllem2 15638* | Lemma for gcdn0cl 15640, gcddvds 15641 and dvdslegcd 15642. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} & ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆) | ||
Theorem | gcdcllem3 15639* | Lemma for gcdn0cl 15640, gcddvds 15641 and dvdslegcd 15642. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛} & ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)} ⇒ ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < )))) | ||
Theorem | gcdn0cl 15640 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcddvds 15641 | The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁)) | ||
Theorem | dvdslegcd 15642 | 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 15643 | 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 15644 | Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcdnncl 15645 | Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | gcdcld 15646 | Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0) | ||
Theorem | gcd2n0cl 15647 | Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ) | ||
Theorem | zeqzmulgcd 15648* | 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 15649 | 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 15650 | 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 15651 | The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀)) | ||
Theorem | divgcdnn 15652 | 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 15653 | 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 15654 | 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 15655 | 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 15656 | 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 15657 | 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 15658 | The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁) | ||
Theorem | gcdneg 15659 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | neggcd 15660 | Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁)) | ||
Theorem | gcdaddmlem 15661 | Lemma for gcdaddm 15662. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ 𝐾 ∈ ℤ & ⊢ 𝑀 ∈ ℤ & ⊢ 𝑁 ∈ ℤ ⇒ ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁)) | ||
Theorem | gcdaddm 15662 | 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 15663 | 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 15664 | The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.) |
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁)) | ||
Theorem | gcd1 15665 | 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 15666 | 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 15667 | 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 15668 | 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 15669 | 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 15670 | 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 | 6gcd4e2 15671 | 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 15672* | Lemma for bezout 15676. (Contributed by Mario Carneiro, 15-Mar-2014.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀)) | ||
Theorem | bezoutlem2 15673* | Lemma for bezout 15676. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → 𝐺 ∈ 𝑀) | ||
Theorem | bezoutlem3 15674* | Lemma for bezout 15676. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶)) | ||
Theorem | bezoutlem4 15675* | Lemma for bezout 15676. (Contributed by Mario Carneiro, 22-Feb-2014.) |
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))} & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ 𝐺 = inf(𝑀, ℝ, < ) & ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0)) ⇒ ⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀) | ||
Theorem | bezout 15676* | 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 15677 | 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 15678 | Biconditional form of dvdsgcd 15677. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁))) | ||
Theorem | dfgcd2 15679* | Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷)))) | ||
Theorem | gcdass 15680 | 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 15681 | 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 15682 | 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 15683 | 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 15684 | Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶))) | ||
Theorem | gcdmultiple 15685 | 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 15686 | Extend gcdmultiple 15685 so 𝑁 can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀) | ||
Theorem | gcdzeq 15687 | A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 15688. (Contributed by AV, 1-Jul-2020.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵)) | ||
Theorem | gcdeq 15688 | 𝐴 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 15689 | Unidirectional form of dvdssq 15696. (Contributed by Scott Fenton, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | dvdsmulgcd 15690 | A divisibility equivalent for odmulg 18368. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴)))) | ||
Theorem | rpmulgcd 15691 | 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 15692 | 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 15693 | 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 15694 | 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 15695 | Lemma for dvdssq 15696. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2))) | ||
Theorem | dvdssq 15696 | 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 15697 | Partial converse to bezout 15676. 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 15698 | Converse of bezout 15676 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 | nn0seqcvgd 15699* | 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 | seq1st 15700 | A sequence whose iteration function ignores the second argument is only affected by the first point of the initial value function. (Contributed by Mario Carneiro, 11-Feb-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴})) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝐴 ∈ 𝑉) → 𝑅 = seq𝑀((𝐹 ∘ 1st ), {〈𝑀, 𝐴〉})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |