| Metamath
Proof Explorer Theorem List (p. 476 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | prprval 47501* | The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.) |
| ⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
| Theorem | prprvalpw 47502* | 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 47503 | 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 47504* | 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 47505* | 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 47506* | 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 47507* | 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 47508* | 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 47509* | 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 47510* | 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 47511 | Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.) |
| ⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
| Theorem | 2exopprim 47512 | 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 47513* | 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‘𝑋)∃𝑎∃𝑏(𝑝 = {𝑎, 𝑏} ∧ 𝜑))) | ||
At first, the (sequence of) Fermat numbers FermatNo (the 𝑛-th Fermat number is denoted as (FermatNo‘𝑛)) is defined, see df-fmtno 47515, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 47564, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 47570. 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 47563 (previously, it was ;;;4001, see 4001prm 17182). Another important result of this section is Goldbach's theorem goldbachth 47534, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 47575. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 47577. | ||
| Syntax | cfmtno 47514 | Extend class notation with the Fermat numbers. |
| class FermatNo | ||
| Definition | df-fmtno 47515 | 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 47516 | The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) | ||
| Theorem | fmtnoge3 47517 | Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3)) | ||
| Theorem | fmtnonn 47518 | Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ) | ||
| Theorem | fmtnom1nn 47519 | 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 47520 | Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.) |
| ⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁)) | ||
| Theorem | fmtnorn 47521* | 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 47522 | 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 47523 | The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.) |
| ⊢ ran FermatNo ∉ Fin | ||
| Theorem | fmtnorec1 47524 | 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 47525 | 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 47526 | The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.) |
| ⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1)))) | ||
| Theorem | fmtno0 47527 | The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘0) = 3 | ||
| Theorem | fmtno1 47528 | The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘1) = 5 | ||
| Theorem | fmtnorec2lem 47529* | Lemma for fmtnorec2 47530 (induction step). (Contributed by AV, 29-Jul-2021.) |
| ⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) | ||
| Theorem | fmtnorec2 47530* | 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 47531 | Any Fermat number divides a greater Fermat number minus 2. Corollary of fmtnorec2 47530, 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 47532 | Lemma 1 for goldbachth 47534. (Contributed by AV, 1-Aug-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2)) | ||
| Theorem | goldbachthlem2 47533 | Lemma 2 for goldbachth 47534. (Contributed by AV, 1-Aug-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) | ||
| Theorem | goldbachth 47534 | 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 47535* | 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 47536 | 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 47537 | The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘2) = ;17 | ||
| Theorem | fmtno3 47538 | The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘3) = ;;257 | ||
| Theorem | fmtno4 47539 | The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘4) = ;;;;65537 | ||
| Theorem | fmtno5lem1 47540 | Lemma 1 for fmtno5 47544. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;65536 · 6) = ;;;;;393216 | ||
| Theorem | fmtno5lem2 47541 | Lemma 2 for fmtno5 47544. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;65536 · 5) = ;;;;;327680 | ||
| Theorem | fmtno5lem3 47542 | Lemma 3 for fmtno5 47544. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;65536 · 3) = ;;;;;196608 | ||
| Theorem | fmtno5lem4 47543 | Lemma 4 for fmtno5 47544. (Contributed by AV, 30-Jul-2021.) |
| ⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296 | ||
| Theorem | fmtno5 47544 | The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.) |
| ⊢ (FermatNo‘5) = ;;;;;;;;;4294967297 | ||
| Theorem | fmtno0prm 47545 | The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘0) ∈ ℙ | ||
| Theorem | fmtno1prm 47546 | The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘1) ∈ ℙ | ||
| Theorem | fmtno2prm 47547 | The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.) |
| ⊢ (FermatNo‘2) ∈ ℙ | ||
| Theorem | 257prm 47548 | 257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
| ⊢ ;;257 ∈ ℙ | ||
| Theorem | fmtno3prm 47549 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
| ⊢ (FermatNo‘3) ∈ ℙ | ||
| Theorem | odz2prm2pw 47550 | 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 47551 | Lemma for fmtnoprmfac1 47552: 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 47552* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 47557): 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 47553 | Lemma for fmtnoprmfac2 47554. (Contributed by AV, 26-Jul-2021.) |
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) | ||
| Theorem | fmtnoprmfac2 47554* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 47556): 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 47555* | Lemma for fmtnofac2 47556 (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 47556* | Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 47557: 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 47557* |
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 47556. (Contributed by AV, 30-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1)) | ||
| Theorem | fmtno4sqrt 47558 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
| ⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256 | ||
| Theorem | fmtno4prmfac 47559 | 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 47560 | 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 47561 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
| ⊢ ¬ ;;193 ∥ (FermatNo‘4) | ||
| Theorem | fmtno4prm 47562 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
| ⊢ (FermatNo‘4) ∈ ℙ | ||
| Theorem | 65537prm 47563 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
| ⊢ ;;;;65537 ∈ ℙ | ||
| Theorem | fmtnofz04prm 47564 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
| ⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
| Theorem | fmtnole4prm 47565 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
| Theorem | fmtno5faclem1 47566 | Lemma 1 for fmtno5fac 47569. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
| Theorem | fmtno5faclem2 47567 | Lemma 2 for fmtno5fac 47569. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
| Theorem | fmtno5faclem3 47568 | Lemma 3 for fmtno5fac 47569. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
| Theorem | fmtno5fac 47569 | 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 47570 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
| ⊢ (FermatNo‘5) ∉ ℙ | ||
| Theorem | prmdvdsfmtnof1lem1 47571* | Lemma 1 for prmdvdsfmtnof1 47574. (Contributed by AV, 3-Aug-2021.) |
| ⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
| Theorem | prmdvdsfmtnof1lem2 47572 | Lemma 2 for prmdvdsfmtnof1 47574. (Contributed by AV, 3-Aug-2021.) |
| ⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
| Theorem | prmdvdsfmtnof 47573* | 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 47574* | 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 47575 | The set of prime numbers is infinite. The proof of this variant of prminf 16953 is based on Goldbach's theorem goldbachth 47534 (via prmdvdsfmtnof1 47574 and prmdvdsfmtnof1lem2 47572), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 47572. (Contributed by AV, 4-Aug-2021.) |
| ⊢ ℙ ∉ Fin | ||
| Theorem | 2pwp1prm 47576* | For ((2↑𝑘) + 1) to be prime, 𝑘 must be a power of 2, see Wikipedia "Fermat number", section "Other theorms 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 47577* | Every prime number of the form ((2↑𝑘) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.) |
| ⊢ ((𝐾 ∈ ℕ ∧ 𝑃 = ((2↑𝐾) + 1) ∧ 𝑃 ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝑃 = (FermatNo‘𝑛)) | ||
"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 27271. 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 47588. This is an example of sgprmdvdsmersenne 47591, 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 47591. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 47590, 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 47598. | ||
| Theorem | m2prm 47578 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
| ⊢ ((2↑2) − 1) ∈ ℙ | ||
| Theorem | m3prm 47579 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
| ⊢ ((2↑3) − 1) ∈ ℙ | ||
| Theorem | flsqrt 47580 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
| ⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
| Theorem | flsqrt5 47581 | 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 47582 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
| ⊢ ¬ 3 ∥ 4 | ||
| Theorem | 139prmALT 47583 | 139 is a prime number. In contrast to 139prm 17161, the proof of this theorem uses 3dvds2dec 16370 for checking the divisibility by 3. Although the proof using 3dvds2dec 16370 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17161), the number of essential steps is smaller (301 compared with 327 for 139prm 17161). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ ;;139 ∈ ℙ | ||
| Theorem | 31prm 47584 | 31 is a prime number. In contrast to 37prm 17158, the proof of this theorem is not based on the "blanket" prmlem2 17157, but on isprm7 16745. 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 17158 (1810 characters compared with 1213 for 37prm 17158). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17158). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
| ⊢ ;31 ∈ ℙ | ||
| Theorem | m5prm 47585 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
| ⊢ ((2↑5) − 1) ∈ ℙ | ||
| Theorem | 127prm 47586 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
| ⊢ ;;127 ∈ ℙ | ||
| Theorem | m7prm 47587 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
| ⊢ ((2↑7) − 1) ∈ ℙ | ||
| Theorem | m11nprm 47588 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
| ⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
| Theorem | mod42tp1mod8 47589 | 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 47590 | 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 47591 | 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 47592 | Lemma 1 for lighneal 47598. (Contributed by AV, 11-Aug-2021.) |
| ⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
| Theorem | lighneallem2 47593 | Lemma 2 for lighneal 47598. (Contributed by AV, 13-Aug-2021.) |
| ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
| Theorem | lighneallem3 47594 | Lemma 3 for lighneal 47598. (Contributed by AV, 11-Aug-2021.) |
| ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
| Theorem | lighneallem4a 47595 | Lemma 1 for lighneallem4 47597. (Contributed by AV, 16-Aug-2021.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
| Theorem | lighneallem4b 47596* | Lemma 2 for lighneallem4 47597. (Contributed by AV, 16-Aug-2021.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
| Theorem | lighneallem4 47597 | Lemma 3 for lighneal 47598. (Contributed by AV, 16-Aug-2021.) |
| ⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
| Theorem | lighneal 47598 | If a power of a prime 𝑃 (i.e. 𝑃↑𝑀) is of the form 2↑𝑁 − 1, then 𝑁 must be prime and 𝑀 must be 1. Generalization of mersenne 27271 (where 𝑀 = 1 is a prerequisite). Theorem of S. Ligh and L. Neal (1974) "A note on Mersenne mumbers", Mathematics Magazine, 47:4, 231-233. (Contributed by AV, 16-Aug-2021.) |
| ⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → (𝑀 = 1 ∧ 𝑁 ∈ ℙ)) | ||
| Theorem | modexp2m1d 47599 | The square of an integer which is -1 modulo a number greater than 1 is 1 modulo the same modulus. (Contributed by AV, 5-Jul-2020.) |
| ⊢ (𝜑 → 𝐴 ∈ ℤ) & ⊢ (𝜑 → 𝐸 ∈ ℝ+) & ⊢ (𝜑 → 1 < 𝐸) & ⊢ (𝜑 → (𝐴 mod 𝐸) = (-1 mod 𝐸)) ⇒ ⊢ (𝜑 → ((𝐴↑2) mod 𝐸) = 1) | ||
| Theorem | proththdlem 47600 | Lemma for proththd 47601. (Contributed by AV, 4-Jul-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |