P. 167 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16601-16700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nprm 16601	A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐴 · 𝐵) ∈ ℙ)
Theorem	nprmi 16602	An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 1 < 𝐴    &   ⊢ 1 < 𝐵    &   ⊢ (𝐴 · 𝐵) = 𝑁    ⇒   ⊢ ¬ 𝑁 ∈ ℙ
Theorem	dvdsnprmd 16603	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 16604	A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.)
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃))
Theorem	2prm 16605	2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.)
⊢ 2 ∈ ℙ
Theorem	2mulprm 16606	A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.)
⊢ (𝐴 ∈ ℤ → ((2 · 𝐴) ∈ ℙ ↔ 𝐴 = 1))
Theorem	3prm 16607	3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.)
⊢ 3 ∈ ℙ
Theorem	4nprm 16608	4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.)
⊢ ¬ 4 ∈ ℙ
Theorem	prmuz2 16609	A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.)
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2))
Theorem	prmgt1 16610	A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ (𝑃 ∈ ℙ → 1 < 𝑃)
Theorem	prmm2nn0 16611	Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈ ℕ0)
Theorem	oddprmgt2 16612	An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.)
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃)
Theorem	oddprmge3 16613	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 16614	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 16615	A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.)
⊢ (𝐴 ∈ ℤ → ¬ (𝐴↑2) ∈ ℙ)
Theorem	dvdsprm 16616	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 16617*	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 16618*	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 16619	No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.)
⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1)
Theorem	isprm5 16620*	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 16621*	One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. This version of isprm5 16620 combines the primality and bound on 𝑧 into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃))
Theorem	maxprmfct 16622*	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 16623	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 16626.
Theorem	coprm 16624	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 16625	Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄))
Theorem	euclemma 16626	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 16627*	A number is prime iff it satisfies Euclid's lemma euclemma 16626. (Contributed by Mario Carneiro, 6-Sep-2015.)
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦))))
Theorem	prmdvdsexp 16628	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 16629	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 16630	If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑃 ∥ (𝑄↑𝑁) → 𝑃 = 𝑄))
Theorem	prmdvdssq 16631	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	prmexpb 16632	Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.)
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (𝑄↑𝑁) ↔ (𝑃 = 𝑄 ∧ 𝑀 = 𝑁)))
Theorem	prmfac1 16633	The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (!‘𝑁)) → 𝑃 ≤ 𝑁)
Theorem	dvdszzq 16634	Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
⊢ 𝑁 = (𝐴 / 𝐵)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ≠ 0)    &   ⊢ (𝜑 → 𝑃 ∥ 𝐴)    &   ⊢ (𝜑 → ¬ 𝑃 ∥ 𝐵)    ⇒   ⊢ (𝜑 → 𝑃 ∥ 𝑁)
Theorem	rpexp 16635	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 16636	Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd 𝐵) = 1))
Theorem	rpexp12i 16637	Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd (𝐵↑𝑁)) = 1))
Theorem	prmndvdsfaclt 16638	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	prmdvdsbc 16639	Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁))
Theorem	prmdvdsncoprmbd 16640*	Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b 16563 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 16641	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 16642	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 16643	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 16644	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 16645	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 16646	Extend class notation to include canonical numerator function.
class numer
Syntax	cdenom 16647	Extend class notation to include canonical denominator function.
class denom
Definition	df-numer 16648*	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 16649*	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 16650*	Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) = (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qdenval 16651*	Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumdencl 16652	Lemma for qnumcl 16653 and qdencl 16654. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ))
Theorem	qnumcl 16653	The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ)
Theorem	qdencl 16654	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ)
Theorem	fnum 16655	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ numer:ℚ⟶ℤ
Theorem	fden 16656	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom:ℚ⟶ℕ
Theorem	qnumdenbi 16657	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 16658	The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1)
Theorem	qeqnumdivden 16659	Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴)))
Theorem	qmuldeneqnum 16660	Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴))
Theorem	divnumden 16661	Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))
Theorem	divdenle 16662	Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (denom‘(𝐴 / 𝐵)) ≤ 𝐵)
Theorem	qnumgt0 16663	A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (0 < 𝐴 ↔ 0 < (numer‘𝐴)))
Theorem	qgt0numnn 16664	A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → (numer‘𝐴) ∈ ℕ)
Theorem	nn0gcdsq 16665	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 16666	nn0gcdsq 16665 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2)))
Theorem	numdensq 16667	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 16668	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘(𝐴↑2)) = ((numer‘𝐴)↑2))
Theorem	densq 16669	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2))
Theorem	qden1elz 16670	A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((denom‘𝐴) = 1 ↔ 𝐴 ∈ ℤ))
Theorem	zsqrtelqelz 16671	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 16672	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))) → ¬ (√‘𝐴) ∈ ℚ)
Theorem	numdenexp 16673	Elevating a rational number to the power 𝑁 has the same effect on its canonical components. Same as numdensq 16667, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)))
Theorem	numexp 16674	Elevating to a nonnegative power commutes with canonical numerator. Similar to numsq 16668, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁))
Theorem	denexp 16675	Elevating to a nonnegative power commutes with canonical denominator. Similar to densq 16669, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))
6.2.4  Euler's theorem
Syntax	codz 16676	Extend class notation with the order function on the class of integers modulo N.
class odℤ
Syntax	cphi 16677	Extend class notation with the Euler phi function.
class ϕ
Definition	df-odz 16678*	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 16679*	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 16680*	Value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}))
Theorem	phicl2 16681	Bounds and closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ (1...𝑁))
Theorem	phicl 16682	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ)
Theorem	phibndlem 16683*	Lemma for phibnd 16684. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1)))
Theorem	phibnd 16684	A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1))
Theorem	phicld 16685	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
Theorem	phi1 16686	Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (ϕ‘1) = 1
Theorem	dfphi2 16687*	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 16688*	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 16689	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 16690	Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
Theorem	crth 16691*	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 16692*	Lemma for phimul 16693. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    &   ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}    &   ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}    ⇒   ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	phimul 16693	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 16694*	Lemma for eulerth 16696. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
Theorem	eulerthlem2 16695*	Lemma for eulerth 16696. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	eulerth 16696	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 16697	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 16698	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)))
Theorem	prmdiveq 16699	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅))
Theorem	prmdivdiv 16700	The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (1...(𝑃 − 1))) → 𝐴 = ((𝑅↑(𝑃 − 2)) mod 𝑃))