Home | Metamath
Proof Explorer Theorem List (p. 402 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dfodd3 40101 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
Theorem | iseven2 40102 | The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ 2 ∥ 𝑍)) | ||
Theorem | isodd3 40103 | The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ¬ 2 ∥ 𝑍)) | ||
Theorem | 2dvdseven 40104 | 2 divides an even number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍) | ||
Theorem | 2ndvdsodd 40105 | 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍) | ||
Theorem | 2dvdsoddp1 40106 | 2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1)) | ||
Theorem | 2dvdsoddm1 40107 | 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1)) | ||
Theorem | dfeven3 40108 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0} | ||
Theorem | dfodd4 40109 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1} | ||
Theorem | dfodd5 40110 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0} | ||
Theorem | zefldiv2ALTV 40111 | The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ (𝑁 ∈ Even → (⌊‘(𝑁 / 2)) = (𝑁 / 2)) | ||
Theorem | zofldiv2ALTV 40112 | The floor of an odd numer divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ (𝑁 ∈ Odd → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2)) | ||
Theorem | oddflALTV 40113 | Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 18-Jun-2020.) |
⊢ (𝐾 ∈ Odd → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1)) | ||
Theorem | iseven5 40114 | The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) |
⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (2 gcd 𝑍) = 2)) | ||
Theorem | isodd7 40115 | The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.) |
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ (2 gcd 𝑍) = 1)) | ||
Theorem | dfeven5 40116 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2} | ||
Theorem | dfodd7 40117 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1} | ||
Theorem | zneoALTV 40118 | No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Revised by AV, 16-Jun-2020.) |
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → 𝐴 ≠ 𝐵) | ||
Theorem | zeoALTV 40119 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd )) | ||
Theorem | zeo2ALTV 40120 | An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.) (Revised by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ↔ ¬ 𝑍 ∈ Odd )) | ||
Theorem | nneoALTV 40121 | A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )) | ||
Theorem | nneoiALTV 40122 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.) |
⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) | ||
Theorem | odd2np1ALTV 40123* | An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) | ||
Theorem | oddm1evenALTV 40124 | An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ (𝑁 − 1) ∈ Even )) | ||
Theorem | oddp1evenALTV 40125 | An integer is odd iff its successor is even. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (𝑁 ∈ Odd ↔ (𝑁 + 1) ∈ Even )) | ||
Theorem | oexpnegALTV 40126 | The exponential of the negative of a number, when the exponent is odd. (Contributed by Mario Carneiro, 25-Apr-2015.) (Revised by AV, 19-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) | ||
Theorem | oexpnegnz 40127 | The exponential of the negative of a number not being 0, when the exponent is odd. (Contributed by AV, 19-Jun-2020.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁)) | ||
Theorem | bits0ALTV 40128 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd )) | ||
Theorem | bits0eALTV 40129 | The zeroth bit of an even number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ Even → ¬ 0 ∈ (bits‘𝑁)) | ||
Theorem | bits0oALTV 40130 | The zeroth bit of an odd number is zero. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ Odd → 0 ∈ (bits‘𝑁)) | ||
Theorem | divgcdoddALTV 40131 | Either 𝐴 / (𝐴 gcd 𝐵) is odd or 𝐵 / (𝐴 gcd 𝐵) is odd. (Contributed by Scott Fenton, 19-Apr-2014.) (Revised by AV, 21-Jun-2020.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ((𝐴 / (𝐴 gcd 𝐵)) ∈ Odd ∨ (𝐵 / (𝐴 gcd 𝐵)) ∈ Odd )) | ||
Theorem | opoeALTV 40132 | The sum of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) |
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Even ) | ||
Theorem | opeoALTV 40133 | The sum of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) |
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Odd ) | ||
Theorem | omoeALTV 40134 | The difference of two odds is even. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) |
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Even ) | ||
Theorem | omeoALTV 40135 | The difference of an odd and an even is odd. (Contributed by Scott Fenton, 7-Apr-2014.) (Revised by AV, 20-Jun-2020.) |
⊢ ((𝐴 ∈ Odd ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Odd ) | ||
Theorem | oddprmALTV 40136 | A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.) |
⊢ (𝑁 ∈ (ℙ ∖ {2}) → 𝑁 ∈ Odd ) | ||
Theorem | 0evenALTV 40137 | 0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.) |
⊢ 0 ∈ Even | ||
Theorem | 0noddALTV 40138 | 0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.) |
⊢ 0 ∉ Odd | ||
Theorem | 1oddALTV 40139 | 1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ 1 ∈ Odd | ||
Theorem | 1nevenALTV 40140 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ 1 ∉ Even | ||
Theorem | 2evenALTV 40141 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ 2 ∈ Even | ||
Theorem | 2noddALTV 40142 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
⊢ 2 ∉ Odd | ||
Theorem | nn0o1gt2ALTV 40143 | An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Odd ) → (𝑁 = 1 ∨ 2 < 𝑁)) | ||
Theorem | nnoALTV 40144 | An alternate characterization of an odd number greater than 1. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.) |
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ Odd ) → ((𝑁 − 1) / 2) ∈ ℕ) | ||
Theorem | nn0oALTV 40145 | An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Odd ) → ((𝑁 − 1) / 2) ∈ ℕ0) | ||
Theorem | nn0e 40146 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0) | ||
Theorem | nn0onn0exALTV 40147* | For each odd nonnegative integer there is a nonnegative integer which, multiplied by 2 and increased by 1, results in the odd nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Odd ) → ∃𝑚 ∈ ℕ0 𝑁 = ((2 · 𝑚) + 1)) | ||
Theorem | nn0enn0exALTV 40148* | For each even nonnegative integer there is a nonnegative integer which, multiplied by 2, results in the even nonnegative integer. (Contributed by AV, 30-May-2020.) (Revised by AV, 22-Jun-2020.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → ∃𝑚 ∈ ℕ0 𝑁 = (2 · 𝑚)) | ||
Theorem | nnpw2evenALTV 40149 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.) |
⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ Even ) | ||
Theorem | epoo 40150 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) |
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd ) | ||
Theorem | emoo 40151 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) |
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd ) | ||
Theorem | epee 40152 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) |
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even ) | ||
Theorem | emee 40153 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) |
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even ) | ||
Theorem | evensumeven 40154 | If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020.) |
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → (𝐴 ∈ Even ↔ (𝐴 + 𝐵) ∈ Even )) | ||
Theorem | 3odd 40155 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) |
⊢ 3 ∈ Odd | ||
Theorem | 4even 40156 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) |
⊢ 4 ∈ Even | ||
Theorem | 5odd 40157 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) |
⊢ 5 ∈ Odd | ||
Theorem | 6even 40158 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) |
⊢ 6 ∈ Even | ||
Theorem | 7odd 40159 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) |
⊢ 7 ∈ Odd | ||
Theorem | 8even 40160 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) |
⊢ 8 ∈ Even | ||
Theorem | evenprm2 40161 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) |
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2)) | ||
Theorem | oddprmne2 40162 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2})) | ||
Theorem | oddprmuzge3 40163 | A prime number which is odd is an integer greater than or equal to 3. (Contributed by AV, 20-Jul-2020.) (Proof shortened by AV, 21-Aug-2021.) |
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) → 𝑃 ∈ (ℤ≥‘3)) | ||
Theorem | perfectALTVlem1 40164 | Lemma for perfectALTV 40166. (Contributed by Mario Carneiro, 7-Jun-2016.) (Revised by AV, 1-Jul-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Odd ) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → ((2↑(𝐴 + 1)) ∈ ℕ ∧ ((2↑(𝐴 + 1)) − 1) ∈ ℕ ∧ (𝐵 / ((2↑(𝐴 + 1)) − 1)) ∈ ℕ)) | ||
Theorem | perfectALTVlem2 40165 | Lemma for perfectALTV 40166. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Odd ) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | ||
Theorem | perfectALTV 40166* | The Euclid-Euler theorem, or Perfect Number theorem. A positive even integer 𝑁 is a perfect number (that is, its divisor sum is 2𝑁) if and only if it is of the form 2↑(𝑝 − 1) · (2↑𝑝 − 1), where 2↑𝑝 − 1 is prime (a Mersenne prime). (It follows from this that 𝑝 is also prime.) This is Metamath 100 proof #70. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) (Proof modification is discouraged.) |
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → ((1 σ 𝑁) = (2 · 𝑁) ↔ ∃𝑝 ∈ ℤ (((2↑𝑝) − 1) ∈ ℙ ∧ 𝑁 = ((2↑(𝑝 − 1)) · ((2↑𝑝) − 1))))) | ||
According to Wikipedia ("Goldbach's conjecture", 20-Jul-2020, https://en.wikipedia.org/wiki/Goldbach's_conjecture) "Goldbach's conjecture ... states: Every even integer greater than 2 can be expressed as the sum of two primes." "It is also known as strong, even or binary Goldbach conjecture, to distinguish it from a weaker conjecture, known ... as the Goldbach's weak conjecture, the odd Goldbach conjecture, or the ternary Goldbach conjecture. This weak conjecture asserts that all odd numbers greater than 7 are the sum of three odd primes.". In the following, the terms "binary Goldbach conjecture" resp. "ternary Goldbach conjecture" will be used, because there are are a strong and a weak version of the ternary Goldbach conjecture. The term Goldbach partion is used for a sum of two resp. three (odd) primes resulting in an even resp. odd number without further specialization. Using the definition of a Goldbach number, which is "a positive even integer that can be expressed as the sum of two odd primes." (see df-gbe 40170), "another form of the statement of Goldbach's conjecture is that all even integers greater than 4 are Goldbach numbers.". 4 is not a Goldbach number, but it is the sum of two primes (2 and 2) nevertheless. sgoldbalt 40203 shows that both forms are equivalent. Hint (see Wikipedia, ("Goldbach's weak conjecture", 26-Jul-2020, https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture): "Some state the [weak] conjecture as 'Every odd number greater than 7 can be expressed as the sum of three odd primes.' This version excludes 7 = 2+2+3 because this requires the even prime 2. On odd numbers larger than 7 it is slightly stronger as it also excludes sums like 17 = 2+2+13, which are allowed in the other formulation. Helfgott's proof [see below] covers both versions of the conjecture. Like the other formulation, this one also immediately follows from Goldbach's strong conjecture." Our definition of "odd Goldbach Numbers", see df-gbo 40171, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternatively, df-gboa 40172 provides a definition allowing for stating the strong ternaty Goldbach conjecture. In contrast to the two versions of the binary Goldbach conjecture, the two versions of the ternary Goldbach conjecture are different not only for small numbers, but the strong version excludes cases like a=2+2+b in general, e.g. 23=2+2+19. Therefore, it seems to be more difficult to prove the strong ternary Goldbach conjecture than the weak version, because there are fewer possible partitions available. Although the binary Goldbach conjecture is not proven yet, the ternary Goldbach conjecture seems to be proven by Harald Helfgott in 2014 (the weak as well as the strong version, see Main theorem in [Helfgott] p. 2. It would be great if this proof can be formalized with Metamath (although it is not in the Metamath 100 list), providing the still missing official acceptance (usually obtained by a publication in a peer-reviewed journal). This section should be a starting point for this. The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the strong Goldbach conjecture (see result of [OeSilva] p. ?) resp. about 9 x 10^30 for the weak Goldbach conjecture (see section 1.2.2 in [Helfgott] p. 4). Maybe each of the results must be provided as theorem, like 6gbe 40193, which would be quite a lot... As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w/m/O3oBPuzhBAAJ , this problem could be solved by using a reflective verifier or adding a concept of verification certificates that can be added into the metamath databases as a reference. To sidestep the computation problem for now, the corresponding theorems are temporarily provided as axioms, see ax-bgbltosilva 40226, ax-hgprmladder 40228 and ax-tgoldbachgt 40231. | ||
Syntax | cgbe 40167 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. |
class GoldbachEven | ||
Syntax | cgbo 40168 | Extend the definition of a class to include the set of odd numbers which can be written as sum of three primes. |
class GoldbachOdd | ||
Syntax | cgboa 40169 | Extend the definition of a class to include the set of odd numbers which can be written as sum of three odd primes. |
class GoldbachOddALTV | ||
Definition | df-gbe 40170* | Define the set of (even) Goldbach numbers, which are positive even integers that can be expressed as the sum of two odd primes. By this definition, the binary Goldbach conjecture can be expressed as ∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ). (Contributed by AV, 14-Jun-2020.) |
⊢ GoldbachEven = {𝑧 ∈ Even ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑧 = (𝑝 + 𝑞))} | ||
Definition | df-gbo 40171* | Define the set of odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three primes. By this definition, the (weak) ternary Goldbach conjecture can be expressed as ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd ). (Contributed by AV, 14-Jun-2020.) |
⊢ GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)} | ||
Definition | df-gboa 40172* | Define the set of odd Goldbach numbers, which are positive odd integers that can be expressed as the sum of three odd primes. By this definition, the strong ternary Goldbach conjecture can be expressed as ∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV ). (Contributed by AV, 26-Jul-2020.) |
⊢ GoldbachOddALTV = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} | ||
Theorem | isgbe 40173* | The predicate "is an even Goldbach number". An even Goldbach number is an even number having a Goldbach partition, i.e. which can be written as sum of two odd primes. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachEven ↔ (𝑍 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)))) | ||
Theorem | isgbo 40174* | The predicate "is an odd Goldbach number". An odd Goldbach number is an odd number integer having a Goldbach partition, i.e. which which can be written as sum of three primes. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOdd ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟))) | ||
Theorem | isgboa 40175* | The predicate "is an odd Goldbach number". An odd Goldbach number is an odd number integer having a Goldbach partition, i.e. which can be written as sum of three odd primes. (Contributed by AV, 26-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOddALTV ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))) | ||
Theorem | gbeeven 40176 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even ) | ||
Theorem | gboodd 40177 | An odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd ) | ||
Theorem | gboagbo 40178 | An odd Goldbach number (strong version) is an odd Goldbach number (weak version). (Contributed by AV, 26-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOddALTV → 𝑍 ∈ GoldbachOdd ) | ||
Theorem | gboaodd 40179 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOddALTV → 𝑍 ∈ Odd ) | ||
Theorem | gbepos 40180 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ) | ||
Theorem | gbopos 40181 | Any odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ) | ||
Theorem | gboapos 40182 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOddALTV → 𝑍 ∈ ℕ) | ||
Theorem | gbegt5 40183 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍) | ||
Theorem | gbogt5 40184 | Any odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOdd → 5 < 𝑍) | ||
Theorem | gboge7 40185 | Any odd Goldbach number is greater than or equal to 7. Because of 7gbo 40194, this bound is strict. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOdd → 7 ≤ 𝑍) | ||
Theorem | gboage9 40186 | Any odd Goldbach number (strong version) is greater than or equal to 9. Because of 9gboa 40196, this bound is strict. (Contributed by AV, 26-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachOddALTV → 9 ≤ 𝑍) | ||
Theorem | gbege6 40187 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 40193, this bound is strict. (Contributed by AV, 20-Jul-2020.) |
⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍) | ||
Theorem | gbpart6 40188 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) |
⊢ 6 = (3 + 3) | ||
Theorem | gbpart7 40189 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) |
⊢ 7 = ((2 + 2) + 3) | ||
Theorem | gbpart8 40190 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) |
⊢ 8 = (3 + 5) | ||
Theorem | gbpart9 40191 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) |
⊢ 9 = ((3 + 3) + 3) | ||
Theorem | gbpart11 40192 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) |
⊢ ;11 = ((3 + 3) + 5) | ||
Theorem | 6gbe 40193 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) |
⊢ 6 ∈ GoldbachEven | ||
Theorem | 7gbo 40194 | 7 is an odd Goldbach number. (Contributed by AV, 20-Jul-2020.) |
⊢ 7 ∈ GoldbachOdd | ||
Theorem | 8gbe 40195 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) |
⊢ 8 ∈ GoldbachEven | ||
Theorem | 9gboa 40196 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) |
⊢ 9 ∈ GoldbachOddALTV | ||
Theorem | 11gboa 40197 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) |
⊢ ;11 ∈ GoldbachOddALTV | ||
Theorem | stgoldbwt 40198 | If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.) |
⊢ (∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOddALTV ) → ∀𝑛 ∈ Odd (5 < 𝑛 → 𝑛 ∈ GoldbachOdd )) | ||
Theorem | bgoldbwt 40199* | If the binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.) |
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOdd )) | ||
Theorem | bgoldbst 40200* | If the binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.) |
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOddALTV )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |