Home | Metamath
Proof Explorer Theorem List (p. 162 of 449) | < 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: | Metamath Proof Explorer
(1-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | phibndlem 16101* | Lemma for phibnd 16102. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1))) | ||
Theorem | phibnd 16102 | A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1)) | ||
Theorem | phicld 16103 | Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ) | ||
Theorem | phi1 16104 | Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (ϕ‘1) = 1 | ||
Theorem | dfphi2 16105* | 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 16106* | 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 16107 | 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 16108 | Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1)) | ||
Theorem | crth 16109* | 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 16110* | Lemma for phimul 16111. (Contributed by Mario Carneiro, 24-Feb-2014.) |
⊢ 𝑆 = (0..^(𝑀 · 𝑁)) & ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁)) & ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ 〈(𝑥 mod 𝑀), (𝑥 mod 𝑁)〉) & ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1)) & ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1} & ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} & ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1} ⇒ ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁))) | ||
Theorem | phimul 16111 | 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 16112* | Lemma for eulerth 16114. (Contributed by Mario Carneiro, 8-May-2015.) |
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) & ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} & ⊢ 𝑇 = (1...(ϕ‘𝑁)) & ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) & ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) ⇒ ⊢ (𝜑 → 𝐺:𝑇⟶𝑆) | ||
Theorem | eulerthlem2 16113* | Lemma for eulerth 16114. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) & ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} & ⊢ 𝑇 = (1...(ϕ‘𝑁)) & ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆) & ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁)) ⇒ ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁)) | ||
Theorem | eulerth 16114 | 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 16115 | 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 16116 | Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1))) | ||
Theorem | prmdiveq 16117 | The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅)) | ||
Theorem | prmdivdiv 16118 | 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 16119* | 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 16120* | Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁 ∥ 𝑀, (ϕ‘(𝑀 / 𝑁)), 0)) | ||
Theorem | phisum 16121* | The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁) | ||
Theorem | odzval 16122* | Value of the order function. This is a function of functions; the inner argument selects the base (i.e., mod 𝑁 for some 𝑁, often prime) and the outer argument selects the integer or equivalence class (if you want to think about it that way) from the integers mod 𝑁. In order to ensure the supremum is well-defined, we only define the expression when 𝐴 and 𝑁 are coprime. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, < )) | ||
Theorem | odzcllem 16123 | - Lemma for odzcl 16124, showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → (((odℤ‘𝑁)‘𝐴) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑((odℤ‘𝑁)‘𝐴)) − 1))) | ||
Theorem | odzcl 16124 | The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) ∈ ℕ) | ||
Theorem | odzid 16125 | Any element raised to the power of its order is 1. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝑁 ∥ ((𝐴↑((odℤ‘𝑁)‘𝐴)) − 1)) | ||
Theorem | odzdvds 16126 | The only powers of 𝐴 that are congruent to 1 are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.) |
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴↑𝐾) − 1) ↔ ((odℤ‘𝑁)‘𝐴) ∥ 𝐾)) | ||
Theorem | odzphi 16127 | The order of any group element is a divisor of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) ∥ (ϕ‘𝑁)) | ||
Theorem | modprm1div 16128 | A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑃) = 1 ↔ 𝑃 ∥ (𝐴 − 1))) | ||
Theorem | m1dvdsndvds 16129 | If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ¬ 𝑃 ∥ 𝐴)) | ||
Theorem | modprminv 16130 | Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. This is an application of prmdiv 16116. (Contributed by Alexander van der Vekens, 15-May-2018.) |
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · 𝑅) mod 𝑃) = 1)) | ||
Theorem | modprminveq 16131 | The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ ((𝐴 · 𝑆) mod 𝑃) = 1) ↔ 𝑆 = 𝑅)) | ||
Theorem | vfermltl 16132 | Variant of Fermat's little theorem if 𝐴 is not a multiple of 𝑃, see theorem 5.18 in [ApostolNT] p. 113. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 5-Sep-2020.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1) | ||
Theorem | vfermltlALT 16133 | Alternate proof of vfermltl 16132, not using Euler's theorem. (Contributed by AV, 21-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1) | ||
Theorem | powm2modprm 16134 | If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1)) | ||
Theorem | reumodprminv 16135* | For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑖 ∈ (1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1) | ||
Theorem | modprm0 16136* | For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) | ||
Theorem | nnnn0modprm0 16137* | For a positive integer and a nonnegative integer both less than a given prime number there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the positive integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 8-Nov-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (0..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0) | ||
Theorem | modprmn0modprm0 16138* | For an integer not being 0 modulo a given prime number and a nonnegative integer less than the prime number, there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 10-Nov-2018.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ (𝑁 mod 𝑃) ≠ 0) → (𝐼 ∈ (0..^𝑃) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)) | ||
Theorem | coprimeprodsq 16139 | If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) → 𝐴 = ((𝐴 gcd 𝐶)↑2))) | ||
Theorem | coprimeprodsq2 16140 | If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) → 𝐵 = ((𝐵 gcd 𝐶)↑2))) | ||
Theorem | oddprm 16141 | A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ (𝑁 ∈ (ℙ ∖ {2}) → ((𝑁 − 1) / 2) ∈ ℕ) | ||
Theorem | nnoddn2prm 16142 | A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝑁 ∈ (ℙ ∖ {2}) → (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁)) | ||
Theorem | oddn2prm 16143 | A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝑁 ∈ (ℙ ∖ {2}) → ¬ 2 ∥ 𝑁) | ||
Theorem | nnoddn2prmb 16144 | A number is a prime number not equal to 2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021.) |
⊢ (𝑁 ∈ (ℙ ∖ {2}) ↔ (𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁)) | ||
Theorem | prm23lt5 16145 | A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 = 2 ∨ 𝑃 = 3)) | ||
Theorem | prm23ge5 16146 | A prime is either 2 or 3 or greater than or equal to 5. (Contributed by AV, 5-Jul-2021.) |
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ (ℤ≥‘5))) | ||
Theorem | pythagtriplem1 16147* | Lemma for pythagtrip 16165. Prove a weaker version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) | ||
Theorem | pythagtriplem2 16148* | Lemma for pythagtrip 16165. Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))) | ||
Theorem | pythagtriplem3 16149 | Lemma for pythagtrip 16165. Show that 𝐶 and 𝐵 are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐵 gcd 𝐶) = 1) | ||
Theorem | pythagtriplem4 16150 | Lemma for pythagtrip 16165. Show that 𝐶 − 𝐵 and 𝐶 + 𝐵 are relatively prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 − 𝐵) gcd (𝐶 + 𝐵)) = 1) | ||
Theorem | pythagtriplem10 16151 | Lemma for pythagtrip 16165. Show that 𝐶 − 𝐵 is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵)) | ||
Theorem | pythagtriplem6 16152 | Lemma for pythagtrip 16165. Calculate (√‘(𝐶 − 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) = ((𝐶 − 𝐵) gcd 𝐴)) | ||
Theorem | pythagtriplem7 16153 | Lemma for pythagtrip 16165. Calculate (√‘(𝐶 + 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) = ((𝐶 + 𝐵) gcd 𝐴)) | ||
Theorem | pythagtriplem8 16154 | Lemma for pythagtrip 16165. Show that (√‘(𝐶 − 𝐵)) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℕ) | ||
Theorem | pythagtriplem9 16155 | Lemma for pythagtrip 16165. Show that (√‘(𝐶 + 𝐵)) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℕ) | ||
Theorem | pythagtriplem11 16156 | Lemma for pythagtrip 16165. Show that 𝑀 (which will eventually be closely related to the 𝑚 in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑀 ∈ ℕ) | ||
Theorem | pythagtriplem12 16157 | Lemma for pythagtrip 16165. Calculate the square of 𝑀. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀↑2) = ((𝐶 + 𝐴) / 2)) | ||
Theorem | pythagtriplem13 16158 | Lemma for pythagtrip 16165. Show that 𝑁 (which will eventually be closely related to the 𝑛 in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑁 ∈ ℕ) | ||
Theorem | pythagtriplem14 16159 | Lemma for pythagtrip 16165. Calculate the square of 𝑁. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2)) | ||
Theorem | pythagtriplem15 16160 | Lemma for pythagtrip 16165. Show the relationship between 𝑀, 𝑁, and 𝐴. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) & ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 = ((𝑀↑2) − (𝑁↑2))) | ||
Theorem | pythagtriplem16 16161 | Lemma for pythagtrip 16165. Show the relationship between 𝑀, 𝑁, and 𝐵. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) & ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 = (2 · (𝑀 · 𝑁))) | ||
Theorem | pythagtriplem17 16162 | Lemma for pythagtrip 16165. Show the relationship between 𝑀, 𝑁, and 𝐶. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2) & ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2) ⇒ ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 = ((𝑀↑2) + (𝑁↑2))) | ||
Theorem | pythagtriplem18 16163* | Lemma for pythagtrip 16165. Wrap the previous 𝑀 and 𝑁 up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝑚↑2) − (𝑛↑2)) ∧ 𝐵 = (2 · (𝑚 · 𝑛)) ∧ 𝐶 = ((𝑚↑2) + (𝑛↑2)))) | ||
Theorem | pythagtriplem19 16164* | Lemma for pythagtrip 16165. Introduce 𝑘 and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))) | ||
Theorem | pythagtrip 16165* | Parameterize the Pythagorean triples. If 𝐴, 𝐵, and 𝐶 are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml. This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))) | ||
Theorem | iserodd 16166* | Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.) |
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ) & ⊢ (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶) ⇒ ⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ 𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴)) | ||
Syntax | cpc 16167 | Extend class notation with the prime count function. |
class pCnt | ||
Definition | df-pc 16168* | Define the prime count function, which returns the largest exponent of a given prime (or other positive integer) that divides the number. For rational numbers, it returns negative values according to the power of a prime in the denominator. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < )))))) | ||
Theorem | pclem 16169* | - Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) | ||
Theorem | pcprecl 16170* | Closure of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} & ⊢ 𝑆 = sup(𝐴, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 ∈ ℕ0 ∧ (𝑃↑𝑆) ∥ 𝑁)) | ||
Theorem | pcprendvds 16171* | Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} & ⊢ 𝑆 = sup(𝐴, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑(𝑆 + 1)) ∥ 𝑁) | ||
Theorem | pcprendvds2 16172* | Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} & ⊢ 𝑆 = sup(𝐴, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑𝑆))) | ||
Theorem | pcpre1 16173* | Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁} & ⊢ 𝑆 = sup(𝐴, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 = 1) → 𝑆 = 0) | ||
Theorem | pcpremul 16174* | Multiplicative property of the prime count pre-function. Note that the primality of 𝑃 is essential for this property; (4 pCnt 2) = 0 but (4 pCnt (2 · 2)) = 1 ≠ 2 · (4 pCnt 2) = 0. Since this is needed to show uniqueness for the real prime count function (over ℚ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑀}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) & ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) = 𝑈) | ||
Theorem | pcval 16175* | The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.) |
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))) | ||
Theorem | pceulem 16176* | Lemma for pceu 16177. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) & ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < ) & ⊢ 𝑉 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ≠ 0) & ⊢ (𝜑 → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ)) & ⊢ (𝜑 → 𝑁 = (𝑥 / 𝑦)) & ⊢ (𝜑 → (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ)) & ⊢ (𝜑 → 𝑁 = (𝑠 / 𝑡)) ⇒ ⊢ (𝜑 → (𝑆 − 𝑇) = (𝑈 − 𝑉)) | ||
Theorem | pceu 16177* | Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < ) & ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))) | ||
Theorem | pczpre 16178* | Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.) |
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < ) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = 𝑆) | ||
Theorem | pczcl 16179 | Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ0) | ||
Theorem | pccl 16180 | Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃 pCnt 𝑁) ∈ ℕ0) | ||
Theorem | pccld 16181 | Closure of the prime power function. (Contributed by Mario Carneiro, 29-May-2016.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℕ0) | ||
Theorem | pcmul 16182 | Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) | ||
Theorem | pcdiv 16183 | Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) | ||
Theorem | pcqmul 16184 | Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵))) | ||
Theorem | pc0 16185 | The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞) | ||
Theorem | pc1 16186 | Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0) | ||
Theorem | pcqcl 16187 | Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ) | ||
Theorem | pcqdiv 16188 | Division property of the prime power function. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵))) | ||
Theorem | pcrec 16189 | Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (1 / 𝐴)) = -(𝑃 pCnt 𝐴)) | ||
Theorem | pcexp 16190 | Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴))) | ||
Theorem | pcxcl 16191 | Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑃 pCnt 𝑁) ∈ ℝ*) | ||
Theorem | pcge0 16192 | The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁)) | ||
Theorem | pczdvds 16193 | Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pcdvds 16194 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pczndvds 16195 | Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pcndvds 16196 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pczndvds2 16197 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcndvds2 16198 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcdvdsb 16199 | 𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) | ||
Theorem | pcelnn 16200 | There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |