P. 165 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16401-16500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sadcp1 16401*	The carry sequence (which is a sequence of wffs, encoded as 1o and ∅) is defined recursively as the carry operation applied to the previous carry and the two current inputs. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ cadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁))))
Theorem	sadval 16402*	The full adder sequence is the half adder function applied to the inputs and the carry sequence. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ hadd(𝑁 ∈ 𝐴, 𝑁 ∈ 𝐵, ∅ ∈ (𝐶‘𝑁))))
Theorem	sadcaddlem 16403*	Lemma for sadcadd 16404. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐾 = ◡(bits ↾ ℕ0)    &   ⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))    ⇒   ⊢ (𝜑 → (∅ ∈ (𝐶‘(𝑁 + 1)) ↔ (2↑(𝑁 + 1)) ≤ ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1)))))))
Theorem	sadcadd 16404*	Non-recursive definition of the carry sequence. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐾 = ◡(bits ↾ ℕ0)    ⇒   ⊢ (𝜑 → (∅ ∈ (𝐶‘𝑁) ↔ (2↑𝑁) ≤ ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁))))))
Theorem	sadadd2lem 16405*	Lemma for sadadd2 16406. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐾 = ◡(bits ↾ ℕ0)    &   ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))    ⇒   ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^(𝑁 + 1)))) + if(∅ ∈ (𝐶‘(𝑁 + 1)), (2↑(𝑁 + 1)), 0)) = ((𝐾‘(𝐴 ∩ (0..^(𝑁 + 1)))) + (𝐾‘(𝐵 ∩ (0..^(𝑁 + 1))))))
Theorem	sadadd2 16406*	Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 8-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐾 = ◡(bits ↾ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) + if(∅ ∈ (𝐶‘𝑁), (2↑𝑁), 0)) = ((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))))
Theorem	sadadd3 16407*	Sum of initial segments of the sadd sequence. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ 𝐾 = ◡(bits ↾ ℕ0)    ⇒   ⊢ (𝜑 → ((𝐾‘((𝐴 sadd 𝐵) ∩ (0..^𝑁))) mod (2↑𝑁)) = (((𝐾‘(𝐴 ∩ (0..^𝑁))) + (𝐾‘(𝐵 ∩ (0..^𝑁)))) mod (2↑𝑁)))
Theorem	sadcl 16408	The sum of two sequences is a sequence. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) ⊆ ℕ0)
Theorem	sadcom 16409	The adder sequence function is commutative. (Contributed by Mario Carneiro, 5-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 sadd 𝐵) = (𝐵 sadd 𝐴))
Theorem	saddisjlem 16410*	Lemma for sadadd 16413. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ (𝜑 → (𝐴 ∩ 𝐵) = ∅)    &   ⊢ 𝐶 = seq0((𝑐 ∈ 2o, 𝑚 ∈ ℕ0 ↦ if(cadd(𝑚 ∈ 𝐴, 𝑚 ∈ 𝐵, ∅ ∈ 𝑐), 1o, ∅)), (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ∅, (𝑛 − 1))))    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝑁 ∈ (𝐴 sadd 𝐵) ↔ 𝑁 ∈ (𝐴 ∪ 𝐵)))
Theorem	saddisj 16411	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 16412*	Lemma for sadadd 16413. (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 16413	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 1594 and df-cad 1607. 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 16414	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 16415	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 16416	Lemma for sadass 16417. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐶 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((𝐴 sadd 𝐵) sadd 𝐶) ∩ (0..^𝑁)) = ((𝐴 sadd (𝐵 sadd 𝐶)) ∩ (0..^𝑁)))
Theorem	sadass 16417	Sequence addition is associative. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0 ∧ 𝐶 ⊆ ℕ0) → ((𝐴 sadd 𝐵) sadd 𝐶) = (𝐴 sadd (𝐵 sadd 𝐶)))
Theorem	sadeq 16418	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 16419	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 16420	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 16421*	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 16422*	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 16423*	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 16424*	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 16425*	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 16426*	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 16427*	Define the addition of two bit sequences, using df-had 1594 and df-cad 1607 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 16428*	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 16429*	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 16430	The product of two sequences is a sequence. (Contributed by Mario Carneiro, 19-Sep-2016.)
⊢ ((𝐴 ⊆ ℕ0 ∧ 𝐵 ⊆ ℕ0) → (𝐴 smul 𝐵) ⊆ ℕ0)
Theorem	smu01lem 16431*	Lemma for smu01 16432 and smu02 16433. (Contributed by Mario Carneiro, 19-Sep-2016.)
⊢ (𝜑 → 𝐴 ⊆ ℕ0)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ0)    &   ⊢ ((𝜑 ∧ (𝑘 ∈ ℕ0 ∧ 𝑛 ∈ ℕ0)) → ¬ (𝑘 ∈ 𝐴 ∧ (𝑛 − 𝑘) ∈ 𝐵))    ⇒   ⊢ (𝜑 → (𝐴 smul 𝐵) = ∅)
Theorem	smu01 16432	Multiplication of a sequence by 0 on the right. (Contributed by Mario Carneiro, 19-Sep-2016.)
⊢ (𝐴 ⊆ ℕ0 → (𝐴 smul ∅) = ∅)
Theorem	smu02 16433	Multiplication of a sequence by 0 on the left. (Contributed by Mario Carneiro, 9-Sep-2016.)
⊢ (𝐴 ⊆ ℕ0 → (∅ smul 𝐴) = ∅)
Theorem	smupval 16434*	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 16435*	Rewrite smupp1 16426 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 16436*	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 16437	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 16438	Lemma for smumul 16439. (Contributed by Mario Carneiro, 22-Sep-2016.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (((bits‘𝐴) ∩ (0..^𝑁)) smul (bits‘𝐵)) = (bits‘((𝐴 mod (2↑𝑁)) · 𝐵)))
Theorem	smumul 16439	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 16397, whose correctness is verified in sadadd 16413. 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‘(𝐴 · 𝐵)))
6.1.7  The greatest common divisor operator
Syntax	cgcd 16440	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 16441*	Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 29974). For an alternate definition, based on the definition in [ApostolNT] p. 15, see dfgcd2 16493. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < )))
Theorem	gcdval 16442*	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 16443	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 16444*	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 16445*	Lemma for gcdn0cl 16448, gcddvds 16449 and dvdslegcd 16450. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ 𝐴 𝑧 ∥ 𝑛}    ⇒   ⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑛 ∈ 𝐴 𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))
Theorem	gcdcllem2 16446*	Lemma for gcdn0cl 16448, gcddvds 16449 and dvdslegcd 16450. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛}    &   ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆)
Theorem	gcdcllem3 16447*	Lemma for gcdn0cl 16448, gcddvds 16449 and dvdslegcd 16450. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛}    &   ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}    ⇒   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < ))))
Theorem	gcdn0cl 16448	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcddvds 16449	The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
Theorem	dvdslegcd 16450	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 16451	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 16452	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcdnncl 16453	Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcdcld 16454	Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcd2n0cl 16455	Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	zeqzmulgcd 16456*	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 16457	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 16458	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 16459	The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	gcdcomd 16460	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	divgcdnn 16461	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 16462	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 16463	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 16464	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 16465	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 16466	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 16467	The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁)
Theorem	gcdneg 16468	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁))
Theorem	neggcd 16469	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁))
Theorem	gcdaddmlem 16470	Lemma for gcdaddm 16471. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐾 ∈ ℤ    &   ⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑁 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))
Theorem	gcdaddm 16471	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 16472	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 16473	The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁))
Theorem	gcd1 16474	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	gcdabs1 16475	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 16476	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	gcdabs 16477	The gcd of two integers is the same as that of their absolute values. (Contributed by Paul Chapman, 31-Mar-2011.) (Proof shortened by SN, 15-Sep-2024.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) gcd (abs‘𝑁)) = (𝑀 gcd 𝑁))
Theorem	gcdabsOLD 16478	Obsolete version of gcdabs 16477 as of 15-Sep-2024. (Contributed by Paul Chapman, 31-Mar-2011.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((abs‘𝑀) gcd (abs‘𝑁)) = (𝑀 gcd 𝑁))
Theorem	modgcd 16479	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 16480	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 16481	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 16482	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 16483	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 16484	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 16485	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
6.1.8  Bézout's identity
Theorem	bezoutlem1 16486*	Lemma for bezout 16490. (Contributed by Mario Carneiro, 15-Mar-2014.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀))
Theorem	bezoutlem2 16487*	Lemma for bezout 16490. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	bezoutlem3 16488*	Lemma for bezout 16490. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶))
Theorem	bezoutlem4 16489*	Lemma for bezout 16490. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀)
Theorem	bezout 16490*	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 16491	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 16492	Biconditional form of dvdsgcd 16491. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁)))
Theorem	dfgcd2 16493*	Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))
Theorem	gcdass 16494	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 16495	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 16496	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 16497	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 16498	Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶)))
Theorem	gcdzeq 16499	A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 16500. (Contributed by AV, 1-Jul-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵))
Theorem	gcdeq 16500	𝐴 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 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵))