![]() |
Metamath
Proof Explorer Theorem List (p. 168 of 491) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cncongr2 16701 | The other direction of the bicondition in cncongr 16702. (Contributed by AV, 11-Jul-2021.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℤ) ∧ (𝑁 ∈ ℕ ∧ 𝑀 = (𝑁 / (𝐶 gcd 𝑁)))) → ((𝐴 mod 𝑀) = (𝐵 mod 𝑀) → ((𝐴 · 𝐶) mod 𝑁) = ((𝐵 · 𝐶) mod 𝑁))) | ||
Theorem | cncongr 16702 | 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 16703 | 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 𝑁))) | ||
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 4790. | ||
Syntax | cprime 16704 | Extend the definition of a class to include the set of prime numbers. |
class ℙ | ||
Definition | df-prm 16705* | Define the set of prime numbers. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ℙ = {𝑝 ∈ ℕ ∣ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o} | ||
Theorem | isprm 16706* | 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 16707 | A prime number is a positive integer. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℕ) | ||
Theorem | prmz 16708 | A prime number is an integer. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Jonathan Yan, 16-Jul-2017.) |
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ ℤ) | ||
Theorem | prmssnn 16709 | The prime numbers are a subset of the positive integers. (Contributed by AV, 22-Jul-2020.) |
⊢ ℙ ⊆ ℕ | ||
Theorem | prmex 16710 | The set of prime numbers exists. (Contributed by AV, 22-Jul-2020.) |
⊢ ℙ ∈ V | ||
Theorem | 0nprm 16711 | 0 is not a prime number. Already Definition df-prm 16705 excludes 0 from being prime (ℙ = {𝑝 ∈ ℕ ∣ ...), but even if 𝑝 ∈ ℕ0 was allowed, the condition {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑝} ≈ 2o would not hold for 𝑝 = 0, because {𝑛 ∈ ℕ ∣ 𝑛 ∥ 0} = ℕ, see dvds0 16305, and ¬ ℕ ≈ 2o (there are more than 2 positive integers). (Contributed by AV, 29-May-2023.) |
⊢ ¬ 0 ∈ ℙ | ||
Theorem | 1nprm 16712 | 1 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 3-Jul-2016.) |
⊢ ¬ 1 ∈ ℙ | ||
Theorem | 1idssfct 16713* | The positive divisors of a positive integer include 1 and itself. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ (𝑁 ∈ ℕ → {1, 𝑁} ⊆ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑁}) | ||
Theorem | isprm2lem 16714* | Lemma for isprm2 16715. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ ((𝑃 ∈ ℕ ∧ 𝑃 ≠ 1) → ({𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} ≈ 2o ↔ {𝑛 ∈ ℕ ∣ 𝑛 ∥ 𝑃} = {1, 𝑃})) | ||
Theorem | isprm2 16715* | 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 16716* | 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 16717* | 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 16718* | A variation on prmind 16719 assuming complete induction for primes. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝑥 = 1 → (𝜑 ↔ 𝜓)) & ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒)) & ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜃)) & ⊢ (𝑥 = (𝑦 · 𝑧) → (𝜑 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜂)) & ⊢ 𝜓 & ⊢ ((𝑥 ∈ ℙ ∧ ∀𝑦 ∈ (1...(𝑥 − 1))𝜒) → 𝜑) & ⊢ ((𝑦 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((𝜒 ∧ 𝜃) → 𝜏)) ⇒ ⊢ (𝐴 ∈ ℕ → 𝜂) | ||
Theorem | prmind 16719* | 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 16720 | If 𝑀 divides a prime, then 𝑀 is either the prime or one. (Contributed by Scott Fenton, 8-Apr-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ) → (𝑀 ∥ 𝑃 ↔ (𝑀 = 𝑃 ∨ 𝑀 = 1))) | ||
Theorem | nprm 16721 | A product of two integers greater than one is composite. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝐵 ∈ (ℤ≥‘2)) → ¬ (𝐴 · 𝐵) ∈ ℙ) | ||
Theorem | nprmi 16722 | An inference for compositeness. (Contributed by Mario Carneiro, 18-Feb-2014.) (Revised by Mario Carneiro, 20-Jun-2015.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ & ⊢ 1 < 𝐴 & ⊢ 1 < 𝐵 & ⊢ (𝐴 · 𝐵) = 𝑁 ⇒ ⊢ ¬ 𝑁 ∈ ℙ | ||
Theorem | dvdsnprmd 16723 | 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 16724 | A prime number is either 2 or odd. (Contributed by AV, 19-Jun-2021.) |
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ ¬ 2 ∥ 𝑃)) | ||
Theorem | 2prm 16725 | 2 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Fan Zheng, 16-Jun-2016.) |
⊢ 2 ∈ ℙ | ||
Theorem | 2mulprm 16726 | A multiple of two is prime iff the multiplier is one. (Contributed by AV, 8-Jun-2023.) |
⊢ (𝐴 ∈ ℤ → ((2 · 𝐴) ∈ ℙ ↔ 𝐴 = 1)) | ||
Theorem | 3prm 16727 | 3 is a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) |
⊢ 3 ∈ ℙ | ||
Theorem | 4nprm 16728 | 4 is not a prime number. (Contributed by Paul Chapman, 22-Jun-2011.) (Proof shortened by Mario Carneiro, 18-Feb-2014.) |
⊢ ¬ 4 ∈ ℙ | ||
Theorem | prmuz2 16729 | A prime number is an integer greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
⊢ (𝑃 ∈ ℙ → 𝑃 ∈ (ℤ≥‘2)) | ||
Theorem | prmgt1 16730 | A prime number is an integer greater than 1. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ (𝑃 ∈ ℙ → 1 < 𝑃) | ||
Theorem | prmm2nn0 16731 | Subtracting 2 from a prime number results in a nonnegative integer. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
⊢ (𝑃 ∈ ℙ → (𝑃 − 2) ∈ ℕ0) | ||
Theorem | oddprmgt2 16732 | An odd prime is greater than 2. (Contributed by AV, 20-Aug-2021.) |
⊢ (𝑃 ∈ (ℙ ∖ {2}) → 2 < 𝑃) | ||
Theorem | oddprmge3 16733 | 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 16734 | 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 16735 | A square is never prime. (Contributed by Mario Carneiro, 20-Jun-2015.) |
⊢ (𝐴 ∈ ℤ → ¬ (𝐴↑2) ∈ ℙ) | ||
Theorem | dvdsprm 16736 | 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 16737* | 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 16738* | 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 16739 | No prime number divides 1. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 2-Jul-2015.) |
⊢ (𝑃 ∈ ℙ → ¬ 𝑃 ∥ 1) | ||
Theorem | isprm5 16740* | 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 16741* | One need only check prime divisors of 𝑃 up to √𝑃 in order to ensure primality. This version of isprm5 16740 combines the primality and bound on 𝑧 into a finite interval of prime numbers. (Contributed by Steve Rodriguez, 20-Jan-2020.) |
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑧 ∈ ((2...(⌊‘(√‘𝑃))) ∩ ℙ) ¬ 𝑧 ∥ 𝑃)) | ||
Theorem | maxprmfct 16742* | 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 16743 | Either 𝐴 / (𝐴 gcd 𝐵) is odd or 𝐵 / (𝐴 gcd 𝐵) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵)) ∨ ¬ 2 ∥ (𝐵 / (𝐴 gcd 𝐵)))) | ||
This section is about coprimality with respect to primes, and a special version of Euclid's lemma for primes is provided, see euclemma 16746. | ||
Theorem | coprm 16744 | 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 16745 | Unequal prime numbers are relatively prime. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑃 gcd 𝑄) = 1 ↔ 𝑃 ≠ 𝑄)) | ||
Theorem | euclemma 16746 | 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 16747* | A number is prime iff it satisfies Euclid's lemma euclemma 16746. (Contributed by Mario Carneiro, 6-Sep-2015.) |
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈ (ℤ≥‘2) ∧ ∀𝑥 ∈ ℤ ∀𝑦 ∈ ℤ (𝑃 ∥ (𝑥 · 𝑦) → (𝑃 ∥ 𝑥 ∨ 𝑃 ∥ 𝑦)))) | ||
Theorem | prmdvdsexp 16748 | 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 16749 | 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 16750 | If a prime divides a nonnegative power of another, then they are equal. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → (𝑃 ∥ (𝑄↑𝑁) → 𝑃 = 𝑄)) | ||
Theorem | prmdvdssq 16751 | 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 16752 | Two positive prime powers are equal iff the primes and the powers are equal. (Contributed by Paul Chapman, 30-Nov-2012.) |
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ)) → ((𝑃↑𝑀) = (𝑄↑𝑁) ↔ (𝑃 = 𝑄 ∧ 𝑀 = 𝑁))) | ||
Theorem | prmfac1 16753 | The factorial of a number only contains primes less than the base. (Contributed by Mario Carneiro, 6-Mar-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (!‘𝑁)) → 𝑃 ≤ 𝑁) | ||
Theorem | dvdszzq 16754 | Divisibility for an integer quotient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ 𝑁 = (𝐴 / 𝐵) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ≠ 0) & ⊢ (𝜑 → 𝑃 ∥ 𝐴) & ⊢ (𝜑 → ¬ 𝑃 ∥ 𝐵) ⇒ ⊢ (𝜑 → 𝑃 ∥ 𝑁) | ||
Theorem | rpexp 16755 | 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 16756 | Relative primality passes to asymmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝑀 ∈ ℕ0) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd 𝐵) = 1)) | ||
Theorem | rpexp12i 16757 | Relative primality passes to symmetric powers. (Contributed by Stefan O'Rear, 27-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝐴 gcd 𝐵) = 1 → ((𝐴↑𝑀) gcd (𝐵↑𝑁)) = 1)) | ||
Theorem | prmndvdsfaclt 16758 | 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 16759 | Condition for a prime number to divide a binomial coefficient. (Contributed by Thierry Arnoux, 17-Sep-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1...(𝑃 − 1))) → 𝑃 ∥ (𝑃C𝑁)) | ||
Theorem | prmdvdsncoprmbd 16760* | Two positive integers are not coprime iff a prime divides both integers. Deduction version of ncoprmgcdne1b 16683 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 16761 | 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 16762 | 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 16763 | 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 16764 | 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 16765 | 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 | ||
Syntax | cnumer 16766 | Extend class notation to include canonical numerator function. |
class numer | ||
Syntax | cdenom 16767 | Extend class notation to include canonical denominator function. |
class denom | ||
Definition | df-numer 16768* | 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 16769* | 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 16770* | Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) = (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) | ||
Theorem | qdenval 16771* | Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥)))))) | ||
Theorem | qnumdencl 16772 | Lemma for qnumcl 16773 and qdencl 16774. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ)) | ||
Theorem | qnumcl 16773 | The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ) | ||
Theorem | qdencl 16774 | The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ) | ||
Theorem | fnum 16775 | Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ numer:ℚ⟶ℤ | ||
Theorem | fden 16776 | Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ denom:ℚ⟶ℕ | ||
Theorem | qnumdenbi 16777 | 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 16778 | The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1) | ||
Theorem | qeqnumdivden 16779 | Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴))) | ||
Theorem | qmuldeneqnum 16780 | Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴)) | ||
Theorem | divnumden 16781 | Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵)))) | ||
Theorem | divdenle 16782 | Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (denom‘(𝐴 / 𝐵)) ≤ 𝐵) | ||
Theorem | qnumgt0 16783 | A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (0 < 𝐴 ↔ 0 < (numer‘𝐴))) | ||
Theorem | qgt0numnn 16784 | A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → (numer‘𝐴) ∈ ℕ) | ||
Theorem | nn0gcdsq 16785 | 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 16786 | nn0gcdsq 16785 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2))) | ||
Theorem | numdensq 16787 | 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 16788 | Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (numer‘(𝐴↑2)) = ((numer‘𝐴)↑2)) | ||
Theorem | densq 16789 | Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2)) | ||
Theorem | qden1elz 16790 | A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.) |
⊢ (𝐴 ∈ ℚ → ((denom‘𝐴) = 1 ↔ 𝐴 ∈ ℤ)) | ||
Theorem | zsqrtelqelz 16791 | 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 16792 | 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 16793 | Elevating a rational number to the power 𝑁 has the same effect on its canonical components. Same as numdensq 16787, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))) | ||
Theorem | numexp 16794 | Elevating to a nonnegative power commutes with canonical numerator. Similar to numsq 16788, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁)) | ||
Theorem | denexp 16795 | Elevating to a nonnegative power commutes with canonical denominator. Similar to densq 16789, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)) | ||
Syntax | codz 16796 | Extend class notation with the order function on the class of integers modulo N. |
class odℤ | ||
Syntax | cphi 16797 | Extend class notation with the Euler phi function. |
class ϕ | ||
Definition | df-odz 16798* | 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 16799* | 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 16800* | Value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1})) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |