P. 161 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16001-16100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sincos1sgn 16001	The signs of the sine and cosine of 1. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘1) ∧ 0 < (cos‘1))
Theorem	sincos2sgn 16002	The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (0 < (sin‘2) ∧ (cos‘2) < 0)
Theorem	sin4lt0 16003	The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008.)
⊢ (sin‘4) < 0
Theorem	absefi 16004	The absolute value of the exponential of an imaginary number is one. Equation 48 of [Rudin] p. 167. (Contributed by Jason Orendorff, 9-Feb-2007.)
⊢ (𝐴 ∈ ℝ → (abs‘(exp‘(i · 𝐴))) = 1)
Theorem	absef 16005	The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007.)
⊢ (𝐴 ∈ ℂ → (abs‘(exp‘𝐴)) = (exp‘(ℜ‘𝐴)))
Theorem	absefib 16006	A complex number is real iff the exponential of its product with i has absolute value one. (Contributed by NM, 21-Aug-2008.)
⊢ (𝐴 ∈ ℂ → (𝐴 ∈ ℝ ↔ (abs‘(exp‘(i · 𝐴))) = 1))
Theorem	efieq1re 16007	A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008.)
⊢ ((𝐴 ∈ ℂ ∧ (exp‘(i · 𝐴)) = 1) → 𝐴 ∈ ℝ)
Theorem	demoivre 16008	De Moivre's Formula. Proof by induction given at http://en.wikipedia.org/wiki/De_Moivre's_formula, but restricted to nonnegative integer powers. See also demoivreALT 16009 for an alternate longer proof not using the exponential function. (Contributed by NM, 24-Jul-2007.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℤ) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
Theorem	demoivreALT 16009	Alternate proof of demoivre 16008. It is longer but does not use the exponential function. This is Metamath 100 proof #17. (Contributed by Steve Rodriguez, 10-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (((cos‘𝐴) + (i · (sin‘𝐴)))↑𝑁) = ((cos‘(𝑁 · 𝐴)) + (i · (sin‘(𝑁 · 𝐴)))))
5.11.1.1  The circle constant (tau = 2 pi)
Syntax	ctau 16010	Extend class notation to include the constant tau, τ = 6.28318....
class τ
Definition	df-tau 16011	Define the circle constant tau, τ = 6.28318..., which is the smallest positive real number whose cosine is one. Various notations have been used or proposed for this number including τ, a three-legged variant of π, or 2π. Note the difference between this constant τ and the formula variable 𝜏. Following our convention, the constant is displayed in upright font while the variable is in italic font; furthermore, the colors are different. (Contributed by Jim Kingdon, 9-Apr-2018.) (Revised by AV, 1-Oct-2020.)
⊢ τ = inf((ℝ+ ∩ (◡cos “ {1})), ℝ, < )
5.11.2  _e is irrational
Theorem	eirrlem 16012*	Lemma for eirr 16013. (Contributed by Paul Chapman, 9-Feb-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ0 ↦ (1 / (!‘𝑛)))    &   ⊢ (𝜑 → 𝑃 ∈ ℤ)    &   ⊢ (𝜑 → 𝑄 ∈ ℕ)    &   ⊢ (𝜑 → e = (𝑃 / 𝑄))    ⇒   ⊢ ¬ 𝜑
Theorem	eirr 16013	e is irrational. (Contributed by Paul Chapman, 9-Feb-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
⊢ e ∉ ℚ
Theorem	egt2lt3 16014	Euler's constant e = 2.71828... is strictly bounded below by 2 and above by 3. (Contributed by NM, 28-Nov-2008.) (Revised by Mario Carneiro, 29-Apr-2014.)
⊢ (2 < e ∧ e < 3)
Theorem	epos 16015	Euler's constant e is greater than 0. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ 0 < e
Theorem	epr 16016	Euler's constant e is a positive real. (Contributed by Jeff Hankins, 22-Nov-2008.)
⊢ e ∈ ℝ+
Theorem	ene0 16017	e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 0
Theorem	ene1 16018	e is not 1. (Contributed by David A. Wheeler, 17-Oct-2017.)
⊢ e ≠ 1
5.12  Cardinality of real and complex number subsets
5.12.1  Countability of integers and rationals
Theorem	xpnnen 16019	The Cartesian product of the set of positive integers with itself is equinumerous to the set of positive integers. (Contributed by NM, 1-Aug-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
⊢ (ℕ × ℕ) ≈ ℕ
Theorem	znnen 16020	The set of integers and the set of positive integers are equinumerous. Exercise 1 of [Gleason] p. 140. (Contributed by NM, 31-Jul-2004.) (Proof shortened by Mario Carneiro, 13-Jun-2014.)
⊢ ℤ ≈ ℕ
Theorem	qnnen 16021	The rational numbers are countable. This proof does not use the Axiom of Choice, even though it uses an onto function, because the base set (ℤ × ℕ) is numerable. Exercise 2 of [Enderton] p. 133. For purposes of the Metamath 100 list, we are considering Mario Carneiro's revision as the date this proof was completed. This is Metamath 100 proof #3. (Contributed by NM, 31-Jul-2004.) (Revised by Mario Carneiro, 3-Mar-2013.)
⊢ ℚ ≈ ℕ
5.12.2  The reals are uncountable
Theorem	rpnnen2lem1 16022*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑁 ∈ ℕ) → ((𝐹‘𝐴)‘𝑁) = if(𝑁 ∈ 𝐴, ((1 / 3)↑𝑁), 0))
Theorem	rpnnen2lem2 16023*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ (𝐴 ⊆ ℕ → (𝐹‘𝐴):ℕ⟶ℝ)
Theorem	rpnnen2lem3 16024*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ seq1( + , (𝐹‘ℕ)) ⇝ (1 / 2)
Theorem	rpnnen2lem4 16025*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 31-Aug-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑘 ∈ ℕ) → (0 ≤ ((𝐹‘𝐴)‘𝑘) ∧ ((𝐹‘𝐴)‘𝑘) ≤ ((𝐹‘𝐵)‘𝑘)))
Theorem	rpnnen2lem5 16026*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → seq𝑀( + , (𝐹‘𝐴)) ∈ dom ⇝ )
Theorem	rpnnen2lem6 16027*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ∈ ℝ)
Theorem	rpnnen2lem7 16028*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘) ≤ Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐵)‘𝑘))
Theorem	rpnnen2lem8 16029*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ 𝑀 ∈ ℕ) → Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = (Σ𝑘 ∈ (1...(𝑀 − 1))((𝐹‘𝐴)‘𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘𝐴)‘𝑘)))
Theorem	rpnnen2lem9 16030*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ (𝑀 ∈ ℕ → Σ𝑘 ∈ (ℤ≥‘𝑀)((𝐹‘(ℕ ∖ {𝑀}))‘𝑘) = (0 + (((1 / 3)↑(𝑀 + 1)) / (1 − (1 / 3)))))
Theorem	rpnnen2lem10 16031*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 30-Apr-2014.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵)))    &   ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ (ℤ≥‘𝑚)((𝐹‘𝐵)‘𝑘))
Theorem	rpnnen2lem11 16032*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    &   ⊢ (𝜑 → 𝐴 ⊆ ℕ)    &   ⊢ (𝜑 → 𝐵 ⊆ ℕ)    &   ⊢ (𝜑 → 𝑚 ∈ (𝐴 ∖ 𝐵))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ (𝑛 < 𝑚 → (𝑛 ∈ 𝐴 ↔ 𝑛 ∈ 𝐵)))    &   ⊢ (𝜓 ↔ Σ𝑘 ∈ ℕ ((𝐹‘𝐴)‘𝑘) = Σ𝑘 ∈ ℕ ((𝐹‘𝐵)‘𝑘))    ⇒   ⊢ (𝜑 → ¬ 𝜓)
Theorem	rpnnen2lem12 16033*	Lemma for rpnnen2 16034. (Contributed by Mario Carneiro, 13-May-2013.)
⊢ 𝐹 = (𝑥 ∈ 𝒫 ℕ ↦ (𝑛 ∈ ℕ ↦ if(𝑛 ∈ 𝑥, ((1 / 3)↑𝑛), 0)))    ⇒   ⊢ 𝒫 ℕ ≼ (0[,]1)
Theorem	rpnnen2 16034	The other half of rpnnen 16035, where we show an injection from sets of positive integers to real numbers. The obvious choice for this is binary expansion, but it has the unfortunate property that it does not produce an injection on numbers which end with all 0's or all 1's (the more well-known decimal version of this is 0.999... 15692). Instead, we opt for a ternary expansion, which produces (a scaled version of) the Cantor set. Since the Cantor set is riddled with gaps, we can show that any two sequences that are not equal must differ somewhere, and when they do, they are placed a finite distance apart, thus ensuring that the map is injective. Our map assigns to each subset 𝐴 of the positive integers the number Σ𝑘 ∈ 𝐴(3↑-𝑘) = Σ𝑘 ∈ ℕ((𝐹‘𝐴)‘𝑘), where ((𝐹‘𝐴)‘𝑘) = if(𝑘 ∈ 𝐴, (3↑-𝑘), 0)) (rpnnen2lem1 16022). This is an infinite sum of real numbers (rpnnen2lem2 16023), and since 𝐴 ⊆ 𝐵 implies (𝐹‘𝐴) ≤ (𝐹‘𝐵) (rpnnen2lem4 16025) and (𝐹‘ℕ) converges to 1 / 2 (rpnnen2lem3 16024) by geoisum1 15690, the sum is convergent to some real (rpnnen2lem5 16026 and rpnnen2lem6 16027) by the comparison test for convergence cvgcmp 15627. The comparison test also tells us that 𝐴 ⊆ 𝐵 implies Σ(𝐹‘𝐴) ≤ Σ(𝐹‘𝐵) (rpnnen2lem7 16028). Putting it all together, if we have two sets 𝑥 ≠ 𝑦, there must differ somewhere, and so there must be an 𝑚 such that ∀𝑛 < 𝑚(𝑛 ∈ 𝑥 ↔ 𝑛 ∈ 𝑦) but 𝑚 ∈ (𝑥 ∖ 𝑦) or vice versa. In this case, we split off the first 𝑚 − 1 terms (rpnnen2lem8 16029) and cancel them (rpnnen2lem10 16031), since these are the same for both sets. For the remaining terms, we use the subset property to establish that Σ(𝐹‘𝑦) ≤ Σ(𝐹‘(ℕ ∖ {𝑚})) and Σ(𝐹‘{𝑚}) ≤ Σ(𝐹‘𝑥) (where these sums are only over (ℤ≥‘𝑚)), and since Σ(𝐹‘(ℕ ∖ {𝑚})) = (3↑-𝑚) / 2 (rpnnen2lem9 16030) and Σ(𝐹‘{𝑚}) = (3↑-𝑚), we establish that Σ(𝐹‘𝑦) < Σ(𝐹‘𝑥) (rpnnen2lem11 16032) so that they must be different. By contraposition (rpnnen2lem12 16033), we find that this map is an injection. (Contributed by Mario Carneiro, 13-May-2013.) (Proof shortened by Mario Carneiro, 30-Apr-2014.) (Revised by NM, 17-Aug-2021.)
⊢ 𝒫 ℕ ≼ (0[,]1)
Theorem	rpnnen 16035	The cardinality of the continuum is the same as the powerset of ω. This is a stronger statement than ruc 16051, which only asserts that ℝ is uncountable, i.e. has a cardinality larger than ω. The main proof is in two parts, rpnnen1 12824 and rpnnen2 16034, each showing an injection in one direction, and this last part uses sbth 8958 to prove that the sets are equinumerous. By constructing explicit injections, we avoid the use of AC. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 23-Aug-2014.)
⊢ ℝ ≈ 𝒫 ℕ
Theorem	rexpen 16036	The real numbers are equinumerous to their own Cartesian product, even though it is not necessarily true that ℝ is well-orderable (so we cannot use infxpidm2 9874 directly). (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.)
⊢ (ℝ × ℝ) ≈ ℝ
Theorem	cpnnen 16037	The complex numbers are equinumerous to the powerset of the positive integers. (Contributed by Mario Carneiro, 16-Jun-2013.)
⊢ ℂ ≈ 𝒫 ℕ
Theorem	rucALT 16038	Alternate proof of ruc 16051. This proof is a simple corollary of rpnnen 16035, which determines the exact cardinality of the reals. For an alternate proof discussed at mmcomplex.html#uncountable 16035, see ruc 16051. (Contributed by NM, 13-Oct-2004.) (Revised by Mario Carneiro, 13-May-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ℕ ≺ ℝ
Theorem	ruclem1 16039*	Lemma for ruc 16051 (the reals are uncountable). Substitutions for the function 𝐷. (Contributed by Mario Carneiro, 28-May-2014.) (Revised by Fan Zheng, 6-Jun-2016.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑋 = (1st ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    &   ⊢ 𝑌 = (2nd ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    ⇒   ⊢ (𝜑 → ((⟨𝐴, 𝐵⟩𝐷𝑀) ∈ (ℝ × ℝ) ∧ 𝑋 = if(((𝐴 + 𝐵) / 2) < 𝑀, 𝐴, ((((𝐴 + 𝐵) / 2) + 𝐵) / 2)) ∧ 𝑌 = if(((𝐴 + 𝐵) / 2) < 𝑀, ((𝐴 + 𝐵) / 2), 𝐵)))
Theorem	ruclem2 16040*	Lemma for ruc 16051. Ordering property for the input to 𝐷. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑋 = (1st ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    &   ⊢ 𝑌 = (2nd ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝐴 ≤ 𝑋 ∧ 𝑋 < 𝑌 ∧ 𝑌 ≤ 𝐵))
Theorem	ruclem3 16041*	Lemma for ruc 16051. The constructed interval [𝑋, 𝑌] always excludes 𝑀. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝑀 ∈ ℝ)    &   ⊢ 𝑋 = (1st ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    &   ⊢ 𝑌 = (2nd ‘(⟨𝐴, 𝐵⟩𝐷𝑀))    &   ⊢ (𝜑 → 𝐴 < 𝐵)    ⇒   ⊢ (𝜑 → (𝑀 < 𝑋 ∨ 𝑌 < 𝑀))
Theorem	ruclem4 16042*	Lemma for ruc 16051. Initial value of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    ⇒   ⊢ (𝜑 → (𝐺‘0) = ⟨0, 1⟩)
Theorem	ruclem6 16043*	Lemma for ruc 16051. Domain and codomain of the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    ⇒   ⊢ (𝜑 → 𝐺:ℕ0⟶(ℝ × ℝ))
Theorem	ruclem7 16044*	Lemma for ruc 16051. Successor value for the interval sequence. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (𝐺‘(𝑁 + 1)) = ((𝐺‘𝑁)𝐷(𝐹‘(𝑁 + 1))))
Theorem	ruclem8 16045*	Lemma for ruc 16051. The intervals of the 𝐺 sequence are all nonempty. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (1st ‘(𝐺‘𝑁)) < (2nd ‘(𝐺‘𝑁)))
Theorem	ruclem9 16046*	Lemma for ruc 16051. The first components of the 𝐺 sequence are increasing, and the second components are decreasing. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    ⇒   ⊢ (𝜑 → ((1st ‘(𝐺‘𝑀)) ≤ (1st ‘(𝐺‘𝑁)) ∧ (2nd ‘(𝐺‘𝑁)) ≤ (2nd ‘(𝐺‘𝑀))))
Theorem	ruclem10 16047*	Lemma for ruc 16051. Every first component of the 𝐺 sequence is less than every second component. That is, the sequences form a chain a1 < a2 <... < b2 < b1, where ai are the first components and bi are the second components. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (1st ‘(𝐺‘𝑀)) < (2nd ‘(𝐺‘𝑁)))
Theorem	ruclem11 16048*	Lemma for ruc 16051. Closure lemmas for supremum. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    ⇒   ⊢ (𝜑 → (ran (1st ∘ 𝐺) ⊆ ℝ ∧ ran (1st ∘ 𝐺) ≠ ∅ ∧ ∀𝑧 ∈ ran (1st ∘ 𝐺)𝑧 ≤ 1))
Theorem	ruclem12 16049*	Lemma for ruc 16051. The supremum of the increasing sequence 1st ∘ 𝐺 is a real number that is not in the range of 𝐹. (Contributed by Mario Carneiro, 28-May-2014.)
⊢ (𝜑 → 𝐹:ℕ⟶ℝ)    &   ⊢ (𝜑 → 𝐷 = (𝑥 ∈ (ℝ × ℝ), 𝑦 ∈ ℝ ↦ ⦋(((1st ‘𝑥) + (2nd ‘𝑥)) / 2) / 𝑚⦌if(𝑚 < 𝑦, ⟨(1st ‘𝑥), 𝑚⟩, ⟨((𝑚 + (2nd ‘𝑥)) / 2), (2nd ‘𝑥)⟩)))    &   ⊢ 𝐶 = ({⟨0, ⟨0, 1⟩⟩} ∪ 𝐹)    &   ⊢ 𝐺 = seq0(𝐷, 𝐶)    &   ⊢ 𝑆 = sup(ran (1st ∘ 𝐺), ℝ, < )    ⇒   ⊢ (𝜑 → 𝑆 ∈ (ℝ ∖ ran 𝐹))
Theorem	ruclem13 16050	Lemma for ruc 16051. There is no function that maps ℕ onto ℝ. (Use nex 1801 if you want this in the form ¬ ∃𝑓𝑓:ℕ–onto→ℝ.) (Contributed by NM, 14-Oct-2004.) (Proof shortened by Fan Zheng, 6-Jun-2016.)
⊢ ¬ 𝐹:ℕ–onto→ℝ
Theorem	ruc 16051	The set of positive integers is strictly dominated by the set of real numbers, i.e. the real numbers are uncountable. The proof consists of lemmas ruclem1 16039 through ruclem13 16050 and this final piece. Our proof is based on the proof of Theorem 5.18 of [Truss] p. 114. See ruclem13 16050 for the function existence version of this theorem. For an informal discussion of this proof, see mmcomplex.html#uncountable 16050. For an alternate proof see rucALT 16038. This is Metamath 100 proof #22. (Contributed by NM, 13-Oct-2004.)
⊢ ℕ ≺ ℝ
Theorem	resdomq 16052	The set of rationals is strictly less equinumerous than the set of reals (ℝ strictly dominates ℚ). (Contributed by NM, 18-Dec-2004.)
⊢ ℚ ≺ ℝ
Theorem	aleph1re 16053	There are at least aleph-one real numbers. (Contributed by NM, 2-Feb-2005.)
⊢ (ℵ‘1o) ≼ ℝ
Theorem	aleph1irr 16054	There are at least aleph-one irrationals. (Contributed by NM, 2-Feb-2005.)
⊢ (ℵ‘1o) ≼ (ℝ ∖ ℚ)
Theorem	cnso 16055	The complex numbers can be linearly ordered. (Contributed by Stefan O'Rear, 16-Nov-2014.)
⊢ ∃𝑥 𝑥 Or ℂ
PART 6  ELEMENTARY NUMBER THEORY Here we introduce elementary number theory, in particular the elementary properties of divisibility and elementary prime number theory.
6.1  Elementary properties of divisibility
6.1.1  Irrationality of square root of 2
Theorem	sqrt2irrlem 16056	Lemma for sqrt2irr 16057. This is the core of the proof: if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd by the method of infinite descent (here implemented by strong induction). This is Metamath 100 proof #1. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.) (Proof shortened by JV, 4-Jan-2022.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (√‘2) = (𝐴 / 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ))
Theorem	sqrt2irr 16057	The square root of 2 is irrational. See zsqrtelqelz 16559 for a generalization to all non-square integers. The proof's core is proven in sqrt2irrlem 16056, which shows that if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd. An older version of this proof was included in The Seventeen Provers of the World compiled by Freek Wiedijk. It is also the first of the "top 100" mathematical theorems whose formalization is tracked by Freek Wiedijk on his Formalizing 100 Theorems page at http://www.cs.ru.nl/~freek/100/ 16056. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ (√‘2) ∉ ℚ
Theorem	sqrt2re 16058	The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)
⊢ (√‘2) ∈ ℝ
Theorem	sqrt2irr0 16059	The square root of 2 is an irrational number. (Contributed by AV, 23-Dec-2022.)
⊢ (√‘2) ∈ (ℝ ∖ ℚ)
6.1.2  Some Number sets are chains of proper subsets
Theorem	nthruc 16060	The sequence ℕ, ℤ, ℚ, ℝ, and ℂ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to ℤ but not ℕ, one-half belongs to ℚ but not ℤ, the square root of 2 belongs to ℝ but not ℚ, and finally that the imaginary number i belongs to ℂ but not ℝ. See nthruz 16061 for a further refinement. (Contributed by NM, 12-Jan-2002.)
⊢ ((ℕ ⊊ ℤ ∧ ℤ ⊊ ℚ) ∧ (ℚ ⊊ ℝ ∧ ℝ ⊊ ℂ))
Theorem	nthruz 16061	The sequence ℕ, ℕ0, and ℤ forms a chain of proper subsets. In each case the proper subset relationship is shown by demonstrating a number that belongs to one set but not the other. We show that zero belongs to ℕ0 but not ℕ and minus one belongs to ℤ but not ℕ0. This theorem refines the chain of proper subsets nthruc 16060. (Contributed by NM, 9-May-2004.)
⊢ (ℕ ⊊ ℕ0 ∧ ℕ0 ⊊ ℤ)
6.1.3  The divides relation
Syntax	cdvds 16062	Extend the definition of a class to include the divides relation. See df-dvds 16063.
class ∥
Definition	df-dvds 16063*	Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ∥ = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ) ∧ ∃𝑛 ∈ ℤ (𝑛 · 𝑥) = 𝑦)}
Theorem	divides 16064*	Define the divides relation. 𝑀 ∥ 𝑁 means 𝑀 divides into 𝑁 with no remainder. For example, 3 ∥ 6 (ex-dvds 29108). As proven in dvdsval3 16066, 𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0. See divides 16064 and dvdsval2 16065 for other equivalent expressions. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = 𝑁))
Theorem	dvdsval2 16065	One nonzero integer divides another integer if and only if their quotient is an integer. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 / 𝑀) ∈ ℤ))
Theorem	dvdsval3 16066	One nonzero integer divides another integer if and only if the remainder upon division is zero, see remark in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 15-Jul-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (𝑁 mod 𝑀) = 0))
Theorem	dvdszrcl 16067	Reverse closure for the divisibility relation. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ (𝑋 ∥ 𝑌 → (𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ))
Theorem	dvdsmod0 16068	If a positive integer divides another integer, then the remainder upon division is zero. (Contributed by AV, 3-Mar-2022.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑀 ∥ 𝑁) → (𝑁 mod 𝑀) = 0)
Theorem	p1modz1 16069	If a number greater than 1 divides another number, the second number increased by 1 is 1 modulo the first number. (Contributed by AV, 19-Mar-2022.)
⊢ ((𝑀 ∥ 𝐴 ∧ 1 < 𝑀) → ((𝐴 + 1) mod 𝑀) = 1)
Theorem	dvdsmodexp 16070	If a positive integer divides another integer, this other integer is equal to its positive powers modulo the positive integer. (Formerly part of the proof for fermltl 16582). (Contributed by Mario Carneiro, 28-Feb-2014.) (Revised by AV, 19-Mar-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∥ 𝐴) → ((𝐴↑𝐵) mod 𝑁) = (𝐴 mod 𝑁))
Theorem	nndivdvds 16071	Strong form of dvdsval2 16065 for positive integers. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐵 ∥ 𝐴 ↔ (𝐴 / 𝐵) ∈ ℕ))
Theorem	nndivides 16072*	Definition of the divides relation for positive integers. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑀 ∥ 𝑁 ↔ ∃𝑛 ∈ ℕ (𝑛 · 𝑀) = 𝑁))
Theorem	moddvds 16073	Two ways to say 𝐴≡𝐵 (mod 𝑁), see also definition in [ApostolNT] p. 106. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 mod 𝑁) = (𝐵 mod 𝑁) ↔ 𝑁 ∥ (𝐴 − 𝐵)))
Theorem	modm1div 16074	An integer greater than one divides another integer minus one iff the second integer modulo the first integer is one. (Contributed by AV, 30-May-2023.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑁) = 1 ↔ 𝑁 ∥ (𝐴 − 1)))
Theorem	dvds0lem 16075	A lemma to assist theorems of ∥ with no antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝐾 · 𝑀) = 𝑁) → 𝑀 ∥ 𝑁)
Theorem	dvds1lem 16076*	A lemma to assist theorems of ∥ with one antecedent. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝜑 → (𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ))    &   ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → 𝑍 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ ℤ) → ((𝑥 · 𝐽) = 𝐾 → (𝑍 · 𝑀) = 𝑁))    ⇒   ⊢ (𝜑 → (𝐽 ∥ 𝐾 → 𝑀 ∥ 𝑁))
Theorem	dvds2lem 16077*	A lemma to assist theorems of ∥ with two antecedents. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝜑 → (𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ))    &   ⊢ (𝜑 → (𝐾 ∈ ℤ ∧ 𝐿 ∈ ℤ))    &   ⊢ (𝜑 → (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → 𝑍 ∈ ℤ)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ)) → (((𝑥 · 𝐼) = 𝐽 ∧ (𝑦 · 𝐾) = 𝐿) → (𝑍 · 𝑀) = 𝑁))    ⇒   ⊢ (𝜑 → ((𝐼 ∥ 𝐽 ∧ 𝐾 ∥ 𝐿) → 𝑀 ∥ 𝑁))
Theorem	iddvds 16078	An integer divides itself. Theorem 1.1(a) in [ApostolNT] p. 14 (reflexive property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 𝑁)
Theorem	1dvds 16079	1 divides any integer. Theorem 1.1(f) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → 1 ∥ 𝑁)
Theorem	dvds0 16080	Any integer divides 0. Theorem 1.1(g) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → 𝑁 ∥ 0)
Theorem	negdvdsb 16081	An integer divides another iff its negation does. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ -𝑀 ∥ 𝑁))
Theorem	dvdsnegb 16082	An integer divides another iff it divides its negation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ -𝑁))
Theorem	absdvdsb 16083	An integer divides another iff its absolute value does. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ (abs‘𝑀) ∥ 𝑁))
Theorem	dvdsabsb 16084	An integer divides another iff it divides its absolute value. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 ∥ 𝑁 ↔ 𝑀 ∥ (abs‘𝑁)))
Theorem	0dvds 16085	Only 0 is divisible by 0. Theorem 1.1(h) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (𝑁 ∈ ℤ → (0 ∥ 𝑁 ↔ 𝑁 = 0))
Theorem	dvdsmul1 16086	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∥ (𝑀 · 𝑁))
Theorem	dvdsmul2 16087	An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∥ (𝑀 · 𝑁))
Theorem	iddvdsexp 16088	An integer divides a positive integer power of itself. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → 𝑀 ∥ (𝑀↑𝑁))
Theorem	muldvds1 16089	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝐾 ∥ 𝑁))
Theorem	muldvds2 16090	If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 · 𝑀) ∥ 𝑁 → 𝑀 ∥ 𝑁))
Theorem	dvdscmul 16091	Multiplication by a constant maintains the divides relation. Theorem 1.1(d) in [ApostolNT] p. 14 (multiplication property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝐾 · 𝑀) ∥ (𝐾 · 𝑁)))
Theorem	dvdsmulc 16092	Multiplication by a constant maintains the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑀 ∥ 𝑁 → (𝑀 · 𝐾) ∥ (𝑁 · 𝐾)))
Theorem	dvdscmulr 16093	Cancellation law for the divides relation. Theorem 1.1(e) in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝐾 · 𝑀) ∥ (𝐾 · 𝑁) ↔ 𝑀 ∥ 𝑁))
Theorem	dvdsmulcr 16094	Cancellation law for the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ (𝐾 ∈ ℤ ∧ 𝐾 ≠ 0)) → ((𝑀 · 𝐾) ∥ (𝑁 · 𝐾) ↔ 𝑀 ∥ 𝑁))
Theorem	summodnegmod 16095	The sum of two integers modulo a positive integer equals zero iff the first of the two integers equals the negative of the other integer modulo the positive integer. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴 + 𝐵) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = (-𝐵 mod 𝑁)))
Theorem	modmulconst 16096	Constant multiplication in a modulo operation, see theorem 5.3 in [ApostolNT] p. 108. (Contributed by AV, 21-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) ∧ 𝑀 ∈ ℕ) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ ((𝐶 · 𝐴) mod (𝐶 · 𝑀)) = ((𝐶 · 𝐵) mod (𝐶 · 𝑀))))
Theorem	dvds2ln 16097	If an integer divides each of two other integers, it divides any linear combination of them. Theorem 1.1(c) in [ApostolNT] p. 14 (linearity property of the divides relation). (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ (((𝐼 ∈ ℤ ∧ 𝐽 ∈ ℤ) ∧ (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ ((𝐼 · 𝑀) + (𝐽 · 𝑁))))
Theorem	dvds2add 16098	If an integer divides each of two other integers, it divides their sum. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 + 𝑁)))
Theorem	dvds2sub 16099	If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁) → 𝐾 ∥ (𝑀 − 𝑁)))
Theorem	dvds2addd 16100	Deduction form of dvds2add 16098. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐾 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑀)    &   ⊢ (𝜑 → 𝐾 ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐾 ∥ (𝑀 + 𝑁))