P. 170 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16901-17000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pczdvds 16901	Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pcdvds 16902	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pczndvds 16903	Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pcndvds 16904	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pczndvds2 16905	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))
Theorem	pcndvds2 16906	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))
Theorem	pcdvdsb 16907	𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
Theorem	pcelnn 16908	There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁))
Theorem	pceq0 16909	There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does not divide 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁))
Theorem	pcidlem 16910	The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcid 16911	The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcneg 16912	The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))
Theorem	pcabs 16913	The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴))
Theorem	pcdvdstr 16914	The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
Theorem	pcgcd1 16915	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 16916	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 16917*	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 16918*	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 16919*	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 16920*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	pcprmpw 16921*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	dvdsprmpweq 16922*	If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)))
Theorem	dvdsprmpweqnn 16923*	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 16924*	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 16925	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 16926	Lemma for pcadd 16927. 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 16927	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 16928	The inequality of pcadd 16927 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 16929	Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
Theorem	pcmpt 16930*	Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))
Theorem	pcmpt2 16931*	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 16932	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 16933*	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 16934*	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 16935	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 16936	Lemma for pcfac 16937. (Contributed by Mario Carneiro, 20-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0)
Theorem	pcfac 16937*	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 16938*	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 16939	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 16940	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 16941*	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})𝑝 ∥ 𝐾)
6.2.8  Pocklington's theorem
Theorem	prmpwdvds 16942	A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)
Theorem	pockthlem 16943	Lemma for pockthg 16944. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 < 𝐴)    &   ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑄 ∈ ℙ)    &   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)    &   ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Theorem	pockthg 16944*	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 16945	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 16944 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐺 ∈ ℕ    &   ⊢ 𝑀 = (𝐺 · 𝑃)    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝐷 ∈ ℕ    &   ⊢ 𝐸 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸))    &   ⊢ 𝐷 < (𝑃↑𝐸)    &   ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁)    &   ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1    ⇒   ⊢ 𝑁 ∈ ℙ
6.2.9  Infinite primes theorem
Theorem	unbenlem 16946*	Lemma for unben 16947. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ω)
Theorem	unben 16947*	An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
Theorem	infpnlem1 16948*	Lemma for infpn 16950. 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 16949*	Lemma for infpn 16950. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.)
⊢ 𝐾 = ((!‘𝑁) + 1)    ⇒   ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn 16950*	There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 16951 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.)
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn2 16951*	There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 16950, so by unben 16947 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))}    ⇒   ⊢ 𝑆 ≈ ℕ
Theorem	prmunb 16952*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝)
Theorem	prminf 16953	There are an infinite number of primes. Theorem 1.7 in [ApostolNT] p. 16. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ ℙ ≈ ℕ
6.2.10  Sum of prime reciprocals
Theorem	prmreclem1 16954*	Lemma for prmrec 16960. 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 16955*	Lemma for prmrec 16960. 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 16956*	Lemma for prmrec 16960. 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 16957*	Lemma for prmrec 16960. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16812, 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 16958*	Lemma for prmrec 16960. 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 16957 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 16959*	Lemma for prmrec 16960. 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 16958 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 16960*	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 ⇝
6.2.11  Fundamental theorem of arithmetic
Theorem	1arithlem1 16961*	Lemma for 1arith 16965. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁)))
Theorem	1arithlem2 16962*	Lemma for 1arith 16965. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁))
Theorem	1arithlem3 16963*	Lemma for 1arith 16965. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0)
Theorem	1arithlem4 16964*	Lemma for 1arith 16965. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1))    &   ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥))
Theorem	1arith 16965*	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 16966*	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}    ⇒   ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔
6.2.12  Lagrange's four-square theorem
Syntax	cgz 16967	Extend class notation with the set of gaussian integers.
class ℤ[i]
Definition	df-gz 16968	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 16969	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
Theorem	gzcn 16970	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
Theorem	zgz 16971	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i])
Theorem	igz 16972	i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ i ∈ ℤ[i]
Theorem	gznegcl 16973	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i])
Theorem	gzcjcl 16974	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
Theorem	gzaddcl 16975	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i])
Theorem	gzmulcl 16976	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i])
Theorem	gzreim 16977	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
Theorem	gzsubcl 16978	The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i])
Theorem	gzabssqcl 16979	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0)
Theorem	4sqlem5 16980	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
Theorem	4sqlem6 16981	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
Theorem	4sqlem7 16982	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2))
Theorem	4sqlem8 16983	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
Theorem	4sqlem9 16984	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2))
Theorem	4sqlem10 16985	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
Theorem	4sqlem1 16986*	Lemma for 4sq 17002. 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 16987*	Lemma for 4sq 17002. Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
Theorem	4sqlem3 16988*	Lemma for 4sq 17002. Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
Theorem	4sqlem4a 16989*	Lemma for 4sqlem4 16990. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
Theorem	4sqlem4 16990*	Lemma for 4sq 17002. 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 16991*	Lemma for mul4sq 16992: algebraic manipulations. The extra assumptions involving 𝑀 are for a part of 4sqlem17 16999 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 16992*	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 16991. (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 16993*	Lemma for 4sq 17002. 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 16994*	Lemma for 4sq 17002. 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 16995*	Lemma for 4sq 17002. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → (𝑇 ≠ ∅ ∧ 𝑀 < 𝑃))
Theorem	4sqlem14 16996*	Lemma for 4sq 17002. (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 16997*	Lemma for 4sq 17002. (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 16998*	Lemma for 4sq 17002. (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 16999*	Lemma for 4sq 17002. (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))))    ⇒   ⊢ ¬ 𝜑
Theorem	4sqlem18 17000*	Lemma for 4sq 17002. Inductive step, odd prime case. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)