P. 120 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 11901-12000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	halfleoddlt 11901	An integer is greater than half of an odd number iff it is greater than or equal to the half of the odd number. (Contributed by AV, 1-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁 ∧ 𝑀 ∈ ℤ) → ((𝑁 / 2) ≤ 𝑀 ↔ (𝑁 / 2) < 𝑀))
Theorem	opoe 11902	The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 + 𝐵))
Theorem	omoe 11903	The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ ¬ 2 ∥ 𝐵)) → 2 ∥ (𝐴 − 𝐵))
Theorem	opeo 11904	The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 + 𝐵))
Theorem	omeo 11905	The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ ¬ 2 ∥ 𝐴) ∧ (𝐵 ∈ ℤ ∧ 2 ∥ 𝐵)) → ¬ 2 ∥ (𝐴 − 𝐵))
Theorem	m1expe 11906	Exponentiation of -1 by an even power. Variant of m1expeven 10569. (Contributed by AV, 25-Jun-2021.)
⊢ (2 ∥ 𝑁 → (-1↑𝑁) = 1)
Theorem	m1expo 11907	Exponentiation of -1 by an odd power. (Contributed by AV, 26-Jun-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (-1↑𝑁) = -1)
Theorem	m1exp1 11908	Exponentiation of negative one is one iff the exponent is even. (Contributed by AV, 20-Jun-2021.)
⊢ (𝑁 ∈ ℤ → ((-1↑𝑁) = 1 ↔ 2 ∥ 𝑁))
Theorem	nn0enne 11909	A positive integer is an even nonnegative integer iff it is an even positive integer. (Contributed by AV, 30-May-2020.)
⊢ (𝑁 ∈ ℕ → ((𝑁 / 2) ∈ ℕ0 ↔ (𝑁 / 2) ∈ ℕ))
Theorem	nn0ehalf 11910	The half of an even nonnegative integer is a nonnegative integer. (Contributed by AV, 22-Jun-2020.) (Revised by AV, 28-Jun-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ0)
Theorem	nnehalf 11911	The half of an even positive integer is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 2 ∥ 𝑁) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0o1gt2 11912	An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → (𝑁 = 1 ∨ 2 < 𝑁))
Theorem	nno 11913	An alternate characterization of an odd integer greater than 1. (Contributed by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ)
Theorem	nn0o 11914	An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Proof shortened by AV, 2-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ ((𝑁 + 1) / 2) ∈ ℕ0) → ((𝑁 − 1) / 2) ∈ ℕ0)
Theorem	nn0ob 11915	Alternate characterizations of an odd nonnegative integer. (Contributed by AV, 4-Jun-2020.)
⊢ (𝑁 ∈ ℕ0 → (((𝑁 + 1) / 2) ∈ ℕ0 ↔ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nn0oddm1d2 11916	A positive integer is odd iff its predecessor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (¬ 2 ∥ 𝑁 ↔ ((𝑁 − 1) / 2) ∈ ℕ0))
Theorem	nnoddm1d2 11917	A positive integer is odd iff its successor divided by 2 is a positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ ℕ → (¬ 2 ∥ 𝑁 ↔ ((𝑁 + 1) / 2) ∈ ℕ))
Theorem	z0even 11918	0 is even. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 0
Theorem	n2dvds1 11919	2 does not divide 1 (common case). That means 1 is odd. (Contributed by David A. Wheeler, 8-Dec-2018.)
⊢ ¬ 2 ∥ 1
Theorem	n2dvdsm1 11920	2 does not divide -1. That means -1 is odd. (Contributed by AV, 15-Aug-2021.)
⊢ ¬ 2 ∥ -1
Theorem	z2even 11921	2 is even. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 23-Jun-2021.)
⊢ 2 ∥ 2
Theorem	n2dvds3 11922	2 does not divide 3, i.e. 3 is an odd number. (Contributed by AV, 28-Feb-2021.)
⊢ ¬ 2 ∥ 3
Theorem	z4even 11923	4 is an even number. (Contributed by AV, 23-Jul-2020.) (Revised by AV, 4-Jul-2021.)
⊢ 2 ∥ 4
Theorem	4dvdseven 11924	An integer which is divisible by 4 is an even integer. (Contributed by AV, 4-Jul-2021.)
⊢ (4 ∥ 𝑁 → 2 ∥ 𝑁)
5.1.3  The division algorithm
Theorem	divalglemnn 11925*	Lemma for divalg 11931. Existence for a positive denominator. (Contributed by Jim Kingdon, 30-Nov-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemqt 11926	Lemma for divalg 11931. The 𝑄 = 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 5-Dec-2021.)
⊢ (𝜑 → 𝐷 ∈ ℤ)    &   ⊢ (𝜑 → 𝑅 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℤ)    &   ⊢ (𝜑 → 𝑇 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 = 𝑇)    &   ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   ⊢ (𝜑 → 𝑅 = 𝑆)
Theorem	divalglemnqt 11927	Lemma for divalg 11931. The 𝑄 < 𝑇 case involved in showing uniqueness. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ (𝜑 → 𝐷 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ ℤ)    &   ⊢ (𝜑 → 𝑆 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℤ)    &   ⊢ (𝜑 → 𝑇 ∈ ℤ)    &   ⊢ (𝜑 → 0 ≤ 𝑆)    &   ⊢ (𝜑 → 𝑅 < 𝐷)    &   ⊢ (𝜑 → ((𝑄 · 𝐷) + 𝑅) = ((𝑇 · 𝐷) + 𝑆))    ⇒   ⊢ (𝜑 → ¬ 𝑄 < 𝑇)
Theorem	divalglemeunn 11928*	Lemma for divalg 11931. Uniqueness for a positive denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemex 11929*	Lemma for divalg 11931. The quotient and remainder exist. (Contributed by Jim Kingdon, 30-Nov-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalglemeuneg 11930*	Lemma for divalg 11931. Uniqueness for a negative denominator. (Contributed by Jim Kingdon, 4-Dec-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 < 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalg 11931*	The division algorithm (theorem). Dividing an integer 𝑁 by a nonzero integer 𝐷 produces a (unique) quotient 𝑞 and a unique remainder 0 ≤ 𝑟 < (abs‘𝐷). Theorem 1.14 in [ApostolNT] p. 19. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → ∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)))
Theorem	divalgb 11932*	Express the division algorithm as stated in divalg 11931 in terms of ∥. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℤ ∧ 𝐷 ≠ 0) → (∃!𝑟 ∈ ℤ ∃𝑞 ∈ ℤ (0 ≤ 𝑟 ∧ 𝑟 < (abs‘𝐷) ∧ 𝑁 = ((𝑞 · 𝐷) + 𝑟)) ↔ ∃!𝑟 ∈ ℕ0 (𝑟 < (abs‘𝐷) ∧ 𝐷 ∥ (𝑁 − 𝑟))))
Theorem	divalg2 11933*	The division algorithm (theorem) for a positive divisor. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → ∃!𝑟 ∈ ℕ0 (𝑟 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑟)))
Theorem	divalgmod 11934	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor (compare divalg2 11933 and divalgb 11932). This demonstration theorem justifies the use of mod to yield an explicit remainder from this point forward. (Contributed by Paul Chapman, 31-Mar-2011.) (Revised by AV, 21-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 ∈ ℕ0 ∧ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅)))))
Theorem	divalgmodcl 11935	The result of the mod operator satisfies the requirements for the remainder 𝑅 in the division algorithm for a positive divisor. Variant of divalgmod 11934. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Proof shortened by AV, 21-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 𝑅 ∈ ℕ0) → (𝑅 = (𝑁 mod 𝐷) ↔ (𝑅 < 𝐷 ∧ 𝐷 ∥ (𝑁 − 𝑅))))
Theorem	modremain 11936*	The result of the modulo operation is the remainder of the division algorithm. (Contributed by AV, 19-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝑅 ∈ ℕ0 ∧ 𝑅 < 𝐷)) → ((𝑁 mod 𝐷) = 𝑅 ↔ ∃𝑧 ∈ ℤ ((𝑧 · 𝐷) + 𝑅) = 𝑁))
Theorem	ndvdssub 11937	Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 − 1, 𝑁 − 2... 𝑁 − (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 − 𝐾)))
Theorem	ndvdsadd 11938	Corollary of the division algorithm. If an integer 𝐷 greater than 1 divides 𝑁, then it does not divide any of 𝑁 + 1, 𝑁 + 2... 𝑁 + (𝐷 − 1). (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐾 < 𝐷)) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 𝐾)))
Theorem	ndvdsp1 11939	Special case of ndvdsadd 11938. If an integer 𝐷 greater than 1 divides 𝑁, it does not divide 𝑁 + 1. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ ((𝑁 ∈ ℤ ∧ 𝐷 ∈ ℕ ∧ 1 < 𝐷) → (𝐷 ∥ 𝑁 → ¬ 𝐷 ∥ (𝑁 + 1)))
Theorem	ndvdsi 11940	A quick test for non-divisibility. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑄 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ    &   ⊢ ((𝐴 · 𝑄) + 𝑅) = 𝐵    &   ⊢ 𝑅 < 𝐴    ⇒   ⊢ ¬ 𝐴 ∥ 𝐵
Theorem	flodddiv4 11941	The floor of an odd integer divided by 4. (Contributed by AV, 17-Jun-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 = ((2 · 𝑀) + 1)) → (⌊‘(𝑁 / 4)) = if(2 ∥ 𝑀, (𝑀 / 2), ((𝑀 − 1) / 2)))
Theorem	fldivndvdslt 11942	The floor of an integer divided by a nonzero integer not dividing the first integer is less than the integer divided by the positive integer. (Contributed by AV, 4-Jul-2021.)
⊢ ((𝐾 ∈ ℤ ∧ (𝐿 ∈ ℤ ∧ 𝐿 ≠ 0) ∧ ¬ 𝐿 ∥ 𝐾) → (⌊‘(𝐾 / 𝐿)) < (𝐾 / 𝐿))
Theorem	flodddiv4lt 11943	The floor of an odd number divided by 4 is less than the odd number divided by 4. (Contributed by AV, 4-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → (⌊‘(𝑁 / 4)) < (𝑁 / 4))
Theorem	flodddiv4t2lthalf 11944	The floor of an odd number divided by 4, multiplied by 2 is less than the half of the odd number. (Contributed by AV, 4-Jul-2021.)
⊢ ((𝑁 ∈ ℤ ∧ ¬ 2 ∥ 𝑁) → ((⌊‘(𝑁 / 4)) · 2) < (𝑁 / 2))
5.1.4  The greatest common divisor operator
Syntax	cgcd 11945	Extend the definition of a class to include the greatest common divisor operator.
class gcd
Definition	df-gcd 11946*	Define the gcd operator. For example, (-6 gcd 9) = 3 (ex-gcd 14568). (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ gcd = (𝑥 ∈ ℤ, 𝑦 ∈ ℤ ↦ if((𝑥 = 0 ∧ 𝑦 = 0), 0, sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦)}, ℝ, < )))
Theorem	gcdmndc 11947	Decidablity lemma used in various proofs related to gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID (𝑀 = 0 ∧ 𝑁 = 0))
Theorem	zsupcllemstep 11948*	Lemma for zsupcl 11950. Induction step. (Contributed by Jim Kingdon, 7-Dec-2021.)
⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    ⇒   ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → (((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘𝐾) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧))) → ((𝜑 ∧ ∀𝑛 ∈ (ℤ≥‘(𝐾 + 1)) ¬ 𝜓) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))))
Theorem	zsupcllemex 11949*	Lemma for zsupcl 11950. Existence of the supremum. (Contributed by Jim Kingdon, 7-Dec-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    &   ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ 𝜓} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ 𝜓}𝑦 < 𝑧)))
Theorem	zsupcl 11950*	Closure of supremum for decidable integer properties. The property which defines the set we are taking the supremum of must (a) be true at 𝑀 (which corresponds to the nonempty condition of classical supremum theorems), (b) decidable at each value after 𝑀, and (c) be false after 𝑗 (which corresponds to the upper bound condition found in classical supremum theorems). (Contributed by Jim Kingdon, 7-Dec-2021.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜒))    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘𝑀)) → DECID 𝜓)    &   ⊢ (𝜑 → ∃𝑗 ∈ (ℤ≥‘𝑀)∀𝑛 ∈ (ℤ≥‘𝑗) ¬ 𝜓)    ⇒   ⊢ (𝜑 → sup({𝑛 ∈ ℤ ∣ 𝜓}, ℝ, < ) ∈ (ℤ≥‘𝑀))
Theorem	zssinfcl 11951*	The infimum of a set of integers is an element of the set. (Contributed by Jim Kingdon, 16-Jan-2022.)
⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐵 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐵 𝑧 < 𝑦)))    &   ⊢ (𝜑 → 𝐵 ⊆ ℤ)    &   ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ ℤ)    ⇒   ⊢ (𝜑 → inf(𝐵, ℝ, < ) ∈ 𝐵)
Theorem	infssuzex 11952*	Existence of the infimum of a subset of an upper set of integers. (Contributed by Jim Kingdon, 13-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝑆 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝑆 𝑧 < 𝑦)))
Theorem	infssuzledc 11953*	The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by Jim Kingdon, 13-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   ⊢ (𝜑 → inf(𝑆, ℝ, < ) ≤ 𝐴)
Theorem	infssuzcldc 11954*	The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by Jim Kingdon, 20-Jan-2022.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ 𝑆 = {𝑛 ∈ (ℤ≥‘𝑀) ∣ 𝜓}    &   ⊢ (𝜑 → 𝐴 ∈ 𝑆)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (𝑀...𝐴)) → DECID 𝜓)    ⇒   ⊢ (𝜑 → inf(𝑆, ℝ, < ) ∈ 𝑆)
Theorem	suprzubdc 11955*	The supremum of a bounded-above decidable set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℤ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → 𝐵 ∈ 𝐴)    ⇒   ⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < ))
Theorem	nninfdcex 11956*	A decidable set of natural numbers has an infimum. (Contributed by Jim Kingdon, 28-Sep-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℕ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑦 𝑦 ∈ 𝐴)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
Theorem	zsupssdc 11957*	An inhabited decidable bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-suploc 7934.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 5-Oct-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℤ)    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ 𝐵 (𝑦 < 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 < 𝑧)))
Theorem	suprzcl2dc 11958*	The supremum of a bounded-above decidable set of integers is a member of the set. (This theorem avoids ax-pre-suploc 7934.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Jim Kingdon, 6-Oct-2024.)
⊢ (𝜑 → 𝐴 ⊆ ℤ)    &   ⊢ (𝜑 → ∀𝑥 ∈ ℤ DECID 𝑥 ∈ 𝐴)    &   ⊢ (𝜑 → ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴)    ⇒   ⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ 𝐴)
Theorem	dvdsbnd 11959*	There is an upper bound to the divisors of a nonzero integer. (Contributed by Jim Kingdon, 11-Dec-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) → ∃𝑛 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑛) ¬ 𝑚 ∥ 𝐴)
Theorem	gcdsupex 11960*	Existence of the supremum used in defining gcd. (Contributed by Jim Kingdon, 12-Dec-2021.)
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → ∃𝑥 ∈ ℤ (∀𝑦 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}𝑦 < 𝑧)))
Theorem	gcdsupcl 11961*	Closure of the supremum used in defining gcd. A lemma for gcdval 11962 and gcdn0cl 11965. (Contributed by Jim Kingdon, 11-Dec-2021.)
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ ¬ (𝑋 = 0 ∧ 𝑌 = 0)) → sup({𝑛 ∈ ℤ ∣ (𝑛 ∥ 𝑋 ∧ 𝑛 ∥ 𝑌)}, ℝ, < ) ∈ ℕ)
Theorem	gcdval 11962*	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 11963	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 11964*	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	gcdn0cl 11965	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ¬ (𝑀 = 0 ∧ 𝑁 = 0)) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcddvds 11966	The gcd of two integers divides each of them. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 gcd 𝑁) ∥ 𝑀 ∧ (𝑀 gcd 𝑁) ∥ 𝑁))
Theorem	dvdslegcd 11967	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 11968	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 11969	Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcdnncl 11970	Closure of the gcd operator. (Contributed by Thierry Arnoux, 2-Feb-2020.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	gcdcld 11971	Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) ∈ ℕ0)
Theorem	gcd2n0cl 11972	Closure of the gcd operator if the second operand is not 0. (Contributed by AV, 10-Jul-2021.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0) → (𝑀 gcd 𝑁) ∈ ℕ)
Theorem	zeqzmulgcd 11973*	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 11974	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 11975	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 11976	The gcd operator is commutative. Theorem 1.4(a) in [ApostolNT] p. 16. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	gcdcomd 11977	The gcd operator is commutative, deduction version. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    ⇒   ⊢ (𝜑 → (𝑀 gcd 𝑁) = (𝑁 gcd 𝑀))
Theorem	divgcdnn 11978	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 11979	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 11980	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 11981	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 11982	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 11983	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 11984	The gcd of a nonnegative integer with 0 is itself. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℕ0 → (𝑁 gcd 0) = 𝑁)
Theorem	gcdneg 11985	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 gcd -𝑁) = (𝑀 gcd 𝑁))
Theorem	neggcd 11986	Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑀 gcd 𝑁) = (𝑀 gcd 𝑁))
Theorem	gcdaddm 11987	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 11988	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 11989	The gcd of a number and itself is its absolute value. (Contributed by Paul Chapman, 31-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (𝑁 gcd 𝑁) = (abs‘𝑁))
Theorem	gcd1 11990	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 11991	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 11992	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 11993	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 11994	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 11995	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 11996	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 11997	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 11998	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 11999*	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 12000*	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 ([𝑊 / 𝑥]𝜓 ∧ 𝜑))