P. 122 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12101-12200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvdslegcd 12101	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 12102	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 12103	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcdnncl 12104	Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcdcld 12105	Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcd2n0cl 12106	Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	zeqzmulgcd 12107*	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 12108	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 12109	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 12110	The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	gcdcomd 12111	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	divgcdnn 12112	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 12113	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 12114	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 12115	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 12116	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 12117	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 12118	The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁)
Theorem	gcdneg 12119	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁))
Theorem	neggcd 12120	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁))
Theorem	gcdaddm 12121	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 12122	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 12123	The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁))
Theorem	gcd1 12124	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 12125	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 12126	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 12127	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 12128	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 12129	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 12130	The greatest common divisor of a nonnegative integer 𝑀 and a multiple of it is 𝑀 itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd (𝑁 · 𝑀)) = 𝑀)
Theorem	dvdsgcdidd 12131	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 12132	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
5.1.5  Bézout's identity
Theorem	bezoutlemnewy 12133*	Lemma for Bézout's identity. The is-bezout predicate holds for (𝑦 mod 𝑊). (Contributed by Jim Kingdon, 6-Jan-2022.)
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   ⊢ (𝜃 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜃 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜃 → 𝑊 ∈ ℕ)    &   ⊢ (𝜃 → [𝑦 / 𝑟]𝜑)    &   ⊢ (𝜃 → 𝑦 ∈ ℕ0)    &   ⊢ (𝜃 → [𝑊 / 𝑟]𝜑)    ⇒   ⊢ (𝜃 → [(𝑦 mod 𝑊) / 𝑟]𝜑)
Theorem	bezoutlemstep 12134*	Lemma for Bézout's identity. This is the induction step for the proof by induction. (Contributed by Jim Kingdon, 3-Jan-2022.)
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   ⊢ (𝜃 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜃 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜃 → 𝑊 ∈ ℕ)    &   ⊢ (𝜃 → [𝑦 / 𝑟]𝜑)    &   ⊢ (𝜃 → 𝑦 ∈ ℕ0)    &   ⊢ (𝜃 → [𝑊 / 𝑟]𝜑)    &   ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))    &   ⊢ ((𝜃 ∧ [(𝑦 mod 𝑊) / 𝑟]𝜑) → ∃𝑟 ∈ ℕ0 ([(𝑦 mod 𝑊) / 𝑥][𝑊 / 𝑦]𝜓 ∧ 𝜑))    &   ⊢ Ⅎ𝑥𝜃    &   ⊢ Ⅎ𝑟𝜃    ⇒   ⊢ (𝜃 → ∃𝑟 ∈ ℕ0 ([𝑊 / 𝑥]𝜓 ∧ 𝜑))
Theorem	bezoutlemmain 12135*	Lemma for Bézout's identity. This is the main result which we prove by induction and which represents the application of the Extended Euclidean algorithm. (Contributed by Jim Kingdon, 30-Dec-2021.)
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   ⊢ (𝜓 ↔ ∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑟 → (𝑧 ∥ 𝑥 ∧ 𝑧 ∥ 𝑦)))    &   ⊢ (𝜃 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜃 → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜃 → ∀𝑥 ∈ ℕ0 ([𝑥 / 𝑟]𝜑 → ∀𝑦 ∈ ℕ0 ([𝑦 / 𝑟]𝜑 → ∃𝑟 ∈ ℕ0 (𝜓 ∧ 𝜑))))
Theorem	bezoutlema 12136*	Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐴. (Contributed by Jim Kingdon, 30-Dec-2021.)
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   ⊢ (𝜃 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜃 → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜃 → [𝐴 / 𝑟]𝜑)
Theorem	bezoutlemb 12137*	Lemma for Bézout's identity. The is-bezout condition is satisfied by 𝐵. (Contributed by Jim Kingdon, 30-Dec-2021.)
⊢ (𝜑 ↔ ∃𝑠 ∈ ℤ ∃𝑡 ∈ ℤ 𝑟 = ((𝐴 · 𝑠) + (𝐵 · 𝑡)))    &   ⊢ (𝜃 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜃 → 𝐵 ∈ ℕ0)    ⇒   ⊢ (𝜃 → [𝐵 / 𝑟]𝜑)
Theorem	bezoutlemex 12138*	Lemma for Bézout's identity. Existence of a number which we will later show to be the greater common divisor and its decomposition into cofactors. (Contributed by Mario Carneiro and Jim Kingdon, 3-Jan-2022.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℕ0 (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
Theorem	bezoutlemzz 12139*	Lemma for Bézout's identity. Like bezoutlemex 12138 but where ' z ' is any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
Theorem	bezoutlemaz 12140*	Lemma for Bézout's identity. Like bezoutlemzz 12139 but where ' A ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
Theorem	bezoutlembz 12141*	Lemma for Bézout's identity. Like bezoutlemaz 12140 but where ' B ' can be any integer, not just a nonnegative one. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 → (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
Theorem	bezoutlembi 12142*	Lemma for Bézout's identity. Like bezoutlembz 12141 but the greatest common divisor condition is a biconditional, not just an implication. (Contributed by Mario Carneiro and Jim Kingdon, 8-Jan-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑑 ∈ ℕ0 (∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)) ∧ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑑 = ((𝐴 · 𝑥) + (𝐵 · 𝑦))))
Theorem	bezoutlemmo 12143*	Lemma for Bézout's identity. There is at most one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   ⊢ (𝜑 → 𝐸 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐸 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    ⇒   ⊢ (𝜑 → 𝐷 = 𝐸)
Theorem	bezoutlemeu 12144*	Lemma for Bézout's identity. There is exactly one nonnegative integer meeting the greatest common divisor condition. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    ⇒   ⊢ (𝜑 → ∃!𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))
Theorem	bezoutlemle 12145*	Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the largest number which divides both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → ∀𝑧 ∈ ℤ ((𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵) → 𝑧 ≤ 𝐷))
Theorem	bezoutlemsup 12146*	Lemma for Bézout's identity. The number satisfying the greatest common divisor condition is the supremum of divisors of both 𝐴 and 𝐵. (Contributed by Mario Carneiro and Jim Kingdon, 9-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ ℕ0)    &   ⊢ (𝜑 → ∀𝑧 ∈ ℤ (𝑧 ∥ 𝐷 ↔ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)))    &   ⊢ (𝜑 → ¬ (𝐴 = 0 ∧ 𝐵 = 0))    ⇒   ⊢ (𝜑 → 𝐷 = sup({𝑧 ∈ ℤ ∣ (𝑧 ∥ 𝐴 ∧ 𝑧 ∥ 𝐵)}, ℝ, < ))
Theorem	dfgcd3 12147*	Alternate definition of the gcd operator. (Contributed by Jim Kingdon, 31-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (℩𝑑 ∈ ℕ0 ∀𝑧 ∈ ℤ (𝑧 ∥ 𝑑 ↔ (𝑧 ∥ 𝑀 ∧ 𝑧 ∥ 𝑁))))
Theorem	bezout 12148*	Bézout's identity: For any integers 𝐴 and 𝐵, there are integers 𝑥, 𝑦 such that (𝐴 gcd 𝐵) = 𝐴 · 𝑥 + 𝐵 · 𝑦. This is Metamath 100 proof #60. The proof is constructive, in the sense that it applies the Extended Euclidian Algorithm to constuct a number which can be shown to be (𝐴 gcd 𝐵) and which satisfies the rest of the theorem. In the presence of excluded middle, it is common to prove Bézout's identity by taking the smallest number which satisfies the Bézout condition, and showing it is the greatest common divisor. But we do not have the ability to show that number exists other than by providing a way to determine it. (Contributed by Mario Carneiro, 22-Feb-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ (𝐴 gcd 𝐵) = ((𝐴 · 𝑥) + (𝐵 · 𝑦)))
Theorem	dvdsgcd 12149	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 12150	Biconditional form of dvdsgcd 12149. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) ↔ 𝐾 ∥ (𝑀 gcd 𝑁)))
Theorem	dfgcd2 12151*	Alternate definition of the gcd operator, see definition in [ApostolNT] p. 15. (Contributed by AV, 8-Aug-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐷 = (𝑀 gcd 𝑁) ↔ (0 ≤ 𝐷 ∧ (𝐷 ∥ 𝑀 ∧ 𝐷 ∥ 𝑁) ∧ ∀𝑒 ∈ ℤ ((𝑒 ∥ 𝑀 ∧ 𝑒 ∥ 𝑁) → 𝑒 ∥ 𝐷))))
Theorem	gcdass 12152	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 12153	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 12154	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 12155	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 12156	Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ (𝐶 ∥ 𝐴 ∧ 𝐶 ∥ 𝐵)) → ((𝐴 gcd 𝐵) / 𝐶) = ((𝐴 / 𝐶) gcd (𝐵 / 𝐶)))
Theorem	gcdmultiple 12157	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 12158	Extend gcdmultiple 12157 so 𝑁 can be an integer. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd (𝑀 · 𝑁)) = 𝑀)
Theorem	gcdzeq 12159	A positive integer 𝐴 is equal to its gcd with an integer 𝐵 if and only if 𝐴 divides 𝐵. Generalization of gcdeq 12160. (Contributed by AV, 1-Jul-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵) = 𝐴 ↔ 𝐴 ∥ 𝐵))
Theorem	gcdeq 12160	𝐴 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 12161	Unidirectional form of dvdssq 12168. (Contributed by Scott Fenton, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀↑2) ∥ (𝑁↑2)))
Theorem	dvdsmulgcd 12162	Relationship between the order of an element and that of a multiple. (a divisibility equivalent). (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (𝐴 ∥ (𝐵 · 𝐶) ↔ 𝐴 ∥ (𝐵 · (𝐶 gcd 𝐴))))
Theorem	rpmulgcd 12163	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 12164	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 12165	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 12166	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 12167	Lemma for dvdssq 12168. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ (𝑀↑2) ∥ (𝑁↑2)))
Theorem	dvdssq 12168	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 12169	Partial converse to bezout 12148. 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 12170	Converse of bezout 12148 for when the greater common divisor is one (sufficient condition for relative primality). (Contributed by Stefan O'Rear, 23-Sep-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 1 → (𝐴 gcd 𝐵) = 1))
5.1.6  Decidable sets of integers
Theorem	nnmindc 12171*	An inhabited decidable subset of the natural numbers has a minimum. (Contributed by Jim Kingdon, 23-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 ∈ 𝐴) → inf(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	nnminle 12172*	The infimum of a decidable subset of the natural numbers is less than an element of the set. The infimum is also a minimum as shown at nnmindc 12171. (Contributed by Jim Kingdon, 26-Sep-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐴) → inf(𝐴, ℝ, < ) ≤ 𝐵)
Theorem	nnwodc 12173*	Well-ordering principle: any inhabited decidable set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 23-Oct-2024.)
⊢ ((𝐴 ⊆ ℕ ∧ ∃𝑤 𝑤 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	uzwodc 12174*	Well-ordering principle: any inhabited decidable subset of an upper set of integers has a least element. (Contributed by NM, 8-Oct-2005.) (Revised by Jim Kingdon, 22-Oct-2024.)
⊢ ((𝑆 ⊆ (ℤ≥‘𝑀) ∧ ∃𝑥 𝑥 ∈ 𝑆 ∧ ∀𝑥 ∈ (ℤ≥‘𝑀)DECID 𝑥 ∈ 𝑆) → ∃𝑗 ∈ 𝑆 ∀𝑘 ∈ 𝑆 𝑗 ≤ 𝑘)
Theorem	nnwofdc 12175*	Well-ordering principle: any inhabited decidable set of positive integers has a least element. This version allows 𝑥 and 𝑦 to be present in 𝐴 as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.)
⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑦𝐴    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ ∃𝑧 𝑧 ∈ 𝐴 ∧ ∀𝑗 ∈ ℕ DECID 𝑗 ∈ 𝐴) → ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦)
Theorem	nnwosdc 12176*	Well-ordering principle: any inhabited decidable set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) (Revised by Jim Kingdon, 25-Oct-2024.)
⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))    ⇒   ⊢ ((∃𝑥 ∈ ℕ 𝜑 ∧ ∀𝑥 ∈ ℕ DECID 𝜑) → ∃𝑥 ∈ ℕ (𝜑 ∧ ∀𝑦 ∈ ℕ (𝜓 → 𝑥 ≤ 𝑦)))
Theorem	nninfctlemfo 12177*	Lemma for nninfct 12178. (Contributed by Jim Kingdon, 10-Jul-2025.)
⊢ 𝐺 = frec((𝑥 ∈ ℤ ↦ (𝑥 + 1)), 0)    &   ⊢ 𝐹 = (𝑛 ∈ ω ↦ (𝑖 ∈ ω ↦ if(𝑖 ∈ 𝑛, 1o, ∅)))    &   ⊢ 𝐼 = ((𝐹 ∘ ◡𝐺) ∪ {⟨+∞, (ω × {1o})⟩})    ⇒   ⊢ (ω ∈ Omni → 𝐼:ℕ0*–onto→ℕ∞)
Theorem	nninfct 12178	The limited principle of omniscience (LPO) implies that ℕ∞ is countable. (Contributed by Jim Kingdon, 8-Jul-2025.)
⊢ (ω ∈ Omni → ∃𝑓 𝑓:ω–onto→(ℕ∞ ⊔ 1o))
5.1.7  Algorithms
Theorem	nn0seqcvgd 12179*	A strictly-decreasing nonnegative integer sequence with initial term 𝑁 reaches zero by the 𝑁 th term. Deduction version. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝜑 → 𝐹:ℕ0⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 = (𝐹‘0))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝐹‘(𝑘 + 1)) ≠ 0 → (𝐹‘(𝑘 + 1)) < (𝐹‘𝑘)))    ⇒   ⊢ (𝜑 → (𝐹‘𝑁) = 0)
Theorem	ialgrlem1st 12180	Lemma for ialgr0 12182. Expressing algrflemg 6283 in a form suitable for theorems such as seq3-1 10533 or seqf 10535. (Contributed by Jim Kingdon, 22-Jul-2021.)
⊢ (𝜑 → 𝐹:𝑆⟶𝑆)    ⇒   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(𝐹 ∘ 1st )𝑦) ∈ 𝑆)
Theorem	ialgrlemconst 12181	Lemma for ialgr0 12182. Closure of a constant function, in a form suitable for theorems such as seq3-1 10533 or seqf 10535. (Contributed by Jim Kingdon, 22-Jul-2021.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ (ℤ≥‘𝑀)) → ((𝑍 × {𝐴})‘𝑥) ∈ 𝑆)
Theorem	ialgr0 12182	The value of the algorithm iterator 𝑅 at 0 is the initial state 𝐴. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆⟶𝑆)    ⇒   ⊢ (𝜑 → (𝑅‘𝑀) = 𝐴)
Theorem	algrf 12183	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 12184	The value of the algorithm iterator 𝑅 at (𝐾 + 1). (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by Jim Kingdon, 12-Mar-2023.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝑅 = seq𝑀((𝐹 ∘ 1st ), (𝑍 × {𝐴}))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ (𝜑 → 𝐹:𝑆⟶𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝐾 ∈ 𝑍) → (𝑅‘(𝐾 + 1)) = (𝐹‘(𝑅‘𝐾)))
Theorem	alginv 12185*	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 12186*	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 12187	Lemma for algcvgb 12188. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑁 ≠ 0 → 𝑁 < 𝑀) ↔ ((𝑀 ≠ 0 → 𝑁 < 𝑀) ∧ (𝑀 = 0 → 𝑁 = 0))))
Theorem	algcvgb 12188	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 12189*	The countdown function 𝐶 remains 0 after 𝑁 steps. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 𝐹:𝑆⟶𝑆    &   ⊢ 𝑅 = seq0((𝐹 ∘ 1st ), (ℕ0 × {𝐴}))    &   ⊢ 𝐶:𝑆⟶ℕ0    &   ⊢ (𝑧 ∈ 𝑆 → ((𝐶‘(𝐹‘𝑧)) ≠ 0 → (𝐶‘(𝐹‘𝑧)) < (𝐶‘𝑧)))    &   ⊢ 𝑁 = (𝐶‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝐶‘(𝑅‘𝐾)) = 0))
Theorem	algfx 12190*	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 → (𝐹‘𝑧) = 𝑧))    ⇒   ⊢ (𝐴 ∈ 𝑆 → (𝐾 ∈ (ℤ≥‘𝑁) → (𝑅‘𝐾) = (𝑅‘𝑁)))
5.1.8  Euclid's Algorithm
Theorem	eucalgval2 12191*	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 12192*	Euclid's Algorithm eucalg 12197 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 12193*	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 12194*	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 12195*	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 12196*	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 12197*	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 1st 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 𝑁))
5.1.9  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." In this section, an operation calculating the least common multiple of two integers (df-lcm 12199). The definition is valid for all integers, including negative integers and 0, obeying the above mentioned convention.
Syntax	clcm 12198	Extend the definition of a class to include the least common multiple operator.
class lcm
Definition	df-lcm 12199*	Define the lcm operator. For example, (6 lcm 9) = 18. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Revised by AV, 16-Sep-2020.)
⊢ lcm = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∨ 𝑦 = 0), 0, inf({𝑛 ∈ ℕ ∣ (𝑥 ∥ 𝑛 ∧ 𝑦 ∥ 𝑛)}, ℝ, < )))
Theorem	lcmmndc 12200	Decidablity lemma used in various proofs related to lcm. (Contributed by Jim Kingdon, 21-Jan-2022.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∨ 𝑁 = 0))