P. 482 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48101-48200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sprsymrelfo 48101*	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 48102*	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 48103*	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 48104*	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 12442). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4823), {1, V} = {1} (see prprc2 4728) or {V, V} = ∅ (see prprc 4729).
Theorem	prpair 48105*	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 48106	Lemma 0 for prproropf1o 48111. 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 48107*	Lemma 1 for prproropf1o 48111. (Contributed by AV, 12-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃)
Theorem	prproropf1olem2 48108*	Lemma 2 for prproropf1o 48111. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → ⟨inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)⟩ ∈ 𝑂)
Theorem	prproropf1olem3 48109*	Lemma 3 for prproropf1o 48111. (Contributed by AV, 13-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = ⟨(1st ‘𝑊), (2nd ‘𝑊)⟩)
Theorem	prproropf1olem4 48110*	Lemma 4 for prproropf1o 48111. (Contributed by AV, 14-Mar-2023.)
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉))    &   ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2}    &   ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ ⟨inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)⟩)    ⇒   ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊))
Theorem	prproropf1o 48111*	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 48112*	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 48113*	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 48114*	Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.)
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2}    ⇒   ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑))
Theorem	paireqne 48115*	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 48116	Extend class notation with set of proper unordered pairs.
class Pairsproper
Definition	df-prpr 48117*	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 48118*	The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprvalpw 48119*	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 48120	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 48121*	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 48122*	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 48123*	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 48124*	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 48125*	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 48126*	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 48127*	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 48128	Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	2exopprim 48129	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 48130*	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  Properties of non-prime numbers
Theorem	nprmmul1 48131*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 5-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ ∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)𝑁 = (𝑎 · 𝑏)))
Theorem	nprmmul2 48132*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 6-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ ∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)(𝑎 ≤ 𝑏 ∧ 𝑁 = (𝑎 · 𝑏))))
Theorem	nprmmul3 48133*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 4-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ (∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)(𝑎 < 𝑏 ∧ 𝑁 = (𝑎 · 𝑏)) ∨ ∃𝑎 ∈ (2..^𝑁)𝑁 = (𝑎↑2))))
21.48.12.2  Fermat numbers At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 48135, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 48184, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 48190. 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 48183 (previously, it was ;;;4001, see 4001prm 17195). Another important result of this section is Goldbach's theorem goldbachth 48154, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 48195. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 48197.
Syntax	cfmtno 48134	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 48135	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 48136	The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
Theorem	fmtnoge3 48137	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3))
Theorem	fmtnonn 48138	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ)
Theorem	fmtnom1nn 48139	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 48140	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
Theorem	fmtnorn 48141*	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 48142	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 48143	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
⊢ ran FermatNo ∉ Fin
Theorem	fmtnorec1 48144	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 48145	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 48146	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtno0 48147	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) = 3
Theorem	fmtno1 48148	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) = 5
Theorem	fmtnorec2lem 48149*	Lemma for fmtnorec2 48150 (induction step). (Contributed by AV, 29-Jul-2021.)
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)))
Theorem	fmtnorec2 48150*	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 48151	Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 48150, 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 48152	Lemma 1 for goldbachth 48154. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2))
Theorem	goldbachthlem2 48153	Lemma 2 for goldbachth 48154. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	goldbachth 48154	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 48155*	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 48156	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 48157	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) = ;17
Theorem	fmtno3 48158	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘3) = ;;257
Theorem	fmtno4 48159	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘4) = ;;;;65537
Theorem	fmtno5lem1 48160	Lemma 1 for fmtno5 48164. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 6) = ;;;;;393216
Theorem	fmtno5lem2 48161	Lemma 2 for fmtno5 48164. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 5) = ;;;;;327680
Theorem	fmtno5lem3 48162	Lemma 3 for fmtno5 48164. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 3) = ;;;;;196608
Theorem	fmtno5lem4 48163	Lemma 4 for fmtno5 48164. (Contributed by AV, 30-Jul-2021.)
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296
Theorem	fmtno5 48164	The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.)
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297
Theorem	fmtno0prm 48165	The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) ∈ ℙ
Theorem	fmtno1prm 48166	The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) ∈ ℙ
Theorem	fmtno2prm 48167	The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) ∈ ℙ
Theorem	257prm 48168	257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ ;;257 ∈ ℙ
Theorem	fmtno3prm 48169	The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ (FermatNo‘3) ∈ ℙ
Theorem	odz2prm2pw 48170	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 48171	Lemma for fmtnoprmfac1 48172: 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 48172*	Divisor of Fermat number (special form of Euler's result, see fmtnofac1 48177): 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 48173	Lemma for fmtnoprmfac2 48174. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
Theorem	fmtnoprmfac2 48174*	Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 48176): 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 48175*	Lemma for fmtnofac2 48176 (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 48176*	Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 48177: 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 48177*	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 48176. (Contributed by AV, 30-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1))
Theorem	fmtno4sqrt 48178	The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.)
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256
Theorem	fmtno4prmfac 48179	If P was a (prime) factor of the fourth Fermat number less than the square root of the fourth Fermat number, it would be either 65 or 129 or 193. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘4) ∧ 𝑃 ≤ (⌊‘(√‘(FermatNo‘4)))) → (𝑃 = ;65 ∨ 𝑃 = ;;129 ∨ 𝑃 = ;;193))
Theorem	fmtno4prmfac193 48180	If P was a (prime) factor of the fourth Fermat number, it would be 193. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∥ (FermatNo‘4) ∧ 𝑃 ≤ (⌊‘(√‘(FermatNo‘4)))) → 𝑃 = ;;193)
Theorem	fmtno4nprmfac193 48181	193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.)
⊢ ¬ ;;193 ∥ (FermatNo‘4)
Theorem	fmtno4prm 48182	The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ (FermatNo‘4) ∈ ℙ
Theorem	65537prm 48183	65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ ;;;;65537 ∈ ℙ
Theorem	fmtnofz04prm 48184	The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtnole4prm 48185	The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtno5faclem1 48186	Lemma 1 for fmtno5fac 48189. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668
Theorem	fmtno5faclem2 48187	Lemma 2 for fmtno5fac 48189. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502
Theorem	fmtno5faclem3 48188	Lemma 3 for fmtno5fac 48189. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688
Theorem	fmtno5fac 48189	The factorization of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.)
⊢ (FermatNo‘5) = (;;;;;;6700417 · ;;641)
Theorem	fmtno5nprm 48190	The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.)
⊢ (FermatNo‘5) ∉ ℙ
Theorem	prmdvdsfmtnof1lem1 48191*	Lemma 1 for prmdvdsfmtnof1 48194. (Contributed by AV, 3-Aug-2021.)
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < )    &   ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < )    ⇒   ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)))
Theorem	prmdvdsfmtnof1lem2 48192	Lemma 2 for prmdvdsfmtnof1 48194. (Contributed by AV, 3-Aug-2021.)
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))
Theorem	prmdvdsfmtnof 48193*	The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021.) (Proof shortened by II, 16-Feb-2023.)
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ))    ⇒   ⊢ 𝐹:ran FermatNo⟶ℙ
Theorem	prmdvdsfmtnof1 48194*	The mapping of a Fermat number to its smallest prime factor is a one-to-one function. (Contributed by AV, 4-Aug-2021.)
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < ))    ⇒   ⊢ 𝐹:ran FermatNo–1-1→ℙ
Theorem	prminf2 48195	The set of prime numbers is infinite. The proof of this variant of prminf 16965 is based on Goldbach's theorem goldbachth 48154 (via prmdvdsfmtnof1 48194 and prmdvdsfmtnof1lem2 48192), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 48192. (Contributed by AV, 4-Aug-2021.)
⊢ ℙ ∉ Fin
Theorem	2pwp1prm 48196*	For ((2↑𝑘) + 1) to be prime, 𝑘 must be a power of 2, see Wikipedia "Fermat number", section "Other theorems about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number, 5-Aug-2021. (Contributed by AV, 7-Aug-2021.)
⊢ ((𝐾 ∈ ℕ ∧ ((2↑𝐾) + 1) ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛))
Theorem	2pwp1prmfmtno 48197*	Every prime number of the form ((2↑𝑘) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑃 = ((2↑𝐾) + 1) ∧ 𝑃 ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝑃 = (FermatNo‘𝑛))
21.48.12.3  Mersenne primes "In mathematics, a Mersenne prime is a prime number that is one less than a power of two. That is, it is a prime number of the form Mn = 2^n-1 for some integer n. They are named after Marin Mersenne ... If n is a composite number then so is 2^n-1. Therefore, an equivalent definition of the Mersenne primes is that they are the prime numbers of the form Mp = 2^p-1 for some prime p.", see Wikipedia "Mersenne prime", 16-Aug-2021, https://en.wikipedia.org/wiki/Mersenne_prime. See also definition in [ApostolNT] p. 4. This means that if Mn = 2^n-1 is prime, than n must be prime, too, see mersenne 27349. The reverse direction is not generally valid: If p is prime, then Mp = 2^p-1 needs not be prime, e.g. M11 = 2047 = 23 x 89, see m11nprm 48208. This is an example of sgprmdvdsmersenne 48211, stating that if p with p = 3 modulo 4 (here 11) and q=2p+1 (here 23) are prime, then q divides Mp. "In number theory, a prime number p is a Sophie Germain prime if 2p+1 is also prime. The number 2p+1 associated with a Sophie Germain prime is called a safe prime.", see Wikipedia "Safe and Sophie Germain primes", 21-Aug-2021, https://en.wikipedia.org/wiki/Safe_and_Sophie_Germain_primes 48211. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 48210, it is shown that if a safe prime q is congruent to 7 modulo 8, then it is a divisor of the Mersenne number with its matching Sophie Germain prime as exponent. The main result of this section, however, is the formal proof of a theorem of S. Ligh and L. Neal in "A note on Mersenne numbers", see lighneal 48218.
Theorem	m2prm 48198	The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑2) − 1) ∈ ℙ
Theorem	m3prm 48199	The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑3) − 1) ∈ ℙ
Theorem	flsqrt 48200	A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))))