P. 452 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 45101-45200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfeven4 45101*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)}
Theorem	evenm1odd 45102	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd )
Theorem	evenp1odd 45103	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd )
Theorem	oddp1eveni 45104	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even )
Theorem	oddm1eveni 45105	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even )
Theorem	evennodd 45106	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd )
Theorem	oddneven 45107	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even )
Theorem	enege 45108	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even )
Theorem	onego 45109	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd )
Theorem	m1expevenALTV 45110	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 45111	Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1)
20.41.13.2  Alternate definitions using the "divides" relation
Theorem	dfeven2 45112	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}
Theorem	dfodd3 45113	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
Theorem	iseven2 45114	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 45115	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 45116	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)
Theorem	m2even 45117	A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )
Theorem	2ndvdsodd 45118	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)
Theorem	2dvdsoddp1 45119	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))
Theorem	2dvdsoddm1 45120	2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1))
20.41.13.3  Alternate definitions using the "modulo" operation
Theorem	dfeven3 45121	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}
Theorem	dfodd4 45122	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1}
Theorem	dfodd5 45123	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0}
Theorem	zefldiv2ALTV 45124	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 45125	The floor of an odd numer 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 45126	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))
20.41.13.4  Alternate definitions using the "gcd" operation
Theorem	iseven5 45127	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 45128	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 45129	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2}
Theorem	dfodd7 45130	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1}
Theorem	gcd2odd1 45131	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 45130 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ Odd → (𝑍 gcd 2) = 1)
20.41.13.5  Theorems of part 5 revised
Theorem	zneoALTV 45132	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 45133	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd ))
Theorem	zeo2ALTV 45134	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 45135	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 45136	A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.)
⊢ 𝑁 ∈ ℕ    ⇒   ⊢ (𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd )
20.41.13.6  Theorems of part 6 revised
Theorem	odd2np1ALTV 45137*	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 45138	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 45139	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 45140	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 45141	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 45142	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd ))
Theorem	bits0eALTV 45143	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 45144	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 45145	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 45146	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 45147	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 45148	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 45149	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 45150	A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.)
⊢ (𝑁 ∈ (ℙ ∖ {2}) → 𝑁 ∈ Odd )
20.41.13.7  Theorems of AV's mathbox revised
Theorem	0evenALTV 45151	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∈ Even
Theorem	0noddALTV 45152	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∉ Odd
Theorem	1oddALTV 45153	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∈ Odd
Theorem	1nevenALTV 45154	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∉ Even
Theorem	2evenALTV 45155	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∈ Even
Theorem	2noddALTV 45156	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∉ Odd
Theorem	nn0o1gt2ALTV 45157	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 45158	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 45159	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 45160	An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0)
Theorem	nneven 45161	An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0onn0exALTV 45162*	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 45163*	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 45164*	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 45165	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.)
⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ Even )
20.41.13.8  Additional theorems
Theorem	epoo 45166	The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd )
Theorem	emoo 45167	The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.)
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd )
Theorem	epee 45168	The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.)
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even )
Theorem	emee 45169	The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.)
⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even )
Theorem	evensumeven 45170	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 45171	3 is an odd number. (Contributed by AV, 20-Jul-2020.)
⊢ 3 ∈ Odd
Theorem	4even 45172	4 is an even number. (Contributed by AV, 23-Jul-2020.)
⊢ 4 ∈ Even
Theorem	5odd 45173	5 is an odd number. (Contributed by AV, 23-Jul-2020.)
⊢ 5 ∈ Odd
Theorem	6even 45174	6 is an even number. (Contributed by AV, 20-Jul-2020.)
⊢ 6 ∈ Even
Theorem	7odd 45175	7 is an odd number. (Contributed by AV, 20-Jul-2020.)
⊢ 7 ∈ Odd
Theorem	8even 45176	8 is an even number. (Contributed by AV, 23-Jul-2020.)
⊢ 8 ∈ Even
Theorem	evenprm2 45177	A prime number is even iff it is 2. (Contributed by AV, 21-Jul-2020.)
⊢ (𝑃 ∈ ℙ → (𝑃 ∈ Even ↔ 𝑃 = 2))
Theorem	oddprmne2 45178	Every prime number not being 2 is an odd prime number. (Contributed by AV, 21-Aug-2021.)
⊢ ((𝑃 ∈ ℙ ∧ 𝑃 ∈ Odd ) ↔ 𝑃 ∈ (ℙ ∖ {2}))
Theorem	oddprmuzge3 45179	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 45180	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 45181	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 45182	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 45183*	Lemma for mogoldbb 45248. (Contributed by AV, 26-Dec-2021.)
⊢ (((𝑃 ∈ ℙ ∧ 𝑄 ∈ ℙ ∧ 𝑅 ∈ ℙ) ∧ 𝑁 ∈ Even ∧ (𝑁 + 2) = ((𝑃 + 𝑄) + 𝑅)) → ∃𝑝 ∈ ℙ ∃𝑞 ∈ ℙ 𝑁 = (𝑝 + 𝑞))
20.41.13.9  Perfect Number Theorem (revised)
Theorem	perfectALTVlem1 45184	Lemma for perfectALTV 45186. (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 45185	Lemma for perfectALTV 45186. (Contributed by Mario Carneiro, 17-May-2016.) (Revised by AV, 1-Jul-2020.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ Odd )    &   ⊢ (𝜑 → (1 σ ((2↑𝐴) · 𝐵)) = (2 · ((2↑𝐴) · 𝐵)))    ⇒   ⊢ (𝜑 → (𝐵 ∈ ℙ ∧ 𝐵 = ((2↑(𝐴 + 1)) − 1)))
Theorem	perfectALTV 45186*	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)))))
20.41.14  Number theory (extension 2)
20.41.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 16494]. 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 45206] 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 45206, 29-May-2023.
Syntax	cfppr 45187	Extend class notation with the Fermat pseudoprimes.
class FPPr
Definition	df-fppr 45188*	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 45189*	The set of Fermat pseudoprimes to the base 𝑁. (Contributed by AV, 29-May-2023.)
⊢ (𝑁 ∈ ℕ → ( FPPr ‘𝑁) = {𝑥 ∈ (ℤ≥‘4) ∣ (𝑥 ∉ ℙ ∧ 𝑥 ∥ ((𝑁↑(𝑥 − 1)) − 1))})
Theorem	fpprmod 45190*	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 45191	A Fermat pseudoprime to the base 𝑁. (Contributed by AV, 30-May-2023.)
⊢ (𝑁 ∈ ℕ → (𝑋 ∈ ( FPPr ‘𝑁) ↔ (𝑋 ∈ (ℤ≥‘4) ∧ 𝑋 ∉ ℙ ∧ ((𝑁↑(𝑋 − 1)) mod 𝑋) = 1)))
Theorem	fpprbasnn 45192	The base of a Fermat pseudoprime is a positive integer. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑁 ∈ ℕ)
Theorem	fpprnn 45193	A Fermat pseudoprime to the base 𝑁 is a positive integer. (Contributed by AV, 30-May-2023.)
⊢ (𝑋 ∈ ( FPPr ‘𝑁) → 𝑋 ∈ ℕ)
Theorem	fppr2odd 45194	A Fermat pseudoprime to the base 2 is odd. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑋 ∈ ( FPPr ‘2) → 𝑋 ∈ Odd )
Theorem	11t31e341 45195	341 is the product of 11 and 31. (Contributed by AV, 3-Jun-2023.)
⊢ (;11 · ;31) = ;;341
Theorem	2exp340mod341 45196	Eight to the eighth power modulo nine is one. (Contributed by AV, 3-Jun-2023.)
⊢ ((2↑;;340) mod ;;341) = 1
Theorem	341fppr2 45197	341 is the (smallest) Poulet number (Fermat pseudoprime to the base 2). (Contributed by AV, 3-Jun-2023.)
⊢ ;;341 ∈ ( FPPr ‘2)
Theorem	4fppr1 45198	4 is the (smallest) Fermat pseudoprime to the base 1. (Contributed by AV, 3-Jun-2023.)
⊢ 4 ∈ ( FPPr ‘1)
Theorem	8exp8mod9 45199	Eight to the eighth power modulo nine is one. (Contributed by AV, 2-Jun-2023.)
⊢ ((8↑8) mod 9) = 1
Theorem	9fppr8 45200	9 is the (smallest) Fermat pseudoprime to the base 8. (Contributed by AV, 2-Jun-2023.)
⊢ 9 ∈ ( FPPr ‘8)