P. 478 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

zeo2ALTV 47701

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 47702

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 47703

A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.)

⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )

21.48.13.6  Theorems of part 6 revised

Theorem

odd2np1ALTV 47704*

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 47705

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 47706

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 47707

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.) (Proof shortened by AV, 10-Jul-2022.)

⊢ ((𝐴 ∈ ℂ ∧ 𝑁 ∈ ℕ ∧ 𝑁 ∈ Odd ) → (-𝐴↑𝑁) = -(𝐴↑𝑁))

Theorem

oexpnegnz 47708

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 47709

Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)

⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd ))

Theorem

bits0eALTV 47710

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 47711

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 47712

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 47713

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 47714

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 47715

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 47716

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 47717

A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.)

⊢ (𝑁 ∈ (ℙ ∖ {2}) → 𝑁 ∈ Odd )

21.48.13.7  Theorems of AV's mathbox revised

Theorem

0evenALTV 47718

0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)

⊢ 0 ∈ Even

Theorem

0noddALTV 47719

0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)

⊢ 0 ∉ Odd

Theorem

1oddALTV 47720

1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)

⊢ 1 ∈ Odd

Theorem

1nevenALTV 47721

1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)

⊢ 1 ∉ Even

Theorem

2evenALTV 47722

2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)

⊢ 2 ∈ Even

Theorem

2noddALTV 47723

2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)

⊢ 2 ∉ Odd

Theorem

nn0o1gt2ALTV 47724

An odd nonnegative integer is either 1 or greater than 2. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 21-Jun-2020.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑁 ∈ Odd ) → (𝑁 = 1 ∨ 2 < 𝑁))

Theorem

nnoALTV 47725

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 47726

An alternate characterization of an odd nonnegative integer. (Contributed by AV, 28-May-2020.) (Revised by AV, 21-Jun-2020.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑁 ∈ Odd ) → ((𝑁 − 1) / 2) ∈ ℕ₀)

Theorem

nn0e 47727

An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ₀)

Theorem

nneven 47728

An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.)

⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ)

Theorem

nn0onn0exALTV 47729*

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.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑁 ∈ Odd ) → ∃𝑚 ∈ ℕ₀ 𝑁 = ((2 · 𝑚) + 1))

Theorem

nn0enn0exALTV 47730*

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.)

⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑁 ∈ Even ) → ∃𝑚 ∈ ℕ₀ 𝑁 = (2 · 𝑚))

Theorem

nnennexALTV 47731*

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 47732

2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.)

⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ Even )

21.48.13.8  Additional theorems

Theorem

epoo 47733

The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd )

Theorem

emoo 47734

The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd )

Theorem

epee 47735

The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even )

Theorem

emee 47736

The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.)

⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even )

Theorem

evensumeven 47737

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 47738

3 is an odd number. (Contributed by AV, 20-Jul-2020.)

⊢ 3 ∈ Odd

Theorem

4even 47739

4 is an even number. (Contributed by AV, 23-Jul-2020.)

⊢ 4 ∈ Even

Theorem

5odd 47740

5 is an odd number. (Contributed by AV, 23-Jul-2020.)

⊢ 5 ∈ Odd

Theorem

6even 47741

6 is an even number. (Contributed by AV, 20-Jul-2020.)

⊢ 6 ∈ Even

Theorem

7odd 47742

7 is an odd number. (Contributed by AV, 20-Jul-2020.)

⊢ 7 ∈ Odd

Theorem

8even 47743

8 is an even number. (Contributed by AV, 23-Jul-2020.)

⊢ 8 ∈ Even

Theorem

evenprm2 47744

A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.)

⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2))

Theorem

oddprmne2 47745

Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.)

⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2}))

Theorem

oddprmuzge3 47746

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 47747

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 47748

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 47749

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 47750*

Lemma for mogoldbb 47815. (Contributed by AV, 26-Dec-2021.)

⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞))

21.48.13.9  Perfect Number Theorem (revised)

Theorem

perfectALTVlem1 47751

Lemma for perfectALTV 47753. (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 47752

Lemma for perfectALTV 47753. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)

⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ Odd )    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))

Theorem

perfectALTV 47753*

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)))))

21.48.14  Number theory (extension 2)

21.48.14.1  Fermat pseudoprimes

"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 16692].

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 47773] 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 47773, 29-May-2023.

Syntax

cfppr 47754

Extend class notation with the Fermat pseudoprimes.

class FPPr

Definition

df-fppr 47755*

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 47756*

The set of Fermat pseudoprimes to the base 𝑁. (Contributed by AV, 29-May-2023.)

⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ_≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑁↑(𝑥 − 1)) − 1))})

Theorem

fpprmod 47757*

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 47758

A Fermat pseudoprime to the base 𝑁. (Contributed by AV, 30-May-2023.)

⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ( FPPr ‘𝑁) ↔ (𝑋 ∈ (ℤ_≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((𝑁↑(𝑋 − 1)) mod 𝑋) = 1)))

Theorem

fpprbasnn 47759

The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.)

⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑁 ∈ ℕ)

Theorem

fpprnn 47760

A Fermat pseudoprime to the base 𝑁 is a positive integer. (Contributed by AV, 30-May-2023.)

⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑋 ∈ ℕ)

Theorem

fppr2odd 47761

A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.)

⊢ (𝑋 ∈ ( FPPr ‘2) → 𝑋 ∈ Odd )

Theorem

11t31e341 47762

341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.)

⊢ (;11 · ;31) = ;;341

Theorem

2exp340mod341 47763

Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.)

⊢ ((2↑;;340) mod ;;341) = 1

Theorem

341fppr2 47764

341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.)

⊢ ;;341 ∈ ( FPPr ‘2)

Theorem

4fppr1 47765

4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.)

⊢ 4 ∈ ( FPPr ‘1)

Theorem

8exp8mod9 47766

Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.)

⊢ ((8↑8) mod 9) = 1

Theorem

9fppr8 47767

9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.)

⊢ 9 ∈ ( FPPr ‘8)

Theorem

dfwppr 47768

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 47769

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 47770

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 47771

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 47772

Fermat's little theorem with base 8 reversed is not generally true: There is an integer 𝑝 (for example 9, see 9fppr8 47767) so that "𝑝 is prime" does not follow from 8↑𝑝≡8 (mod 𝑝). (Contributed by AV, 3-Jun-2023.)

⊢ ∃𝑝 ∈ (ℤ_≥‘3) ¬ (((8↑𝑝) mod 𝑝) = (8 mod 𝑝) → 𝑝 ∈ ℙ)

Theorem

nfermltl2rev 47773

Fermat's little theorem with base 2 reversed is not generally true: There is an integer 𝑝 (for example 341, see 341fppr2 47764) so that "𝑝 is prime" does not follow from 2↑𝑝≡2 (mod 𝑝). (Contributed by AV, 3-Jun-2023.)

⊢ ∃𝑝 ∈ (ℤ_≥‘3) ¬ (((2↑𝑝) mod 𝑝) = (2 mod 𝑝) → 𝑝 ∈ ℙ)

Theorem

nfermltlrev 47774*

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 𝑝) → 𝑝 ∈ ℙ)

21.48.14.2  Goldbach's conjectures

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.

Using the definition of a _Goldbach number_, which is "a positive even integer that can be expressed as the sum of two odd primes." (see df-gbe 47778), "another form of the statement of Goldbach's conjecture is that all even integers greater than 4 are Goldbach numbers.". 4 is not a Goldbach number, but it is the sum of two primes (2 and 2) nevertheless. sbgoldbalt 47811 shows that both forms are equivalent.

Hint (see Wikipedia, ("Goldbach's weak conjecture", 26-Jul-2020, https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 47811): "Some state the [weak] conjecture as 'Every odd number greater than 7 can be expressed as the sum of three odd primes.' This version excludes 7 = 2+2+3 because this requires the even prime 2. On odd numbers larger than 7 it is slightly stronger as it also excludes sums like 17 = 2+2+13, which are allowed in the other formulation. Helfgott's proof [see below] covers both versions of the conjecture. Like the other formulation, this one also immediately follows from Goldbach's strong conjecture." The definition of "weak odd Goldbach numbers", see df-gbow 47779, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternately, df-gbo 47780 provides a definition of "(strong) odd Goldbach numbers" allowing for stating the strong ternary Goldbach conjecture. In literature, the term "Goldbach number" is used for "even Goldbach numbers" (according to definition df-gbe 47778), whereas there seems to be no explicit names and definitions for "odd Goldbach numbers". Since there are more theorems for "strong odd Goldbach numbers", "odd Goldbach numbers" refers to "strong odd Goldbach numbers" in the following. Otherwise, the term "weak odd Goldbach numbers" is explicitly used.

In contrast to the two versions of the binary Goldbach conjecture, the two versions of the ternary Goldbach conjecture are different not only for small numbers, but the strong version excludes cases like a=2+2+b in general, e.g., 23=2+2+19. Therefore, it seems to be more difficult to prove the strong ternary Goldbach conjecture than the weak version, because there are fewer possible partitions available.

Although the binary Goldbach conjecture is not proven yet, the ternary Goldbach conjecture was proven by Harald Helfgott in 2014 (the weak as well as the strong version, see Main theorem in [Helfgott] p. 2). It would be great if this proof can be formalized with Metamath (although it is not in the Metamath 100 list). This section should be a starting point for this.

The main problem will be to provide means to express the results from checking "small" numbers (performed with a computer): numbers up to about 4 x 10^18 for the binary Goldbach conjecture (see section 2 in [OeSilva] p. 2042, called "even Goldbach conjecture" here) resp. about 9 x 10^30 for the ternary Goldbach conjecture (see section 1.2.2 in [Helfgott] p. 4) or 8 x 10^26 (see theorem 2.1 in [OeSilva] p. 2057, called "odd Goldbach conjecture" here). Maybe each of the results must be provided as theorem, like 6gbe 47801, which would be quite a lot...

As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w 47801, this problem could be solved by using a reflective verifier or adding a concept of verification certificates that can be added into the Metamath databases as a reference. To sidestep the computation problem for now, the corresponding theorems are temporarily provided as axioms, see ax-bgbltosilva 47840, ax-hgprmladder 47844 and ax-tgoldbachgt 47841.

Summary/glossary:

Term	Synonyms	Label fragment	Definition/Theorem	Remarks
binary Goldbach partition	simply "Goldbach partition"			A pair of primes (p,q) that sum to an even integer 2n=p+q	See https://mathworld.wolfram.com/GoldbachPartition.html 47841
weak Goldbach partition		gbpart		A sum of two resp. three primes resulting in an even resp. odd number without further specialization.
Goldbach partition		gbpart		A sum of two resp. three odd primes resulting in an even resp. odd number without further specialization.
even Goldbach number	simply "Goldbach number"	gbe	df-gbe 47778	A positive even integer that can be expressed as the sum of two odd primes.	See https://mathworld.wolfram.com/GoldbachNumber.html 47778
weak odd Goldbach number		gbow	df-gbow 47779	A positive odd integer that can be expressed as the sum of three primes.
odd Goldbach number	strong odd Goldbach number	gbo	df-gbo 47780	A positive odd integer that can be expressed as the sum of three odd primes.
strong binary Goldbach conjecture	"the" Goldbach conjecture" [*1], even Goldbach conjecture [*2]	sbgoldb		Every even integer greater than 4 can be expressed as the sum of two odd primes.	[*1] Equation (1) in [ApostolNT] p. 304 or [*2] introduction of [OeSilva] p. 2033.
binary Goldbach conjecture[*1][*3]	strong Goldbach conjecture [*1], even Goldbach conjecture [*1], or simply "the Goldbach conjecture" [*1][*2]	bgoldb, b	sbgoldbb 47812	Every even integer greater than 2 can be expressed as the sum of two primes.	See [*1] https://en.wikipedia.org/wiki/Goldbach's_conjecture 47812, [*2] statement in [ApostolNT] p. 9 or [*3] section 1.1 in [Helfgott] p. 2.
weak ternary Goldbach conjecture	Goldbach's weak conjecture [*1], odd Goldbach conjecture [*1][*3], ternary Goldbach conjecture [*2], ternary Goldbach problem[*1], three-primes problem [*1][*2]	wtgoldb, wt	stgoldbwt 47806, sbgoldbwt 47807	Every odd number greater than 5 can be expressed as the sum of three primes.	See [*1] https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture, 47807 [*2] section 1.1 in [Helfgott] p. 2 or [*3] section 2.4 in [OeSilva] p. 2057.
ternary Goldbach conjecture	strong ternary Goldbach conjecture, the "weak" Goldbach conjecture	tgoldb, stgoldb, st	sbgoldbst 47808	Every odd number greater than 7 can be expressed as the sum of three odd primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 47808, https://mathworld.wolfram.com/GoldbachConjecture.html 47808 or section 7.4 in [Helfgott] p. 71.
Goldbach's original conjecture (modern version)	the "ternary" Goldbach conjecture	mogoldb, m	sbgoldbm 47814	Every integer greater than 5 can be written as the sum of three primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 47814, and https://mathworld.wolfram.com/GoldbachConjecture.html 47814
Goldbach's original conjecture (original version)		ogoldb, o	sbgoldbo 47817	Every integer greater than 2 can be written as the sum of three "primes" (considered the number 1 to be a "prime").	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 47817, and https://mathworld.wolfram.com/GoldbachConjecture.html 47817

Syntax

cgbe 47775

Extend the definition of a class to include the set of even numbers which have a Goldbach partition.

class GoldbachEven

Syntax

cgbow 47776

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 47777

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 47778*

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 47779*

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 47780*

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 47781*

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 47782*

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 47783*

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 47784

An even Goldbach number is even. (Contributed by AV, 25-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ Even )

Theorem

gbowodd 47785

A weak odd Goldbach number is odd. (Contributed by AV, 25-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ Odd )

Theorem

gbogbow 47786

A (strong) odd Goldbach number is a weak Goldbach number. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ GoldbachOddW )

Theorem

gboodd 47787

An odd Goldbach number is odd. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ Odd )

Theorem

gbepos 47788

Any even Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 𝑍 ∈ ℕ)

Theorem

gbowpos 47789

Any weak odd Goldbach number is positive. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 𝑍 ∈ ℕ)

Theorem

gbopos 47790

Any odd Goldbach number is positive. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 𝑍 ∈ ℕ)

Theorem

gbegt5 47791

Any even Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 5 < 𝑍)

Theorem

gbowgt5 47792

Any weak odd Goldbach number is greater than 5. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 5 < 𝑍)

Theorem

gbowge7 47793

Any weak odd Goldbach number is greater than or equal to 7. Because of 7gbow 47802, this bound is strict. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOddW → 7 ≤ 𝑍)

Theorem

gboge9 47794

Any odd Goldbach number is greater than or equal to 9. Because of 9gbo 47804, this bound is strict. (Contributed by AV, 26-Jul-2020.)

⊢ (𝑍 ∈ GoldbachOdd → 9 ≤ 𝑍)

Theorem

gbege6 47795

Any even Goldbach number is greater than or equal to 6. Because of 6gbe 47801, this bound is strict. (Contributed by AV, 20-Jul-2020.)

⊢ (𝑍 ∈ GoldbachEven → 6 ≤ 𝑍)

Theorem

gbpart6 47796

The Goldbach partition of 6. (Contributed by AV, 20-Jul-2020.)

⊢ 6 = (3 + 3)

Theorem

gbpart7 47797

The (weak) Goldbach partition of 7. (Contributed by AV, 20-Jul-2020.)

⊢ 7 = ((2 + 2) + 3)

Theorem

gbpart8 47798

The Goldbach partition of 8. (Contributed by AV, 20-Jul-2020.)

⊢ 8 = (3 + 5)

Theorem

gbpart9 47799

The (strong) Goldbach partition of 9. (Contributed by AV, 26-Jul-2020.)

⊢ 9 = ((3 + 3) + 3)

Theorem

gbpart11 47800

The (strong) Goldbach partition of 11. (Contributed by AV, 29-Jul-2020.)

⊢ ;11 = ((3 + 3) + 5)