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	gcdn0val 16401*	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 16402*	Lemma for gcdn0cl 16405, gcddvds 16406 and dvdslegcd 16407. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ 𝐴 𝑧 ∥ 𝑛}    ⇒   ⊢ ((𝐴 ⊆ ℤ ∧ ∃𝑛 ∈ 𝐴 𝑛 ≠ 0) → (𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥))
Theorem	gcdcllem2 16403*	Lemma for gcdn0cl 16405, gcddvds 16406 and dvdslegcd 16407. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛}    &   ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑅 = 𝑆)
Theorem	gcdcllem3 16404*	Lemma for gcdn0cl 16405, gcddvds 16406 and dvdslegcd 16407. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ 𝑆 = {𝑧 ∈ ℤ ∣ ∀𝑛 ∈ {𝑀, 𝑁}𝑧 ∥ 𝑛}    &   ⊢ 𝑅 = {𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁)}    ⇒   ⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (sup(𝑅, ℝ, < ) ∈ ℕ ∧ (sup(𝑅, ℝ, < ) ∥ 𝑀 ∧ sup(𝑅, ℝ, < ) ∥ 𝑁) ∧ ((𝐾 ∈ ℤ ∧ 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ≤ sup(𝑅, ℝ, < ))))
Theorem	gcdn0cl 16405	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcddvds 16406	The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
Theorem	dvdslegcd 16407	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 16408	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 16409	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcdnncl 16410	Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcdcld 16411	Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcd2n0cl 16412	Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	zeqzmulgcd 16413*	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 16414	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 16415	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 16416	The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	gcdcomd 16417	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	divgcdnn 16418	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 16419	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 16420	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 16421	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 16422	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 16423	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 16424	The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁)
Theorem	gcdneg 16425	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁))
Theorem	neggcd 16426	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁))
Theorem	gcdaddmlem 16427	Lemma for gcdaddm 16428. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐾 ∈ ℤ    &   ⊢ 𝑀 ∈ ℤ    &   ⊢ 𝑁 ∈ ℤ    ⇒   ⊢ (𝑀 gcd 𝑁) = (𝑀 gcd ((𝐾 · 𝑀) + 𝑁))
Theorem	gcdaddm 16428	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 16429	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 16430	The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁))
Theorem	gcd1 16431	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 16432	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 16433	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 16434	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	modgcd 16435	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 16436	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 16437	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 16438	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 16439	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 16440	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 16441	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 16442*	Lemma for bezout 16446. (Contributed by Mario Carneiro, 15-Mar-2014.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝐴 ≠ 0 → (abs‘𝐴) ∈ 𝑀))
Theorem	bezoutlem2 16443*	Lemma for bezout 16446. (Contributed by Mario Carneiro, 15-Mar-2014.) ( Revised by AV, 30-Sep-2020.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → 𝐺 ∈ 𝑀)
Theorem	bezoutlem3 16444*	Lemma for bezout 16446. (Contributed by Mario Carneiro, 22-Feb-2014.) ( Revised by AV, 30-Sep-2020.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐶 ∈ 𝑀 → 𝐺 ∥ 𝐶))
Theorem	bezoutlem4 16445*	Lemma for bezout 16446. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ 𝑀 = {𝑧 ∈ ℕ ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑧 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))}    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ 𝐺 = inf(𝑀, ℝ, < )    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∈ 𝑀)
Theorem	bezout 16446*	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 16447	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 16448	Biconditional form of dvdsgcd 16447. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁)))
Theorem	dfgcd2 16449*	Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))
Theorem	gcdass 16450	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 16451	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 16452	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 16453	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 16454	Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶)))
Theorem	gcdzeq 16455	A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 16456. (Contributed by AV, 1-Jul-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵))
Theorem	gcdeq 16456	𝐴 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 16457	Unidirectional form of dvdssq 16470. (Contributed by Scott Fenton, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀↑2) ∥ (𝑁↑2)))
Theorem	dvdsexpim 16458	If two numbers are divisible, so are their nonnegative exponents. Similar to dvdssqim 16457 for nonnegative exponents. (Contributed by Steven Nguyen, 2-Apr-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ 𝐵 → (𝐴↑𝑁) ∥ (𝐵↑𝑁)))
Theorem	dvdsmulgcd 16459	A divisibility equivalent for odmulg 19461. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
Theorem	rpmulgcd 16460	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 16461	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	rprpwr 16462	If 𝐴 and 𝐵 are relatively prime, then so are 𝐴 and 𝐵↑𝑁. Originally a subproof of rppwr 16463. (Contributed by SN, 21-Aug-2024.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐴 gcd 𝐵) = 1 → (𝐴 gcd (𝐵↑𝑁)) = 1))
Theorem	rppwr 16463	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	nn0rppwr 16464	If 𝐴 and 𝐵 are relatively prime, then so are 𝐴↑𝑁 and 𝐵↑𝑁. rppwr 16463 extended to nonnegative integers. Less general than rpexp12i 16627. (Contributed by Steven Nguyen, 4-Apr-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑁) gcd (𝐵↑𝑁)) = 1))
Theorem	sqgcd 16465	Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((𝑀 gcd 𝑁)↑2) = ((𝑀↑2) gcd (𝑁↑2)))
Theorem	expgcd 16466	Exponentiation distributes over GCD. sqgcd 16465 extended to nonnegative exponents. (Contributed by Steven Nguyen, 4-Apr-2023.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))
Theorem	nn0expgcd 16467	Exponentiation distributes over GCD. nn0gcdsq 16655 extended to nonnegative exponents. expgcd 16466 extended to nonnegative bases. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))
Theorem	zexpgcd 16468	Exponentiation distributes over GCD. zgcdsq 16656 extended to nonnegative exponents. nn0expgcd 16467 extended to integer bases by symmetry. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑𝑁) = ((𝐴↑𝑁) gcd (𝐵↑𝑁)))
Theorem	dvdssqlem 16469	Lemma for dvdssq 16470. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2)))
Theorem	dvdssq 16470	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 16471	Partial converse to bezout 16446. 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 16472	Converse of bezout 16446 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 1 → (𝐴 gcd 𝐵) = 1))
6.1.9  Algorithms
Theorem	nn0seqcvgd 16473*	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 16474	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 ), {⟨𝑀, 𝐴⟩}))
Theorem	algr0 16475	The value of the algorithm iterator 𝑅 at 0 is the initial state 𝐴. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ (𝜑 → (𝑅‘𝑀) = 𝐴)
Theorem	algrf 16476	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 16477	The value of the algorithm iterator 𝑅 at (𝐾 + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆⟶𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝑅‘(𝐾 + 1)) = (𝐹‘(𝑅‘𝐾)))
Theorem	alginv 16478*	If 𝐼 is an invariant of 𝐹, then its value is unchanged after any number of iterations of 𝐹. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐹:𝑆⟶𝑆    &   ⊢ (𝑥 ∈ 𝑆 → (𝐼‘(𝐹‘𝑥)) = (𝐼‘𝑥))    ⇒   ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐾 ∈ ℕ0) → (𝐼‘(𝑅‘𝐾)) = (𝐼‘(𝑅‘0)))
Theorem	algcvg 16479*	One way to prove that an algorithm halts is to construct a countdown function 𝐶:𝑆⟶ℕ0 whose value is guaranteed to decrease for each iteration of 𝐹 until it reaches 0. That is, if 𝑋 ∈ 𝑆 is not a fixed point of 𝐹, then (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋). If 𝐶 is a countdown function for algorithm 𝐹, the sequence (𝐶‘(𝑅‘𝑘)) reaches 0 after at most 𝑁 steps, where 𝑁 is the value of 𝐶 for the initial state 𝐴. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹:𝑆⟶𝑆    &   ⊢ 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐶:𝑆⟶ℕ0    &   ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))    &   ⊢ 𝑁 = (𝐶‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑆 → (𝐶‘(𝑅‘𝑁)) = 0)
Theorem	algcvgblem 16480	Lemma for algcvgb 16481. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0))))
Theorem	algcvgb 16481	Two ways of expressing that 𝐶 is a countdown function for algorithm 𝐹. The first is used in these theorems. The second states the condition more intuitively as a conjunction: if the countdown function's value is currently nonzero, it must decrease at the next step; if it has reached zero, it must remain zero at the next step. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ 𝐹:𝑆⟶𝑆    &   ⊢ 𝐶:𝑆⟶ℕ0    ⇒   ⊢ (𝑋 ∈ 𝑆 → (((𝐶‘(𝐹‘𝑋)) ≠ 0 → (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋)) ↔ (((𝐶‘𝑋) ≠ 0 → (𝐶‘(𝐹‘𝑋)) < (𝐶‘𝑋)) ∧ ((𝐶‘𝑋) = 0 → (𝐶‘(𝐹‘𝑋)) = 0))))
Theorem	algcvga 16482*	The countdown function 𝐶 remains 0 after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹:𝑆⟶𝑆    &   ⊢ 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐶:𝑆⟶ℕ0    &   ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))    &   ⊢ 𝑁 = (𝐶‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝐾)) = 0))
Theorem	algfx 16483*	If 𝐹 reaches a fixed point when the countdown function 𝐶 reaches 0, 𝐹 remains fixed after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹:𝑆⟶𝑆    &   ⊢ 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐶:𝑆⟶ℕ0    &   ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))    &   ⊢ 𝑁 = (𝐶‘𝐴)    &   ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘𝑧) = 0 → (𝐹‘𝑧) = 𝑧))    ⇒   ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))
6.1.10  Euclid's Algorithm
Theorem	eucalgval2 16484*	The value of the step function 𝐸 for Euclid's Algorithm on an ordered pair. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (𝑀𝐸𝑁) = if(𝑁 = 0, ⟨𝑀, 𝑁⟩, ⟨𝑁, (𝑀 mod 𝑁)⟩))
Theorem	eucalgval 16485*	Euclid's Algorithm eucalg 16490 computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. The value of the step function 𝐸 for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    ⇒   ⊢ (𝑋 ∈ (ℕ0 × ℕ0) → (𝐸‘𝑋) = if((2nd ‘𝑋) = 0, 𝑋, ⟨(2nd ‘𝑋), ( mod ‘𝑋)⟩))
Theorem	eucalgf 16486*	Domain and codomain of the step function 𝐸 for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 28-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    ⇒   ⊢ 𝐸:(ℕ0 × ℕ0)⟶(ℕ0 × ℕ0)
Theorem	eucalginv 16487*	The invariant of the step function 𝐸 for Euclid's Algorithm is the gcd operator applied to the state. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    ⇒   ⊢ (𝑋 ∈ (ℕ0 × ℕ0) → ( gcd ‘(𝐸‘𝑋)) = ( gcd ‘𝑋))
Theorem	eucalglt 16488*	The second member of the state decreases with each iteration of the step function 𝐸 for Euclid's Algorithm. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Mario Carneiro, 29-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    ⇒   ⊢ (𝑋 ∈ (ℕ0 × ℕ0) → ((2nd ‘(𝐸‘𝑋)) ≠ 0 → (2nd ‘(𝐸‘𝑋)) < (2nd ‘𝑋)))
Theorem	eucalgcvga 16489*	Once Euclid's Algorithm halts after 𝑁 steps, the second element of the state remains 0 . (Contributed by Paul Chapman, 22-Jun-2011.) (Revised by Mario Carneiro, 29-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    &   ⊢ 𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝑁 = (2nd ‘𝐴)    ⇒   ⊢ (𝐴 ∈ (ℕ0 × ℕ0) → (𝐾 ∈ (ℤ≥‘𝑁) → (2nd ‘(𝑅‘𝐾)) = 0))
Theorem	eucalg 16490*	Euclid's Algorithm computes the greatest common divisor of two nonnegative integers by repeatedly replacing the larger of them with its remainder modulo the smaller until the remainder is 0. Theorem 1.15 in [ApostolNT] p. 20. Upon halting, the first member of the final state (𝑅‘𝑁) is equal to the gcd of the values comprising the input state ⟨𝑀, 𝑁⟩. This is Metamath 100 proof #69 (greatest common divisor algorithm). (Contributed by Paul Chapman, 31-Mar-2011.) (Proof shortened by Mario Carneiro, 29-May-2014.)
⊢ 𝐸 = (𝑥 ∈ ℕ0, 𝑦 ∈ ℕ0 ↦ if(𝑦 = 0, ⟨𝑥, 𝑦⟩, ⟨𝑦, (𝑥 mod 𝑦)⟩))    &   ⊢ 𝑅 = seq0((𝐸 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐴 = ⟨𝑀, 𝑁⟩    ⇒   ⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → (1st ‘(𝑅‘𝑁)) = (𝑀 gcd 𝑁))
6.1.11  The least common multiple According to Wikipedia ("Least common multiple", 27-Aug-2020, https://en.wikipedia.org/wiki/Least_common_multiple): "In arithmetic and number theory, the least common multiple, lowest common multiple, or smallest common multiple of two integers a and b, usually denoted by lcm(a, b), is the smallest positive integer that is divisible by both a and b. Since division of integers by zero is undefined, this definition has meaning only if a and b are both different from zero. However, some authors define lcm(a,0) as 0 for all a, which is the result of taking the lcm to be the least upper bound in the lattice of divisibility. ... The lcm of more than two integers is also well-defined: it is the smallest positive integer hat is divisible by each of them." In this section, an operation calculating the least common multiple of two integers (df-lcm 16493) as well as a function mapping a set of integers to their least common multiple (df-lcmf 16494) are provided. Both definitions are valid for all integers, including negative integers and 0, obeying the above mentioned convention. It is shown by lcmfpr 16530 that the two definitions are compatible.
Syntax	clcm 16491	Extend the definition of a class to include the least common multiple operator.
class lcm
Syntax	clcmf 16492	Extend the definition of a class to include the least common multiple function.
class lcm
Definition	df-lcm 16493*	Define the lcm operator. For example, (6 lcm 9) = 18 (ex-lcm 30428). (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
⊢ lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛)}, ℝ, < )))
Definition	df-lcmf 16494*	Define the lcm function on a set of integers. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.)
⊢ lcm = (𝑧 ∈ 𝒫 ℤ ↦ if(0 ∈ 𝑧, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑧 𝑚 ∥ 𝑛}, ℝ, < )))
Theorem	lcmval 16495*	Value of the lcm operator. (𝑀 lcm 𝑁) is the least common multiple of 𝑀 and 𝑁. If either 𝑀 or 𝑁 is 0, the result is defined conventionally as 0. Contrast with df-gcd 16398 and gcdval 16399. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = if((𝑀 = 0 ∨ 𝑁 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)}, ℝ, < )))
Theorem	lcmcom 16496	The lcm operator is commutative. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 lcm 𝑁) = (𝑁 lcm 𝑀))
Theorem	lcm0val 16497	The value, by convention, of the lcm operator when either operand is 0. (Use lcmcom 16496 for a left-hand 0.) (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ (𝑀 ∈ ℤ → (𝑀 lcm 0) = 0)
Theorem	lcmn0val 16498*	The value of the lcm operator when both operands are nonzero. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) = inf({𝑛 ∈ ℕ ∣ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)}, ℝ, < ))
Theorem	lcmcllem 16499*	Lemma for lcmn0cl 16500 and dvdslcm 16501. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ {𝑛 ∈ ℕ ∣ (𝑀 ∥ 𝑛 ∧ 𝑁 ∥ 𝑛)})
Theorem	lcmn0cl 16500	Closure of the lcm operator. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∨ 𝑁 = 0)) → (𝑀 lcm 𝑁) ∈ ℕ)