P. 485 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48401-48500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prprval 48401*	The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.)
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})})
Theorem	prprvalpw 48402*	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 48403	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 48404*	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 48405*	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 48406*	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 48407*	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 48408*	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 48409*	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 48410*	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 48411	Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.)
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)))
Theorem	2exopprim 48412	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 48413*	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.50.12  Number theory (extension)
21.50.12.1  Properties of non-prime numbers
Theorem	nprmmul1 48414*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 5-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ ∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)𝑁 = (𝑎 · 𝑏)))
Theorem	nprmmul2 48415*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 6-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ ∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)(𝑎 ≤ 𝑏 ∧ 𝑁 = (𝑎 · 𝑏))))
Theorem	nprmmul3 48416*	Special factorization of a non-prime integer greater than 3. (Contributed by AV, 4-Apr-2026.)
⊢ (𝑁 ∈ (ℤ≥‘4) → (𝑁 ∉ ℙ ↔ (∃𝑎 ∈ (2..^𝑁)∃𝑏 ∈ (2..^𝑁)(𝑎 < 𝑏 ∧ 𝑁 = (𝑎 · 𝑏)) ∨ ∃𝑎 ∈ (2..^𝑁)𝑁 = (𝑎↑2))))
21.50.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 48418, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 48467, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 48473. 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 48466 (previously, it was ;;;4001, see 4001prm 17241). Another important result of this section is Goldbach's theorem goldbachth 48437, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 48478. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 48480.
Syntax	cfmtno 48417	Extend class notation with the Fermat numbers.
class FermatNo
Definition	df-fmtno 48418	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 48419	The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1))
Theorem	fmtnoge3 48420	Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3))
Theorem	fmtnonn 48421	Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.)
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ)
Theorem	fmtnom1nn 48422	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 48423	Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.)
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁))
Theorem	fmtnorn 48424*	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 48425	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 48426	The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.)
⊢ ran FermatNo ∉ Fin
Theorem	fmtnorec1 48427	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 48428	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 48429	The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1))))
Theorem	fmtno0 48430	The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) = 3
Theorem	fmtno1 48431	The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) = 5
Theorem	fmtnorec2lem 48432*	Lemma for fmtnorec2 48433 (induction step). (Contributed by AV, 29-Jul-2021.)
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2)))
Theorem	fmtnorec2 48433*	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 48434	Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 48433, 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 48435	Lemma 1 for goldbachth 48437. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2))
Theorem	goldbachthlem2 48436	Lemma 2 for goldbachth 48437. (Contributed by AV, 1-Aug-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1)
Theorem	goldbachth 48437	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 48438*	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 48439	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 48440	The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) = ;17
Theorem	fmtno3 48441	The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘3) = ;;257
Theorem	fmtno4 48442	The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘4) = ;;;;65537
Theorem	fmtno5lem1 48443	Lemma 1 for fmtno5 48447. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 6) = ;;;;;393216
Theorem	fmtno5lem2 48444	Lemma 2 for fmtno5 48447. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 5) = ;;;;;327680
Theorem	fmtno5lem3 48445	Lemma 3 for fmtno5 48447. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;65536 · 3) = ;;;;;196608
Theorem	fmtno5lem4 48446	Lemma 4 for fmtno5 48447. (Contributed by AV, 30-Jul-2021.)
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296
Theorem	fmtno5 48447	The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.)
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297
Theorem	fmtno0prm 48448	The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘0) ∈ ℙ
Theorem	fmtno1prm 48449	The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘1) ∈ ℙ
Theorem	fmtno2prm 48450	The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.)
⊢ (FermatNo‘2) ∈ ℙ
Theorem	257prm 48451	257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ ;;257 ∈ ℙ
Theorem	fmtno3prm 48452	The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.)
⊢ (FermatNo‘3) ∈ ℙ
Theorem	odz2prm2pw 48453	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 48454	Lemma for fmtnoprmfac1 48455: 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 48455*	Divisor of Fermat number (special form of Euler's result, see fmtnofac1 48460): 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 48456	Lemma for fmtnoprmfac2 48457. (Contributed by AV, 26-Jul-2021.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1)
Theorem	fmtnoprmfac2 48457*	Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 48459): 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 48458*	Lemma for fmtnofac2 48459 (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 48459*	Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 48460: 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 48460*	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 48459. (Contributed by AV, 30-Jul-2021.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1))
Theorem	fmtno4sqrt 48461	The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.)
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256
Theorem	fmtno4prmfac 48462	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 48463	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 48464	193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.)
⊢ ¬ ;;193 ∥ (FermatNo‘4)
Theorem	fmtno4prm 48465	The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ (FermatNo‘4) ∈ ℙ
Theorem	65537prm 48466	65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.)
⊢ ;;;;65537 ∈ ℙ
Theorem	fmtnofz04prm 48467	The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.)
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtnole4prm 48468	The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ)
Theorem	fmtno5faclem1 48469	Lemma 1 for fmtno5fac 48472. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668
Theorem	fmtno5faclem2 48470	Lemma 2 for fmtno5fac 48472. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502
Theorem	fmtno5faclem3 48471	Lemma 3 for fmtno5fac 48472. (Contributed by AV, 22-Jul-2021.)
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688
Theorem	fmtno5fac 48472	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 48473	The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.)
⊢ (FermatNo‘5) ∉ ℙ
Theorem	prmdvdsfmtnof1lem1 48474*	Lemma 1 for prmdvdsfmtnof1 48477. (Contributed by AV, 3-Aug-2021.)
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < )    &   ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < )    ⇒   ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺)))
Theorem	prmdvdsfmtnof1lem2 48475	Lemma 2 for prmdvdsfmtnof1 48477. (Contributed by AV, 3-Aug-2021.)
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺))
Theorem	prmdvdsfmtnof 48476*	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 48477*	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 48478	The set of prime numbers is infinite. The proof of this variant of prminf 17011 is based on Goldbach's theorem goldbachth 48437 (via prmdvdsfmtnof1 48477 and prmdvdsfmtnof1lem2 48475), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 48475. (Contributed by AV, 4-Aug-2021.)
⊢ ℙ ∉ Fin
Theorem	2pwp1prm 48479*	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 48480*	Every prime number of the form ((2↑𝑘) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.)
⊢ ((𝐾 ∈ ℕ ∧ 𝑃 = ((2↑𝐾) + 1) ∧ 𝑃 ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝑃 = (FermatNo‘𝑛))
21.50.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 27461. 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 48491. This is an example of sgprmdvdsmersenne 48494, 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 48494. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 48493, 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 48501.
Theorem	m2prm 48481	The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑2) − 1) ∈ ℙ
Theorem	m3prm 48482	The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑3) − 1) ∈ ℙ
Theorem	flsqrt 48483	A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))))
Theorem	flsqrt5 48484	The floor of the square root of a nonnegative number is 5 iff the number is between 25 and 35. (Contributed by AV, 17-Aug-2021.)
⊢ ((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) → ((;25 ≤ 𝑋 ∧ 𝑋 < ;36) ↔ (⌊‘(√‘𝑋)) = 5))
Theorem	3ndvds4 48485	3 does not divide 4. (Contributed by AV, 18-Aug-2021.)
⊢ ¬ 3 ∥ 4
Theorem	139prmALT 48486	139 is a prime number. In contrast to 139prm 17220, the proof of this theorem uses 3dvds2dec 16427 for checking the divisibility by 3. Although the proof using 3dvds2dec 16427 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17220), the number of essential steps is smaller (301 compared with 327 for 139prm 17220). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ;;139 ∈ ℙ
Theorem	31prm 48487	31 is a prime number. In contrast to 37prm 17217, the proof of this theorem is not based on the "blanket" prmlem2 17216, but on isprm7 16803. Although the checks for non-divisibility by the primes 7 to 23 are not needed, the proof is much longer (regarding size) than the proof of 37prm 17217 (1810 characters compared with 1213 for 37prm 17217). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17217). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.)
⊢ ;31 ∈ ℙ
Theorem	m5prm 48488	The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.)
⊢ ((2↑5) − 1) ∈ ℙ
Theorem	127prm 48489	127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.)
⊢ ;;127 ∈ ℙ
Theorem	m7prm 48490	The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑7) − 1) ∈ ℙ
Theorem	m11nprm 48491	The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑;11) − 1) = (;89 · ;23)
Theorem	mod42tp1mod8 48492	If a number is 3 modulo 4, twice the number plus 1 is 7 modulo 8. (Contributed by AV, 19-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 4) = 3) → (((2 · 𝑁) + 1) mod 8) = 7)
Theorem	sfprmdvdsmersenne 48493	If 𝑄 is a safe prime (i.e. 𝑄 = ((2 · 𝑃) + 1) for a prime 𝑃) with 𝑄≡7 (mod 8), then 𝑄 divides the 𝑃-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑄 ∈ ℙ ∧ (𝑄 mod 8) = 7 ∧ 𝑄 = ((2 · 𝑃) + 1))) → 𝑄 ∥ ((2↑𝑃) − 1))
Theorem	sgprmdvdsmersenne 48494	If 𝑃 is a Sophie Germain prime (i.e. 𝑄 = ((2 · 𝑃) + 1) is also prime) with 𝑃≡3 (mod 4), then 𝑄 divides the 𝑃-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.)
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 3) ∧ (𝑄 = ((2 · 𝑃) + 1) ∧ 𝑄 ∈ ℙ)) → 𝑄 ∥ ((2↑𝑃) − 1))
Theorem	lighneallem1 48495	Lemma 1 for lighneal 48501. (Contributed by AV, 11-Aug-2021.)
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀))
Theorem	lighneallem2 48496	Lemma 2 for lighneal 48501. (Contributed by AV, 13-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem3 48497	Lemma 3 for lighneal 48501. (Contributed by AV, 11-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem4a 48498	Lemma 1 for lighneallem4 48500. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆)
Theorem	lighneallem4b 48499*	Lemma 2 for lighneallem4 48500. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2))
Theorem	lighneallem4 48500	Lemma 3 for lighneal 48501. (Contributed by AV, 16-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)