P. 169 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	fissn0dvdsn0 16801*	For each finite subset of the integers not containing 0 there is a positive integer which is divisible by each element of this subset. (Contributed by AV, 21-Aug-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍) → {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛} ≠ ∅)
Theorem	lcmfval 16802*	Value of the lcm function. (lcm‘𝑍) is the least common multiple of the integers contained in the finite subset of integers 𝑍. If at least one of the elements of 𝑍 is 0, the result is defined conventionally as 0. (Contributed by AV, 21-Apr-2020.) (Revised by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → (lcm‘𝑍) = if(0 ∈ 𝑍, 0, inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < )))
Theorem	lcmf0val 16803	The value, by convention, of the least common multiple for a set containing 0 is 0. (Contributed by AV, 21-Apr-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 0 ∈ 𝑍) → (lcm‘𝑍) = 0)
Theorem	lcmfn0val 16804*	The value of the lcm function for a set without 0. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍) → (lcm‘𝑍) = inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < ))
Theorem	lcmfnnval 16805*	The value of the lcm function for a subset of the positive integers. (Contributed by AV, 21-Aug-2020.) (Revised by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin) → (lcm‘𝑍) = inf({𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛}, ℝ, < ))
Theorem	lcmfcllem 16806*	Lemma for lcmfn0cl 16807 and dvdslcmf 16812. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍) → (lcm‘𝑍) ∈ {𝑛 ∈ ℕ ∣ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑛})
Theorem	lcmfn0cl 16807	Closure of the lcm function. (Contributed by AV, 21-Aug-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍) → (lcm‘𝑍) ∈ ℕ)
Theorem	lcmfpr 16808	The value of the lcm function for an unordered pair is the value of the lcm operator for both elements. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (lcm‘{𝑀, 𝑁}) = (𝑀 lcm 𝑁))
Theorem	lcmfcl 16809	Closure of the lcm function. (Contributed by AV, 21-Aug-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → (lcm‘𝑍) ∈ ℕ0)
Theorem	lcmfnncl 16810	Closure of the lcm function. (Contributed by AV, 20-Apr-2020.)
⊢ ((𝑍 ⊆ ℕ ∧ 𝑍 ∈ Fin) → (lcm‘𝑍) ∈ ℕ)
Theorem	lcmfeq0b 16811	The least common multiple of a set of integers is 0 iff at least one of its element is 0. (Contributed by AV, 21-Aug-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → ((lcm‘𝑍) = 0 ↔ 0 ∈ 𝑍))
Theorem	dvdslcmf 16812*	The least common multiple of a set of integers is divisible by each of its elements. (Contributed by AV, 22-Aug-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → ∀𝑥 ∈ 𝑍 𝑥 ∥ (lcm‘𝑍))
Theorem	lcmfledvds 16813*	A positive integer which is divisible by all elements of a set of integers bounds the least common multiple of the set. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ ((𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍) → ((𝐾 ∈ ℕ ∧ ∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾) → (lcm‘𝑍) ≤ 𝐾))
Theorem	lcmf 16814*	Characterization of the least common multiple of a set of integers (without 0): A positiven integer is the least common multiple of a set of integers iff it divides each of the elements of the set and every integer which divides each of the elements of the set is greater than or equal to this integer. (Contributed by AV, 22-Aug-2020.)
⊢ ((𝐾 ∈ ℕ ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin ∧ 0 ∉ 𝑍)) → (𝐾 = (lcm‘𝑍) ↔ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ∧ ∀𝑘 ∈ ℕ (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝑘 → 𝐾 ≤ 𝑘))))
Theorem	lcmf0 16815	The least common multiple of the empty set is 1. (Contributed by AV, 22-Aug-2020.) (Proof shortened by AV, 16-Sep-2020.)
⊢ (lcm‘∅) = 1
Theorem	lcmfsn 16816	The least common multiple of a singleton is its absolute value. (Contributed by AV, 22-Aug-2020.)
⊢ (𝑀 ∈ ℤ → (lcm‘{𝑀}) = (abs‘𝑀))
Theorem	lcmftp 16817	The least common multiple of a triple of integers is the least common multiple of the third integer and the least common multiple of the first two integers. Although there would be a shorter proof using lcmfunsn 16825, this explicit proof (not based on induction) should be kept. (Proof modification is discouraged.) (Contributed by AV, 23-Aug-2020.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) → (lcm‘{𝐴, 𝐵, 𝐶}) = ((𝐴 lcm 𝐵) lcm 𝐶))
Theorem	lcmfunsnlem1 16818*	Lemma for lcmfdvds 16823 and lcmfunsnlem 16822 (Induction step part 1). (Contributed by AV, 25-Aug-2020.)
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑘 ∈ ℤ (∀𝑚 ∈ (𝑦 ∪ {𝑧})𝑚 ∥ 𝑘 → (lcm‘(𝑦 ∪ {𝑧})) ∥ 𝑘))
Theorem	lcmfunsnlem2lem1 16819*	Lemma 1 for lcmfunsnlem2 16821. (Contributed by AV, 26-Aug-2020.)
⊢ (((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → ∀𝑘 ∈ ℕ (∀𝑖 ∈ ((𝑦 ∪ {𝑧}) ∪ {𝑛})𝑖 ∥ 𝑘 → ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛) ≤ 𝑘))
Theorem	lcmfunsnlem2lem2 16820*	Lemma 2 for lcmfunsnlem2 16821. (Contributed by AV, 26-Aug-2020.)
⊢ (((0 ∉ 𝑦 ∧ 𝑧 ≠ 0 ∧ 𝑛 ≠ 0) ∧ (𝑛 ∈ ℤ ∧ ((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))))) → (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
Theorem	lcmfunsnlem2 16821*	Lemma for lcmfunsn 16825 and lcmfunsnlem 16822 (Induction step part 2). (Contributed by AV, 26-Aug-2020.)
⊢ (((𝑧 ∈ ℤ ∧ 𝑦 ⊆ ℤ ∧ 𝑦 ∈ Fin) ∧ (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑦 𝑚 ∥ 𝑘 → (lcm‘𝑦) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑦 ∪ {𝑛})) = ((lcm‘𝑦) lcm 𝑛))) → ∀𝑛 ∈ ℤ (lcm‘((𝑦 ∪ {𝑧}) ∪ {𝑛})) = ((lcm‘(𝑦 ∪ {𝑧})) lcm 𝑛))
Theorem	lcmfunsnlem 16822*	Lemma for lcmfdvds 16823 and lcmfunsn 16825. These two theorems must be proven simultaneously by induction on the cardinality of a finite set 𝑌, because they depend on each other. This can be seen by the two parts lcmfunsnlem1 16818 and lcmfunsnlem2 16821 of the induction step, each of them using both induction hypotheses. (Contributed by AV, 26-Aug-2020.)
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) → (∀𝑘 ∈ ℤ (∀𝑚 ∈ 𝑌 𝑚 ∥ 𝑘 → (lcm‘𝑌) ∥ 𝑘) ∧ ∀𝑛 ∈ ℤ (lcm‘(𝑌 ∪ {𝑛})) = ((lcm‘𝑌) lcm 𝑛)))
Theorem	lcmfdvds 16823*	The least common multiple of a set of integers divides any integer which is divisible by all elements of the set. (Contributed by AV, 26-Aug-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 → (lcm‘𝑍) ∥ 𝐾))
Theorem	lcmfdvdsb 16824*	Biconditional form of lcmfdvds 16823. (Contributed by AV, 26-Aug-2020.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin) → (∀𝑚 ∈ 𝑍 𝑚 ∥ 𝐾 ↔ (lcm‘𝑍) ∥ 𝐾))
Theorem	lcmfunsn 16825	The lcm function for a union of a set of integer and a singleton. (Contributed by AV, 26-Aug-2020.)
⊢ ((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin ∧ 𝑁 ∈ ℤ) → (lcm‘(𝑌 ∪ {𝑁})) = ((lcm‘𝑌) lcm 𝑁))
Theorem	lcmfun 16826	The lcm function for a union of sets of integers. (Contributed by AV, 27-Aug-2020.)
⊢ (((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin)) → (lcm‘(𝑌 ∪ 𝑍)) = ((lcm‘𝑌) lcm (lcm‘𝑍)))
Theorem	lcmfass 16827	Associative law for the lcm function. (Contributed by AV, 27-Aug-2020.)
⊢ (((𝑌 ⊆ ℤ ∧ 𝑌 ∈ Fin) ∧ (𝑍 ⊆ ℤ ∧ 𝑍 ∈ Fin)) → (lcm‘({(lcm‘𝑌)} ∪ 𝑍)) = (lcm‘(𝑌 ∪ {(lcm‘𝑍)})))
Theorem	lcmf2a3a4e12 16828	The least common multiple of 2 , 3 and 4 is 12. (Contributed by AV, 27-Aug-2020.)
⊢ (lcm‘{2, 3, 4}) = ;12
Theorem	lcmflefac 16829	The least common multiple of all positive integers less than or equal to an integer is less than or equal to the factorial of the integer. (Contributed by AV, 16-Aug-2020.) (Revised by AV, 27-Aug-2020.)
⊢ (𝑁 ∈ ℕ → (lcm‘(1...𝑁)) ≤ (!‘𝑁))
6.1.12  Coprimality and Euclid's lemma According to Wikipedia "Coprime integers", see https://en.wikipedia.org/wiki/Coprime_integers (16-Aug-2020) "[...] two integers a and b are said to be relatively prime, mutually prime, or coprime [...] if the only positive integer (factor) that divides both of them is 1. Consequently, any prime number that divides one does not divide the other. This is equivalent to their greatest common divisor (gcd) being 1.". In the following, we use this equivalent characterization to say that 𝐴 ∈ ℤ and 𝐵 ∈ ℤ are coprime (or relatively prime) if (𝐴 gcd 𝐵) = 1. The equivalence of the definitions is shown by coprmgcdb 16830. The negation, i.e. two integers are not coprime, can be expressed either by (𝐴 gcd 𝐵) ≠ 1, see ncoprmgcdne1b 16831, or equivalently by 1 < (𝐴 gcd 𝐵), see ncoprmgcdgt1b 16832. A proof of Euclid's lemma based on coprimality is provided in coprmdvds 16834 (see euclemma 16895 for a version of Euclid's lemma for primes).
Theorem	coprmgcdb 16830*	Two positive integers are coprime, i.e. the only positive integer that divides both of them is 1, iff their greatest common divisor is 1. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1))
Theorem	ncoprmgcdne1b 16831*	Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is not 1. See prmdvdsncoprmbd 16909 for a version where the existential quantifier is restricted to primes. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑖 ∈ (ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1))
Theorem	ncoprmgcdgt1b 16832*	Two positive integers are not coprime, i.e. there is an integer greater than 1 which divides both integers, iff their greatest common divisor is greater than 1. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑖 ∈ (ℤ≥‘2)(𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) ↔ 1 < (𝐴 gcd 𝐵)))
Theorem	coprmdvds1 16833	If two positive integers are coprime, i.e. their greatest common divisor is 1, the only positive integer that divides both of them is 1. (Contributed by AV, 4-Aug-2021.)
⊢ ((𝐹 ∈ ℕ ∧ 𝐺 ∈ ℕ ∧ (𝐹 gcd 𝐺) = 1) → ((𝐼 ∈ ℕ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐼 = 1))
Theorem	coprmdvds 16834	Euclid's Lemma (see ProofWiki "Euclid's Lemma", 10-Jul-2021, https://proofwiki.org/wiki/Euclid's_Lemma): If an integer divides the product of two integers and is coprime to one of them, then it divides the other. See also theorem 1.5 in [ApostolNT] p. 16. Generalization of euclemma 16895. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by AV, 10-Jul-2021.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐾 ∥ (𝑀 · 𝑁) ∧ (𝐾 gcd 𝑀) = 1) → 𝐾 ∥ 𝑁))
Theorem	coprmdvds2 16835	If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → ((𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾) → (𝑀 · 𝑁) ∥ 𝐾))
Theorem	mulgcddvds 16836	One half of rpmulgcd2 16837, which does not need the coprimality assumption. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 gcd (𝑀 · 𝑁)) ∥ ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))
Theorem	rpmulgcd2 16837	If 𝑀 is relatively prime to 𝑁, then the GCD of 𝐾 with 𝑀 · 𝑁 is the product of the GCDs with 𝑀 and 𝑁 respectively. (Contributed by Mario Carneiro, 2-Jul-2015.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ (𝑀 gcd 𝑁) = 1) → (𝐾 gcd (𝑀 · 𝑁)) = ((𝐾 gcd 𝑀) · (𝐾 gcd 𝑁)))
Theorem	qredeq 16838	Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1) ∧ (𝑃 ∈ ℤ ∧ 𝑄 ∈ ℕ ∧ (𝑃 gcd 𝑄) = 1) ∧ (𝑀 / 𝑁) = (𝑃 / 𝑄)) → (𝑀 = 𝑃 ∧ 𝑁 = 𝑄))
Theorem	qredeu 16839*	Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))
Theorem	rpmul 16840	If 𝐾 is relatively prime to 𝑀 and to 𝑁, it is also relatively prime to their product. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
⊢ ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝐾 gcd 𝑀) = 1 ∧ (𝐾 gcd 𝑁) = 1) → (𝐾 gcd (𝑀 · 𝑁)) = 1))
Theorem	rpdvds 16841	If 𝐾 is relatively prime to 𝑁 then it is also relatively prime to any divisor 𝑀 of 𝑁. (Contributed by Mario Carneiro, 19-Jun-2015.)
⊢ (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝐾 gcd 𝑁) = 1 ∧ 𝑀 ∥ 𝑁)) → (𝐾 gcd 𝑀) = 1)
Theorem	coprmprod 16842*	The product of the elements of a sequence of pairwise coprime positive integers is coprime to a positive integer which is coprime to all integers of the sequence. (Contributed by AV, 18-Aug-2020.)
⊢ (((𝑀 ∈ Fin ∧ 𝑀 ⊆ ℕ ∧ 𝑁 ∈ ℕ) ∧ 𝐹:ℕ⟶ℕ ∧ ∀𝑚 ∈ 𝑀 ((𝐹‘𝑚) gcd 𝑁) = 1) → (∀𝑚 ∈ 𝑀 ∀𝑛 ∈ (𝑀 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 → (∏𝑚 ∈ 𝑀 (𝐹‘𝑚) gcd 𝑁) = 1))
Theorem	coprmproddvdslem 16843*	Lemma for coprmproddvds 16844: Induction step. (Contributed by AV, 19-Aug-2020.)
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((((𝑦 ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ 𝑦 ∀𝑛 ∈ (𝑦 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑦 (𝐹‘𝑚) ∥ 𝐾) → ((((𝑦 ∪ {𝑧}) ⊆ ℕ ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ)) ∧ (∀𝑚 ∈ (𝑦 ∪ {𝑧})∀𝑛 ∈ ((𝑦 ∪ {𝑧}) ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ (𝑦 ∪ {𝑧})(𝐹‘𝑚) ∥ 𝐾)))
Theorem	coprmproddvds 16844*	If a positive integer is divisible by each element of a set of pairwise coprime positive integers, then it is divisible by their product. (Contributed by AV, 19-Aug-2020.)
⊢ (((𝑀 ⊆ ℕ ∧ 𝑀 ∈ Fin) ∧ (𝐾 ∈ ℕ ∧ 𝐹:ℕ⟶ℕ) ∧ (∀𝑚 ∈ 𝑀 ∀𝑛 ∈ (𝑀 ∖ {𝑚})((𝐹‘𝑚) gcd (𝐹‘𝑛)) = 1 ∧ ∀𝑚 ∈ 𝑀 (𝐹‘𝑚) ∥ 𝐾)) → ∏𝑚 ∈ 𝑀 (𝐹‘𝑚) ∥ 𝐾)
6.1.13  Cancellability of congruences
Theorem	congr 16845*	Definition of congruence by integer multiple (see ProofWiki "Congruence (Number Theory)", 11-Jul-2021, https://proofwiki.org/wiki/Definition:Congruence_(Number_Theory)): An integer 𝐴 is congruent to an integer 𝐵 modulo 𝑀 if their difference is a multiple of 𝑀. See also the definition in [ApostolNT] p. 104: "... 𝑎 is congruent to 𝑏 modulo 𝑚, and we write 𝑎≡𝑏 (mod 𝑚) if 𝑚 divides the difference 𝑎 − 𝑏", or Wikipedia "Modular arithmetic - Congruence", https://en.wikipedia.org/wiki/Modular_arithmetic#Congruence, 11-Jul-2021,: "Given an integer n > 1, called a modulus, two integers are said to be congruent modulo n, if n is a divisor of their difference (i.e., if there is an integer k such that a-b = kn)". (Contributed by AV, 11-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) ↔ ∃𝑛 ∈ ℤ (𝑛 · 𝑀) = (𝐴 − 𝐵)))
Theorem	divgcdcoprm0 16846	Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
Theorem	divgcdcoprmex 16847*	Integers divided by gcd are coprime (see ProofWiki "Integers Divided by GCD are Coprime", 11-Jul-2021, https://proofwiki.org/wiki/Integers_Divided_by_GCD_are_Coprime): Any pair of integers, not both zero, can be reduced to a pair of coprime ones by dividing them by their gcd. (Contributed by AV, 12-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) ∧ 𝑀 = (𝐴 gcd 𝐵)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ (𝐴 = (𝑀 · 𝑎) ∧ 𝐵 = (𝑀 · 𝑏) ∧ (𝑎 gcd 𝑏) = 1))
Theorem	cncongr1 16848	One direction of the bicondition in cncongr 16850. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
Theorem	cncongr2 16849	The other direction of the bicondition in cncongr 16850. (Contributed by AV, 11-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)))
Theorem	cncongr 16850	Cancellability of Congruences (see ProofWiki "Cancellability of Congruences, https://proofwiki.org/wiki/Cancellability_of_Congruences, 10-Jul-2021): Two products with a common factor are congruent modulo a positive integer iff the other factors are congruent modulo the integer divided by the greatest common divisor of the integer and the common factor. See also Theorem 5.4 "Cancellation law" in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
Theorem	cncongrcoprm 16851	Corollary 1 of Cancellability of Congruences: Two products with a common factor are congruent modulo an integer being coprime to the common factor iff the other factors are congruent modulo the integer. (Contributed by AV, 13-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ (𝐶 gcd 𝑁) = 1)) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) ↔ (𝐴 mod 𝑁) = (𝐵 mod 𝑁)))
6.2  Elementary prime number theory
6.2.1  Elementary properties Remark: to represent odd prime numbers, i.e., all prime numbers except 2, the idiom 𝑃 ∈ (ℙ ∖ {2}) is used. It is a little bit shorter than (𝑃 ∈ ℙ ∧ 𝑃 ≠ 2). Both representations can be converted into each other by eldifsn 4744.
Syntax	cprime 16852	Extend the definition of a class to include the set of prime numbers.
class ℙ
Definition	df-prm 16853*	Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o}
Theorem	isprm 16854*	The predicate "is a prime number". A prime number is a positive integer with exactly two positive divisors. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ ℕ ∧ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o))
Theorem	prmnn 16855	A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Theorem	prmz 16856	A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
Theorem	prmssnn 16857	The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.)
⊢ ℙ ⊆ ℕ
Theorem	prmex 16858	The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.)
⊢ ℙ ∈ V
Theorem	0nprm 16859	0 is not a prime number. Already Definition df-prm 16853 excludes 0 from being prime (ℙ = {𝑝 ∈ ℕ ∣ ...), but even if 𝑝 ∈ ℕ0 was allowed, the condition {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o would not hold for 𝑝 = 0, because {𝑛 ∈ ℕ ∣ 𝑛 ∥ 0} = ℕ, see dvds0 16447, and ¬ ℕ ≈ 2o (there are more than 2 positive integers). (Contributed by AV, 29-May-2023.)
⊢ ¬ 0 ∈ ℙ
Theorem	1nprm 16860	1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.)
⊢ ¬ 1 ∈ ℙ
Theorem	1idssfct 16861*	The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℕ → {1, 𝑁} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁})
Theorem	isprm2lem 16862*	Lemma for isprm2 16863. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}))
Theorem	isprm2 16863*	The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only positive divisors are 1 and itself. Definition in [ApostolNT] p. 16. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))))
Theorem	isprm3 16864*	The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ (2...(𝑃 − 1)) ¬ 𝑧 ∥ 𝑃))
Theorem	isprm4 16865*	The predicate "is a prime number". A prime number is an integer greater than or equal to 2 whose only divisor greater than or equal to 2 is itself. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ (ℤ≥‘2)(𝑧 ∥ 𝑃 → 𝑧 = 𝑃)))
Theorem	prmind2 16866*	A variation on prmind 16867 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))    &   ⊢ 𝜓    &   ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)    &   ⊢ ((𝑦 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜂)
Theorem	prmind 16867*	Perform induction over the multiplicative structure of ℕ. If a property 𝜑(𝑥) holds for the primes and 1 and is preserved under multiplication, then it holds for every positive integer. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))    &   ⊢ 𝜓    &   ⊢ (𝑥 ∈ ℙ → 𝜑)    &   ⊢ ((𝑦 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜂)
Theorem	dvdsprime 16868	If 𝑀 divides a prime, then 𝑀 is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ) → (𝑀 ∥ 𝑃 ↔ (𝑀 = 𝑃 ∨ 𝑀 = 1)))
Theorem	nprm 16869	A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐴 · 𝐵) ∈ ℙ)
Theorem	nprmi 16870	An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 1 < 𝐴    &   ⊢ 1 < 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝑁    ⇒   ⊢ ¬ 𝑁 ∈ ℙ
Theorem	dvdsnprmd 16871	If a number is divisible by an integer greater than 1 and less than the number, the number is not prime. (Contributed by AV, 24-Jul-2021.)
⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐴 < 𝑁)    &   ⊢ (𝜑 → 𝐴 ∥ 𝑁)    ⇒   ⊢ (𝜑 → ¬ 𝑁 ∈ ℙ)
Theorem	prm2orodd 16872	A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.)
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃))
Theorem	2prm 16873	2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ 2 ∈ ℙ
Theorem	2mulprm 16874	A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.)
⊢ (𝐴 ∈ ℤ → ((2 · 𝐴) ∈ ℙ ↔ 𝐴 = 1))
Theorem	3prm 16875	3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 3 ∈ ℙ
Theorem	4nprm 16876	4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 4 ∈ ℙ
Theorem	prmuz2 16877	A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
Theorem	prmssuz2 16878	The primes are integers greater than 1. (Contributed by AV, 10-Apr-2026.)
⊢ ℙ ⊆ (ℤ≥‘2)
Theorem	prmgt1 16879	A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
Theorem	prmm2nn0 16880	Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈ ℕ0)
Theorem	oddprmgt2 16881	An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
Theorem	oddprmge3 16882	An odd prime is greater than or equal to 3. (Contributed by Alexander van der Vekens, 7-Oct-2018.) (Revised by AV, 20-Aug-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 𝑃 ∈ (ℤ≥‘3))
Theorem	ge2nprmge4 16883	A composite integer greater than or equal to 2 is greater than or equal to 4. (Contributed by AV, 5-Jun-2023.)
⊢ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝑋 ∉ ℙ) → 𝑋 ∈ (ℤ≥‘4))
Theorem	sqnprm 16884	A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝐴 ∈ ℤ → ¬ (𝐴↑2) ∈ ℙ)
Theorem	dvdsprm 16885	An integer greater than or equal to 2 divides a prime number iff it is equal to it. (Contributed by Paul Chapman, 26-Oct-2012.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ) → (𝑁 ∥ 𝑃 ↔ 𝑁 = 𝑃))
Theorem	exprmfct 16886*	Every integer greater than or equal to 2 has a prime factor. (Contributed by Paul Chapman, 26-Oct-2012.) (Proof shortened by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑁 ∈ (ℤ≥‘2) → ∃𝑝 ∈ ℙ 𝑝 ∥ 𝑁)
Theorem	prmdvdsfz 16887*	Each integer greater than 1 and less than or equal to a fixed number is divisible by a prime less than or equal to this fixed number. (Contributed by AV, 15-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → ∃𝑝 ∈ ℙ (𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼))
Theorem	nprmdvds1 16888	No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
Theorem	isprm5 16889*	One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
Theorem	isprm7 16890*	One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. This version of isprm5 16889 combines the primality and bound on 𝑧 into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃))
Theorem	maxprmfct 16891*	The set of prime factors of an integer greater than or equal to 2 satisfies the conditions to have a supremum, and that supremum is a member of the set. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ 𝑆 = {𝑧 ∈ ℙ ∣ 𝑧 ∥ 𝑁}    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘2) → ((𝑆 ⊆ ℤ ∧ 𝑆 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝑆 𝑦 ≤ 𝑥) ∧ sup(𝑆, ℝ, < ) ∈ 𝑆))
Theorem	divgcdodd 16892	Either 𝐴 / (𝐴 gcd 𝐵) is odd or 𝐵 / (𝐴 gcd 𝐵) is odd. (Contributed by Scott Fenton, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
6.2.2  Coprimality and Euclid's lemma (cont.) This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 16895.
Theorem	coprm 16893	A prime number either divides an integer or is coprime to it, but not both. Theorem 1.8 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (¬ 𝑃 ∥ 𝑁 ↔ (𝑃 gcd 𝑁) = 1))
Theorem	prmrp 16894	Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
Theorem	euclemma 16895	Euclid's lemma. A prime number divides the product of two integers iff it divides at least one of them. Theorem 1.9 in [ApostolNT] p. 17. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑃 ∥ (𝑀 · 𝑁) ↔ (𝑃 ∥ 𝑀 ∨ 𝑃 ∥ 𝑁)))
Theorem	isprm6 16896*	A number is prime iff it satisfies Euclid's lemma euclemma 16895. (Contributed by Mario Carneiro, 6-Sep-2015.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))
Theorem	prmdvdsexp 16897	A prime divides a positive power of an integer iff it divides the integer. (Contributed by Mario Carneiro, 24-Feb-2014.) (Revised by Mario Carneiro, 17-Jul-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (𝐴↑𝑁) ↔ 𝑃 ∥ 𝐴))
Theorem	prmdvdsexpb 16898	A prime divides a positive power of another iff they are equal. (Contributed by Paul Chapman, 30-Nov-2012.) (Revised by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃 ∥ (𝑄↑𝑁) ↔ 𝑃 = 𝑄))
Theorem	prmdvdsexpr 16899	If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑃 ∥ (𝑄↑𝑁) → 𝑃 = 𝑄))
Theorem	prmdvdssq 16900	Condition for a prime dividing a square. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof shortened by SN, 21-Aug-2024.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 ∥ 𝑀 ↔ 𝑃 ∥ (𝑀↑2)))