P. 481 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

m1expevenALTV 48001

Exponentiation of -1 by an even power. (Contributed by Glauco Siliprandi, 29-Jun-2017.) (Revised by AV, 6-Jul-2020.)

⊢ (𝑁 ∈ Even → (-1↑𝑁) = 1)

Theorem

m1expoddALTV 48002

Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.)

⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1)

21.48.13.2  Alternate definitions using the "divides" relation

Theorem

dfeven2 48003

Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)

⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}

Theorem

dfodd3 48004

Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)

⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}

Theorem

iseven2 48005

The predicate "is an even number". An even number is an integer which is divisible by 2. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ 2 ∥ 𝑍))

Theorem

isodd3 48006

The predicate "is an odd number". An odd number is an integer which is not divisible by 2. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ¬ 2 ∥ 𝑍))

Theorem

2dvdseven 48007

2 divides an even number. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)

Theorem

m2even 48008

A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)

⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )

Theorem

2ndvdsodd 48009

2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)

Theorem

2dvdsoddp1 48010

2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))

Theorem

2dvdsoddm1 48011

2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.)

⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1))

21.48.13.3  Alternate definitions using the "modulo" operation

Theorem

dfeven3 48012

Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)

⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}

Theorem

dfodd4 48013

Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)

⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1}

Theorem

dfodd5 48014

Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)

⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0}

Theorem

zefldiv2ALTV 48015

The floor of an even number divided by 2 is equal to the even number divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.)

⊢ (𝑁 ∈ Even → (⌊‘(𝑁 / 2)) = (𝑁 / 2))

Theorem

zofldiv2ALTV 48016

The floor of an odd number divided by 2 is equal to the odd number first decreased by 1 and then divided by 2. (Contributed by AV, 7-Jun-2020.) (Revised by AV, 18-Jun-2020.)

⊢ (𝑁 ∈ Odd → (⌊‘(𝑁 / 2)) = ((𝑁 − 1) / 2))

Theorem

oddflALTV 48017

Odd number representation by using the floor function. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 18-Jun-2020.)

⊢ (𝐾 ∈ Odd → 𝐾 = ((2 · (⌊‘(𝐾 / 2))) + 1))

21.48.13.4  Alternate definitions using the "gcd" operation

Theorem

iseven5 48018

The predicate "is an even number". An even number and 2 have 2 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)

⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (2 gcd 𝑍) = 2))

Theorem

isodd7 48019

The predicate "is an odd number". An odd number and 2 have 1 as greatest common divisor. (Contributed by AV, 1-Jul-2020.)

⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ (2 gcd 𝑍) = 1))

Theorem

dfeven5 48020

Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)

⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2}

Theorem

dfodd7 48021

Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)

⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1}

Theorem

gcd2odd1 48022

The greatest common divisor of an odd number and 2 is 1, i.e., 2 and any odd number are coprime. Remark: The proof using dfodd7 48021 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.)

⊢ (𝑍 ∈ Odd → (𝑍 gcd 2) = 1)

21.48.13.5  Theorems of part 5 revised

Theorem

zneoALTV 48023

No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of [Apostol] p. 28. (Contributed by NM, 31-Jul-2004.) (Revised by AV, 16-Jun-2020.)

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

Theorem

zeoALTV 48024

An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)

⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd ))

Theorem

zeo2ALTV 48025

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 48026

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 48027

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

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 48029

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 48030

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 48031

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 48032

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 48033

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

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

Theorem

bits0eALTV 48034

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 48035

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 48036

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 48037

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 48038

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 48039

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 48040

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 48041

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 48042

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

⊢ 0 ∈ Even

Theorem

0noddALTV 48043

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

⊢ 0 ∉ Odd

Theorem

1oddALTV 48044

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

⊢ 1 ∈ Odd

Theorem

1nevenALTV 48045

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

⊢ 1 ∉ Even

Theorem

2evenALTV 48046

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

⊢ 2 ∈ Even

Theorem

2noddALTV 48047

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

⊢ 2 ∉ Odd

Theorem

nn0o1gt2ALTV 48048

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 48049

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 48050

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 48051

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

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

Theorem

nneven 48052

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

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

Theorem

nn0onn0exALTV 48053*

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

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

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 48056

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 48057

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

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

Theorem

emoo 48058

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

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

Theorem

epee 48059

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

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

Theorem

emee 48060

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

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

Theorem

evensumeven 48061

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 48062

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

⊢ 3 ∈ Odd

Theorem

4even 48063

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

⊢ 4 ∈ Even

Theorem

5odd 48064

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

⊢ 5 ∈ Odd

Theorem

6even 48065

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

⊢ 6 ∈ Even

Theorem

7odd 48066

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

⊢ 7 ∈ Odd

Theorem

8even 48067

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

⊢ 8 ∈ Even

Theorem

evenprm2 48068

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

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

Theorem

oddprmne2 48069

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

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

Theorem

oddprmuzge3 48070

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 48071

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 48072

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 48073

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

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

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

21.48.13.9  Perfect Number Theorem (revised)

Theorem

perfectALTVlem1 48075

Lemma for perfectALTV 48077. (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 48076

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

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

Theorem

perfectALTV 48077*

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 16723].

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

Syntax

cfppr 48078

Extend class notation with the Fermat pseudoprimes.

class FPPr

Definition

df-fppr 48079*

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

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

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

Theorem

fpprmod 48081*

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 48082

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

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

Theorem

fpprbasnn 48083

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

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

Theorem

fpprnn 48084

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

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

Theorem

fppr2odd 48085

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

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

Theorem

11t31e341 48086

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

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

Theorem

2exp340mod341 48087

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

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

Theorem

341fppr2 48088

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

⊢ ;;341 ∈ ( FPPr ‘2)

Theorem

4fppr1 48089

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

⊢ 4 ∈ ( FPPr ‘1)

Theorem

8exp8mod9 48090

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

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

Theorem

9fppr8 48091

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

⊢ 9 ∈ ( FPPr ‘8)

Theorem

dfwppr 48092

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 48093

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 48094

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 48095

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 48096

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

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

Theorem

nfermltl2rev 48097

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

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

Theorem

nfermltlrev 48098*

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 48102), "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 48135 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 48135): "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 48103, is the basis for "the other formulation", to formulate the weak ternary Goldbach conjecture. Alternately, df-gbo 48104 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 48102), 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 48125, which would be quite a lot...

As proposed in the Google group discussion https://groups.google.com/g/metamath/c/DOXS4pg0h8w 48125, 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 48164, ax-hgprmladder 48168 and ax-tgoldbachgt 48165.

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 48165
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 48102	A positive even integer that can be expressed as the sum of two odd primes.	See https://mathworld.wolfram.com/GoldbachNumber.html 48102
weak odd Goldbach number		gbow	df-gbow 48103	A positive odd integer that can be expressed as the sum of three primes.
odd Goldbach number	strong odd Goldbach number	gbo	df-gbo 48104	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 48136	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 48136, [*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 48130, sbgoldbwt 48131	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, 48131 [*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 48132	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 48132, https://mathworld.wolfram.com/GoldbachConjecture.html 48132 or section 7.4 in [Helfgott] p. 71.
Goldbach's original conjecture (modern version)	the "ternary" Goldbach conjecture	mogoldb, m	sbgoldbm 48138	Every integer greater than 5 can be written as the sum of three primes.	See https://en.wikipedia.org/wiki/Goldbach's_weak_conjecture 48138, and https://mathworld.wolfram.com/GoldbachConjecture.html 48138
Goldbach's original conjecture (original version)		ogoldb, o	sbgoldbo 48141	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 48141, and https://mathworld.wolfram.com/GoldbachConjecture.html 48141

Syntax

cgbe 48099

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

class GoldbachEven

Syntax

cgbow 48100

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