P. 129 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	qredeq 12801	Two equal reduced fractions have the same numerator and denominator. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1) ∧ (𝑃 ∈ ℤ ∧ 𝑄 ∈ ℕ ∧ (𝑃 gcd 𝑄) = 1) ∧ (𝑀 / 𝑁) = (𝑃 / 𝑄)) → (𝑀 = 𝑃 ∧ 𝑁 = 𝑄))
Theorem	qredeu 12802*	Every rational number has a unique reduced form. (Contributed by Jeff Hankins, 29-Sep-2013.)
⊢ (𝐴 ∈ ℚ → ∃!𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))
Theorem	rpmul 12803	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 12804	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)
5.1.12  Cancellability of congruences
Theorem	congr 12805*	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 12806	Integers divided by gcd are coprime. (Contributed by AV, 12-Jul-2021.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐵 ≠ 0) → ((𝐴 / (𝐴 gcd 𝐵)) gcd (𝐵 / (𝐴 gcd 𝐵))) = 1)
Theorem	divgcdcoprmex 12807*	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 12808	One direction of the bicondition in cncongr 12810. Theorem 5.4 in [ApostolNT] p. 109. (Contributed by AV, 13-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → (((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁) → (𝐴 mod 𝑀) = (𝐵 mod 𝑀)))
Theorem	cncongr2 12809	The other direction of the bicondition in cncongr 12810. (Contributed by AV, 11-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁)))
Theorem	cncongr 12810	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 greates 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 12811	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 𝑁)))
5.2  Elementary prime number theory
5.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 3822.
Syntax	cprime 12812	Extend the definition of a class to include the set of prime numbers.
class ℙ
Definition	df-prm 12813*	Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o}
Theorem	isprm 12814*	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 12815	A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ)
Theorem	prmz 12816	A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ)
Theorem	prmssnn 12817	The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.)
⊢ ℙ ⊆ ℕ
Theorem	prmex 12818	The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.)
⊢ ℙ ∈ V
Theorem	1nprm 12819	1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.)
⊢ ¬ 1 ∈ ℙ
Theorem	1idssfct 12820*	The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ (𝑁 ∈ ℕ → {1, 𝑁} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁})
Theorem	isprm2lem 12821*	Lemma for isprm2 12822. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃}))
Theorem	isprm2 12822*	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 12823*	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 12824*	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 12825*	A variation on prmind 12826 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓))    &   ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃))    &   ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂))    &   ⊢ 𝜓    &   ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑)    &   ⊢ ((𝑦 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏))    ⇒   ⊢ (𝐴 ∈ ℕ → 𝜂)
Theorem	prmind 12826*	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 12827	If 𝑀 divides a prime, then 𝑀 is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ) → (𝑀 ∥ 𝑃 ↔ (𝑀 = 𝑃 ∨ 𝑀 = 1)))
Theorem	nprm 12828	A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐴 · 𝐵) ∈ ℙ)
Theorem	nprmi 12829	An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 1 < 𝐴    &   ⊢ 1 < 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝑁    ⇒   ⊢ ¬ 𝑁 ∈ ℙ
Theorem	dvdsnprmd 12830	If a number is divisible by an integer greater than 1 and less then the number, the number is not prime. (Contributed by AV, 24-Jul-2021.)
⊢ (𝜑 → 1 < 𝐴)    &   ⊢ (𝜑 → 𝐴 < 𝑁)    &   ⊢ (𝜑 → 𝐴 ∥ 𝑁)    ⇒   ⊢ (𝜑 → ¬ 𝑁 ∈ ℙ)
Theorem	prm2orodd 12831	A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.)
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃))
Theorem	2prm 12832	2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ 2 ∈ ℙ
Theorem	3prm 12833	3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 3 ∈ ℙ
Theorem	4nprm 12834	4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 4 ∈ ℙ
Theorem	prmdc 12835	Primality is decidable. (Contributed by Jim Kingdon, 30-Sep-2024.)
⊢ (𝑁 ∈ ℕ → DECID 𝑁 ∈ ℙ)
Theorem	prmuz2 12836	A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
Theorem	prmgt1 12837	A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
Theorem	prmm2nn0 12838	Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈ ℕ0)
Theorem	oddprmgt2 12839	An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
Theorem	oddprmge3 12840	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	sqnprm 12841	A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝐴 ∈ ℤ → ¬ (𝐴↑2) ∈ ℙ)
Theorem	dvdsprm 12842	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 12843*	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 12844*	Each integer greater than 1 and less then or equal to a fixed number is divisible by a prime less then or equal to this fixed number. (Contributed by AV, 15-Aug-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐼 ∈ (2...𝑁)) → ∃𝑝 ∈ ℙ (𝑝 ≤ 𝑁 ∧ 𝑝 ∥ 𝐼))
Theorem	nprmdvds1 12845	No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
Theorem	isprm5lem 12846*	Lemma for isprm5 12847. The interesting direction (showing that one only needs to check prime divisors up to the square root of 𝑃). (Contributed by Jim Kingdon, 20-Oct-2024.)
⊢ (𝜑 → 𝑃 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃))    &   ⊢ (𝜑 → 𝑋 ∈ (2...(𝑃 − 1)))    ⇒   ⊢ (𝜑 → ¬ 𝑋 ∥ 𝑃)
Theorem	isprm5 12847*	One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ℙ ((𝑧↑2) ≤ 𝑃 → ¬ 𝑧 ∥ 𝑃)))
Theorem	divgcdodd 12848	Either 𝐴 / (𝐴 gcd 𝐵) is odd or 𝐵 / (𝐴 gcd 𝐵) is odd. (Contributed by Scott Fenton, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵))))
5.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 12851.
Theorem	coprm 12849	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 12850	Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
Theorem	euclemma 12851	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 12852*	A number is prime iff it satisfies Euclid's lemma euclemma 12851. (Contributed by Mario Carneiro, 6-Sep-2015.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))
Theorem	prmdvdsexp 12853	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 12854	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 12855	If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑃 ∥ (𝑄↑𝑁) → 𝑃 = 𝑄))
Theorem	prmexpb 12856	Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (𝑄↑𝑁) ↔ (𝑃 = 𝑄 ∧ 𝑀 = 𝑁)))
Theorem	prmfac1 12857	The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (!‘𝑁)) → 𝑃 ≤ 𝑁)
Theorem	rpexp 12858	If two numbers 𝐴 and 𝐵 are relatively prime, then they are still relatively prime if raised to a power. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (((𝐴↑𝑁) gcd 𝐵) = 1 ↔ (𝐴 gcd 𝐵) = 1))
Theorem	rpexp1i 12859	Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd 𝐵) = 1))
Theorem	rpexp12i 12860	Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd (𝐵↑𝑁)) = 1))
Theorem	prmndvdsfaclt 12861	A prime number does not divide the factorial of a nonnegative integer less than the prime number. (Contributed by AV, 13-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑁 < 𝑃 → ¬ 𝑃 ∥ (!‘𝑁)))
Theorem	cncongrprm 12862	Corollary 2 of Cancellability of Congruences: Two products with a common factor are congruent modulo a prime number not dividing the common factor iff the other factors are congruent modulo the prime number. (Contributed by AV, 13-Jul-2021.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ ¬ 𝑃 ∥ 𝐶)) → (((𝐴 · 𝐶) mod 𝑃) = ((𝐵 · 𝐶) mod 𝑃) ↔ (𝐴 mod 𝑃) = (𝐵 mod 𝑃)))
Theorem	isevengcd2 12863	The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.)
⊢ (𝑍 ∈ ℤ → (2 ∥ 𝑍 ↔ (2 gcd 𝑍) = 2))
Theorem	isoddgcd1 12864	The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) (Revised by AV, 8-Aug-2021.)
⊢ (𝑍 ∈ ℤ → (¬ 2 ∥ 𝑍 ↔ (2 gcd 𝑍) = 1))
Theorem	3lcm2e6 12865	The least common multiple of three and two is six. The operands are unequal primes and thus coprime, so the result is (the absolute value of) their product. (Contributed by Steve Rodriguez, 20-Jan-2020.) (Proof shortened by AV, 27-Aug-2020.)
⊢ (3 lcm 2) = 6
5.2.3  Non-rationality of square root of 2
Theorem	sqrt2irrlem 12866	Lemma for sqrt2irr 12867. 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). (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 12-Sep-2015.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (√‘2) = (𝐴 / 𝐵))    ⇒   ⊢ (𝜑 → ((𝐴 / 2) ∈ ℤ ∧ (𝐵 / 2) ∈ ℕ))
Theorem	sqrt2irr 12867	The square root of 2 is not rational. That is, for any rational number, (√‘2) does not equal it. However, if we were to say "the square root of 2 is irrational" that would mean something stronger: "for any rational number, (√‘2) is apart from it" (the two statements are equivalent given excluded middle). See sqrt2irrap 12885 for the proof that the square root of two is irrational. The proof's core is proven in sqrt2irrlem 12866, which shows that if 𝐴 / 𝐵 = √(2), then 𝐴 and 𝐵 are even, so 𝐴 / 2 and 𝐵 / 2 are smaller representatives, which is absurd. (Contributed by NM, 8-Jan-2002.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ (√‘2) ∉ ℚ
Theorem	sqrt2re 12868	The square root of 2 exists and is a real number. (Contributed by NM, 3-Dec-2004.)
⊢ (√‘2) ∈ ℝ
Theorem	sqrt2irr0 12869	The square root of 2 is not rational. (Contributed by AV, 23-Dec-2022.)
⊢ (√‘2) ∈ (ℝ ∖ ℚ)
Theorem	pw2dvdslemn 12870*	Lemma for pw2dvds 12871. If a natural number has some power of two which does not divide it, there is a highest power of two which does divide it. (Contributed by Jim Kingdon, 14-Nov-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ ¬ (2↑𝐴) ∥ 𝑁) → ∃𝑚 ∈ ℕ0 ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁))
Theorem	pw2dvds 12871*	A natural number has a highest power of two which divides it. (Contributed by Jim Kingdon, 14-Nov-2021.)
⊢ (𝑁 ∈ ℕ → ∃𝑚 ∈ ℕ0 ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁))
Theorem	pw2dvdseulemle 12872	Lemma for pw2dvdseu 12873. Powers of two which do and do not divide a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ0)    &   ⊢ (𝜑 → (2↑𝐴) ∥ 𝑁)    &   ⊢ (𝜑 → ¬ (2↑(𝐵 + 1)) ∥ 𝑁)    ⇒   ⊢ (𝜑 → 𝐴 ≤ 𝐵)
Theorem	pw2dvdseu 12873*	A natural number has a unique highest power of two which divides it. (Contributed by Jim Kingdon, 16-Nov-2021.)
⊢ (𝑁 ∈ ℕ → ∃!𝑚 ∈ ℕ0 ((2↑𝑚) ∥ 𝑁 ∧ ¬ (2↑(𝑚 + 1)) ∥ 𝑁))
Theorem	oddpwdclemxy 12874*	Lemma for oddpwdc 12879. Another way of stating that decomposing a natural number into a power of two and an odd number is unique. (Contributed by Jim Kingdon, 16-Nov-2021.)
⊢ ((((𝑋 ∈ ℕ ∧ ¬ 2 ∥ 𝑋) ∧ 𝑌 ∈ ℕ0) ∧ 𝐴 = ((2↑𝑌) · 𝑋)) → (𝑋 = (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))))
Theorem	oddpwdclemdvds 12875*	Lemma for oddpwdc 12879. A natural number is divisible by the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ (𝐴 ∈ ℕ → (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴))) ∥ 𝐴)
Theorem	oddpwdclemndvds 12876*	Lemma for oddpwdc 12879. A natural number is not divisible by one more than the highest power of two which divides it. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ (𝐴 ∈ ℕ → ¬ (2↑((℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)) + 1)) ∥ 𝐴)
Theorem	oddpwdclemodd 12877*	Lemma for oddpwdc 12879. Removing the powers of two from a natural number produces an odd number. (Contributed by Jim Kingdon, 16-Nov-2021.)
⊢ (𝐴 ∈ ℕ → ¬ 2 ∥ (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))
Theorem	oddpwdclemdc 12878*	Lemma for oddpwdc 12879. Decomposing a number into odd and even parts. (Contributed by Jim Kingdon, 16-Nov-2021.)
⊢ ((((𝑋 ∈ ℕ ∧ ¬ 2 ∥ 𝑋) ∧ 𝑌 ∈ ℕ0) ∧ 𝐴 = ((2↑𝑌) · 𝑋)) ↔ (𝐴 ∈ ℕ ∧ (𝑋 = (𝐴 / (2↑(℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))) ∧ 𝑌 = (℩𝑧 ∈ ℕ0 ((2↑𝑧) ∥ 𝐴 ∧ ¬ (2↑(𝑧 + 1)) ∥ 𝐴)))))
Theorem	oddpwdc 12879*	The function 𝐹 that decomposes a number into its "odd" and "even" parts, which is to say the largest power of two and largest odd divisor of a number, is a bijection from pairs of a nonnegative integer and an odd number to positive integers. (Contributed by Thierry Arnoux, 15-Aug-2017.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ 𝐹:(𝐽 × ℕ0)–1-1-onto→ℕ
Theorem	sqpweven 12880*	The greatest power of two dividing the square of an integer is an even power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℕ → 2 ∥ (2nd ‘(◡𝐹‘(𝐴↑2))))
Theorem	2sqpwodd 12881*	The greatest power of two dividing twice the square of an integer is an odd power of two. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ 𝐽 = {𝑧 ∈ ℕ ∣ ¬ 2 ∥ 𝑧}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐽, 𝑦 ∈ ℕ0 ↦ ((2↑𝑦) · 𝑥))    ⇒   ⊢ (𝐴 ∈ ℕ → ¬ 2 ∥ (2nd ‘(◡𝐹‘(2 · (𝐴↑2)))))
Theorem	sqne2sq 12882	The square of a natural number can never be equal to two times the square of a natural number. (Contributed by Jim Kingdon, 17-Nov-2021.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴↑2) ≠ (2 · (𝐵↑2)))
Theorem	znege1 12883	The absolute value of the difference between two unequal integers is at least one. (Contributed by Jim Kingdon, 31-Jan-2022.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ≠ 𝐵) → 1 ≤ (abs‘(𝐴 − 𝐵)))
Theorem	sqrt2irraplemnn 12884	Lemma for sqrt2irrap 12885. The square root of 2 is apart from a positive rational expressed as a numerator and denominator. (Contributed by Jim Kingdon, 2-Oct-2021.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (√‘2) # (𝐴 / 𝐵))
Theorem	sqrt2irrap 12885	The square root of 2 is irrational. That is, for any rational number, (√‘2) is apart from it. In the absence of excluded middle, we can distinguish between this and "the square root of 2 is not rational" which is sqrt2irr 12867. (Contributed by Jim Kingdon, 2-Oct-2021.)
⊢ (𝑄 ∈ ℚ → (√‘2) # 𝑄)
5.2.4  Properties of the canonical representation of a rational
Syntax	cnumer 12886	Extend class notation to include canonical numerator function.
class numer
Syntax	cdenom 12887	Extend class notation to include canonical denominator function.
class denom
Definition	df-numer 12888*	The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ numer = (𝑦 ∈ ℚ ↦ (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Definition	df-denom 12889*	The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom = (𝑦 ∈ ℚ ↦ (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumval 12890*	Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) = (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qdenval 12891*	Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumdencl 12892	Lemma for qnumcl 12893 and qdencl 12894. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ))
Theorem	qnumcl 12893	The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ)
Theorem	qdencl 12894	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ)
Theorem	fnum 12895	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ numer:ℚ⟶ℤ
Theorem	fden 12896	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom:ℚ⟶ℕ
Theorem	qnumdenbi 12897	Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (((𝐵 gcd 𝐶) = 1 ∧ 𝐴 = (𝐵 / 𝐶)) ↔ ((numer‘𝐴) = 𝐵 ∧ (denom‘𝐴) = 𝐶)))
Theorem	qnumdencoprm 12898	The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1)
Theorem	qeqnumdivden 12899	Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴)))
Theorem	qmuldeneqnum 12900	Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴))