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
Definition	df-denom 16801*	The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom = (𝑦 ∈ ℚ ↦ (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumval 16802*	Value of the canonical numerator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) = (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qdenval 16803*	Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) = (2nd ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝐴 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
Theorem	qnumdencl 16804	Lemma for qnumcl 16805 and qdencl 16806. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) ∈ ℤ ∧ (denom‘𝐴) ∈ ℕ))
Theorem	qnumcl 16805	The canonical numerator of a rational is an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘𝐴) ∈ ℤ)
Theorem	qdencl 16806	The canonical denominator is a positive integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘𝐴) ∈ ℕ)
Theorem	fnum 16807	Canonical numerator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ numer:ℚ⟶ℤ
Theorem	fden 16808	Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ denom:ℚ⟶ℕ
Theorem	qnumdenbi 16809	Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (((𝐵 gcd 𝐶) = 1 ∧ 𝐴 = (𝐵 / 𝐶)) ↔ ((numer‘𝐴) = 𝐵 ∧ (denom‘𝐴) = 𝐶)))
Theorem	qnumdencoprm 16810	The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘𝐴) gcd (denom‘𝐴)) = 1)
Theorem	qeqnumdivden 16811	Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → 𝐴 = ((numer‘𝐴) / (denom‘𝐴)))
Theorem	qmuldeneqnum 16812	Multiplying a rational by its denominator results in an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (𝐴 · (denom‘𝐴)) = (numer‘𝐴))
Theorem	divnumden 16813	Calculate the reduced form of a quotient using gcd. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → ((numer‘(𝐴 / 𝐵)) = (𝐴 / (𝐴 gcd 𝐵)) ∧ (denom‘(𝐴 / 𝐵)) = (𝐵 / (𝐴 gcd 𝐵))))
Theorem	divdenle 16814	Reducing a quotient never increases the denominator. (Contributed by Stefan O'Rear, 13-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℕ) → (denom‘(𝐴 / 𝐵)) ≤ 𝐵)
Theorem	qnumgt0 16815	A rational is positive iff its canonical numerator is. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (0 < 𝐴 ↔ 0 < (numer‘𝐴)))
Theorem	qgt0numnn 16816	A rational is positive iff its canonical numerator is a positive integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℚ ∧ 0 < 𝐴) → (numer‘𝐴) ∈ ℕ)
Theorem	nn0gcdsq 16817	Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2)))
Theorem	zgcdsq 16818	nn0gcdsq 16817 extended to integers by symmetry. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → ((𝐴 gcd 𝐵)↑2) = ((𝐴↑2) gcd (𝐵↑2)))
Theorem	numdensq 16819	Squaring a rational squares its canonical components. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((numer‘(𝐴↑2)) = ((numer‘𝐴)↑2) ∧ (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2)))
Theorem	numsq 16820	Square commutes with canonical numerator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (numer‘(𝐴↑2)) = ((numer‘𝐴)↑2))
Theorem	densq 16821	Square commutes with canonical denominator. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → (denom‘(𝐴↑2)) = ((denom‘𝐴)↑2))
Theorem	qden1elz 16822	A rational is an integer iff it has denominator 1. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (𝐴 ∈ ℚ → ((denom‘𝐴) = 1 ↔ 𝐴 ∈ ℤ))
Theorem	zsqrtelqelz 16823	If an integer has a rational square root, that root is must be an integer. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ ((𝐴 ∈ ℤ ∧ (√‘𝐴) ∈ ℚ) → (√‘𝐴) ∈ ℤ)
Theorem	nonsq 16824	Any integer strictly between two adjacent squares has an irrational square root. (Contributed by Stefan O'Rear, 15-Sep-2014.)
⊢ (((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐵↑2) < 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))) → ¬ (√‘𝐴) ∈ ℚ)
Theorem	numdenexp 16825	Elevating a rational number to the power 𝑁 has the same effect on its canonical components. Same as numdensq 16819, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → ((numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁) ∧ (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁)))
Theorem	numexp 16826	Elevating to a nonnegative power commutes with canonical numerator. Similar to numsq 16820, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (numer‘(𝐴↑𝑁)) = ((numer‘𝐴)↑𝑁))
Theorem	denexp 16827	Elevating to a nonnegative power commutes with canonical denominator. Similar to densq 16821, extended to nonnegative exponents. (Contributed by Steven Nguyen, 5-Apr-2023.)
⊢ ((𝐴 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (denom‘(𝐴↑𝑁)) = ((denom‘𝐴)↑𝑁))
6.2.4  Euler's theorem
Syntax	codz 16828	Extend class notation with the order function on the class of integers modulo N.
class odℤ
Syntax	cphi 16829	Extend class notation with the Euler phi function.
class ϕ
Definition	df-odz 16830*	Define the order function on the class of integers modulo N. (Contributed by Mario Carneiro, 23-Feb-2014.) (Revised by AV, 26-Sep-2020.)
⊢ odℤ = (𝑛 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑛) = 1} ↦ inf({𝑚 ∈ ℕ ∣ 𝑛 ∥ ((𝑥↑𝑚) − 1)}, ℝ, < )))
Definition	df-phi 16831*	Define the Euler phi function (also called "Euler totient function"), which counts the number of integers less than 𝑛 and coprime to it, see definition in [ApostolNT] p. 25. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ ϕ = (𝑛 ∈ ℕ ↦ (♯‘{𝑥 ∈ (1...𝑛) ∣ (𝑥 gcd 𝑛) = 1}))
Theorem	phival 16832*	Value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) = (♯‘{𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1}))
Theorem	phicl2 16833	Bounds and closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ (1...𝑁))
Theorem	phicl 16834	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ)
Theorem	phibndlem 16835*	Lemma for phibnd 16836. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → {𝑥 ∈ (1...𝑁) ∣ (𝑥 gcd 𝑁) = 1} ⊆ (1...(𝑁 − 1)))
Theorem	phibnd 16836	A slightly tighter bound on the value of the Euler ϕ function. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (ϕ‘𝑁) ≤ (𝑁 − 1))
Theorem	phicld 16837	Closure for the value of the Euler ϕ function. (Contributed by Mario Carneiro, 29-May-2016.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (ϕ‘𝑁) ∈ ℕ)
Theorem	phi1 16838	Value of the Euler ϕ function at 1. (Contributed by Mario Carneiro, 23-Feb-2014.)
⊢ (ϕ‘1) = 1
Theorem	dfphi2 16839*	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 16840*	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 16841	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 16842	Value of the Euler ϕ function at a prime. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝑃 ∈ ℙ → (ϕ‘𝑃) = (𝑃 − 1))
Theorem	crth 16843*	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 16844*	Lemma for phimul 16845. (Contributed by Mario Carneiro, 24-Feb-2014.)
⊢ 𝑆 = (0..^(𝑀 · 𝑁))    &   ⊢ 𝑇 = ((0..^𝑀) × (0..^𝑁))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ⟨(𝑥 mod 𝑀), (𝑥 mod 𝑁)⟩)    &   ⊢ (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ (𝑀 gcd 𝑁) = 1))    &   ⊢ 𝑈 = {𝑦 ∈ (0..^𝑀) ∣ (𝑦 gcd 𝑀) = 1}    &   ⊢ 𝑉 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑊 = {𝑦 ∈ 𝑆 ∣ (𝑦 gcd (𝑀 · 𝑁)) = 1}    ⇒   ⊢ (𝜑 → (ϕ‘(𝑀 · 𝑁)) = ((ϕ‘𝑀) · (ϕ‘𝑁)))
Theorem	phimul 16845	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 16846*	Lemma for eulerth 16848. (Contributed by Mario Carneiro, 8-May-2015.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → 𝐺:𝑇⟶𝑆)
Theorem	eulerthlem2 16847*	Lemma for eulerth 16848. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1))    &   ⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1}    &   ⊢ 𝑇 = (1...(ϕ‘𝑁))    &   ⊢ (𝜑 → 𝐹:𝑇–1-1-onto→𝑆)    &   ⊢ 𝐺 = (𝑥 ∈ 𝑇 ↦ ((𝐴 · (𝐹‘𝑥)) mod 𝑁))    ⇒   ⊢ (𝜑 → ((𝐴↑(ϕ‘𝑁)) mod 𝑁) = (1 mod 𝑁))
Theorem	eulerth 16848	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 16849	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 16850	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑅) − 1)))
Theorem	prmdiveq 16851	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ 𝑃 ∥ ((𝐴 · 𝑆) − 1)) ↔ 𝑆 = 𝑅))
Theorem	prmdivdiv 16852	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 16853*	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	dvdsfi 16854*	A natural number has finitely many divisors. (Contributed by Jim Kingdon, 9-Oct-2025.)
⊢ (𝑁 ∈ ℕ → {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ∈ Fin)
Theorem	hashgcdeq 16855*	Number of initial positive integers with specified divisors. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (♯‘{𝑥 ∈ (0..^𝑀) ∣ (𝑥 gcd 𝑀) = 𝑁}) = if(𝑁 ∥ 𝑀, (ϕ‘(𝑀 / 𝑁)), 0))
Theorem	phisum 16856*	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 16857*	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 16858	- Lemma for odzcl 16859, 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 16859	The order of a group element is an integer. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((odℤ‘𝑁)‘𝐴) ∈ ℕ)
Theorem	odzid 16860	Any element raised to the power of its order is 1. (Contributed by Mario Carneiro, 28-Feb-2014.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → 𝑁 ∥ ((𝐴↑((odℤ‘𝑁)‘𝐴)) − 1))
Theorem	odzdvds 16861	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 16862	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 16863	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 16864	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 16865	Show an explicit expression for the modular inverse of 𝐴 mod 𝑃. This is an application of prmdiv 16850. (Contributed by Alexander van der Vekens, 15-May-2018.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → (𝑅 ∈ (1...(𝑃 − 1)) ∧ ((𝐴 · 𝑅) mod 𝑃) = 1))
Theorem	modprminveq 16866	The modular inverse of 𝐴 mod 𝑃 is unique. (Contributed by Alexander van der Vekens, 17-May-2018.)
⊢ 𝑅 = ((𝐴↑(𝑃 − 2)) mod 𝑃)    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝑆 ∈ (0...(𝑃 − 1)) ∧ ((𝐴 · 𝑆) mod 𝑃) = 1) ↔ 𝑆 = 𝑅))
Theorem	vfermltl 16867	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 16868	Alternate proof of vfermltl 16867, not using Euler's theorem. (Contributed by AV, 21-Aug-2020.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ ℤ ∧ ¬ 𝑃 ∥ 𝐴) → ((𝐴↑(𝑃 − 1)) mod 𝑃) = 1)
Theorem	powm2modprm 16869	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 16870*	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 16871*	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 16872*	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 16873*	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 16874	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 16875	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 16876	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 16877	A prime not equal to 2 is an odd positive integer. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → (𝑁 ∈ ℕ ∧ ¬ 2 ∥ 𝑁))
Theorem	oddn2prm 16878	A prime not equal to 2 is odd. (Contributed by AV, 28-Jun-2021.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → ¬ 2 ∥ 𝑁)
Theorem	nnoddn2prmb 16879	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 16880	A prime less than 5 is either 2 or 3. (Contributed by AV, 5-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 < 5) → (𝑃 = 2 ∨ 𝑃 = 3))
Theorem	prm23ge5 16881	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 16882*	Lemma for pythagtrip 16900. 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 16883*	Lemma for pythagtrip 16900. 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 16884	Lemma for pythagtrip 16900. 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 16885	Lemma for pythagtrip 16900. 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 16886	Lemma for pythagtrip 16900. Show that 𝐶 − 𝐵 is positive. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2)) → 0 < (𝐶 − 𝐵))
Theorem	pythagtriplem6 16887	Lemma for pythagtrip 16900. Calculate (√‘(𝐶 − 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 − 𝐵)) = ((𝐶 − 𝐵) gcd 𝐴))
Theorem	pythagtriplem7 16888	Lemma for pythagtrip 16900. Calculate (√‘(𝐶 + 𝐵)). (Contributed by Scott Fenton, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (√‘(𝐶 + 𝐵)) = ((𝐶 + 𝐵) gcd 𝐴))
Theorem	pythagtriplem8 16889	Lemma for pythagtrip 16900. 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 16890	Lemma for pythagtrip 16900. 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 16891	Lemma for pythagtrip 16900. 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 16892	Lemma for pythagtrip 16900. 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 16893	Lemma for pythagtrip 16900. 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 16894	Lemma for pythagtrip 16900. 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 16895	Lemma for pythagtrip 16900. 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 16896	Lemma for pythagtrip 16900. 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 16897	Lemma for pythagtrip 16900. 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 16898*	Lemma for pythagtrip 16900. 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 16899*	Lemma for pythagtrip 16900. 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 16900*	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))))))