P. 169 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 16801-16900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	phicl2 16801	Bounds and closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ (1...𝑁))
Theorem	phicl 16802	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ)
Theorem	phibndlem 16803*	Lemma for phibnd 16804. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1)))
Theorem	phibnd 16804	A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1))
Theorem	phicld 16805	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
Theorem	phi1 16806	Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (ϕ‘1) = 1
Theorem	dfphi2 16807*	Alternate definition of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by Mario Carneiro, 2-May-2016.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (0..^𝑁) ∣ (𝑥 gcd 𝑁) = 1}))
Theorem	hashdvds 16808*	The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐵 ∈ (ℤ≥‘(𝐴 − 1)))    &   ⊢ (𝜑 → 𝐶 ∈ ℤ)    ⇒   ⊢ (𝜑 → (♯‘{𝑥 ∈ (𝐴...𝐵) ∣ 𝑁 ∥ (𝑥 − 𝐶)}) = ((⌊‘((𝐵 − 𝐶) / 𝑁)) − (⌊‘(((𝐴 − 1) − 𝐶) / 𝑁))))
Theorem	phiprmpw 16809	Value of the Euler ϕ function at a prime power. Theorem 2.5(a) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐾 ∈ ℕ) → (ϕ‘(𝑃↑𝐾)) = ((𝑃↑(𝐾 − 1)) · (𝑃 − 1)))
Theorem	phiprm 16810	Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
Theorem	crth 16811*	The Chinese Remainder Theorem: the function that maps 𝑥 to its remainder classes mod 𝑀 and mod 𝑁 is 1-1 and onto when 𝑀 and 𝑁 are coprime. (Contributed by Mario Carneiro, 24-Feb-2014.) (Proof shortened by Mario Carneiro, 2-May-2016.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    ⇒   ⊢ (𝜑 → 𝐹:𝑆–1-1-onto→𝑇)
Theorem	phimullem 16812*	Lemma for phimul 16813. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    &   ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}    &   ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}    ⇒   ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	phimul 16813	The Euler ϕ function is a multiplicative function, meaning that it distributes over multiplication at relatively prime arguments. Theorem 2.5(c) in [ApostolNT] p. 28. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1) → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	eulerthlem1 16814*	Lemma for eulerth 16816. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
Theorem	eulerthlem2 16815*	Lemma for eulerth 16816. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	eulerth 16816	Euler's theorem, a generalization of Fermat's little theorem. If 𝐴 and 𝑁 are coprime, then 𝐴↑ϕ(𝑁)≡1 (mod 𝑁). This is Metamath 100 proof #10. Also called Euler-Fermat theorem, see theorem 5.17 in [ApostolNT] p. 113. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	fermltl 16817	Fermat's little theorem. When 𝑃 is prime, 𝐴↑𝑃≡𝐴 (mod 𝑃) for any 𝐴, see theorem 5.19 in [ApostolNT] p. 114. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 19-Mar-2022.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴↑𝑃) mod 𝑃) = (𝐴 mod 𝑃))
Theorem	prmdiv 16818	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)))
Theorem	prmdiveq 16819	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅))
Theorem	prmdivdiv 16820	The (modular) inverse of the inverse of a number is itself. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ (1...(𝑃 − 1))) → 𝐴 = ((𝑅↑(𝑃 − 2)) mod 𝑃))
Theorem	hashgcdlem 16821*	A correspondence between elements of specific GCD and relative primes in a smaller ring. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐴 = {𝑦 ∈ (0..^(𝑀 / 𝑁)) ∣ (𝑦 gcd (𝑀 / 𝑁)) = 1}    &   ⊢ 𝐵 = {𝑧 ∈ (0..^𝑀) ∣ (𝑧 gcd 𝑀) = 𝑁}    &   ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝑥 · 𝑁))    ⇒   ⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∥ 𝑀) → 𝐹:𝐴–1-1-onto→𝐵)
Theorem	hashgcdeq 16822*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁 ∥ 𝑀, (ϕ‘(𝑀 / 𝑁)), 0))
Theorem	phisum 16823*	The divisor sum identity of the totient function. Theorem 2.2 in [ApostolNT] p. 26. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (ϕ‘𝑑) = 𝑁)
Theorem	odzval 16824*	Value of the order function. This is a function of functions; the inner argument selects the base (i.e., mod 𝑁 for some 𝑁, often prime) and the outer argument selects the integer or equivalence class (if you want to think about it that way) from the integers mod 𝑁. In order to ensure the supremum is well-defined, we only define the expression when 𝐴 and 𝑁 are coprime. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, < ))
Theorem	odzcllem 16825	- Lemma for odzcl 16826, showing existence of a recurrent point for the exponential. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → (((odℤ‘𝑁)‘𝐴) ∈ ℕ ∧ 𝑁 ∥ ((𝐴↑((odℤ‘𝑁)‘𝐴)) − 1)))
Theorem	odzcl 16826	The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) ∈ ℕ)
Theorem	odzid 16827	Any element raised to the power of its order is 1. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝑁 ∥ ((𝐴↑((odℤ‘𝑁)‘𝐴)) − 1))
Theorem	odzdvds 16828	The only powers of 𝐴 that are congruent to 1 are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 28-Feb-2014.) (Proof shortened by AV, 26-Sep-2020.)
⊢ (((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) ∧ 𝐾 ∈ ℕ0) → (𝑁 ∥ ((𝐴↑𝐾) − 1) ↔ ((odℤ‘𝑁)‘𝐴) ∥ 𝐾))
Theorem	odzphi 16829	The order of any group element is a divisor of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) ∥ (ϕ‘𝑁))
6.2.5  Arithmetic modulo a prime number
Theorem	modprm1div 16830	A prime number divides an integer minus 1 iff the integer modulo the prime number is 1. (Contributed by Alexander van der Vekens, 17-May-2018.) (Proof shortened by AV, 30-May-2023.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → ((𝐴 mod 𝑃) = 1 ↔ 𝑃 ∥ (𝐴 − 1)))
Theorem	m1dvdsndvds 16831	If an integer minus 1 is divisible by a prime number, the integer itself is not divisible by this prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ¬ 𝑃 ∥ 𝐴))
Theorem	modprminv 16832	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. This is an application of prmdiv 16818. (Contributed by Alexander van der Vekens, 15-May-2018.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · 𝑅) mod 𝑃) = 1))
Theorem	modprminveq 16833	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ ((𝐴 · 𝑆) mod 𝑃) = 1) ↔ 𝑆 = 𝑅))
Theorem	vfermltl 16834	Variant of Fermat's little theorem if 𝐴 is not a multiple of 𝑃, see theorem 5.18 in [ApostolNT] p. 113. (Contributed by AV, 21-Aug-2020.) (Proof shortened by AV, 5-Sep-2020.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1)
Theorem	vfermltlALT 16835	Alternate proof of vfermltl 16834, not using Euler's theorem. (Contributed by AV, 21-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1)
Theorem	powm2modprm 16836	If an integer minus 1 is divisible by a prime number, then the integer to the power of the prime number minus 2 is 1 modulo the prime number. (Contributed by Alexander van der Vekens, 30-Aug-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ) → (𝑃 ∥ (𝐴 − 1) → ((𝐴↑(𝑃 − 2)) mod 𝑃) = 1))
Theorem	reumodprminv 16837*	For any prime number and for any positive integer less than this prime number, there is a unique modular inverse of this positive integer. (Contributed by Alexander van der Vekens, 12-May-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃)) → ∃!𝑖 ∈ (1...(𝑃 − 1))((𝑁 · 𝑖) mod 𝑃) = 1)
Theorem	modprm0 16838*	For two positive integers less than a given prime number there is always a nonnegative integer (less than the given prime number) so that the sum of one of the two positive integers and the other of the positive integers multiplied by the nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (1..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)
Theorem	nnnn0modprm0 16839*	For a positive integer and a nonnegative integer both less than a given prime number there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the positive integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 8-Nov-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (1..^𝑃) ∧ 𝐼 ∈ (0..^𝑃)) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0)
Theorem	modprmn0modprm0 16840*	For an integer not being 0 modulo a given prime number and a nonnegative integer less than the prime number, there is always a second nonnegative integer (less than the given prime number) so that the sum of this second nonnegative integer multiplied with the integer and the first nonnegative integer is 0 ( modulo the given prime number). (Contributed by Alexander van der Vekens, 10-Nov-2018.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ ∧ (𝑁 mod 𝑃) ≠ 0) → (𝐼 ∈ (0..^𝑃) → ∃𝑗 ∈ (0..^𝑃)((𝐼 + (𝑗 · 𝑁)) mod 𝑃) = 0))
6.2.6  Pythagorean Triples
Theorem	coprimeprodsq 16841	If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) → 𝐴 = ((𝐴 gcd 𝐶)↑2)))
Theorem	coprimeprodsq2 16842	If three numbers are coprime, and the square of one is the product of the other two, then there is a formula for the other two in terms of gcd and square. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ0 ∧ 𝐶 ∈ ℕ0) ∧ ((𝐴 gcd 𝐵) gcd 𝐶) = 1) → ((𝐶↑2) = (𝐴 · 𝐵) → 𝐵 = ((𝐵 gcd 𝐶)↑2)))
Theorem	oddprm 16843	A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → ((𝑁 − 1) / 2) ∈ ℕ)
Theorem	nnoddn2prm 16844	A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁))
Theorem	oddn2prm 16845	A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → ¬ 2 ∥ 𝑁)
Theorem	nnoddn2prmb 16846	A number is a prime number not equal to 2 iff it is an odd prime number. Conversion theorem for two representations of odd primes. (Contributed by AV, 14-Jul-2021.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) ↔ (𝑁 ∈ ℙ ∧ ¬ 2 ∥ 𝑁))
Theorem	prm23lt5 16847	A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 = 2 ∨ 𝑃 = 3))
Theorem	prm23ge5 16848	A prime is either 2 or 3 or greater than or equal to 5. (Contributed by AV, 5-Jul-2021.)
⊢ (𝑃 ∈ ℙ → (𝑃 = 2 ∨ 𝑃 = 3 ∨ 𝑃 ∈ (ℤ≥‘5)))
Theorem	pythagtriplem1 16849*	Lemma for pythagtrip 16867. Prove a weaker version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))
Theorem	pythagtriplem2 16850*	Lemma for pythagtrip 16867. Prove the full version of one direction of the theorem. (Contributed by Scott Fenton, 28-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))) → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)))
Theorem	pythagtriplem3 16851	Lemma for pythagtrip 16867. Show that 𝐶 and 𝐵 are relatively prime under some conditions. (Contributed by Scott Fenton, 8-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝐵 gcd 𝐶) = 1)
Theorem	pythagtriplem4 16852	Lemma for pythagtrip 16867. Show that 𝐶 − 𝐵 and 𝐶 + 𝐵 are relatively prime. (Contributed by Scott Fenton, 12-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ((𝐶 − 𝐵) gcd (𝐶 + 𝐵)) = 1)
Theorem	pythagtriplem10 16853	Lemma for pythagtrip 16867. Show that 𝐶 − 𝐵 is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵))
Theorem	pythagtriplem6 16854	Lemma for pythagtrip 16867. Calculate (√‘(𝐶 − 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) = ((𝐶 − 𝐵) gcd 𝐴))
Theorem	pythagtriplem7 16855	Lemma for pythagtrip 16867. Calculate (√‘(𝐶 + 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) = ((𝐶 + 𝐵) gcd 𝐴))
Theorem	pythagtriplem8 16856	Lemma for pythagtrip 16867. Show that (√‘(𝐶 − 𝐵)) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) ∈ ℕ)
Theorem	pythagtriplem9 16857	Lemma for pythagtrip 16867. Show that (√‘(𝐶 + 𝐵)) is a positive integer. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) ∈ ℕ)
Theorem	pythagtriplem11 16858	Lemma for pythagtrip 16867. Show that 𝑀 (which will eventually be closely related to the 𝑚 in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑀 ∈ ℕ)
Theorem	pythagtriplem12 16859	Lemma for pythagtrip 16867. Calculate the square of 𝑀. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀↑2) = ((𝐶 + 𝐴) / 2))
Theorem	pythagtriplem13 16860	Lemma for pythagtrip 16867. Show that 𝑁 (which will eventually be closely related to the 𝑛 in the final statement) is a natural. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝑁 ∈ ℕ)
Theorem	pythagtriplem14 16861	Lemma for pythagtrip 16867. Calculate the square of 𝑁. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑁↑2) = ((𝐶 − 𝐴) / 2))
Theorem	pythagtriplem15 16862	Lemma for pythagtrip 16867. Show the relationship between 𝑀, 𝑁, and 𝐴. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐴 = ((𝑀↑2) − (𝑁↑2)))
Theorem	pythagtriplem16 16863	Lemma for pythagtrip 16867. Show the relationship between 𝑀, 𝑁, and 𝐵. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐵 = (2 · (𝑀 · 𝑁)))
Theorem	pythagtriplem17 16864	Lemma for pythagtrip 16867. Show the relationship between 𝑀, 𝑁, and 𝐶. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → 𝐶 = ((𝑀↑2) + (𝑁↑2)))
Theorem	pythagtriplem18 16865*	Lemma for pythagtrip 16867. Wrap the previous 𝑀 and 𝑁 up in quantifiers. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ (𝐴 = ((𝑚↑2) − (𝑛↑2)) ∧ 𝐵 = (2 · (𝑚 · 𝑛)) ∧ 𝐶 = ((𝑚↑2) + (𝑛↑2))))
Theorem	pythagtriplem19 16866*	Lemma for pythagtrip 16867. Introduce 𝑘 and remove the relative primality requirement. (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ¬ 2 ∥ (𝐴 / (𝐴 gcd 𝐵))) → ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ (𝐴 = (𝑘 · ((𝑚↑2) − (𝑛↑2))) ∧ 𝐵 = (𝑘 · (2 · (𝑚 · 𝑛))) ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2)))))
Theorem	pythagtrip 16867*	Parameterize the Pythagorean triples. If 𝐴, 𝐵, and 𝐶 are naturals, then they obey the Pythagorean triple formula iff they are parameterized by three naturals. This proof follows the Isabelle proof at http://afp.sourceforge.net/entries/Fermat3_4.shtml. This is Metamath 100 proof #23. (Contributed by Scott Fenton, 19-Apr-2014.)
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) → (((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ↔ ∃𝑛 ∈ ℕ ∃𝑚 ∈ ℕ ∃𝑘 ∈ ℕ ({𝐴, 𝐵} = {(𝑘 · ((𝑚↑2) − (𝑛↑2))), (𝑘 · (2 · (𝑚 · 𝑛)))} ∧ 𝐶 = (𝑘 · ((𝑚↑2) + (𝑛↑2))))))
Theorem	iserodd 16868*	Collect the odd terms in a sequence. (Contributed by Mario Carneiro, 7-Apr-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐶 ∈ ℂ)    &   ⊢ (𝑛 = ((2 · 𝑘) + 1) → 𝐵 = 𝐶)    ⇒   ⊢ (𝜑 → (seq0( + , (𝑘 ∈ ℕ0 ↦ 𝐶)) ⇝ 𝐴 ↔ seq1( + , (𝑛 ∈ ℕ ↦ if(2 ∥ 𝑛, 0, 𝐵))) ⇝ 𝐴))
6.2.7  The prime count function
Syntax	cpc 16869	Extend class notation with the prime count function.
class pCnt
Definition	df-pc 16870*	Define the prime count function, which returns the largest exponent of a given prime (or other positive integer) that divides the number. For rational numbers, it returns negative values according to the power of a prime in the denominator. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ pCnt = (𝑝 ∈ ℙ, 𝑟 ∈ ℚ ↦ if(𝑟 = 0, +∞, (℩𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑟 = (𝑥 / 𝑦) ∧ 𝑧 = (sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑥}, ℝ, < ) − sup({𝑛 ∈ ℕ0 ∣ (𝑝↑𝑛) ∥ 𝑦}, ℝ, < ))))))
Theorem	pclem 16871*	- Lemma for the prime power pre-function's properties. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝐴 ⊆ ℤ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℤ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))
Theorem	pcprecl 16872*	Closure of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑆 ∈ ℕ0 ∧ (𝑃↑𝑆) ∥ 𝑁))
Theorem	pcprendvds 16873*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑(𝑆 + 1)) ∥ 𝑁)
Theorem	pcprendvds2 16874*	Non-divisibility property of the prime power pre-function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝐴 = {𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑁}    &   ⊢ 𝑆 = sup(𝐴, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ (ℤ≥‘2) ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑𝑆)))
Theorem	pcpre1 16875*	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 16876*	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 16877*	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 16878*	Lemma for pceu 16879. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )    &   ⊢ 𝑈 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑠}, ℝ, < )    &   ⊢ 𝑉 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑡}, ℝ, < )    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ≠ 0)    &   ⊢ (𝜑 → (𝑥 ∈ ℤ ∧ 𝑦 ∈ ℕ))    &   ⊢ (𝜑 → 𝑁 = (𝑥 / 𝑦))    &   ⊢ (𝜑 → (𝑠 ∈ ℤ ∧ 𝑡 ∈ ℕ))    &   ⊢ (𝜑 → 𝑁 = (𝑠 / 𝑡))    ⇒   ⊢ (𝜑 → (𝑆 − 𝑇) = (𝑈 − 𝑉))
Theorem	pceu 16879*	Uniqueness for the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ 𝑆 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑥}, ℝ, < )    &   ⊢ 𝑇 = sup({𝑛 ∈ ℕ0 ∣ (𝑃↑𝑛) ∥ 𝑦}, ℝ, < )    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → ∃!𝑧∃𝑥 ∈ ℤ ∃𝑦 ∈ ℕ (𝑁 = (𝑥 / 𝑦) ∧ 𝑧 = (𝑆 − 𝑇)))
Theorem	pczpre 16880*	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 16881	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pccl 16882	Closure of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pccld 16883	Closure of the prime power function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑃 pCnt 𝑁) ∈ ℕ0)
Theorem	pcmul 16884	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℤ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))
Theorem	pcdiv 16885	Division property of the prime power function. (Contributed by Mario Carneiro, 1-Mar-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℤ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℕ) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))
Theorem	pcqmul 16886	Multiplication property of the prime power function. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 · 𝐵)) = ((𝑃 pCnt 𝐴) + (𝑃 pCnt 𝐵)))
Theorem	pc0 16887	The value of the prime power function at zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 0) = +∞)
Theorem	pc1 16888	Value of the prime count function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (𝑃 pCnt 1) = 0)
Theorem	pcqcl 16889	Closure of the general prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℚ ∧ 𝑁 ≠ 0)) → (𝑃 pCnt 𝑁) ∈ ℤ)
Theorem	pcqdiv 16890	Division property of the prime power function. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ (𝐵 ∈ ℚ ∧ 𝐵 ≠ 0)) → (𝑃 pCnt (𝐴 / 𝐵)) = ((𝑃 pCnt 𝐴) − (𝑃 pCnt 𝐵)))
Theorem	pcrec 16891	Prime power of a reciprocal. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0)) → (𝑃 pCnt (1 / 𝐴)) = -(𝑃 pCnt 𝐴))
Theorem	pcexp 16892	Prime power of an exponential. (Contributed by Mario Carneiro, 10-Aug-2015.)
⊢ ((𝑃 ∈ ℙ ∧ (𝐴 ∈ ℚ ∧ 𝐴 ≠ 0) ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt (𝐴↑𝑁)) = (𝑁 · (𝑃 pCnt 𝐴)))
Theorem	pcxnn0cl 16893	Extended nonnegative integer closure of the general prime count function. (Contributed by Jim Kingdon, 13-Oct-2024.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → (𝑃 pCnt 𝑁) ∈ ℕ0*)
Theorem	pcxcl 16894	Extended real closure of the general prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℚ) → (𝑃 pCnt 𝑁) ∈ ℝ*)
Theorem	pcge0 16895	The prime count of an integer is greater than or equal to zero. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℤ) → 0 ≤ (𝑃 pCnt 𝑁))
Theorem	pczdvds 16896	Defining property of the prime count function. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pcdvds 16897	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → (𝑃↑(𝑃 pCnt 𝑁)) ∥ 𝑁)
Theorem	pczndvds 16898	Defining property of the prime count function. (Contributed by Mario Carneiro, 3-Oct-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pcndvds 16899	Defining property of the prime count function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ) → ¬ (𝑃↑((𝑃 pCnt 𝑁) + 1)) ∥ 𝑁)
Theorem	pczndvds2 16900	The remainder after dividing out all factors of 𝑃 is not divisible by 𝑃. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑁 ∈ ℤ ∧ 𝑁 ≠ 0)) → ¬ 𝑃 ∥ (𝑁 / (𝑃↑(𝑃 pCnt 𝑁))))