Home | Metamath
Proof Explorer Theorem List (p. 438 of 450) | < 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: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sprsymrelfvlem 43701* | Lemma for sprsymrelf 43706 and sprsymrelfv 43705. (Contributed by AV, 19-Nov-2021.) |
⊢ (𝑃 ⊆ (Pairs‘𝑉) → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑃 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉)) | ||
Theorem | sprsymrelf1lem 43702* | Lemma for sprsymrelf1 43707. (Contributed by AV, 22-Nov-2021.) |
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏)) | ||
Theorem | sprsymrelfolem1 43703* | Lemma 1 for sprsymrelfo 43708. (Contributed by AV, 22-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ 𝑄 ∈ 𝒫 (Pairs‘𝑉) | ||
Theorem | sprsymrelfolem2 43704* | Lemma 2 for sprsymrelfo 43708. (Contributed by AV, 23-Nov-2021.) |
⊢ 𝑄 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑅𝑏)} ⇒ ⊢ ((𝑉 ∈ 𝑊 ∧ 𝑅 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑅𝑦 ↔ 𝑦𝑅𝑥)) → (𝑥𝑅𝑦 ↔ ∃𝑐 ∈ 𝑄 𝑐 = {𝑥, 𝑦})) | ||
Theorem | sprsymrelfv 43705* | 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 43706* | 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 43707* | 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 43708* | 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 43709* | 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 43710* | 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 43711* | 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‘𝑉) & ⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} ⇒ ⊢ (𝑉 ∈ 𝑊 → 𝑃 ≈ 𝑅) | ||
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 11846). Examples for not proper unordered pairs are {1, 1} = {1} (see preqsn 4792), {1, V} = {1} (see prprc2 4702) or {V, V} = ∅ (see prprc 4703). | ||
Theorem | prpair 43712* | 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 43713 | Lemma 0 for prproropf1o 43718. 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 43714* | Lemma 1 for prproropf1o 43718. (Contributed by AV, 12-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → {(1st ‘𝑊), (2nd ‘𝑊)} ∈ 𝑃) | ||
Theorem | prproropf1olem2 43715* | Lemma 2 for prproropf1o 43718. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑋 ∈ 𝑃) → 〈inf(𝑋, 𝑉, 𝑅), sup(𝑋, 𝑉, 𝑅)〉 ∈ 𝑂) | ||
Theorem | prproropf1olem3 43716* | Lemma 3 for prproropf1o 43718. (Contributed by AV, 13-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑂) → (𝐹‘{(1st ‘𝑊), (2nd ‘𝑊)}) = 〈(1st ‘𝑊), (2nd ‘𝑊)〉) | ||
Theorem | prproropf1olem4 43717* | Lemma 4 for prproropf1o 43718. (Contributed by AV, 14-Mar-2023.) |
⊢ 𝑂 = (𝑅 ∩ (𝑉 × 𝑉)) & ⊢ 𝑃 = {𝑝 ∈ 𝒫 𝑉 ∣ (♯‘𝑝) = 2} & ⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ 〈inf(𝑝, 𝑉, 𝑅), sup(𝑝, 𝑉, 𝑅)〉) ⇒ ⊢ ((𝑅 Or 𝑉 ∧ 𝑊 ∈ 𝑃 ∧ 𝑍 ∈ 𝑃) → ((𝐹‘𝑍) = (𝐹‘𝑊) → 𝑍 = 𝑊)) | ||
Theorem | prproropf1o 43718* | 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 43719* | 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 43720* | 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 43721* | Two equivalent representations of the existence of a unique proper pair. (Contributed by AV, 1-Mar-2023.) |
⊢ 𝑃 = {𝑥 ∈ 𝒫 𝑉 ∣ (♯‘𝑥) = 2} ⇒ ⊢ (∃!𝑝 ∈ 𝑃 𝜑 ↔ ∃!𝑝 ∈ 𝒫 𝑉((♯‘𝑝) = 2 ∧ 𝜑)) | ||
Theorem | paireqne 43722* | 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} ⇒ ⊢ (𝜑 → (∃!𝑝 ∈ 𝑃 ∀𝑥 ∈ 𝑝 (𝑥 = 𝐴 ∨ 𝑥 = 𝐵) ↔ 𝐴 ≠ 𝐵)) | ||
Syntax | cprpr 43723 | Extend class notation with set of proper unordered pairs. |
class Pairsproper | ||
Definition | df-prpr 43724* | 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 43725* | The set of all proper unordered pairs over a given set 𝑉. (Contributed by AV, 29-Apr-2023.) |
⊢ (𝑉 ∈ 𝑊 → (Pairsproper‘𝑉) = {𝑝 ∣ ∃𝑎 ∈ 𝑉 ∃𝑏 ∈ 𝑉 (𝑎 ≠ 𝑏 ∧ 𝑝 = {𝑎, 𝑏})}) | ||
Theorem | prprvalpw 43726* | 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 43727 | 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 43728* | 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 43729* | 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 43730* | 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 43731* | 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 43732* | 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 43733* | 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 43734* | 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 43735 | Equality for unordered pairs with partially ordered elements. (Contributed by AV, 9-Jul-2023.) |
⊢ (((Rel 𝑅 ∧ 𝑅 Po 𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐴𝑅𝐵 ∧ 𝐶𝑅𝐷)) → ({𝐴, 𝐵} = {𝐶, 𝐷} ↔ (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | 2exopprim 43736 | 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 43737* | 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 43739, and basic theorems are provided. Afterwards, it is shown that the first five Fermat numbers are prime, the (first) five Fermat primes, see fmtnofz04prm 43788, but that the fifth Fermat number (counting starts at 0!) is not prime, see fmtno5nprm 43794. 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 43787 (previously, it was ;;;4001, see 4001prm 16478). Another important result of this section is Goldbach's theorem goldbachth 43758, showing that two different Fermut numbers are coprime. By this, it can be proven that there is an infinite number of primes, see prminf2 43799. Finally, it is shown that every prime of the form ((2↑𝑘) + 1) must be a Fermat number (i.e., a Fermat prime), see 2pwp1prmfmtno 43801. | ||
Syntax | cfmtno 43738 | Extend class notation with the Fermat numbers. |
class FermatNo | ||
Definition | df-fmtno 43739 | 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 43740 | The 𝑁 th Fermat number. (Contributed by AV, 13-Jun-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) = ((2↑(2↑𝑁)) + 1)) | ||
Theorem | fmtnoge3 43741 | Each Fermat number is greater than or equal to 3. (Contributed by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ (ℤ≥‘3)) | ||
Theorem | fmtnonn 43742 | Each Fermat number is a positive integer. (Contributed by AV, 26-Jul-2021.) (Proof shortened by AV, 4-Aug-2021.) |
⊢ (𝑁 ∈ ℕ0 → (FermatNo‘𝑁) ∈ ℕ) | ||
Theorem | fmtnom1nn 43743 | 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 43744 | Each Fermat number is odd. (Contributed by AV, 26-Jul-2021.) |
⊢ (𝑁 ∈ ℕ0 → ¬ 2 ∥ (FermatNo‘𝑁)) | ||
Theorem | fmtnorn 43745* | 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 43746 | 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 43747 | The set of Fermat numbers is infinite. (Contributed by AV, 3-Aug-2021.) |
⊢ ran FermatNo ∉ Fin | ||
Theorem | fmtnorec1 43748 | 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 43749 | 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 43750 | The floor of the square root of a Fermat number. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ ℕ → (⌊‘(√‘(FermatNo‘𝑁))) = (2↑(2↑(𝑁 − 1)))) | ||
Theorem | fmtno0 43751 | The 0 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) = 3 | ||
Theorem | fmtno1 43752 | The 1 st Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) = 5 | ||
Theorem | fmtnorec2lem 43753* | Lemma for fmtnorec2 43754 (induction step). (Contributed by AV, 29-Jul-2021.) |
⊢ (𝑦 ∈ ℕ0 → ((FermatNo‘(𝑦 + 1)) = (∏𝑛 ∈ (0...𝑦)(FermatNo‘𝑛) + 2) → (FermatNo‘((𝑦 + 1) + 1)) = (∏𝑛 ∈ (0...(𝑦 + 1))(FermatNo‘𝑛) + 2))) | ||
Theorem | fmtnorec2 43754* | 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 43755 | Any Fermat number divides a greater Fermat number minus 2. Corrolary of fmtnorec2 43754, 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 43756 | Lemma 1 for goldbachth 43758. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → (FermatNo‘𝑀) ∥ ((FermatNo‘𝑁) − 2)) | ||
Theorem | goldbachthlem2 43757 | Lemma 2 for goldbachth 43758. (Contributed by AV, 1-Aug-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ∧ 𝑀 < 𝑁) → ((FermatNo‘𝑁) gcd (FermatNo‘𝑀)) = 1) | ||
Theorem | goldbachth 43758 | 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 43759* | 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 43760 | 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 43761 | The 2 nd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘2) = ;17 | ||
Theorem | fmtno3 43762 | The 3 rd Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘3) = ;;257 | ||
Theorem | fmtno4 43763 | The 4 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘4) = ;;;;65537 | ||
Theorem | fmtno5lem1 43764 | Lemma 1 for fmtno5 43768. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 6) = ;;;;;393216 | ||
Theorem | fmtno5lem2 43765 | Lemma 2 for fmtno5 43768. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 5) = ;;;;;327680 | ||
Theorem | fmtno5lem3 43766 | Lemma 3 for fmtno5 43768. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;65536 · 3) = ;;;;;196608 | ||
Theorem | fmtno5lem4 43767 | Lemma 4 for fmtno5 43768. (Contributed by AV, 30-Jul-2021.) |
⊢ (;;;;65536↑2) = ;;;;;;;;;4294967296 | ||
Theorem | fmtno5 43768 | The 5 th Fermat number. (Contributed by AV, 30-Jul-2021.) |
⊢ (FermatNo‘5) = ;;;;;;;;;4294967297 | ||
Theorem | fmtno0prm 43769 | The 0 th Fermat number is a prime (first Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘0) ∈ ℙ | ||
Theorem | fmtno1prm 43770 | The 1 st Fermat number is a prime (second Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘1) ∈ ℙ | ||
Theorem | fmtno2prm 43771 | The 2 nd Fermat number is a prime (third Fermat prime). (Contributed by AV, 13-Jun-2021.) |
⊢ (FermatNo‘2) ∈ ℙ | ||
Theorem | 257prm 43772 | 257 is a prime number (the fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ ;;257 ∈ ℙ | ||
Theorem | fmtno3prm 43773 | The 3 rd Fermat number is a prime (fourth Fermat prime). (Contributed by AV, 15-Jun-2021.) |
⊢ (FermatNo‘3) ∈ ℙ | ||
Theorem | odz2prm2pw 43774 | 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 43775 | Lemma for fmtnoprmfac1 43776: 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 43776* | Divisor of Fermat number (special form of Euler's result, see fmtnofac1 43781): 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 43777 | Lemma for fmtnoprmfac2 43778. (Contributed by AV, 26-Jul-2021.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑃 ∥ (FermatNo‘𝑁)) → ((2↑((𝑃 − 1) / 2)) mod 𝑃) = 1) | ||
Theorem | fmtnoprmfac2 43778* | Divisor of Fermat number (special form of Lucas' result, see fmtnofac2 43780): 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 43779* | Lemma for fmtnofac2 43780 (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 43780* | Divisor of Fermat number (Euler's Result refined by François Édouard Anatole Lucas), see fmtnofac1 43781: 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 43781* |
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 43780. (Contributed by AV, 30-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ∧ 𝑀 ∥ (FermatNo‘𝑁)) → ∃𝑘 ∈ ℕ0 𝑀 = ((𝑘 · (2↑(𝑁 + 1))) + 1)) | ||
Theorem | fmtno4sqrt 43782 | The floor of the square root of the fourth Fermat number is 256. (Contributed by AV, 28-Jul-2021.) |
⊢ (⌊‘(√‘(FermatNo‘4))) = ;;256 | ||
Theorem | fmtno4prmfac 43783 | 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 43784 | 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 43785 | 193 is not a (prime) factor of the fourth Fermat number. (Contributed by AV, 24-Jul-2021.) |
⊢ ¬ ;;193 ∥ (FermatNo‘4) | ||
Theorem | fmtno4prm 43786 | The 4-th Fermat number (65537) is a prime (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ (FermatNo‘4) ∈ ℙ | ||
Theorem | 65537prm 43787 | 65537 is a prime number (the fifth Fermat prime). (Contributed by AV, 28-Jul-2021.) |
⊢ ;;;;65537 ∈ ℙ | ||
Theorem | fmtnofz04prm 43788 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtnole4prm 43789 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtno5faclem1 43790 | Lemma 1 for fmtno5fac 43793. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 43791 | Lemma 2 for fmtno5fac 43793. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 43792 | Lemma 3 for fmtno5fac 43793. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 43793 | The factorisation of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) = (;;;;;;6700417 · ;;641) | ||
Theorem | fmtno5nprm 43794 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) ∉ ℙ | ||
Theorem | prmdvdsfmtnof1lem1 43795* | Lemma 1 for prmdvdsfmtnof1 43798. (Contributed by AV, 3-Aug-2021.) |
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
Theorem | prmdvdsfmtnof1lem2 43796 | Lemma 2 for prmdvdsfmtnof1 43798. (Contributed by AV, 3-Aug-2021.) |
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
Theorem | prmdvdsfmtnof 43797* | 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 43798* | 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 43799 | The set of prime numbers is infinite. The proof of this variant of prminf 16251 is based on Goldbach's theorem goldbachth 43758 (via prmdvdsfmtnof1 43798 and prmdvdsfmtnof1lem2 43796), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 43796. (Contributed by AV, 4-Aug-2021.) |
⊢ ℙ ∉ Fin | ||
Theorem | 2pwp1prm 43800* | For every prime number of the form ((2↑𝑘) + 1) 𝑘 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↑𝑛)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |