| Metamath
Proof Explorer Theorem List (p. 478 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 | evenprm2 47701 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | oddprmne2 47702 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2})) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | oddprmuzge3 47703 | 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 47704 | 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 47705 | 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 47706 | 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 47707* | Lemma for mogoldbb 47772. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | perfectALTVlem1 47708 | Lemma for perfectALTV 47710. (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 47709 | Lemma for perfectALTV 47710. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Odd ) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | perfectALTV 47710* | 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))))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
"In number theory, the Fermat pseudoprimes make up the most important class of pseudoprimes that come from Fermat's little theorem ... [which] states that if p is prime and a is coprime to p, then a^(p-1)-1 is divisible by p [see fermltl 16821]. For an integer a > 1, if a composite integer x divides a^(x-1)-1, then x is called a Fermat pseudoprime to base a. In other words, a composite integer is a Fermat pseudoprime to base a if it successfully passes the Fermat primality test for the base a. The false statement [see nfermltl2rev 47730] that all numbers that pass the Fermat primality test for base 2, are prime, is called the Chinese hypothesis.", see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime 47730, 29-May-2023. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Syntax | cfppr 47711 | Extend class notation with the Fermat pseudoprimes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| class FPPr | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Definition | df-fppr 47712* | Define the function that maps a positive integer to the set of Fermat pseudoprimes to the base of this positive integer. Since Fermat pseudoprimes shall be composite (positive) integers, they must be nonprime integers greater than or equal to 4 (we cannot use 𝑥 ∈ ℕ ∧ 𝑥 ∉ ℙ because 𝑥 = 1 would fulfil this requirement, but should not be regarded as "composite" integer). (Contributed by AV, 29-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ FPPr = (𝑛 ∈ ℕ ↦ {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑛↑(𝑥 − 1)) − 1))}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fppr 47713* | The set of Fermat pseudoprimes to the base 𝑁. (Contributed by AV, 29-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑁↑(𝑥 − 1)) − 1))}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprmod 47714* | The set of Fermat pseudoprimes to the base 𝑁, expressed by a modulo operation instead of the divisibility relation. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ ((𝑁↑(𝑥 − 1)) mod 𝑥) = 1)}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprel 47715 | A Fermat pseudoprime to the base 𝑁. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ( FPPr ‘𝑁) ↔ (𝑋 ∈ (ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((𝑁↑(𝑋 − 1)) mod 𝑋) = 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprbasnn 47716 | The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑁 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprnn 47717 | A Fermat pseudoprime to the base 𝑁 is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑋 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fppr2odd 47718 | A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑋 ∈ ( FPPr ‘2) → 𝑋 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 11t31e341 47719 | 341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (;11 · ;31) = ;;341 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 2exp340mod341 47720 | Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((2↑;;340) mod ;;341) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 341fppr2 47721 | 341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ;;341 ∈ ( FPPr ‘2) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 4fppr1 47722 | 4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 4 ∈ ( FPPr ‘1) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 8exp8mod9 47723 | Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((8↑8) mod 9) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 9fppr8 47724 | 9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 9 ∈ ( FPPr ‘8) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | dfwppr 47725 | Alternate definition of a weak pseudoprime 𝑋, which fulfils (𝑁↑𝑋)≡𝑁 (modulo 𝑋), see Wikipedia "Fermat pseudoprime", https://en.wikipedia.org/wiki/Fermat_pseudoprime, 29-May-2023. (Contributed by AV, 31-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ ℕ) → (((𝑁↑𝑋) mod 𝑋) = (𝑁 mod 𝑋) ↔ 𝑋 ∥ ((𝑁↑𝑋) − 𝑁))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprwppr 47726 | A Fermat pseudoprime to the base 𝑁 is a weak pseudoprime (see Wikipedia "Fermat pseudoprime", 29-May-2023, https://en.wikipedia.org/wiki/Fermat_pseudoprime. (Contributed by AV, 31-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑋 ∈ ( FPPr ‘𝑁) → ((𝑁↑𝑋) mod 𝑋) = (𝑁 mod 𝑋)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprwpprb 47727 | An integer 𝑋 which is coprime with an integer 𝑁 is a Fermat pseudoprime to the base 𝑁 iff it is a weak pseudoprime to the base 𝑁. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑋 gcd 𝑁) = 1 → (𝑋 ∈ ( FPPr ‘𝑁) ↔ ((𝑋 ∈ (ℤ≥‘4) ∧ 𝑋 ∉ ℙ) ∧ (𝑁 ∈ ℕ ∧ ((𝑁↑𝑋) mod 𝑋) = (𝑁 mod 𝑋))))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | fpprel2 47728 | An alternate definition for a Fermat pseudoprime to the base 2. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑋 ∈ ( FPPr ‘2) ↔ ((𝑋 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ Odd ∧ 𝑋 ∉ ℙ) ∧ ((2↑𝑋) mod 𝑋) = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nfermltl8rev 47729 | Fermat's little theorem with base 8 reversed is not generally true: There is an integer 𝑝 (for example 9, see 9fppr8 47724) so that "𝑝 is prime" does not follow from 8↑𝑝≡8 (mod 𝑝). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑝 ∈ (ℤ≥‘3) ¬ (((8↑𝑝) mod 𝑝) = (8 mod 𝑝) → 𝑝 ∈ ℙ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nfermltl2rev 47730 | Fermat's little theorem with base 2 reversed is not generally true: There is an integer 𝑝 (for example 341, see 341fppr2 47721) so that "𝑝 is prime" does not follow from 2↑𝑝≡2 (mod 𝑝). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑝 ∈ (ℤ≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nfermltlrev 47731* | Fermat's little theorem reversed is not generally true: There are integers 𝑎 and 𝑝 so that "𝑝 is prime" does not follow from 𝑎↑𝑝≡𝑎 (mod 𝑝). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑎 ∈ ℤ ∃𝑝 ∈ (ℤ≥‘3) ¬ (((𝑎↑𝑝) mod 𝑝) = (𝑎 mod 𝑝) → 𝑝 ∈ ℙ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
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 47732 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| class GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Syntax | cgbow 47733 | 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 47734 | 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 47735* | 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 47736* | 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 47737* | 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 47738* | 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 47739* | 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 47740* | 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 47741 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbowodd 47742 | A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbogbow 47743 | A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gboodd 47744 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbepos 47745 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbowpos 47746 | Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbopos 47747 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbegt5 47748 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbowgt5 47749 | Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbowge7 47750 | Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 47759, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gboge9 47751 | Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 47761, this bound is strict. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbege6 47752 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 47758, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbpart6 47753 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 6 = (3 + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbpart7 47754 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 7 = ((2 + 2) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbpart8 47755 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 8 = (3 + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbpart9 47756 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 9 = ((3 + 3) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | gbpart11 47757 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ;11 = ((3 + 3) + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 6gbe 47758 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 6 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 7gbow 47759 | 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 7 ∈ GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 8gbe 47760 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 8 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 9gbo 47761 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 9 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | 11gbo 47762 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ;11 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | stgoldbwt 47763 | 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 47764* | 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 47765* | 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 47766 | Lemma 1 for sbgoldbalt 47768: 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 47767 | Lemma 2 for sbgoldbalt 47768: 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 47768* | 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 47769* | 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 47770* | 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 47771* | 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 47772* | 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 47773* | 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 47774* | 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)∃𝑝 ∈ 𝑃 ∃𝑞 ∈ 𝑃 ∃𝑟 ∈ 𝑃 𝑛 = ((𝑝 + 𝑞) + 𝑟)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum3primes4 47775* | 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primes4 47776* | 4 is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum3primesprm 47777* | Every prime is "the sum of at most 3" (actually one - the prime itself) primes. (Contributed by AV, 2-Aug-2020.) (Proof shortened by AV, 17-Apr-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesprm 47778* | Every prime is "the sum of at most 4" (actually one - the prime itself) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑃 ∈ ℙ → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑃 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum3primesgbe 47779* | Any even Goldbach number is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑁 ∈ GoldbachEven → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesgbe 47780* | Any even Goldbach number is the sum of at most 4 (actually 2) primes. (Contributed by AV, 23-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝑁 ∈ GoldbachEven → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum3primesle9 47781* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 3 primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesle9 47782* | Every integer greater than 1 and less than or equal to 8 is the sum of at most 4 primes. (Contributed by AV, 24-Jul-2020.) (Proof shortened by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ≤ 8) → ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑁 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesodd 47783* | If the (weak) ternary Goldbach conjecture is valid, then every odd integer greater than 5 is the sum of 3 primes. (Contributed by AV, 2-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesoddALTV 47784* | If the (strong) ternary Goldbach conjecture is valid, then every odd integer greater than 7 is the sum of 3 primes. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘8) ∧ 𝑁 ∈ Odd ) → ∃𝑓 ∈ (ℙ ↑m (1...3))𝑁 = Σ𝑘 ∈ (1...3)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | evengpop3 47785* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of an odd Goldbach number and 3. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOddW 𝑁 = (𝑜 + 3))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | evengpoap3 47786* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of an odd Goldbach number and 3. (Contributed by AV, 27-Jul-2020.) (Proof shortened by AV, 15-Sep-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑜 ∈ GoldbachOdd 𝑁 = (𝑜 + 3))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primeseven 47787* | If the (weak) ternary Goldbach conjecture is valid, then every even integer greater than 8 is the sum of 4 primes. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ((𝑁 ∈ (ℤ≥‘9) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | nnsum4primesevenALTV 47788* | If the (strong) ternary Goldbach conjecture is valid, then every even integer greater than 10 is the sum of 4 primes. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ((𝑁 ∈ (ℤ≥‘;12) ∧ 𝑁 ∈ Even ) → ∃𝑓 ∈ (ℙ ↑m (1...4))𝑁 = Σ𝑘 ∈ (1...4)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | wtgoldbnnsum4prm 47789* | If the (weak) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes, showing that Schnirelmann's constant would be less than or equal to 4. See corollary 1.1 in [Helfgott] p. 4. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (5 < 𝑚 → 𝑚 ∈ GoldbachOddW ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | stgoldbnnsum4prm 47790* | If the (strong) ternary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 4 primes. (Contributed by AV, 27-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Odd (7 < 𝑚 → 𝑚 ∈ GoldbachOdd ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 4 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbnnsum3prm 47791* | If the binary Goldbach conjecture is valid, then every integer greater than 1 is the sum of at most 3 primes, showing that Schnirelmann's constant would be equal to 3. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (∀𝑚 ∈ Even (4 < 𝑚 → 𝑚 ∈ GoldbachEven ) → ∀𝑛 ∈ (ℤ≥‘2)∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 𝑛 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbtbndlem1 47792 | Lemma 1 for bgoldbtbnd 47796: the odd numbers between 7 and 13 (exclusive) are odd Goldbach numbers. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑁 ∈ Odd ∧ 7 < 𝑁 ∧ 𝑁 ∈ (7[,);13)) → 𝑁 ∈ GoldbachOdd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbtbndlem2 47793* | Lemma 2 for bgoldbtbnd 47796. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ 𝑆 = (𝑋 − (𝐹‘(𝐼 − 1))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbtbndlem3 47794* | Lemma 3 for bgoldbtbnd 47796. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) & ⊢ 𝑆 = (𝑋 − (𝐹‘𝐼)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ Odd ∧ 𝐼 ∈ (1..^𝐷)) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ 4 < 𝑆) → (𝑆 ∈ Even ∧ 𝑆 < 𝑁 ∧ 4 < 𝑆))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbtbndlem4 47795* | Lemma 4 for bgoldbtbnd 47796. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) ⇒ ⊢ (((𝜑 ∧ 𝐼 ∈ (1..^𝐷)) ∧ 𝑋 ∈ Odd ) → ((𝑋 ∈ ((𝐹‘𝐼)[,)(𝐹‘(𝐼 + 1))) ∧ (𝑋 − (𝐹‘𝐼)) ≤ 4) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ Odd ∧ 𝑞 ∈ Odd ∧ 𝑟 ∈ Odd ) ∧ 𝑋 = ((𝑝 + 𝑞) + 𝑟)))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbtbnd 47796* | If the binary Goldbach conjecture is valid up to an integer 𝑁, and there is a series ("ladder") of primes with a difference of at most 𝑁 up to an integer 𝑀, then the strong ternary Goldbach conjecture is valid up to 𝑀, see section 1.2.2 in [Helfgott] p. 4 with N = 4 x 10^18, taken from [OeSilva], and M = 8.875 x 10^30. (Contributed by AV, 1-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘;11)) & ⊢ (𝜑 → ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑁) → 𝑛 ∈ GoldbachEven )) & ⊢ (𝜑 → 𝐷 ∈ (ℤ≥‘3)) & ⊢ (𝜑 → 𝐹 ∈ (RePart‘𝐷)) & ⊢ (𝜑 → ∀𝑖 ∈ (0..^𝐷)((𝐹‘𝑖) ∈ (ℙ ∖ {2}) ∧ ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)) < (𝑁 − 4) ∧ 4 < ((𝐹‘(𝑖 + 1)) − (𝐹‘𝑖)))) & ⊢ (𝜑 → (𝐹‘0) = 7) & ⊢ (𝜑 → (𝐹‘1) = ;13) & ⊢ (𝜑 → 𝑀 < (𝐹‘𝐷)) & ⊢ (𝜑 → (𝐹‘𝐷) ∈ ℝ) ⇒ ⊢ (𝜑 → ∀𝑛 ∈ Odd ((7 < 𝑛 ∧ 𝑛 < 𝑀) → 𝑛 ∈ GoldbachOdd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Axiom | ax-bgbltosilva 47797 | The binary Goldbach conjecture is valid for all even numbers less than or equal to 4x10^18, see section 2 in [OeSilva] p. 2042. Temporarily provided as "axiom". (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ((𝑁 ∈ Even ∧ 4 < 𝑁 ∧ 𝑁 ≤ (4 · (;10↑;18))) → 𝑁 ∈ GoldbachEven ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Axiom | ax-tgoldbachgt 47798* | Temporary duplicate of tgoldbachgt 34678, provided as "axiom" as long as this theorem is in the mathbox of Thierry Arnoux: Odd integers greater than (;10↑;27) have at least a representation as a sum of three odd primes. Final statement in section 7.4 of [Helfgott] p. 70 , expressed using the set 𝐺 of odd numbers which can be written as a sum of three odd primes. (Contributed by Thierry Arnoux, 22-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ 𝑂 = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} & ⊢ 𝐺 = {𝑧 ∈ 𝑂 ∣ ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ ∃𝑟 ∈ ℙ ((𝑝 ∈ 𝑂 ∧ 𝑞 ∈ 𝑂 ∧ 𝑟 ∈ 𝑂) ∧ 𝑧 = ((𝑝 + 𝑞) + 𝑟))} ⇒ ⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ 𝑂 (𝑚 < 𝑛 → 𝑛 ∈ 𝐺)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | tgoldbachgtALTV 47799* | Variant of Thierry Arnoux's tgoldbachgt 34678 using the symbols Odd and GoldbachOdd: The ternary Goldbach conjecture is valid for large odd numbers (i.e. for all odd numbers greater than a fixed 𝑚). This is proven by Helfgott (see section 7.4 in [Helfgott] p. 70) for 𝑚 = 10^27. (Contributed by AV, 2-Aug-2020.) (Revised by AV, 15-Jan-2022.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑚 ∈ ℕ (𝑚 ≤ (;10↑;27) ∧ ∀𝑛 ∈ Odd (𝑚 < 𝑛 → 𝑛 ∈ GoldbachOdd )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| Theorem | bgoldbachlt 47800* | The binary Goldbach conjecture is valid for small even numbers (i.e. for all even numbers less than or equal to a fixed big 𝑚). This is verified for m = 4 x 10^18 by Oliveira e Silva, see ax-bgbltosilva 47797. (Contributed by AV, 3-Aug-2020.) (Revised by AV, 9-Sep-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| ⊢ ∃𝑚 ∈ ℕ ((4 · (;10↑;18)) ≤ 𝑚 ∧ ∀𝑛 ∈ Even ((4 < 𝑛 ∧ 𝑛 < 𝑚) → 𝑛 ∈ GoldbachEven )) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |