![]() |
Metamath
Proof Explorer Theorem List (p. 420 of 429) | < 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-27903) |
![]() (27904-29428) |
![]() (29429-42879) |
Type | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iseven5 41901 | 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 41902 | 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 41903 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfodd7 41904 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zneoALTV 41905 | 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 41906 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | zeo2ALTV 41907 | 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 41908 | 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 41909 | 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 41910* | 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 41911 | 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 41912 | 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 41913 | 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 41914 | 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 41915 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | bits0eALTV 41916 | 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 41917 | 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 41918 | 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 41919 | 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 41920 | 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 41921 | 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 41922 | 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 41923 | 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 41924 | 0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 0 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0noddALTV 41925 | 0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 0 ∉ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1oddALTV 41926 | 1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 1 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1nevenALTV 41927 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 1 ∉ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2evenALTV 41928 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 2 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2noddALTV 41929 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 2 ∉ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0o1gt2ALTV 41930 | 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 41931 | 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 41932 | 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 41933 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0onn0exALTV 41934* | 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 41935* | 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 41936 | 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 41937 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emoo 41938 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epee 41939 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emee 41940 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evensumeven 41941 | 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 41942 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 3 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4even 41943 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 4 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 5odd 41944 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 5 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6even 41945 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7odd 41946 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8even 41947 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenprm2 41948 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmne2 41949 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2})) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmuzge3 41950 | 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 | evenltle 41951 | If an even number is greater than another even number, then it is greater than or equal to the other even number plus 2. (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ Even ∧ 𝑀 ∈ Even ∧ 𝑀 < 𝑁) → (𝑀 + 2) ≤ 𝑁) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | odd2prm2 41952 | If an odd number is the sum of two prime numbers, one of the prime numbers must be 2. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ Odd ∧ (𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) ∧ 𝑁 = (𝑃 + 𝑄)) → (𝑃 = 2 ∨ 𝑄 = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | even3prm2 41953 | If an even number is the sum of three prime numbers, one of the prime numbers must be 2. (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ Even ∧ (𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 = ((𝑃 + 𝑄) + 𝑅)) → (𝑃 = 2 ∨ 𝑄 = 2 ∨ 𝑅 = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mogoldbblem 41954* | Lemma for mogoldbb 41998. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem1 41955 | Lemma for perfectALTV 41957. (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 41956 | Lemma for perfectALTV 41957. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Odd ) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTV 41957* | 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 (following the terminology used in [Helfgott] p. 2), because there
are a strong and a weak version of the ternary Goldbach conjecture. The term
_Goldbach partition_ is used for a sum of two resp. three (odd) primes
resulting in an even resp. odd number without further specialization.
Summary/glossary:
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbe 41958 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbow 41959 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbo 41960 | Extend the definition of a class to include the set of odd numbers which can be written as a sum of three odd primes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbe 41961* | 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-gbow 41962* | Define the set of weak 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 < 𝑚 → 𝑚 ∈ GoldbachOddW ). (Contributed by AV, 14-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ GoldbachOddW = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑧 = ((𝑝 + 𝑞) + 𝑟)} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-gbo 41963* | Define the set of (strong) 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 < 𝑚 → 𝑚 ∈ GoldbachOdd ). (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ GoldbachOdd = {𝑧 ∈ Odd ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbe 41964* | The predicate "is an even Goldbach number". An even Goldbach number is an even integer having a Goldbach partition, i.e. which can be written as a sum of two odd primes. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven ↔ (𝑍 ∈ Even ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ (𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑍 = (𝑝 + 𝑞)))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbow 41965* | The predicate "is a weak odd Goldbach number". A weak odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as a sum of three primes. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑍 = ((𝑝 + 𝑞) + 𝑟))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isgbo 41966* | The predicate "is an odd Goldbach number". An odd Goldbach number is an odd integer having a Goldbach partition, i.e. which can be written as sum of three odd primes. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd ↔ (𝑍 ∈ Odd ∧ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑍 = ((𝑝 + 𝑞) + 𝑟)))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbeeven 41967 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowodd 41968 | A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbogbow 41969 | A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboodd 41970 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbepos 41971 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowpos 41972 | Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbopos 41973 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbegt5 41974 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowgt5 41975 | Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowge7 41976 | Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 41985, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboge9 41977 | Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 41987, this bound is strict. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbege6 41978 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 41984, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart6 41979 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 = (3 + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart7 41980 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 = ((2 + 2) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart8 41981 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 = (3 + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart9 41982 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 9 = ((3 + 3) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart11 41983 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ;11 = ((3 + 3) + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6gbe 41984 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7gbow 41985 | 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 ∈ GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8gbe 41986 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9gbo 41987 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 9 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 11gbo 41988 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ;11 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | stgoldbwt 41989 | If the strong ternary Goldbach conjecture is valid, then the weak ternary Goldbach conjecture holds, too. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Odd (7 < 𝑛 → 𝑛 ∈ GoldbachOdd ) → ∀𝑛 ∈ Odd (5 < 𝑛 → 𝑛 ∈ GoldbachOddW )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbwt 41990* | If the strong binary Goldbach conjecture is valid, then the (weak) ternary Goldbach conjecture holds, too. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbst 41991* | If the strong binary Goldbach conjecture is valid, then the (strong) ternary Goldbach conjecture holds, too. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbaltlem1 41992 | Lemma 1 for sbgoldbalt 41994: If an even number greater than 4 is the sum of two primes, one of the prime summands must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → 𝑄 ∈ Odd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbaltlem2 41993 | Lemma 2 for sbgoldbalt 41994: If an even number greater than 4 is the sum of two primes, the primes must be odd, i.e. not 2. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ) → ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 = (𝑃 + 𝑄)) → (𝑃 ∈ Odd ∧ 𝑄 ∈ Odd ))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbalt 41994* | An alternate (related to the original) formulation of the binary Goldbach conjecture: Every even integer greater than 2 can be expressed as the sum of two primes. (Contributed by AV, 22-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbb 41995* | If the strong binary Goldbach conjecture is valid, the binary Goldbach conjecture is valid. (Contributed by AV, 23-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sgoldbeven3prm 41996* | If the binary Goldbach conjecture is valid, then an even integer greater than 5 can be expressed as the sum of three primes: Since (𝑁 − 2) is even iff 𝑁 is even, there would be primes 𝑝 and 𝑞 with (𝑁 − 2) = (𝑝 + 𝑞), and therefore 𝑁 = ((𝑝 + 𝑞) + 2). (Contributed by AV, 24-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ((𝑁 ∈ Even ∧ 6 ≤ 𝑁) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑁 = ((𝑝 + 𝑞) + 𝑟))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbm 41997* | If the strong binary Goldbach conjecture is valid, the modern version of the original formulation of the Goldbach conjecture also holds: Every integer greater than 5 can be expressed as the sum of three primes. (Contributed by AV, 24-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mogoldbb 41998* | If the modern version of the original formulation of the Goldbach conjecture is valid, the (weak) binary Goldbach conjecture also holds. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ (ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟) → ∀𝑛 ∈ Even (2 < 𝑛 → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑛 = (𝑝 + 𝑞))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbmb 41999* | The strong binary Goldbach conjecture and the modern version of the original formulation of the Goldbach conjecture are equivalent. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) ↔ ∀𝑛 ∈ (ℤ≥‘6)∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ 𝑛 = ((𝑝 + 𝑞) + 𝑟)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | sbgoldbo 42000* | If the strong binary Goldbach conjecture is valid, the original formulation of the Goldbach conjecture also holds: Every integer greater than 2 can be expressed as the sum of three "primes" with regarding 1 to be a prime (as Goldbach did). Original text: "Es scheint wenigstens, dass eine jede Zahl, die groesser ist als 2, ein aggregatum trium numerorum primorum sey." (Goldbach, 1742). (Contributed by AV, 25-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = ({1} ∪ ℙ) ⇒ ⊢ (∀𝑛 ∈ Even (4 < 𝑛 → 𝑛 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ≥‘3)∃𝑝 ∈ 𝑃 ∃𝑞 ∈ 𝑃 ∃𝑟 ∈ 𝑃 𝑛 = ((𝑝 + 𝑞) + 𝑟)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |