P. 476 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47501-47600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ich2exprop 47501*	If the setvar variables are interchangeable in a wff, there is an ordered pair fulfilling the wff iff there is an unordered pair fulfilling the wff. (Contributed by AV, 16-Jul-2023.)
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ [𝑎⇄𝑏]𝜑) → (∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ 𝜑) ↔ ∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑)))
Theorem	ichnreuop 47502*	If the setvar variables are interchangeable in a wff, there is never a unique ordered pair with different components fulfilling the wff (because if ⟨𝑎, 𝑏⟩ fulfils the wff, then also ⟨𝑏, 𝑎⟩ fulfils the wff). (Contributed by AV, 27-Aug-2023.)
⊢ ([𝑎⇄𝑏]𝜑 → ¬ ∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑎 ≠ 𝑏 ∧ 𝜑))
Theorem	ichreuopeq 47503*	If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023.)
⊢ ([𝑎⇄𝑏]𝜑 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏(𝑎 = 𝑏 ∧ 𝜑)))
21.48.11.2  Set of unordered pairs
Theorem	sprid 47504	Two identical representations of the class of all unordered pairs. (Contributed by AV, 21-Nov-2021.)
⊢ {𝑝 ∣ ∃𝑎 ∈ V ∃𝑏 ∈ V 𝑝 = {𝑎, 𝑏}} = {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}
Theorem	elsprel 47505*	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 4720, which is not an element of all unordered pairs, see spr0nelg 47506. (Contributed by AV, 21-Nov-2021.)
⊢ ((𝐴 ∈ 𝑉 ∨ 𝐵 ∈ 𝑊) → {𝐴, 𝐵} ∈ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}})
Theorem	spr0nelg 47506*	The empty set is not an element of all unordered pairs. (Contributed by AV, 21-Nov-2021.)
⊢ ∅ ∉ {𝑝 ∣ ∃𝑎∃𝑏 𝑝 = {𝑎, 𝑏}}
Syntax	cspr 47507	Extend class notation with set of pairs.
class Pairs
Definition	df-spr 47508*	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 47509*	The set of all unordered pairs over a given set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ (𝑉 ∈ 𝑊 → (Pairs‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 𝑝 = {𝑎, 𝑏}})
Theorem	sprvalpw 47510*	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 47511*	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 47512	The empty set is not an unordered pair over any set 𝑉. (Contributed by AV, 21-Nov-2021.)
⊢ ∅ ∉ (Pairs‘𝑉)
Theorem	sprvalpwn0 47513*	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 47514*	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 47515*	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 47516	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 47517	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 47518	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 47519*	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 47520*	Lemma for sprsymrelf 47525 and sprsymrelfv 47524. (Contributed by AV, 19-Nov-2021.)
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉))
Theorem	sprsymrelf1lem 47521*	Lemma for sprsymrelf1 47526. (Contributed by AV, 22-Nov-2021.)
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {⟨𝑥, 𝑦⟩ ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏))
Theorem	sprsymrelfolem1 47522*	Lemma 1 for sprsymrelfo 47527. (Contributed by AV, 22-Nov-2021.)
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)}    ⇒   ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉)
Theorem	sprsymrelfolem2 47523*	Lemma 2 for sprsymrelfo 47527. (Contributed by AV, 23-Nov-2021.)
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)}    ⇒   ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦}))
Theorem	sprsymrelfv 47524*	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 47525*	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 47526*	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 47527*	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 47528*	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 47529*	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 47530*	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‘𝑉)    &   ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}    ⇒   ⊢ (𝑉 ∈ 𝑊 → 𝑃 ≈ 𝑅)
21.48.11.3  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 12325). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4814), {1, V} = {1} (see prprc2 4719) or {V, V} = ∅ (see prprc 4720).
Theorem	prpair 47531*	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 47532	Lemma 0 for prproropf1o 47537. 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 47533*	Lemma 1 for prproropf1o 47537. (Contributed by AV, 12-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃)
Theorem	prproropf1olem2 47534*	Lemma 2 for prproropf1o 47537. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → ⟨inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)⟩ ∈ 𝑂)
Theorem	prproropf1olem3 47535*	Lemma 3 for prproropf1o 47537. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩)
Theorem	prproropf1olem4 47536*	Lemma 4 for prproropf1o 47537. (Contributed by AV, 14-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊))
Theorem	prproropf1o 47537*	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 47538*	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 47539*	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 47540*	Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑))
Theorem	paireqne 47541*	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}    ⇒   ⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵))
21.48.11.4  Set of proper unordered pairs
Syntax	cprpr 47542	Extend class notation with set of proper unordered pairs.
class Pairsproper
Definition	df-prpr 47543*	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 47544*	The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprvalpw 47545*	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 47546	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 47547*	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 47548*	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 47549*	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 47550*	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 ∧ 𝜑)))
Theorem	sbcpr 47551*	The proper substitution of an unordered pair for a setvar variable corresponds to a proper substitution of each of its elements. (Contributed by AV, 7-Apr-2023.)
⊢ (𝑝 = {𝑥, 𝑦} → (𝜑 ↔ 𝜓))    ⇒   ⊢ ([{𝑎, 𝑏} / 𝑝]𝜑 ↔ [𝑏 / 𝑦][𝑎 / 𝑥]𝜓)
Theorem	reupr 47552*	There is a unique unordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 7-Apr-2023.)
⊢ (𝑝 = {𝑎, 𝑏} → (𝜓 ↔ 𝜒))    &   ⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairs‘𝑋)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝜃 → {𝑥, 𝑦} = {𝑎, 𝑏}))))
Theorem	reuprpr 47553*	There is a unique proper unordered pair fulfilling a wff iff there are uniquely two different sets fulfilling a corresponding wff. (Contributed by AV, 30-Apr-2023.)
⊢ (𝑝 = {𝑎, 𝑏} → (𝜓 ↔ 𝜒))    &   ⊢ (𝑝 = {𝑥, 𝑦} → (𝜓 ↔ 𝜃))    ⇒   ⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (Pairsproper‘𝑋)𝜓 ↔ ∃𝑎 ∈ 𝑋 ∃𝑏 ∈ 𝑋 (𝑎 ≠ 𝑏 ∧ 𝜒 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 ≠ 𝑦 ∧ 𝜃) → {𝑥, 𝑦} = {𝑎, 𝑏}))))
Theorem	poprelb 47554	Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	2exopprim 47555	The existence of an ordered pair fulfilling a wff implies the existence of an unordered pair fulfilling the wff. (Contributed by AV, 29-Jul-2023.)
⊢ (∃𝑎∃𝑏(⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃𝑎∃𝑏({𝐴, 𝐵} = {𝑎, 𝑏} ∧ 𝜑))
Theorem	reuopreuprim 47556*	There is a unique unordered pair with ordered elements fulfilling a wff if there is a unique ordered pair fulfilling the wff. (Contributed by AV, 28-Jul-2023.)
⊢ (𝑋 ∈ 𝑉 → (∃!𝑝 ∈ (𝑋 × 𝑋)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝜑) → ∃!𝑝 ∈ (Pairs‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑)))
21.48.12  Number theory (extension)
21.48.12.1  Fermat numbers At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 47558, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 47607, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 47613. 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 47606 (previously, it was ;;;4001, see 4001prm 17053). Another important result of this section is Goldbach's theorem goldbachth 47577, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 47618. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 47620.
Syntax	cfmtno 47557	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 47558	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 47559	The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
Theorem	fmtnoge3 47560	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3))
Theorem	fmtnonn 47561	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ)
Theorem	fmtnom1nn 47562	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 47563	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
Theorem	fmtnorn 47564*	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 47565	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 47566	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
⊢ ran FermatNo ∉ Fin
Theorem	fmtnorec1 47567	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 47568	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 47569	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtno0 47570	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) = 3
Theorem	fmtno1 47571	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) = 5
Theorem	fmtnorec2lem 47572*	Lemma for fmtnorec2 47573 (induction step). (Contributed by AV, 29-Jul-2021.)
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)))
Theorem	fmtnorec2 47573*	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 47574	Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 47573, 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 47575	Lemma 1 for goldbachth 47577. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2))
Theorem	goldbachthlem2 47576	Lemma 2 for goldbachth 47577. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	goldbachth 47577	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 47578*	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 47579	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 47580	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) = ;17
Theorem	fmtno3 47581	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘3) = ;;257
Theorem	fmtno4 47582	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘4) = ;;;;65537
Theorem	fmtno5lem1 47583	Lemma 1 for fmtno5 47587. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 6) = ;;;;;393216
Theorem	fmtno5lem2 47584	Lemma 2 for fmtno5 47587. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 5) = ;;;;;327680
Theorem	fmtno5lem3 47585	Lemma 3 for fmtno5 47587. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 3) = ;;;;;196608
Theorem	fmtno5lem4 47586	Lemma 4 for fmtno5 47587. (Contributed by AV, 30-Jul-2021.)
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296
Theorem	fmtno5 47587	The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.)
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297
Theorem	fmtno0prm 47588	The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) ∈ ℙ
Theorem	fmtno1prm 47589	The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) ∈ ℙ
Theorem	fmtno2prm 47590	The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) ∈ ℙ
Theorem	257prm 47591	257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ ;;257 ∈ ℙ
Theorem	fmtno3prm 47592	The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ (FermatNo‘3) ∈ ℙ
Theorem	odz2prm2pw 47593	Any power of two is coprime to any prime not being two. (Contributed by AV, 25-Jul-2021.)
⊢ (((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2})) ∧ (((2↑(2↑𝑁)) mod 𝑃) ≠ 1 ∧ ((2↑(2↑(𝑁 + 1))) mod 𝑃) = 1)) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
Theorem	fmtnoprmfac1lem 47594	Lemma for fmtnoprmfac1 47595: The order of 2 modulo a prime that divides the n-th Fermat number is 2^(n+1). (Contributed by AV, 25-Jul-2021.) (Proof shortened by AV, 18-Mar-2022.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((odℤ‘𝑃)‘2) = (2↑(𝑁 + 1)))
Theorem	fmtnoprmfac1 47595*	Divisor of Fermat number (special form of Euler's result, see fmtnofac1 47600): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+1)+1 where k is a positive integer. (Contributed by AV, 25-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 1))) + 1))
Theorem	fmtnoprmfac2lem1 47596	Lemma for fmtnoprmfac2 47597. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
Theorem	fmtnoprmfac2 47597*	Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 47599): Let Fn be a Fermat number. Let p be a prime divisor of Fn. Then p is in the form: k*2^(n+2)+1 where k is a positive integer. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ 𝑃 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
Theorem	fmtnofac2lem 47598*	Lemma for fmtnofac2 47599 (Induction step). (Contributed by AV, 30-Jul-2021.)
⊢ ((𝑦 ∈ (ℤ≥‘2) ∧ 𝑧 ∈ (ℤ≥‘2)) → ((((𝑁 ∈ (ℤ≥‘2) ∧ 𝑦 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑦 = ((𝑘 · (2↑(𝑁 + 2))) + 1)) ∧ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑧 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑧 = ((𝑘 · (2↑(𝑁 + 2))) + 1))) → ((𝑁 ∈ (ℤ≥‘2) ∧ (𝑦 · 𝑧) ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 (𝑦 · 𝑧) = ((𝑘 · (2↑(𝑁 + 2))) + 1))))
Theorem	fmtnofac2 47599*	Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 47600: Let Fn be a Fermat number. Let m be divisor of Fn. Then m is in the form: k*2^(n+2)+1 where k is a nonnegative integer. (Contributed by AV, 30-Jul-2021.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 2))) + 1))
Theorem	fmtnofac1 47600*	Divisor of Fermat number (Euler's Result), see ProofWiki "Divisor of Fermat Number/Euler's Result", 24-Jul-2021, https://proofwiki.org/wiki/Divisor_of_Fermat_Number/Euler's_Result): "Let Fn be a Fermat number. Let m be divisor of Fn. Then m is in the form: k*2^(n+1)+1 where k is a positive integer." Here, however, k must be a nonnegative integer, because k must be 0 to represent 1 (which is a divisor of Fn ). Historical Note: In 1747, Leonhard Paul Euler proved that a divisor of a Fermat number Fn is always in the form kx2^(n+1)+1. This was later refined to k*2^(n+2)+1 by François Édouard Anatole Lucas, see fmtnofac2 47599. (Contributed by AV, 30-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1))