Home | Metamath
Proof Explorer Theorem List (p. 155 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pcrec 15401 | Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (1 / 𝐴)) = -(𝑃 pCnt 𝐴)) | ||
Theorem | pcexp 15402 | Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴))) | ||
Theorem | pcxcl 15403 | Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑃 pCnt 𝑁) ∈ ℝ*) | ||
Theorem | pcge0 15404 | The prime count of an integer is greater or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁)) | ||
Theorem | pczdvds 15405 | Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pcdvds 15406 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pczndvds 15407 | Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pcndvds 15408 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pczndvds2 15409 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcndvds2 15410 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcdvdsb 15411 | 𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) | ||
Theorem | pcelnn 15412 | There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) | ||
Theorem | pceq0 15413 | There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does not divide 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁)) | ||
Theorem | pcidlem 15414 | The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) | ||
Theorem | pcid 15415 | The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) | ||
Theorem | pcneg 15416 | The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) | ||
Theorem | pcabs 15417 | The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴)) | ||
Theorem | pcdvdstr 15418 | The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) | ||
Theorem | pcgcd1 15419 | The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ (((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) → (𝑃 pCnt (𝐴 gcd 𝐵)) = (𝑃 pCnt 𝐴)) | ||
Theorem | pcgcd 15420 | The prime count of a GCD is the minimum of the prime counts of the arguments. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝑃 pCnt (𝐴 gcd 𝐵)) = if((𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵), (𝑃 pCnt 𝐴), (𝑃 pCnt 𝐵))) | ||
Theorem | pc2dvds 15421* | A characterization of divisibility in terms of prime count. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 ∥ 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) ≤ (𝑝 pCnt 𝐵))) | ||
Theorem | pc11 15422* | The prime count function, viewed as a function from ℕ to (ℕ ↑𝑚 ℙ), is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) | ||
Theorem | pcz 15423* | The prime count function can be used as an indicator that a given rational number is an integer. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ (𝐴 ∈ ℚ → (𝐴 ∈ ℤ ↔ ∀𝑝 ∈ ℙ 0 ≤ (𝑝 pCnt 𝐴))) | ||
Theorem | pcprmpw2 15424* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) | ||
Theorem | pcprmpw 15425* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) | ||
Theorem | dvdsprmpweq 15426* | If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) | ||
Theorem | dvdsprmpweqnn 15427* | If an integer greater than 1 divides a prime power, it is a (proper) prime power. (Contributed by AV, 13-Aug-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ 𝐴 = (𝑃↑𝑛))) | ||
Theorem | dvdsprmpweqle 15428* | If a positive integer divides a prime power, it is a prime power with a smaller exponent. (Contributed by AV, 25-Jul-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 (𝑛 ≤ 𝑁 ∧ 𝐴 = (𝑃↑𝑛)))) | ||
Theorem | difsqpwdvds 15429 | If the difference of two squares is a power of a prime, the prime divides twice the second squared number. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ (𝐵 + 1) < 𝐴) ∧ (𝐶 ∈ ℙ ∧ 𝐷 ∈ ℕ0)) → ((𝐶↑𝐷) = ((𝐴↑2) − (𝐵↑2)) → 𝐶 ∥ (2 · 𝐵))) | ||
Theorem | pcaddlem 15430 | Lemma for pcadd 15431. The original numbers 𝐴 and 𝐵 have been decomposed using the prime count function as (𝑃↑𝑀) · (𝑅 / 𝑆) where 𝑅, 𝑆 are both not divisible by 𝑃 and 𝑀 = (𝑃 pCnt 𝐴), and similarly for 𝐵. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 = ((𝑃↑𝑀) · (𝑅 / 𝑆))) & ⊢ (𝜑 → 𝐵 = ((𝑃↑𝑁) · (𝑇 / 𝑈))) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → (𝑅 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑅)) & ⊢ (𝜑 → (𝑆 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑆)) & ⊢ (𝜑 → (𝑇 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝑇)) & ⊢ (𝜑 → (𝑈 ∈ ℕ ∧ ¬ 𝑃 ∥ 𝑈)) ⇒ ⊢ (𝜑 → 𝑀 ≤ (𝑃 pCnt (𝐴 + 𝐵))) | ||
Theorem | pcadd 15431 | An inequality for the prime count of a sum. This is the source of the ultrametric inequality for the p-adic metric. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) ⇒ ⊢ (𝜑 → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt (𝐴 + 𝐵))) | ||
Theorem | pcadd2 15432 | The inequality of pcadd 15431 becomes an equality when one of the factors has prime count strictly less than the other. (Contributed by Mario Carneiro, 16-Jan-2015.) (Revised by Mario Carneiro, 26-Jun-2015.) |
⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ ℚ) & ⊢ (𝜑 → 𝐵 ∈ ℚ) & ⊢ (𝜑 → (𝑃 pCnt 𝐴) < (𝑃 pCnt 𝐵)) ⇒ ⊢ (𝜑 → (𝑃 pCnt 𝐴) = (𝑃 pCnt (𝐴 + 𝐵))) | ||
Theorem | pcmptcl 15433 | Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ)) | ||
Theorem | pcmpt 15434* | Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) | ||
Theorem | pcmpt2 15435* | Dividing two prime count maps yields a number with all dividing primes confined to an interval. (Contributed by Mario Carneiro, 14-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁)) ⇒ ⊢ (𝜑 → (𝑃 pCnt ((seq1( · , 𝐹)‘𝑀) / (seq1( · , 𝐹)‘𝑁))) = if((𝑃 ≤ 𝑀 ∧ ¬ 𝑃 ≤ 𝑁), 𝐵, 0)) | ||
Theorem | pcmptdvds 15436 | The partial products of the prime power map form a divisibility chain. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝑁)) ⇒ ⊢ (𝜑 → (seq1( · , 𝐹)‘𝑁) ∥ (seq1( · , 𝐹)‘𝑀)) | ||
Theorem | pcprod 15437* | The product of the primes taken to their respective powers reconstructs the original number. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑(𝑛 pCnt 𝑁)), 1)) ⇒ ⊢ (𝑁 ∈ ℕ → (seq1( · , 𝐹)‘𝑁) = 𝑁) | ||
Theorem | sumhash 15438* | The sum of 1 over a set is the size of the set. (Contributed by Mario Carneiro, 8-Mar-2014.) (Revised by Mario Carneiro, 20-May-2014.) |
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ⊆ 𝐵) → Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 1, 0) = (#‘𝐴)) | ||
Theorem | fldivp1 15439 | The difference between the floors of adjacent fractions is either 1 or 0. (Contributed by Mario Carneiro, 8-Mar-2014.) |
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → ((⌊‘((𝑀 + 1) / 𝑁)) − (⌊‘(𝑀 / 𝑁))) = if(𝑁 ∥ (𝑀 + 1), 1, 0)) | ||
Theorem | pcfaclem 15440 | Lemma for pcfac 15441. (Contributed by Mario Carneiro, 20-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0) | ||
Theorem | pcfac 15441* | Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (!‘𝑁)) = Σ𝑘 ∈ (1...𝑀)(⌊‘(𝑁 / (𝑃↑𝑘)))) | ||
Theorem | pcbc 15442* | Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ (0...𝑁) ∧ 𝑃 ∈ ℙ) → (𝑃 pCnt (𝑁C𝐾)) = Σ𝑘 ∈ (1...𝑁)((⌊‘(𝑁 / (𝑃↑𝑘))) − ((⌊‘((𝑁 − 𝐾) / (𝑃↑𝑘))) + (⌊‘(𝐾 / (𝑃↑𝑘)))))) | ||
Theorem | qexpz 15443 | If a power of a rational number is an integer, then the number is an integer. In other words, all n-th roots are irrational unless they are integers (so that the original number is an n-th power). (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 𝐴 ∈ ℤ) | ||
Theorem | expnprm 15444 | A second or higher power of a rational number is not a prime number. Or by contraposition, the n-th root of a prime number is irrational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015.) |
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ (ℤ≥‘2)) → ¬ (𝐴↑𝑁) ∈ ℙ) | ||
Theorem | oddprmdvds 15445* | Every positive integer which is not a power of two is divisible by an odd prime number. (Contributed by AV, 6-Aug-2021.) |
⊢ ((𝐾 ∈ ℕ ∧ ¬ ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛)) → ∃𝑝 ∈ (ℙ ∖ {2})𝑝 ∥ 𝐾) | ||
Theorem | prmpwdvds 15446 | A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷) | ||
Theorem | pockthlem 15447 | Lemma for pockthg 15448. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴) & ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) & ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) | ||
Theorem | pockthg 15448* | The generalized Pocklington's theorem. If 𝑁 − 1 = 𝐴 · 𝐵 where 𝐵 < 𝐴, then 𝑁 is prime if and only if for every prime factor 𝑝 of 𝐴, there is an 𝑥 such that 𝑥↑(𝑁 − 1) = 1( mod 𝑁) and gcd (𝑥↑((𝑁 − 1) / 𝑝) − 1, 𝑁) = 1. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴) & ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → ∀𝑝 ∈ ℙ (𝑝 ∥ 𝐴 → ∃𝑥 ∈ ℤ (((𝑥↑(𝑁 − 1)) mod 𝑁) = 1 ∧ (((𝑥↑((𝑁 − 1) / 𝑝)) − 1) gcd 𝑁) = 1))) ⇒ ⊢ (𝜑 → 𝑁 ∈ ℙ) | ||
Theorem | pockthi 15449 | Pocklington's theorem, which gives a sufficient criterion for a number 𝑁 to be prime. This is the preferred method for verifying large primes, being much more efficient to compute than trial division. This form has been optimized for application to specific large primes; see pockthg 15448 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ 𝑃 ∈ ℙ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝑀 = (𝐺 · 𝑃) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝐷 ∈ ℕ & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸)) & ⊢ 𝐷 < (𝑃↑𝐸) & ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁) & ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 ⇒ ⊢ 𝑁 ∈ ℙ | ||
Theorem | unbenlem 15450* | Lemma for unben 15451. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ω) | ||
Theorem | unben 15451* | An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ) | ||
Theorem | infpnlem1 15452* | Lemma for infpn 15454. The smallest divisor (greater than 1) 𝑀 of 𝑁! + 1 is a prime greater than 𝑁. (Contributed by NM, 5-May-2005.) |
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (((1 < 𝑀 ∧ (𝐾 / 𝑀) ∈ ℕ) ∧ ∀𝑗 ∈ ℕ ((1 < 𝑗 ∧ (𝐾 / 𝑗) ∈ ℕ) → 𝑀 ≤ 𝑗)) → (𝑁 < 𝑀 ∧ ∀𝑗 ∈ ℕ ((𝑀 / 𝑗) ∈ ℕ → (𝑗 = 1 ∨ 𝑗 = 𝑀))))) | ||
Theorem | infpnlem2 15453* | Lemma for infpn 15454. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.) |
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) | ||
Theorem | infpn 15454* | There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 15455 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.) |
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) | ||
Theorem | infpn2 15455* | There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 15454, so by unben 15451 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.) |
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))} ⇒ ⊢ 𝑆 ≈ ℕ | ||
Theorem | prmunb 15456* | The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝) | ||
Theorem | prminf 15457 | There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ ℙ ≈ ℕ | ||
Theorem | prmreclem1 15458* | Lemma for prmrec 15464. Properties of the "square part" function, which extracts the 𝑚 of the decomposition 𝑁 = 𝑟𝑚↑2, with 𝑚 maximal and 𝑟 squarefree. (Contributed by Mario Carneiro, 5-Aug-2014.) |
⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) ⇒ ⊢ (𝑁 ∈ ℕ → ((𝑄‘𝑁) ∈ ℕ ∧ ((𝑄‘𝑁)↑2) ∥ 𝑁 ∧ (𝐾 ∈ (ℤ≥‘2) → ¬ (𝐾↑2) ∥ (𝑁 / ((𝑄‘𝑁)↑2))))) | ||
Theorem | prmreclem2 15459* | Lemma for prmrec 15464. There are at most 2↑𝐾 squarefree numbers which divide no primes larger than 𝐾. (We could strengthen this to 2↑#(ℙ ∩ (1...𝐾)) but there's no reason to.) We establish the inequality by showing that the prime counts of the number up to 𝐾 completely determine it because all higher prime counts are zero, and they are all at most 1 because no square divides the number, so there are at most 2↑𝐾 possibilities. (Contributed by Mario Carneiro, 5-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} & ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) ⇒ ⊢ (𝜑 → (#‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾)) | ||
Theorem | prmreclem3 15460* | Lemma for prmrec 15464. The main inequality established here is #𝑀 ≤ #{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} · √𝑁, where {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} is the set of squarefree numbers in 𝑀. This is demonstrated by the map 𝑦 ↦ 〈𝑦 / (𝑄‘𝑦)↑2, (𝑄‘𝑦)〉 where 𝑄‘𝑦 is the largest number whose square divides 𝑦. (Contributed by Mario Carneiro, 5-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} & ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) ⇒ ⊢ (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) | ||
Theorem | prmreclem4 15461* | Lemma for prmrec 15464. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 15318, to show that the number of numbers in 1...𝑁 that divide 𝑘 is at most 𝑁 / 𝑘. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} & ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) & ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) ⇒ ⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) | ||
Theorem | prmreclem5 15462* | Lemma for prmrec 15464. Here we show the inequality 𝑁 / 2 < #𝑀 by decomposing the set (1...𝑁) into the disjoint union of the set 𝑀 of those numbers that are not divisible by any "large" primes (above 𝐾) and the indexed union over 𝐾 < 𝑘 of the numbers 𝑊‘𝑘 that divide the prime 𝑘. By prmreclem4 15461 the second of these has size less than 𝑁 times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part 𝑀 must be at least 𝑁 / 2 large. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} & ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ ) & ⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) & ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) ⇒ ⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁))) | ||
Theorem | prmreclem6 15463* | Lemma for prmrec 15464. If the series 𝐹 was convergent, there would be some 𝑘 such that the sum starting from 𝑘 + 1 sums to less than 1 / 2; this is a sufficient hypothesis for prmreclem5 15462 to produce the contradictory bound 𝑁 / 2 < (2↑𝑘)√𝑁, which is false for 𝑁 = 2↑(2𝑘 + 2). (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) ⇒ ⊢ ¬ seq1( + , 𝐹) ∈ dom ⇝ | ||
Theorem | prmrec 15464* | The sum of the reciprocals of the primes diverges. Theorem 1.13 in [ApostolNT] p. 18. This is the "second" proof at http://en.wikipedia.org/wiki/Prime_harmonic_series, attributed to Paul Erdős. This is Metamath 100 proof #81. (Contributed by Mario Carneiro, 6-Aug-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ Σ𝑘 ∈ (ℙ ∩ (1...𝑛))(1 / 𝑘)) ⇒ ⊢ ¬ 𝐹 ∈ dom ⇝ | ||
Theorem | 1arithlem1 15465* | Lemma for 1arith 15469. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁))) | ||
Theorem | 1arithlem2 15466* | Lemma for 1arith 15469. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁)) | ||
Theorem | 1arithlem3 15467* | Lemma for 1arith 15469. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0) | ||
Theorem | 1arithlem4 15468* | Lemma for 1arith 15469. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1)) & ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) | ||
Theorem | 1arith 15469* | Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function 𝑀 maps the set of positive integers one-to-one onto the set of prime factorizations 𝑅. (Contributed by Paul Chapman, 17-Nov-2012.) (Proof shortened by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝑅 = {𝑒 ∈ (ℕ0 ↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin} ⇒ ⊢ 𝑀:ℕ–1-1-onto→𝑅 | ||
Theorem | 1arith2 15470* | Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in [ApostolNT] p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012.) (Revised by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝑅 = {𝑒 ∈ (ℕ0 ↑𝑚 ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin} ⇒ ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔 | ||
Syntax | cgz 15471 | Extend class notation with the set of gaussian integers. |
class ℤ[i] | ||
Definition | df-gz 15472 | Define the set of gaussian integers, which are complex numbers whose real and imaginary parts are integers. (Note that the [i] is actually part of the symbol token and has no independent meaning.) (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ℤ[i] = {𝑥 ∈ ℂ ∣ ((ℜ‘𝑥) ∈ ℤ ∧ (ℑ‘𝑥) ∈ ℤ)} | ||
Theorem | elgz 15473 | Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ)) | ||
Theorem | gzcn 15474 | A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ) | ||
Theorem | zgz 15475 | An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i]) | ||
Theorem | igz 15476 | i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ i ∈ ℤ[i] | ||
Theorem | gznegcl 15477 | The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i]) | ||
Theorem | gzcjcl 15478 | The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i]) | ||
Theorem | gzaddcl 15479 | The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i]) | ||
Theorem | gzmulcl 15480 | The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i]) | ||
Theorem | gzreim 15481 | Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) | ||
Theorem | gzsubcl 15482 | The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i]) | ||
Theorem | gzabssqcl 15483 | The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0) | ||
Theorem | 4sqlem5 15484 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) | ||
Theorem | 4sqlem6 15485 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) | ||
Theorem | 4sqlem7 15486 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2)) | ||
Theorem | 4sqlem8 15487 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2))) | ||
Theorem | 4sqlem9 15488 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2)) | ||
Theorem | 4sqlem10 15489 | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) | ||
Theorem | 4sqlem1 15490* | Lemma for 4sq 15506. The set 𝑆 is the set of all numbers that are expressible as a sum of four squares. Our goal is to show that 𝑆 = ℕ0; here we show one subset direction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ 𝑆 ⊆ ℕ0 | ||
Theorem | 4sqlem2 15491* | Lemma for 4sq 15506. Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) | ||
Theorem | 4sqlem3 15492* | Lemma for 4sq 15506. Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆) | ||
Theorem | 4sqlem4a 15493* | Lemma for 4sqlem4 15494. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆) | ||
Theorem | 4sqlem4 15494* | Lemma for 4sq 15506. We can express the four-square property more compactly in terms of gaussian integers, because the norms of gaussian integers are exactly sums of two squares. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑢 ∈ ℤ[i] ∃𝑣 ∈ ℤ[i] 𝐴 = (((abs‘𝑢)↑2) + ((abs‘𝑣)↑2))) | ||
Theorem | mul4sqlem 15495* | Lemma for mul4sq 15496: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 15503 which needs to know not just that the product is a sum of squares, but also that it preserves divisibility by 𝑀. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝐴 ∈ ℤ[i]) & ⊢ (𝜑 → 𝐵 ∈ ℤ[i]) & ⊢ (𝜑 → 𝐶 ∈ ℤ[i]) & ⊢ (𝜑 → 𝐷 ∈ ℤ[i]) & ⊢ 𝑋 = (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) & ⊢ 𝑌 = (((abs‘𝐶)↑2) + ((abs‘𝐷)↑2)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → ((𝐴 − 𝐶) / 𝑀) ∈ ℤ[i]) & ⊢ (𝜑 → ((𝐵 − 𝐷) / 𝑀) ∈ ℤ[i]) & ⊢ (𝜑 → (𝑋 / 𝑀) ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝑋 / 𝑀) · (𝑌 / 𝑀)) ∈ 𝑆) | ||
Theorem | mul4sq 15496* | Euler's four-square identity: The product of two sums of four squares is also a sum of four squares. This is usually quoted as an explicit formula involving eight real variables; we save some time by working with complex numbers (gaussian integers) instead, so that we only have to work with four variables, and also hiding the actual formula for the product in the proof of mul4sqlem 15495. (For the curious, the explicit formula that is used is ( ∣ 𝑎 ∣ ↑2 + ∣ 𝑏 ∣ ↑2)( ∣ 𝑐 ∣ ↑2 + ∣ 𝑑 ∣ ↑2) = ∣ 𝑎∗ · 𝑐 + 𝑏 · 𝑑∗ ∣ ↑2 + ∣ 𝑎∗ · 𝑑 − 𝑏 · 𝑐∗ ∣ ↑2.) (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆) → (𝐴 · 𝐵) ∈ 𝑆) | ||
Theorem | 4sqlem11 15497* | Lemma for 4sq 15506. Use the pigeonhole principle to show that the sets {𝑚↑2 ∣ 𝑚 ∈ (0...𝑁)} and {-1 − 𝑛↑2 ∣ 𝑛 ∈ (0...𝑁)} have a common element, mod 𝑃. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} & ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)) ⇒ ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅) | ||
Theorem | 4sqlem12 15498* | Lemma for 4sq 15506. For any odd prime 𝑃, there is a 𝑘 < 𝑃 such that 𝑘𝑃 − 1 is a sum of two squares. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)} & ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣)) ⇒ ⊢ (𝜑 → ∃𝑘 ∈ (1...(𝑃 − 1))∃𝑢 ∈ ℤ[i] (((abs‘𝑢)↑2) + 1) = (𝑘 · 𝑃)) | ||
Theorem | 4sqlem13 15499* | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) & ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} & ⊢ 𝑀 = inf(𝑇, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) | ||
Theorem | 4sqlem14 15500* | Lemma for 4sq 15506. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) & ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} & ⊢ 𝑀 = inf(𝑇, ℝ, < ) & ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2)) & ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐵 ∈ ℤ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℤ) & ⊢ 𝐸 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐹 = (((𝐵 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐺 = (((𝐶 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝐻 = (((𝐷 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ 𝑅 = ((((𝐸↑2) + (𝐹↑2)) + ((𝐺↑2) + (𝐻↑2))) / 𝑀) & ⊢ (𝜑 → (𝑀 · 𝑃) = (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2)))) ⇒ ⊢ (𝜑 → 𝑅 ∈ ℕ0) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |