P. 165 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16401-16500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvdsprime 16401	If 𝑀 divides a prime, then 𝑀 is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ) → (𝑀 ∥ 𝑃 ↔ (𝑀 = 𝑃 ∨ 𝑀 = 1)))
Theorem	nprm 16402	A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐴 · 𝐵) ∈ ℙ)
Theorem	nprmi 16403	An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 1 < 𝐴    &   ⊢ 1 < 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝑁    ⇒   ⊢ ¬ 𝑁 ∈ ℙ
Theorem	dvdsnprmd 16404	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 16405	A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.)
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃))
Theorem	2prm 16406	2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ 2 ∈ ℙ
Theorem	2mulprm 16407	A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.)
⊢ (𝐴 ∈ ℤ → ((2 · 𝐴) ∈ ℙ ↔ 𝐴 = 1))
Theorem	3prm 16408	3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 3 ∈ ℙ
Theorem	4nprm 16409	4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 4 ∈ ℙ
Theorem	prmuz2 16410	A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
Theorem	prmgt1 16411	A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
Theorem	prmm2nn0 16412	Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈ ℕ0)
Theorem	oddprmgt2 16413	An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
Theorem	oddprmge3 16414	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 16415	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 16416	A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝐴 ∈ ℤ → ¬ (𝐴↑2) ∈ ℙ)
Theorem	dvdsprm 16417	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 16418*	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 16419*	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 16420	No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
Theorem	isprm5 16421*	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 16422*	One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. This version of isprm5 16421 combines the primality and bound on 𝑧 into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃))
Theorem	maxprmfct 16423*	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 16424	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 16427.
Theorem	coprm 16425	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 16426	Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
Theorem	euclemma 16427	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 16428*	A number is prime iff it satisfies Euclid's lemma euclemma 16427. (Contributed by Mario Carneiro, 6-Sep-2015.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))
Theorem	prmdvdsexp 16429	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 16430	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 16431	If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑃 ∥ (𝑄↑𝑁) → 𝑃 = 𝑄))
Theorem	prmdvdssq 16432	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)))
Theorem	prmdvdssqOLD 16433	Obsolete version of prmdvdssq 16432 as of 21-Aug-2024. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℤ) → (𝑃 ∥ 𝑀 ↔ 𝑃 ∥ (𝑀↑2)))
Theorem	prmexpb 16434	Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (𝑄↑𝑁) ↔ (𝑃 = 𝑄 ∧ 𝑀 = 𝑁)))
Theorem	prmfac1 16435	The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (!‘𝑁)) → 𝑃 ≤ 𝑁)
Theorem	rpexp 16436	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 16437	Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd 𝐵) = 1))
Theorem	rpexp12i 16438	Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd (𝐵↑𝑁)) = 1))
Theorem	prmndvdsfaclt 16439	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	prmdvdsncoprmbd 16440*	Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b 16364 with the existential quantifier over the primes instead of integers greater than or equal to 2. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    ⇒   ⊢ (𝜑 → (∃𝑝 ∈ ℙ (𝑝 ∥ 𝐴 ∧ 𝑝 ∥ 𝐵) ↔ (𝐴 gcd 𝐵) ≠ 1))
Theorem	ncoprmlnprm 16441	If two positive integers are not coprime, the larger of them is not a prime number. (Contributed by AV, 9-Aug-2020.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐴 < 𝐵) → (1 < (𝐴 gcd 𝐵) → 𝐵 ∉ ℙ))
Theorem	cncongrprm 16442	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 16443	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 16444	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 16445	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
6.2.3  Properties of the canonical representation of a rational
Syntax	cnumer 16446	Extend class notation to include canonical numerator function.
class numer
Syntax	cdenom 16447	Extend class notation to include canonical denominator function.
class denom
Definition	df-numer 16448*	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 16449*	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 16450*	Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) = (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qdenval 16451*	Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumdencl 16452	Lemma for qnumcl 16453 and qdencl 16454. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ))
Theorem	qnumcl 16453	The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ)
Theorem	qdencl 16454	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ)
Theorem	fnum 16455	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ numer:ℚ⟶ℤ
Theorem	fden 16456	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom:ℚ⟶ℕ
Theorem	qnumdenbi 16457	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 16458	The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1)
Theorem	qeqnumdivden 16459	Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴)))
Theorem	qmuldeneqnum 16460	Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴))
Theorem	divnumden 16461	Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))
Theorem	divdenle 16462	Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (denom‘(𝐴 / 𝐵)) ≤ 𝐵)
Theorem	qnumgt0 16463	A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (0 < 𝐴 ↔ 0 < (numer‘𝐴)))
Theorem	qgt0numnn 16464	A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → (numer‘𝐴) ∈ ℕ)
Theorem	nn0gcdsq 16465	Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2)))
Theorem	zgcdsq 16466	nn0gcdsq 16465 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2)))
Theorem	numdensq 16467	Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘(𝐴↑2)) = ((numer‘𝐴)↑2) ∧ (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2)))
Theorem	numsq 16468	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘(𝐴↑2)) = ((numer‘𝐴)↑2))
Theorem	densq 16469	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2))
Theorem	qden1elz 16470	A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((denom‘𝐴) = 1 ↔ 𝐴 ∈ ℤ))
Theorem	zsqrtelqelz 16471	If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (√‘𝐴) ∈ ℚ) → (√‘𝐴) ∈ ℤ)
Theorem	nonsq 16472	Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐵↑2) < 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))) → ¬ (√‘𝐴) ∈ ℚ)
6.2.4  Euler's theorem
Syntax	codz 16473	Extend class notation with the order function on the class of integers modulo N.
class odℤ
Syntax	cphi 16474	Extend class notation with the Euler phi function.
class ϕ
Definition	df-odz 16475*	Define the order function on the class of integers modulo N. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
⊢ odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )))
Definition	df-phi 16476*	Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than 𝑛 and coprime to it, see definition in [ApostolNT] p. 25. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
Theorem	phival 16477*	Value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}))
Theorem	phicl2 16478	Bounds and closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ (1...𝑁))
Theorem	phicl 16479	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ)
Theorem	phibndlem 16480*	Lemma for phibnd 16481. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1)))
Theorem	phibnd 16481	A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1))
Theorem	phicld 16482	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
Theorem	phi1 16483	Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (ϕ‘1) = 1
Theorem	dfphi2 16484*	Alternate definition of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}))
Theorem	hashdvds 16485*	The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘(𝐴 − 1)))    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
Theorem	phiprmpw 16486	Value of the Euler ϕ function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))
Theorem	phiprm 16487	Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
Theorem	crth 16488*	The Chinese Remainder Theorem: the function that maps 𝑥 to its remainder classes mod 𝑀 and mod 𝑁 is 1-1 and onto when 𝑀 and 𝑁 are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    ⇒   ⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇)
Theorem	phimullem 16489*	Lemma for phimul 16490. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    &   ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}    &   ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}    ⇒   ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	phimul 16490	The Euler ϕ function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1) → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	eulerthlem1 16491*	Lemma for eulerth 16493. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
Theorem	eulerthlem2 16492*	Lemma for eulerth 16493. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	eulerth 16493	Euler's theorem, a generalization of Fermat's little theorem. If 𝐴 and 𝑁 are coprime, then 𝐴↑ϕ(𝑁)≡1 (mod 𝑁). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in [ApostolNT] p. 113. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	fermltl 16494	Fermat's little theorem. When 𝑃 is prime, 𝐴↑𝑃≡𝐴 (mod 𝑃) for any 𝐴, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))
Theorem	prmdiv 16495	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)))
Theorem	prmdiveq 16496	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅))
Theorem	prmdivdiv 16497	The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (1...(𝑃 − 1))) → 𝐴 = ((𝑅↑(𝑃 − 2)) mod 𝑃))
Theorem	hashgcdlem 16498*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}    &   ⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑥 · 𝑁))    ⇒   ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	hashgcdeq 16499*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁 ∥ 𝑀, (ϕ‘(𝑀 / 𝑁)), 0))
Theorem	phisum 16500*	The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁)