Home | Metamath
Proof Explorer Theorem List (p. 457 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 1nevenALTV 45601 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 1 ∉ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2evenALTV 45602 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 2 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2noddALTV 45603 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 2 ∉ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0o1gt2ALTV 45604 | 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 45605 | 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 45606 | 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 45607 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nneven 45608 | An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nn0onn0exALTV 45609* | 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 45610* | 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 | nnennexALTV 45611* | For each even positive integer there is a positive integer which, multiplied by 2, results in the even positive integer. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → ∃𝑚 ∈ ℕ 𝑁 = (2 · 𝑚)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnpw2evenALTV 45612 | 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 45613 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emoo 45614 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | epee 45615 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | emee 45616 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evensumeven 45617 | 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 45618 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 3 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4even 45619 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 4 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 5odd 45620 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 5 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6even 45621 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7odd 45622 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 ∈ Odd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8even 45623 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 ∈ Even | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | evenprm2 45624 | A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmne2 45625 | Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2})) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | oddprmuzge3 45626 | 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 45627 | 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 45628 | 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 45629 | 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 45630* | Lemma for mogoldbb 45695. (Contributed by AV, 26-Dec-2021.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTVlem1 45631 | Lemma for perfectALTV 45633. (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 45632 | Lemma for perfectALTV 45633. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ Odd ) & ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵))) ⇒ ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | perfectALTV 45633* | 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 16591]. 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 45653] 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 45653, 29-May-2023. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cfppr 45634 | Extend class notation with the Fermat pseudoprimes. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class FPPr | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-fppr 45635* | 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 45636* | The set of Fermat pseudoprimes to the base 𝑁. (Contributed by AV, 29-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑁↑(𝑥 − 1)) − 1))}) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprmod 45637* | 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 45638 | A Fermat pseudoprime to the base 𝑁. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ( FPPr ‘𝑁) ↔ (𝑋 ∈ (ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((𝑁↑(𝑋 − 1)) mod 𝑋) = 1))) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprbasnn 45639 | The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑁 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fpprnn 45640 | A Fermat pseudoprime to the base 𝑁 is a positive integer. (Contributed by AV, 30-May-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑋 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fppr2odd 45641 | A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑋 ∈ ( FPPr ‘2) → 𝑋 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 11t31e341 45642 | 341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (;11 · ;31) = ;;341 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 2exp340mod341 45643 | Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((2↑;;340) mod ;;341) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 341fppr2 45644 | 341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ;;341 ∈ ( FPPr ‘2) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 4fppr1 45645 | 4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 4 ∈ ( FPPr ‘1) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8exp8mod9 45646 | Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((8↑8) mod 9) = 1 | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9fppr8 45647 | 9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 9 ∈ ( FPPr ‘8) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dfwppr 45648 | 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 45649 | 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 45650 | 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 45651 | 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 45652 | Fermat's little theorem with base 8 reversed is not generally true: There is an integer 𝑝 (for example 9, see 9fppr8 45647) so that "𝑝 is prime" does not follow from 8↑𝑝≡8 (mod 𝑝). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ∃𝑝 ∈ (ℤ≥‘3) ¬ (((8↑𝑝) mod 𝑝) = (8 mod 𝑝) → 𝑝 ∈ ℙ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfermltl2rev 45653 | Fermat's little theorem with base 2 reversed is not generally true: There is an integer 𝑝 (for example 341, see 341fppr2 45644) so that "𝑝 is prime" does not follow from 2↑𝑝≡2 (mod 𝑝). (Contributed by AV, 3-Jun-2023.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ∃𝑝 ∈ (ℤ≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nfermltlrev 45654* | 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 45655 | Extend the definition of a class to include the set of even numbers which have a Goldbach partition. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cgbow 45656 | 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 45657 | 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 45658* | 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 45659* | 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 45660* | 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 45661* | 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 45662* | 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 45663* | 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 45664 | An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowodd 45665 | A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbogbow 45666 | A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboodd 45667 | An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbepos 45668 | Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowpos 45669 | Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbopos 45670 | Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbegt5 45671 | Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowgt5 45672 | Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbowge7 45673 | Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 45682, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gboge9 45674 | Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 45684, this bound is strict. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbege6 45675 | Any even Goldbach number is greater than or equal to 6. Because of 6gbe 45681, this bound is strict. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart6 45676 | The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 = (3 + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart7 45677 | The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 = ((2 + 2) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart8 45678 | The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 = (3 + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart9 45679 | The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 9 = ((3 + 3) + 3) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | gbpart11 45680 | The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ;11 = ((3 + 3) + 5) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 6gbe 45681 | 6 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 6 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 7gbow 45682 | 7 is a weak odd Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 7 ∈ GoldbachOddW | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 8gbe 45683 | 8 is an even Goldbach number. (Contributed by AV, 20-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 8 ∈ GoldbachEven | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 9gbo 45684 | 9 is an odd Goldbach number. (Contributed by AV, 26-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 9 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 11gbo 45685 | 11 is an odd Goldbach number. (Contributed by AV, 29-Jul-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ;11 ∈ GoldbachOdd | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | stgoldbwt 45686 | 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 45687* | 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 45688* | 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 45689 | Lemma 1 for sbgoldbalt 45691: 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 45690 | Lemma 2 for sbgoldbalt 45691: 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 45691* | 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 45692* | 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 45693* | 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 45694* | 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 45695* | 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 45696* | 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 45697* | 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 45698* | 4 is the sum of at most 3 (actually 2) primes. (Contributed by AV, 2-Aug-2020.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ∃𝑑 ∈ ℕ ∃𝑓 ∈ (ℙ ↑m (1...𝑑))(𝑑 ≤ 3 ∧ 4 = Σ𝑘 ∈ (1...𝑑)(𝑓‘𝑘)) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | nnsum4primes4 45699* | 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 45700* | 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...𝑑)(𝑓‘𝑘))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |