P. 425 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 42401-42500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iccpartxr 42401	If there is a partition, then all intermediate points and bounds are extended real numbers. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (0...𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ*)
Theorem	iccpartgtprec 42402	If there is a partition, then all intermediate points and the upper bound are strictly greater than the preceeding intermediate points or lower bound. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (1...𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘(𝐼 − 1)) < (𝑃‘𝐼))
Theorem	iccpartipre 42403	If there is a partition, then all intermediate points are real numbers. (Contributed by AV, 11-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝐼 ∈ (1..^𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘𝐼) ∈ ℝ)
Theorem	iccpartiltu 42404*	If there is a partition, then all intermediate points are strictly less than the upper bound. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀))
Theorem	iccpartigtl 42405*	If there is a partition, then all intermediate points are strictly greater than the lower bound. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1..^𝑀)(𝑃‘0) < (𝑃‘𝑖))
Theorem	iccpartlt 42406	If there is a partition, then the lower bound is strictly less than the upper bound. Corresponds to fourierdlem11 41276 in GS's mathbox. (Contributed by AV, 12-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → (𝑃‘0) < (𝑃‘𝑀))
Theorem	iccpartltu 42407*	If there is a partition, then all intermediate points and the lower bound are strictly less than the upper bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑃‘𝑖) < (𝑃‘𝑀))
Theorem	iccpartgtl 42408*	If there is a partition, then all intermediate points and the upper bound are strictly greater than the lower bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝑃‘0) < (𝑃‘𝑖))
Theorem	iccpartgt 42409*	If there is a partition, then all intermediate points and the bounds are strictly ordered. (Contributed by AV, 18-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)∀𝑗 ∈ (0...𝑀)(𝑖 < 𝑗 → (𝑃‘𝑖) < (𝑃‘𝑗)))
Theorem	iccpartleu 42410*	If there is a partition, then all intermediate points and the lower and the upper bound are less than or equal to the upper bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘𝑖) ≤ (𝑃‘𝑀))
Theorem	iccpartgel 42411*	If there is a partition, then all intermediate points and the upper and the lower bound are greater than or equal to the lower bound. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ∀𝑖 ∈ (0...𝑀)(𝑃‘0) ≤ (𝑃‘𝑖))
Theorem	iccpartrn 42412	If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ran 𝑃 ⊆ ((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccpartf 42413	The range of the partition is between its starting point and its ending point. Corresponds to fourierdlem15 41280 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → 𝑃:(0...𝑀)⟶((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccpartel 42414	If there is a partition, then all intermediate points and bounds are contained in a closed interval of extended reals. (Contributed by AV, 14-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0...𝑀)) → (𝑃‘𝐼) ∈ ((𝑃‘0)[,](𝑃‘𝑀)))
Theorem	iccelpart 42415*	An element of any partitioned half-open interval of extended reals is an element of a part of this partition. (Contributed by AV, 18-Jul-2020.)
⊢ (𝑀 ∈ ℕ → ∀𝑝 ∈ (RePart‘𝑀)(𝑋 ∈ ((𝑝‘0)[,)(𝑝‘𝑀)) → ∃𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑝‘𝑖)[,)(𝑝‘(𝑖 + 1)))))
Theorem	iccpartiun 42416*	A half-open interval of extended reals is the union of the parts of its partition. (Contributed by AV, 18-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ((𝑃‘0)[,)(𝑃‘𝑀)) = ∪ 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	icceuelpartlem 42417	Lemma for icceuelpart 42418. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → ((𝐼 ∈ (0..^𝑀) ∧ 𝐽 ∈ (0..^𝑀)) → (𝐼 < 𝐽 → (𝑃‘(𝐼 + 1)) ≤ (𝑃‘𝐽))))
Theorem	icceuelpart 42418*	An element of a partitioned half-open interval of extended reals is an element of exactly one part of the partition. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ((𝑃‘0)[,)(𝑃‘𝑀))) → ∃!𝑖 ∈ (0..^𝑀)𝑋 ∈ ((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	iccpartdisj 42419*	The segments of a partitioned half-open interval of extended reals are a disjoint collection. (Contributed by AV, 19-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    ⇒   ⊢ (𝜑 → Disj 𝑖 ∈ (0..^𝑀)((𝑃‘𝑖)[,)(𝑃‘(𝑖 + 1))))
Theorem	iccpartnel 42420	A point of a partition is not an element of any open interval determined by the partition. Corresponds to fourierdlem12 41277 in GS's mathbox. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 8-Jul-2020.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 ∈ (RePart‘𝑀))    &   ⊢ (𝜑 → 𝑋 ∈ ran 𝑃)    ⇒   ⊢ ((𝜑 ∧ 𝐼 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑃‘𝐼)(,)(𝑃‘(𝐼 + 1))))
20.36.8  Shifting functions with an integer range domain
Theorem	fargshiftfv 42421*	If a class is a function, then the values of the "shifted function" correspond to the function values of the class. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (𝑋 ∈ (0..^𝑁) → (𝐺‘𝑋) = (𝐹‘(𝑋 + 1))))
Theorem	fargshiftf 42422*	If a class is a function, then also its "shifted function" is a function. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → 𝐺:(0..^(♯‘𝐹))⟶dom 𝐸)
Theorem	fargshiftf1 42423*	If a function is 1-1, then also the shifted function is 1-1. (Contributed by Alexander van der Vekens, 23-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–1-1→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–1-1→dom 𝐸)
Theorem	fargshiftfo 42424*	If a function is onto, then also the shifted function is onto. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)–onto→dom 𝐸) → 𝐺:(0..^(♯‘𝐹))–onto→dom 𝐸)
Theorem	fargshiftfva 42425*	The values of a shifted function correspond to the value of the original function. (Contributed by Alexander van der Vekens, 24-Nov-2017.)
⊢ 𝐺 = (𝑥 ∈ (0..^(♯‘𝐹)) ↦ (𝐹‘(𝑥 + 1)))    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹:(1...𝑁)⟶dom 𝐸) → (∀𝑘 ∈ (1...𝑁)(𝐸‘(𝐹‘𝑘)) = ⦋𝑘 / 𝑥⦌𝑃 → ∀𝑙 ∈ (0..^𝑁)(𝐸‘(𝐺‘𝑙)) = ⦋(𝑙 + 1) / 𝑥⦌𝑃))
20.36.9  Words over a set (extension)
20.36.9.1  Last symbol of a word - extension
Theorem	lswn0 42426	The last symbol of a not empty word exists. The empty set must be excluded as symbol, because otherwise, it cannot be distinguished between valid cases (∅ is the last symbol) and invalid cases (∅ means that no last symbol exists. This is because of the special definition of a function in set.mm. (Contributed by Alexander van der Vekens, 18-Mar-2018.)
⊢ ((𝑊 ∈ Word 𝑉 ∧ ∅ ∉ 𝑉 ∧ (♯‘𝑊) ≠ 0) → (lastS‘𝑊) ≠ ∅)
20.36.10  Unordered pairs
20.36.10.1  Set of unordered pairs
Theorem	sprid 42427	Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.)
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}
Theorem	elsprel 42428*	An unordered pair is an element of all unordered pairs. At least one of the two elements of the unordered pair must be a set. Otherwise, the unordered pair would be the empty set, see prprc 4534, which is not an element of all unordered pairs, see spr0nelg 42429. (Contributed by AV, 21-Nov-2021.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})
Theorem	spr0nelg 42429*	The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.)
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}
Syntax	cspr 42430	Extend class notation with set of pairs.
class Pairs
Definition	df-spr 42431*	Define the function which maps a set 𝑣 to the set of pairs consisting of elements of the set 𝑣. (Contributed by AV, 21-Nov-2021.)
⊢ Pairs = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 𝑝 = {𝑎, 𝑏}})
Theorem	sprval 42432*	The set of all unordered pairs over a given set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}})
Theorem	sprvalpw 42433*	The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 21-Nov-2021.)
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}})
Theorem	sprssspr 42434*	The set of all unordered pairs over a given set 𝑉 is a subset of the set of all unordered pairs. (Contributed by AV, 21-Nov-2021.)
⊢ (Pairs‘𝑉) ⊆ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}
Theorem	spr0el 42435	The empty set is not an unordered pair over any set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ ∅ ∉ (Pairs‘𝑉)
Theorem	sprvalpwn0 42436*	The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 21-Nov-2021.)
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}})
Theorem	sprel 42437*	An element of the set of all unordered pairs over a given set 𝑉 is a pair of elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.)
⊢ (𝑋 ∈ (Pairs‘𝑉) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑋 = {𝑎, 𝑏})
Theorem	prssspr 42438*	An element of a subset of the set of all unordered pairs over a given set 𝑉, is a pair of elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.)
⊢ ((𝑃 ⊆ (Pairs‘𝑉) ∧ 𝑋 ∈ 𝑃) → ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑋 = {𝑎, 𝑏})
Theorem	prelspr 42439	An unordered pair of elements of a fixed set 𝑉 belongs to the set of all unordered pairs over the set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ ((𝑉 ∈ 𝑊 ∧ (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉)) → {𝑋, 𝑌} ∈ (Pairs‘𝑉))
Theorem	prsprel 42440	The elements of a pair from the set of all unordered pairs over a given set 𝑉 are elements of the set 𝑉. (Contributed by AV, 22-Nov-2021.)
⊢ (({𝑋, 𝑌} ∈ (Pairs‘𝑉) ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))
Theorem	prsssprel 42441	The elements of a pair from a subset of the set of all unordered pairs over a given set 𝑉 are elements of the set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ ((𝑃 ⊆ (Pairs‘𝑉) ∧ {𝑋, 𝑌} ∈ 𝑃 ∧ (𝑋 ∈ 𝑈 ∧ 𝑌 ∈ 𝑊)) → (𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉))
Theorem	sprvalpwle2 42442*	The set of all unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 24-Nov-2021.)
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (♯‘𝑝) ≤ 2})
Theorem	sprsymrelfvlem 42443*	Lemma for sprsymrelf 42448 and sprsymrelfv 42447. (Contributed by AV, 19-Nov-2021.)
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉))
Theorem	sprsymrelf1lem 42444*	Lemma for sprsymrelf1 42449. (Contributed by AV, 22-Nov-2021.)
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏))
Theorem	sprsymrelfolem1 42445*	Lemma 1 for sprsymrelfo 42450. (Contributed by AV, 22-Nov-2021.)
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)}    ⇒   ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉)
Theorem	sprsymrelfolem2 42446*	Lemma 2 for sprsymrelfo 42450. (Contributed by AV, 23-Nov-2021.)
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦}))
Theorem	sprsymrelfv 42447*	The value of the function 𝐹 which maps a subset of the set of pairs over a fixed set 𝑉 to the relation relating two elements of the set 𝑉 iff they are in a pair of the subset. (Contributed by AV, 19-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}})    ⇒   ⊢ (𝑋 ∈ 𝑃 → (𝐹‘𝑋) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑋 𝑐 = {𝑥, 𝑦}})
Theorem	sprsymrelf 42448*	The mapping 𝐹 is a function from the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 19-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}})    ⇒   ⊢ 𝐹:𝑃⟶𝑅
Theorem	sprsymrelf1 42449*	The mapping 𝐹 is a one-to-one function from the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 19-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}})    ⇒   ⊢ 𝐹:𝑃–1-1→𝑅
Theorem	sprsymrelfo 42450*	The mapping 𝐹 is a function from the subsets of the set of pairs over a fixed set 𝑉 onto the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}})    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃–onto→𝑅)
Theorem	sprsymrelf1o 42451*	The mapping 𝐹 is a bijection between the subsets of the set of pairs over a fixed set 𝑉 into the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}})    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃–1-1-onto→𝑅)
Theorem	sprbisymrel 42452*	There is a bijection between the subsets of the set of pairs over a fixed set 𝑉 and the symmetric relations 𝑅 on the fixed set 𝑉. (Contributed by AV, 23-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → ∃𝑓 𝑓:𝑃–1-1-onto→𝑅)
Theorem	sprsymrelen 42453*	The class 𝑃 of subsets of the set of pairs over a fixed set 𝑉 and the class 𝑅 of symmetric relations on the fixed set 𝑉 are equinumerous. (Contributed by AV, 27-Nov-2021.)
⊢ 𝑃 = 𝒫 (Pairs‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝑃 ≈ 𝑅)
20.36.10.2  Proper (unordered) pairs Proper (unordered) pairs are unordered pairs with exactly 2 elements. The set of proper pairs with elements of a class 𝑉 is defined by {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}. For example, {1, 2} is a proper pair, because 1 ≠ 2 ( see 1ne2 11595). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4626), {1, V} = {1} (see prprc2 4533) or {V, V} = ∅ (see prprc 4534).
Theorem	prpair 42454*	Characterization of a proper pair: A class is a proper pair iff it consists of exactly two different sets. (Contributed by AV, 11-Mar-2023.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑋 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏))
Theorem	prproropf1olem0 42455	Lemma 0 for prproropf1o 42460. Remark: 𝑂, the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, can alternatively be written as 𝑂 = {𝑥 ∈ (𝑉 × 𝑉) ∣ (1st ‘𝑥)𝑅(2nd ‘𝑥)} or even as 𝑂 = {𝑥 ∈ (𝑉 × 𝑉) ∣ ⟨(1st ‘𝑥), (2nd ‘𝑥)⟩ ∈ 𝑅}, by which the relationship between ordered and unordered pair is immediately visible. (Contributed by AV, 18-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    ⇒   ⊢ (𝑊 ∈ 𝑂 ↔ (𝑊 = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩ ∧ ((1st ‘𝑊) ∈ 𝑉 ∧ (2nd ‘𝑊) ∈ 𝑉) ∧ (1st ‘𝑊)𝑅(2nd ‘𝑊)))
Theorem	prproropf1olem1 42456*	Lemma 1 for prproropf1o 42460. (Contributed by AV, 12-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃)
Theorem	prproropf1olem2 42457*	Lemma 2 for prproropf1o 42460. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → ⟨inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)⟩ ∈ 𝑂)
Theorem	prproropf1olem3 42458*	Lemma 3 for prproropf1o 42460. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩)
Theorem	prproropf1olem4 42459*	Lemma 4 for prproropf1o 42460. (Contributed by AV, 14-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊))
Theorem	prproropf1o 42460*	There is a bijection between the set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component. (Contributed by AV, 15-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ (𝑅 Or 𝑉 → 𝐹:𝑃–1-1-onto→𝑂)
Theorem	prproropen 42461*	The set of proper pairs and the set of ordered ordered pairs, i.e., ordered pairs in which the first component is less than the second component, are equinumerous. (Contributed by AV, 15-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 Or 𝑉) → 𝑂 ≈ 𝑃)
Theorem	prproropreud 42462*	There is exactly one ordered ordered pair fulfilling a wff iff there is exactly one proper pair fulfilling an equivalent wff. (Contributed by AV, 20-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ (𝜑 → 𝑅 Or 𝑉)    &   ⊢ (𝑥 = ⟨inf(𝑦, 𝑉, 𝑅), sup(𝑦, 𝑉, 𝑅)⟩ → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = 𝑧 → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ 𝑂 𝜓 ↔ ∃!𝑦 ∈ 𝑃 𝜒))
Theorem	pairreueq 42463*	Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑))
Theorem	paireqne 42464*	Two sets are not equal iff there is exactly one proper pair whose elements are either one of these sets. (Contributed by AV, 27-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵))
20.36.10.3  Set of proper unordered pairs
Syntax	cprpr 42465	Extend class notation with set of proper unordered pairs.
class Pairsproper
Definition	df-prpr 42466*	Define the function which maps a set 𝑣 to the set of proper unordered pairs consisting of exactly two (different) elements of the set 𝑣. (Contributed by AV, 29-Apr-2023.)
⊢ Pairsproper = (𝑣 ∈ V ↦ {𝑝 ∣ ∃𝑎 ∈ 𝑣 ∃𝑏 ∈ 𝑣 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprval 42467*	The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprvalpw 42468*	The set of all proper unordered pairs over a given set 𝑉, expressed by a restricted class abstraction. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∈ 𝒫 𝑉 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprelb 42469	An element of the set of all proper unordered pairs over a given set 𝑉 is a subset of 𝑉 of size two. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (𝑃 ∈ (Pairsproper‘𝑉) ↔ (𝑃 ∈ 𝒫 𝑉 ∧ (♯‘𝑃) = 2)))
Theorem	prprelprb 42470*	A set is an element of the set of all proper unordered pairs over a given set 𝑋 iff it is a pair of different elements of the set 𝑋. (Contributed by AV, 7-May-2023.)
⊢ (𝑃 ∈ (Pairsproper‘𝑋) ↔ (𝑋 ∈ V ∧ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑃 = {𝑎, 𝑏} ∧ 𝑎 ≠ 𝑏)))
Theorem	prprspr2 42471*	The set of all proper unordered pairs over a given set 𝑉 is the set of all unordered pairs over that set of size two. (Contributed by AV, 29-Apr-2023.)
⊢ (Pairsproper‘𝑉) = {𝑝 ∈ (Pairs‘𝑉) ∣ (♯‘𝑝) = 2}
Theorem	prprsprreu 42472*	There is a unique proper unordered pair over a given set 𝑉 fulfilling a wff iff there is a unique unordered pair over 𝑉 of size two fulfilling this wff. (Contributed by AV, 30-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (∃!𝑝 ∈ (Pairsproper‘𝑉)𝜑 ↔ ∃!𝑝 ∈ (Pairs‘𝑉)((♯‘𝑝) = 2 ∧ 𝜑)))
Theorem	prprreueq 42473*	There is a unique proper unordered pair over a given set 𝑉 fulfilling a wff iff there is a unique subset of 𝑉 of size two fulfilling this wff. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (∃!𝑝 ∈ (Pairsproper‘𝑉)𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑)))
20.36.11  Number theory (extension)
20.36.11.1  Fermat numbers At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 42475, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 42524, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 42530. The fourth Fermat number (i.e., the fifth Fermat prime) (FermatNo‘4) = ;;;;65537 is currently the biggest number proven to be prime in set.mm, see 65537prm 42523 (previously, it was ;;;4001, see 4001prm 16261). Another important result of this section is Goldbach's theorem goldbachth 42494, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 42535. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 42539.
Syntax	cfmtno 42474	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 42475	Define the function that enumerates the Fermat numbers, see definition in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ FermatNo = (𝑛 ∈ ℕ0 ↦ ((2↑(2↑𝑛)) + 1))
Theorem	fmtno 42476	The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
Theorem	fmtnoge3 42477	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3))
Theorem	fmtnonn 42478	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ)
Theorem	fmtnom1nn 42479	A Fermat number minus one is a power of a power of two. (Contributed by AV, 29-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ((FermatNo‘𝑁) − 1) = (2↑(2↑𝑁)))
Theorem	fmtnoodd 42480	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
Theorem	fmtnorn 42481*	A Fermat number is a function value of the enumeration of the Fermat numbers. (Contributed by AV, 3-Aug-2021.)
⊢ (𝐹 ∈ ran FermatNo ↔ ∃𝑛 ∈ ℕ0 (FermatNo‘𝑛) = 𝐹)
Theorem	fmtnof1 42482	The enumeration of the Fermat numbers is a one-one function into the positive integers. (Contributed by AV, 3-Aug-2021.)
⊢ FermatNo:ℕ0–1-1→ℕ
Theorem	fmtnoinf 42483	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
⊢ ran FermatNo ∉ Fin
Theorem	fmtnorec1 42484	The first recurrence relation for Fermat numbers, see Wikipedia "Fermat number", https://en.wikipedia.org/wiki/Fermat_number#Basic_properties, 22-Jul-2021. (Contributed by AV, 22-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = ((((FermatNo‘𝑁) − 1)↑2) + 1))
Theorem	sqrtpwpw2p 42485	The floor of the square root of 2 to the power of 2 to the power of a positive integer plus a bounded nonnegative integer. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < ((2↑((2↑(𝑁 − 1)) + 1)) + 1)) → (⌊‘(√‘((2↑(2↑𝑁)) + 𝑀))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtnosqrt 42486	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtno0 42487	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) = 3
Theorem	fmtno1 42488	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) = 5
Theorem	fmtnorec2lem 42489*	Lemma for fmtnorec2 42490 (induction step). (Contributed by AV, 29-Jul-2021.)
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)))
Theorem	fmtnorec2 42490*	The second recurrence relation for Fermat numbers, see ProofWiki "Product of Sequence of Fermat Numbers plus 2", 29-Jul-2021, https://proofwiki.org/wiki/Product_of_Sequence_of_Fermat_Numbers_plus_2 or Wikipedia "Fermat number", 29-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 29-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘(𝑁 + 1)) = (∏𝑛 ∈ (0...𝑁)(FermatNo‘𝑛) + 2))
Theorem	fmtnodvds 42491	Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 42490, see ProofWiki "Product of Sequence of Fermat Numbers plus 2/Corollary", 31-Jul-2021. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ) → (FermatNo‘𝑁) ∥ ((FermatNo‘(𝑁 + 𝑀)) − 2))
Theorem	goldbachthlem1 42492	Lemma 1 for goldbachth 42494. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2))
Theorem	goldbachthlem2 42493	Lemma 2 for goldbachth 42494. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	goldbachth 42494	Goldbach's theorem: Two different Fermat numbers are coprime. See ProofWiki "Goldbach's theorem", 31-Jul-2021, https://proofwiki.org/wiki/Goldbach%27s_Theorem or Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑁 ≠ 𝑀) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	fmtnorec3 42495*	The third recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 2-Aug-2021.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = ((FermatNo‘(𝑁 − 1)) + ((2↑(2↑(𝑁 − 1))) · ∏𝑛 ∈ (0...(𝑁 − 2))(FermatNo‘𝑛))))
Theorem	fmtnorec4 42496	The fourth recurrence relation for Fermat numbers, see Wikipedia "Fermat number", 31-Jul-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties. (Contributed by AV, 31-Jul-2021.)
⊢ (𝑁 ∈ (ℤ≥‘2) → (FermatNo‘𝑁) = (((FermatNo‘(𝑁 − 1))↑2) − (2 · (((FermatNo‘(𝑁 − 2)) − 1)↑2))))
Theorem	fmtno2 42497	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) = ;17
Theorem	fmtno3 42498	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘3) = ;;257
Theorem	fmtno4 42499	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘4) = ;;;;65537
Theorem	fmtno5lem1 42500	Lemma 1 for fmtno5 42504. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 6) = ;;;;;393216