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	pcprendvds 16901*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑(𝑆 + 1)) ∥ 𝑁)
Theorem	pcprendvds2 16902*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑𝑆)))
Theorem	pcpre1 16903*	Value of the prime power pre-function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 26-Apr-2016.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ 𝑁 = 1) → 𝑆 = 0)
Theorem	pcpremul 16904*	Multiplicative property of the prime count pre-function. Note that the primality of 𝑃 is essential for this property; (4 pCnt 2) = 0 but (4 pCnt (2 · 2)) = 1 ≠ 2 · (4 pCnt 2) = 0. Since this is needed to show uniqueness for the real prime count function (over ℚ), we don't bother to define it off the primes. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑀}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < )    &   ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ (𝑀 · 𝑁)}, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 + 𝑇) = 𝑈)
Theorem	pcval 16905*	The value of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 3-Oct-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇))))
Theorem	pceulem 16906*	Lemma for pceu 16907. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )    &   ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < )    &   ⊢ 𝑉 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ))    &   ⊢ (𝜑 → 𝑁 = (𝑥 / 𝑦))    &   ⊢ (𝜑 → (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ))    &   ⊢ (𝜑 → 𝑁 = (𝑠 / 𝑡))    ⇒   ⊢ (𝜑 → (𝑆 − 𝑇) = (𝑈 − 𝑉))
Theorem	pceu 16907*	Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
Theorem	pczpre 16908*	Connect the prime count pre-function to the actual prime count function, when restricted to the integers. (Contributed by Mario Carneiro, 23-Feb-2014.) (Proof shortened by Mario Carneiro, 24-Dec-2016.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) = 𝑆)
Theorem	pczcl 16909	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pccl 16910	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pccld 16911	Closure of the prime power function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pcmul 16912	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))
Theorem	pcdiv 16913	Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))
Theorem	pcqmul 16914	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))
Theorem	pc0 16915	The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
Theorem	pc1 16916	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0)
Theorem	pcqcl 16917	Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ)
Theorem	pcqdiv 16918	Division property of the prime power function. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))
Theorem	pcrec 16919	Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (1 / 𝐴)) = -(𝑃 pCnt 𝐴))
Theorem	pcexp 16920	Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))
Theorem	pcxnn0cl 16921	Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈ ℕ0*)
Theorem	pcxcl 16922	Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑃 pCnt 𝑁) ∈ ℝ*)
Theorem	pcge0 16923	The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁))
Theorem	pczdvds 16924	Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pcdvds 16925	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pczndvds 16926	Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pcndvds 16927	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pczndvds2 16928	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))
Theorem	pcndvds2 16929	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))
Theorem	pcdvdsb 16930	𝑃↑𝐴 divides 𝑁 if and only if 𝐴 is at most the count of 𝑃. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ 𝐴 ∈ ℕ0) → (𝐴 ≤ (𝑃 pCnt 𝑁) ↔ (𝑃↑𝐴) ∥ 𝑁))
Theorem	pcelnn 16931	There are a positive number of powers of a prime 𝑃 in 𝑁 iff 𝑃 divides 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) ∈ ℕ ↔ 𝑃 ∥ 𝑁))
Theorem	pceq0 16932	There are zero powers of a prime 𝑃 in 𝑁 iff 𝑃 does not divide 𝑁. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ((𝑃 pCnt 𝑁) = 0 ↔ ¬ 𝑃 ∥ 𝑁))
Theorem	pcidlem 16933	The prime count of a prime power. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ0) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcid 16934	The prime count of a prime power. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 pCnt (𝑃↑𝐴)) = 𝐴)
Theorem	pcneg 16935	The prime count of a negative number. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt -𝐴) = (𝑃 pCnt 𝐴))
Theorem	pcabs 16936	The prime count of an absolute value. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℚ) → (𝑃 pCnt (abs‘𝐴)) = (𝑃 pCnt 𝐴))
Theorem	pcdvdstr 16937	The prime count increases under the divisibility relation. (Contributed by Mario Carneiro, 13-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐴 ∥ 𝐵)) → (𝑃 pCnt 𝐴) ≤ (𝑃 pCnt 𝐵))
Theorem	pcgcd1 16938	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 16939	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 16940*	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 16941*	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 16942*	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 16943*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 ∥ (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	pcprmpw 16944*	Self-referential expression for a prime power. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ) → (∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛) ↔ 𝐴 = (𝑃↑(𝑃 pCnt 𝐴))))
Theorem	dvdsprmpweq 16945*	If a positive integer divides a prime power, it is a prime power. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝐴 ∥ (𝑃↑𝑁) → ∃𝑛 ∈ ℕ0 𝐴 = (𝑃↑𝑛)))
Theorem	dvdsprmpweqnn 16946*	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 16947*	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 16948	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 16949	Lemma for pcadd 16950. 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 16950	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 16951	The inequality of pcadd 16950 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 16952	Closure for the prime power map. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → (𝐹:ℕ⟶ℕ ∧ seq1( · , 𝐹):ℕ⟶ℕ))
Theorem	pcmpt 16953*	Construct a function with given prime count characteristics. (Contributed by Mario Carneiro, 12-Mar-2014.)
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (𝑛↑𝐴), 1))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ 𝐴 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝑛 = 𝑃 → 𝐴 = 𝐵)    ⇒   ⊢ (𝜑 → (𝑃 pCnt (seq1( · , 𝐹)‘𝑁)) = if(𝑃 ≤ 𝑁, 𝐵, 0))
Theorem	pcmpt2 16954*	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 16955	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 16956*	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 16957*	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 16958	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 16959	Lemma for pcfac 16960. (Contributed by Mario Carneiro, 20-May-2014.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ (ℤ≥‘𝑁) ∧ 𝑃 ∈ ℙ) → (⌊‘(𝑁 / (𝑃↑𝑀))) = 0)
Theorem	pcfac 16960*	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 16961*	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 16962	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 16963	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 16964*	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 16965	A relation involving divisibility by a prime power. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (((𝐾 ∈ ℤ ∧ 𝐷 ∈ ℤ) ∧ (𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) ∧ (𝐷 ∥ (𝐾 · (𝑃↑𝑁)) ∧ ¬ 𝐷 ∥ (𝐾 · (𝑃↑(𝑁 − 1))))) → (𝑃↑𝑁) ∥ 𝐷)
Theorem	pockthlem 16966	Lemma for pockthg 16967. (Contributed by Mario Carneiro, 2-Mar-2014.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 < 𝐴)    &   ⊢ (𝜑 → 𝑁 = ((𝐴 · 𝐵) + 1))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝑁)    &   ⊢ (𝜑 → 𝑄 ∈ ℙ)    &   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    &   ⊢ (𝜑 → ((𝐶↑(𝑁 − 1)) mod 𝑁) = 1)    &   ⊢ (𝜑 → (((𝐶↑((𝑁 − 1) / 𝑄)) − 1) gcd 𝑁) = 1)    ⇒   ⊢ (𝜑 → (𝑄 pCnt 𝐴) ≤ (𝑄 pCnt (𝑃 − 1)))
Theorem	pockthg 16967*	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 16968	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 16967 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 16969*	Lemma for unben 16970. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ 𝐺 = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)    ⇒   ⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ω)
Theorem	unben 16970*	An unbounded set of positive integers is infinite. (Contributed by NM, 5-May-2005.) (Revised by Mario Carneiro, 15-Sep-2013.)
⊢ ((𝐴 ⊆ ℕ ∧ ∀𝑚 ∈ ℕ ∃𝑛 ∈ 𝐴 𝑚 < 𝑛) → 𝐴 ≈ ℕ)
Theorem	infpnlem1 16971*	Lemma for infpn 16973. 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 16972*	Lemma for infpn 16973. For any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (Contributed by NM, 5-May-2005.)
⊢ 𝐾 = ((!‘𝑁) + 1)    ⇒   ⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn 16973*	There exist infinitely many prime numbers: for any positive integer 𝑁, there exists a prime number 𝑗 greater than 𝑁. (See infpn2 16974 for the equinumerosity version.) (Contributed by NM, 1-Jun-2006.)
⊢ (𝑁 ∈ ℕ → ∃𝑗 ∈ ℕ (𝑁 < 𝑗 ∧ ∀𝑘 ∈ ℕ ((𝑗 / 𝑘) ∈ ℕ → (𝑘 = 1 ∨ 𝑘 = 𝑗))))
Theorem	infpn2 16974*	There exist infinitely many prime numbers: the set of all primes 𝑆 is unbounded by infpn 16973, so by unben 16970 it is infinite. This is Metamath 100 proof #11. (Contributed by NM, 5-May-2005.)
⊢ 𝑆 = {𝑛 ∈ ℕ ∣ (1 < 𝑛 ∧ ∀𝑚 ∈ ℕ ((𝑛 / 𝑚) ∈ ℕ → (𝑚 = 1 ∨ 𝑚 = 𝑛)))}    ⇒   ⊢ 𝑆 ≈ ℕ
Theorem	prmunb 16975*	The primes are unbounded. (Contributed by Paul Chapman, 28-Nov-2012.)
⊢ (𝑁 ∈ ℕ → ∃𝑝 ∈ ℙ 𝑁 < 𝑝)
Theorem	prminf 16976	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 16977*	Lemma for prmrec 16983. 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 16978*	Lemma for prmrec 16983. 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 16979*	Lemma for prmrec 16983. 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 16980*	Lemma for prmrec 16983. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16835, 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 16981*	Lemma for prmrec 16983. 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 16980 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 16982*	Lemma for prmrec 16983. 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 16981 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 16983*	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 16984*	Lemma for 1arith 16988. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁) = (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑁)))
Theorem	1arithlem2 16985*	Lemma for 1arith 16988. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ) → ((𝑀‘𝑁)‘𝑃) = (𝑃 pCnt 𝑁))
Theorem	1arithlem3 16986*	Lemma for 1arith 16988. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    ⇒   ⊢ (𝑁 ∈ ℕ → (𝑀‘𝑁):ℙ⟶ℕ0)
Theorem	1arithlem4 16987*	Lemma for 1arith 16988. (Contributed by Mario Carneiro, 30-May-2014.)
⊢ 𝑀 = (𝑛 ∈ ℕ ↦ (𝑝 ∈ ℙ ↦ (𝑝 pCnt 𝑛)))    &   ⊢ 𝐺 = (𝑦 ∈ ℕ ↦ if(𝑦 ∈ ℙ, (𝑦↑(𝐹‘𝑦)), 1))    &   ⊢ (𝜑 → 𝐹:ℙ⟶ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ ((𝜑 ∧ (𝑞 ∈ ℙ ∧ 𝑁 ≤ 𝑞)) → (𝐹‘𝑞) = 0)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ ℕ 𝐹 = (𝑀‘𝑥))
Theorem	1arith 16988*	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 16989*	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 16990	Extend class notation with the set of gaussian integers.
class ℤ[i]
Definition	df-gz 16991	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 16992	Elementhood in the gaussian integers. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] ↔ (𝐴 ∈ ℂ ∧ (ℜ‘𝐴) ∈ ℤ ∧ (ℑ‘𝐴) ∈ ℤ))
Theorem	gzcn 16993	A gaussian integer is a complex number. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ)
Theorem	zgz 16994	An integer is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ → 𝐴 ∈ ℤ[i])
Theorem	igz 16995	i is a gaussian integer. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ i ∈ ℤ[i]
Theorem	gznegcl 16996	The gaussian integers are closed under negation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → -𝐴 ∈ ℤ[i])
Theorem	gzcjcl 16997	The gaussian integers are closed under conjugation. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ (𝐴 ∈ ℤ[i] → (∗‘𝐴) ∈ ℤ[i])
Theorem	gzaddcl 16998	The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 + 𝐵) ∈ ℤ[i])
Theorem	gzmulcl 16999	The gaussian integers are closed under multiplication. (Contributed by Mario Carneiro, 14-Jul-2014.)
⊢ ((𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i]) → (𝐴 · 𝐵) ∈ ℤ[i])
Theorem	gzreim 17000	Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 + (i · 𝐵)) ∈ ℤ[i])