P. 126 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12501-12600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pcz 12501*	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 12502*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	pcprmpw 12503*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	dvdsprmpweq 12504*	If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)))
Theorem	dvdsprmpweqnn 12505*	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 12506*	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 12507	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 12508	Lemma for pcadd 12509. 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 12509	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 12510	The inequality of pcadd 12509 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 12511	Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
Theorem	pcmpt 12512*	Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))
Theorem	pcmpt2 12513*	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 12514	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 12515*	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	sumhashdc 12516*	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 ∧ 𝐴 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝐵 DECID 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 if(𝑘 ∈ 𝐴, 1, 0) = (♯‘𝐴))
Theorem	fldivp1 12517	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 12518	Lemma for pcfac 12519. (Contributed by Mario Carneiro, 20-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0)
Theorem	pcfac 12519*	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 12520*	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 12521	If a power of a rational number is an integer, then the number is an integer. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ ∧ (𝐴↑𝑁) ∈ ℤ) → 𝐴 ∈ ℤ)
Theorem	expnprm 12522	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 not rational. Suggested by Norm Megill. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ (ℤ≥‘2)) → ¬ (𝐴↑𝑁) ∈ ℙ)
Theorem	oddprmdvds 12523*	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})𝑝 ∥ 𝐾)
5.2.9  Pocklington's theorem
Theorem	prmpwdvds 12524	A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)
Theorem	pockthlem 12525	Lemma for pockthg 12526. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 < 𝐴)    &   ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑄 ∈ ℙ)    &   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)    &   ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Theorem	pockthg 12526*	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 12527	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 12526 for a more general closed-form version. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ 𝑃 ∈ ℙ    &   ⊢ 𝐺 ∈ ℕ    &   ⊢ 𝑀 = (𝐺 · 𝑃)    &   ⊢ 𝑁 = (𝑀 + 1)    &   ⊢ 𝐷 ∈ ℕ    &   ⊢ 𝐸 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝑀 = (𝐷 · (𝑃↑𝐸))    &   ⊢ 𝐷 < (𝑃↑𝐸)    &   ⊢ ((𝐴↑𝑀) mod 𝑁) = (1 mod 𝑁)    &   ⊢ (((𝐴↑𝐺) − 1) gcd 𝑁) = 1    ⇒   ⊢ 𝑁 ∈ ℙ
5.2.10  Infinite primes theorem
Theorem	infpnlem1 12528*	Lemma for infpn 12530. 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 12529*	Lemma for infpn 12530. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.)
⊢ 𝐾 = ((!‘𝑁) + 1)    ⇒   ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn 12530*	There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 12673 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.)
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	prmunb 12531*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝)
5.2.11  Fundamental theorem of arithmetic
Theorem	1arithlem1 12532*	Lemma for 1arith 12536. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁)))
Theorem	1arithlem2 12533*	Lemma for 1arith 12536. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁))
Theorem	1arithlem3 12534*	Lemma for 1arith 12536. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0)
Theorem	1arithlem4 12535*	Lemma for 1arith 12536. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1))    &   ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥))
Theorem	1arith 12536*	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 12537*	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}    ⇒   ⊢ ∀𝑧 ∈ ℕ ∃!𝑔 ∈ 𝑅 (𝑀‘𝑧) = 𝑔
5.2.12  Lagrange's four-square theorem
Syntax	cgz 12538	Extend class notation with the set of gaussian integers.
class ℤ[i]
Definition	df-gz 12539	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 12540	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
Theorem	gzcn 12541	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
Theorem	zgz 12542	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i])
Theorem	igz 12543	i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ i ∈ ℤ[i]
Theorem	gznegcl 12544	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i])
Theorem	gzcjcl 12545	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
Theorem	gzaddcl 12546	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i])
Theorem	gzmulcl 12547	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i])
Theorem	gzreim 12548	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])
Theorem	gzsubcl 12549	The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 − 𝐵) ∈ ℤ[i])
Theorem	gzabssqcl 12550	The squared norm of a gaussian integer is an integer. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → ((abs‘𝐴)↑2) ∈ ℕ0)
Theorem	4sqlem5 12551	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ))
Theorem	4sqlem6 12552	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2)))
Theorem	4sqlem7 12553	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → (𝐵↑2) ≤ (((𝑀↑2) / 2) / 2))
Theorem	4sqlem8 12554	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    ⇒   ⊢ (𝜑 → 𝑀 ∥ ((𝐴↑2) − (𝐵↑2)))
Theorem	4sqlem9 12555	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (𝐴↑2))
Theorem	4sqlem10 12556	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2))    &   ⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2)))
Theorem	4sqlem1 12557*	Lemma for 4sq 12579. 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 12558*	Lemma for 4sq 12579. Change bound variables in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ 𝑆 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
Theorem	4sqlem3 12559*	Lemma for 4sq 12579. Sufficient condition to be in 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) ∧ (𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ)) → (((𝐴↑2) + (𝐵↑2)) + ((𝐶↑2) + (𝐷↑2))) ∈ 𝑆)
Theorem	4sqlem4a 12560*	Lemma for 4sqlem4 12561. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (((abs‘𝐴)↑2) + ((abs‘𝐵)↑2)) ∈ 𝑆)
Theorem	4sqlem4 12561*	Lemma for 4sq 12579. 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 12562*	Lemma for mul4sq 12563: algebraic manipulations. The extra assumptions involving 𝑀 would let us 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 12563*	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 12562. (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	4sqlemafi 12564*	Lemma for 4sq 12579. 𝐴 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    ⇒   ⊢ (𝜑 → 𝐴 ∈ Fin)
Theorem	4sqlemffi 12565*	Lemma for 4sq 12579. ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ Fin)
Theorem	4sqleminfi 12566*	Lemma for 4sq 12579. 𝐴 ∩ ran 𝐹 is finite. (Contributed by Jim Kingdon, 24-May-2025.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℕ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ∈ Fin)
Theorem	4sqexercise1 12567*	Exercise which may help in understanding the proof of 4sqlemsdc 12569. (Contributed by Jim Kingdon, 25-May-2025.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ 𝑛 = (𝑥↑2)}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqexercise2 12568*	Exercise which may help in understanding the proof of 4sqlemsdc 12569. (Contributed by Jim Kingdon, 30-May-2025.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ 𝑛 = ((𝑥↑2) + (𝑦↑2))}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqlemsdc 12569*	Lemma for 4sq 12579. The property of being the sum of four squares is decidable. The proof involves showing that (for a particular 𝐴) there are only a finite number of possible ways that it could be the sum of four squares, so checking each of those possibilities in turn decides whether the number is the sum of four squares. If this proof is hard to follow, especially because of its length, the simplified versions at 4sqexercise1 12567 and 4sqexercise2 12568 may help clarify, as they are using very much the same techniques on simplified versions of this lemma. (Contributed by Jim Kingdon, 25-May-2025.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ (𝐴 ∈ ℕ0 → DECID 𝐴 ∈ 𝑆)
Theorem	4sqlem11 12570*	Lemma for 4sq 12579. Use the pigeonhole principle to show that the sets {𝑚↑2 ∣ 𝑚 ∈ (0...𝑁)} and {-1 − 𝑛↑2 ∣ 𝑛 ∈ (0...𝑁)} have a common element, mod 𝑃. Note that although the conclusion is stated in terms of 𝐴 ∩ ran 𝐹 being nonempty, it is also inhabited by 4sqleminfi 12566 and fin0 6946. (Contributed by Mario Carneiro, 15-Jul-2014.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ 𝐴 = {𝑢 ∣ ∃𝑚 ∈ (0...𝑁)𝑢 = ((𝑚↑2) mod 𝑃)}    &   ⊢ 𝐹 = (𝑣 ∈ 𝐴 ↦ ((𝑃 − 1) − 𝑣))    ⇒   ⊢ (𝜑 → (𝐴 ∩ ran 𝐹) ≠ ∅)
Theorem	4sqlem12 12571*	Lemma for 4sq 12579. 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	4sqlem13m 12572*	Lemma for 4sq 12579. (Contributed by Mario Carneiro, 16-Jul-2014.) (Revised by AV, 14-Sep-2020.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((2 · 𝑁) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (0...(2 · 𝑁)) ⊆ 𝑆)    &   ⊢ 𝑇 = {𝑖 ∈ ℕ ∣ (𝑖 · 𝑃) ∈ 𝑆}    &   ⊢ 𝑀 = inf(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → (∃𝑗 𝑗 ∈ 𝑇 ∧ 𝑀 < 𝑃))
Theorem	4sqlem14 12573*	Lemma for 4sq 12579. (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 12574*	Lemma for 4sq 12579. (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 12575*	Lemma for 4sq 12579. (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 12576*	Lemma for 4sq 12579. (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 12577*	Lemma for 4sq 12579. 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(𝑇, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑆)
Theorem	4sqlem19 12578*	Lemma for 4sq 12579. The proof is by strong induction - we show that if all the integers less than 𝑘 are in 𝑆, then 𝑘 is as well. In this part of the proof we do the induction argument and dispense with all the cases except the odd prime case, which is sent to 4sqlem18 12577. If 𝑘 is 0, 1, 2, we show 𝑘 ∈ 𝑆 directly; otherwise if 𝑘 is composite, 𝑘 is the product of two numbers less than it (and hence in 𝑆 by assumption), so by mul4sq 12563 𝑘 ∈ 𝑆. (Contributed by Mario Carneiro, 14-Jul-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑆 = {𝑛 ∣ ∃𝑥 ∈ ℤ ∃𝑦 ∈ ℤ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ 𝑛 = (((𝑥↑2) + (𝑦↑2)) + ((𝑧↑2) + (𝑤↑2)))}    ⇒   ⊢ ℕ0 = 𝑆
Theorem	4sq 12579*	Lagrange's four-square theorem, or Bachet's conjecture: every nonnegative integer is expressible as a sum of four squares. This is Metamath 100 proof #19. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ (𝐴 ∈ ℕ0 ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ ∃𝑐 ∈ ℤ ∃𝑑 ∈ ℤ 𝐴 = (((𝑎↑2) + (𝑏↑2)) + ((𝑐↑2) + (𝑑↑2))))
5.2.13  Decimal arithmetic (cont.)
Theorem	dec2dvds 12580	Divisibility by two is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    &   ⊢ 𝐷 = (𝐶 + 1)    ⇒   ⊢ ¬ 2 ∥ ;𝐴𝐷
Theorem	dec5dvds 12581	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐵
Theorem	dec5dvds2 12582	Divisibility by five is obvious in base 10. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ    &   ⊢ 𝐵 < 5    &   ⊢ (5 + 𝐵) = 𝐶    ⇒   ⊢ ¬ 5 ∥ ;𝐴𝐶
Theorem	dec5nprm 12583	A decimal number greater than 10 and ending with five is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    ⇒   ⊢ ¬ ;𝐴5 ∈ ℙ
Theorem	dec2nprm 12584	A decimal number greater than 10 and ending with an even digit is not a prime number. (Contributed by Mario Carneiro, 19-Apr-2015.)
⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ (𝐵 · 2) = 𝐶    ⇒   ⊢ ¬ ;𝐴𝐶 ∈ ℙ
Theorem	modxai 12585	Add exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.) (Revised by Mario Carneiro, 5-Feb-2015.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐿 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ ((𝐴↑𝐶) mod 𝑁) = (𝐿 mod 𝑁)    &   ⊢ (𝐵 + 𝐶) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐿)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	mod2xi 12586	Double exponents in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (2 · 𝐵) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐾)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modxp1i 12587	Add one to an exponent in a power mod calculation. (Contributed by Mario Carneiro, 21-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℤ    &   ⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ ((𝐴↑𝐵) mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝐵 + 1) = 𝐸    &   ⊢ ((𝐷 · 𝑁) + 𝑀) = (𝐾 · 𝐴)    ⇒   ⊢ ((𝐴↑𝐸) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	modsubi 12588	Subtract from within a mod calculation. (Contributed by Mario Carneiro, 18-Feb-2014.)
⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐴 ∈ ℕ    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 mod 𝑁) = (𝐾 mod 𝑁)    &   ⊢ (𝑀 + 𝐵) = 𝐾    ⇒   ⊢ ((𝐴 − 𝐵) mod 𝑁) = (𝑀 mod 𝑁)
Theorem	gcdi 12589	Calculate a GCD via Euclid's algorithm. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    &   ⊢ ((𝐾 · 𝑁) + 𝑅) = 𝑀    ⇒   ⊢ (𝑀 gcd 𝑁) = 𝐺
Theorem	gcdmodi 12590	Calculate a GCD via Euclid's algorithm. Theorem 5.6 in [ApostolNT] p. 109. (Contributed by Mario Carneiro, 19-Feb-2014.)
⊢ 𝐾 ∈ ℕ0    &   ⊢ 𝑅 ∈ ℕ0    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ (𝐾 mod 𝑁) = (𝑅 mod 𝑁)    &   ⊢ (𝑁 gcd 𝑅) = 𝐺    ⇒   ⊢ (𝐾 gcd 𝑁) = 𝐺
Theorem	numexp0 12591	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑0) = 1
Theorem	numexp1 12592	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ (𝐴↑1) = 𝐴
Theorem	numexpp1 12593	Calculate an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴↑𝑀) · 𝐴) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	numexp2x 12594	Double an integer power. (Contributed by Mario Carneiro, 17-Apr-2015.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (2 · 𝑀) = 𝑁    &   ⊢ (𝐴↑𝑀) = 𝐷    &   ⊢ (𝐷 · 𝐷) = 𝐶    ⇒   ⊢ (𝐴↑𝑁) = 𝐶
Theorem	decsplit0b 12595	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 𝐵) = (𝐴 + 𝐵)
Theorem	decsplit0 12596	Split a decimal number into two parts. Base case: 𝑁 = 0. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑0)) + 0) = 𝐴
Theorem	decsplit1 12597	Split a decimal number into two parts. Base case: 𝑁 = 1. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    ⇒   ⊢ ((𝐴 · (;10↑1)) + 𝐵) = ;𝐴𝐵
Theorem	decsplit 12598	Split a decimal number into two parts. Inductive step. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 8-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝑀 + 1) = 𝑁    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝐶    ⇒   ⊢ ((𝐴 · (;10↑𝑁)) + ;𝐵𝐷) = ;𝐶𝐷
Theorem	karatsuba 12599	The Karatsuba multiplication algorithm. If 𝑋 and 𝑌 are decomposed into two groups of digits of length 𝑀 (only the lower group is known to be this size but the algorithm is most efficient when the partition is chosen near the middle of the digit string), then 𝑋𝑌 can be written in three groups of digits, where each group needs only one multiplication. Thus, we can halve both inputs with only three multiplications on the smaller operands, yielding an asymptotic improvement of n^(log2 3) instead of n^2 for the "naive" algorithm decmul1c 9521. (Contributed by Mario Carneiro, 16-Jul-2015.) (Revised by AV, 9-Sep-2021.)
⊢ 𝐴 ∈ ℕ0    &   ⊢ 𝐵 ∈ ℕ0    &   ⊢ 𝐶 ∈ ℕ0    &   ⊢ 𝐷 ∈ ℕ0    &   ⊢ 𝑆 ∈ ℕ0    &   ⊢ 𝑀 ∈ ℕ0    &   ⊢ (𝐴 · 𝐶) = 𝑅    &   ⊢ (𝐵 · 𝐷) = 𝑇    &   ⊢ ((𝐴 + 𝐵) · (𝐶 + 𝐷)) = ((𝑅 + 𝑆) + 𝑇)    &   ⊢ ((𝐴 · (;10↑𝑀)) + 𝐵) = 𝑋    &   ⊢ ((𝐶 · (;10↑𝑀)) + 𝐷) = 𝑌    &   ⊢ ((𝑅 · (;10↑𝑀)) + 𝑆) = 𝑊    &   ⊢ ((𝑊 · (;10↑𝑀)) + 𝑇) = 𝑍    ⇒   ⊢ (𝑋 · 𝑌) = 𝑍
Theorem	2exp4 12600	Two to the fourth power is 16. (Contributed by Mario Carneiro, 20-Apr-2015.)
⊢ (2↑4) = ;16