Home | Metamath
Proof Explorer Theorem List (p. 163 of 450) | < 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-28698) |
Hilbert Space Explorer
(28699-30221) |
Users' Mathboxes
(30222-44913) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pcge0 16201 | The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁)) | ||
Theorem | pczdvds 16202 | Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pcdvds 16203 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁) | ||
Theorem | pczndvds 16204 | Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pcndvds 16205 | Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁) | ||
Theorem | pczndvds2 16206 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcndvds2 16207 | The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁)))) | ||
Theorem | pcdvdsb 16208 | 𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁)) | ||
Theorem | pcelnn 16209 | There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁)) | ||
Theorem | pceq0 16210 | There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does not divide 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁)) | ||
Theorem | pcidlem 16211 | The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) | ||
Theorem | pcid 16212 | The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴) | ||
Theorem | pcneg 16213 | The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴)) | ||
Theorem | pcabs 16214 | The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴)) | ||
Theorem | pcdvdstr 16215 | The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.) |
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵)) | ||
Theorem | pcgcd1 16216 | 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 16217 | 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 16218* | 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 16219* | The prime count function, viewed as a function from ℕ to (ℕ ↑m ℙ), is one-to-one. (Contributed by Mario Carneiro, 23-Feb-2014.) |
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → (𝐴 = 𝐵 ↔ ∀𝑝 ∈ ℙ (𝑝 pCnt 𝐴) = (𝑝 pCnt 𝐵))) | ||
Theorem | pcz 16220* | 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 16221* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) | ||
Theorem | pcprmpw 16222* | Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴)))) | ||
Theorem | dvdsprmpweq 16223* | If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛))) | ||
Theorem | dvdsprmpweqnn 16224* | 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 16225* | 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 16226 | 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 16227 | Lemma for pcadd 16228. 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 16228 | 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 16229 | The inequality of pcadd 16228 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 16230 | Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ)) | ||
Theorem | pcmpt 16231* | Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.) |
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1)) & ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0)) | ||
Theorem | pcmpt2 16232* | 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 16233 | 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 16234* | 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 16235* | 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 16236 | 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 16237 | Lemma for pcfac 16238. (Contributed by Mario Carneiro, 20-May-2014.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0) | ||
Theorem | pcfac 16238* | 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 16239* | 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 16240 | 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 16241 | 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 16242* | 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 16243 | A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷) | ||
Theorem | pockthlem 16244 | Lemma for pockthg 16245. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 < 𝐴) & ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑃 ∥ 𝑁) & ⊢ (𝜑 → 𝑄 ∈ ℙ) & ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1) & ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1) ⇒ ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1))) | ||
Theorem | pockthg 16245* | 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 16246 | 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 16245 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.) |
⊢ 𝑃 ∈ ℙ & ⊢ 𝐺 ∈ ℕ & ⊢ 𝑀 = (𝐺 · 𝑃) & ⊢ 𝑁 = (𝑀 + 1) & ⊢ 𝐷 ∈ ℕ & ⊢ 𝐸 ∈ ℕ & ⊢ 𝐴 ∈ ℕ & ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸)) & ⊢ 𝐷 < (𝑃↑𝐸) & ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁) & ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1 ⇒ ⊢ 𝑁 ∈ ℙ | ||
Theorem | unbenlem 16247* | Lemma for unben 16248. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) ⇒ ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ω) | ||
Theorem | unben 16248* | An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.) |
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ) | ||
Theorem | infpnlem1 16249* | Lemma for infpn 16251. 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 16250* | Lemma for infpn 16251. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.) |
⊢ 𝐾 = ((!‘𝑁) + 1) ⇒ ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) | ||
Theorem | infpn 16251* | There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 16252 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.) |
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗)))) | ||
Theorem | infpn2 16252* | There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 16251, so by unben 16248 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.) |
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))} ⇒ ⊢ 𝑆 ≈ ℕ | ||
Theorem | prmunb 16253* | The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝) | ||
Theorem | prminf 16254 | There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.) |
⊢ ℙ ≈ ℕ | ||
Theorem | prmreclem1 16255* | Lemma for prmrec 16261. 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 16256* | Lemma for prmrec 16261. 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 16257* | Lemma for prmrec 16261. 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 16258* | Lemma for prmrec 16261. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16115, 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 16259* | Lemma for prmrec 16261. 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 16258 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 16260* | Lemma for prmrec 16261. 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 16259 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 16261* | 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 16262* | Lemma for 1arith 16266. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁))) | ||
Theorem | 1arithlem2 16263* | Lemma for 1arith 16266. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁)) | ||
Theorem | 1arithlem3 16264* | Lemma for 1arith 16266. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) ⇒ ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0) | ||
Theorem | 1arithlem4 16265* | Lemma for 1arith 16266. (Contributed by Mario Carneiro, 30-May-2014.) |
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛))) & ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1)) & ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥)) | ||
Theorem | 1arith 16266* | 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 ↑m ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin} ⇒ ⊢ 𝑀:ℕ–1-1-onto→𝑅 | ||
Theorem | 1arith2 16267* | 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 ↑m ℙ) ∣ (◡𝑒 “ ℕ) ∈ Fin} ⇒ ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔 | ||
Syntax | cgz 16268 | Extend class notation with the set of gaussian integers. |
class ℤ[i] | ||
Definition | df-gz 16269 | 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 16270 | Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ)) | ||
Theorem | gzcn 16271 | A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ) | ||
Theorem | zgz 16272 | An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i]) | ||
Theorem | igz 16273 | i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ i ∈ ℤ[i] | ||
Theorem | gznegcl 16274 | The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i]) | ||
Theorem | gzcjcl 16275 | The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i]) | ||
Theorem | gzaddcl 16276 | The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i]) | ||
Theorem | gzmulcl 16277 | The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i]) | ||
Theorem | gzreim 16278 | Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i]) | ||
Theorem | gzsubcl 16279 | The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i]) | ||
Theorem | gzabssqcl 16280 | The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0) | ||
Theorem | 4sqlem5 16281 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) | ||
Theorem | 4sqlem6 16282 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) | ||
Theorem | 4sqlem7 16283 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2)) | ||
Theorem | 4sqlem8 16284 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) ⇒ ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2))) | ||
Theorem | 4sqlem9 16285 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 15-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2)) | ||
Theorem | 4sqlem10 16286 | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 16-Jul-2014.) |
⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) & ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0) ⇒ ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) | ||
Theorem | 4sqlem1 16287* | Lemma for 4sq 16303. 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 16288* | Lemma for 4sq 16303. Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2)))) | ||
Theorem | 4sqlem3 16289* | Lemma for 4sq 16303. Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆) | ||
Theorem | 4sqlem4a 16290* | Lemma for 4sqlem4 16291. (Contributed by Mario Carneiro, 14-Jul-2014.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} ⇒ ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆) | ||
Theorem | 4sqlem4 16291* | Lemma for 4sq 16303. 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 16292* | Lemma for mul4sq 16293: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16300 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 16293* | 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 16292. (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 16294* | Lemma for 4sq 16303. 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 16295* | Lemma for 4sq 16303. 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 16296* | Lemma for 4sq 16303. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.) |
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))} & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆) & ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆} & ⊢ 𝑀 = inf(𝑇, ℝ, < ) ⇒ ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃)) | ||
Theorem | 4sqlem14 16297* | Lemma for 4sq 16303. (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) | ||
Theorem | 4sqlem15 16298* | Lemma for 4sq 16303. (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)))) ⇒ ⊢ ((𝜑 ∧ 𝑅 = 𝑀) → ((((((𝑀↑2) / 2) / 2) − (𝐸↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐹↑2)) = 0) ∧ (((((𝑀↑2) / 2) / 2) − (𝐺↑2)) = 0 ∧ ((((𝑀↑2) / 2) / 2) − (𝐻↑2)) = 0))) | ||
Theorem | 4sqlem16 16299* | Lemma for 4sq 16303. (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 ∨ 𝑅 = 𝑀) → (𝑀↑2) ∥ (𝑀 · 𝑃)))) | ||
Theorem | 4sqlem17 16300* | Lemma for 4sq 16303. (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)))) ⇒ ⊢ ¬ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |