P. 482 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 48101-48200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	3exp4mod41 48101	3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.)
⊢ ((3↑4) mod ;41) = (-1 mod ;41)
Theorem	41prothprmlem1 48102	Lemma 1 for 41prothprm 48104. (Contributed by AV, 4-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((𝑃 − 1) / 2) = ;20
Theorem	41prothprmlem2 48103	Lemma 2 for 41prothprm 48104. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)
Theorem	41prothprm 48104	41 is a Proth prime. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ)
21.48.12.5  The prime-counting function according to Ján Mináč
Theorem	nprmdvdsfacm1lem1 48105	Lemma 1 for nprmdvdsfacm1 48109. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 𝑁 ∥ (𝐴 · (2 · 𝐴)))
Theorem	nprmdvdsfacm1lem2 48106	Lemma 2 for nprmdvdsfacm1 48109. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 3 ≤ 𝐴)
Theorem	nprmdvdsfacm1lem3 48107	Lemma 3 for nprmdvdsfacm1 48109. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → (2 · 𝐴) < (𝑁 − 1))
Theorem	nprmdvdsfacm1lem4 48108	Lemma 4 for nprmdvdsfacm1 48109. (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝐴 ∈ (2..^𝑁) ∧ 𝑁 = (𝐴↑2)) → 𝑁 ∥ (!‘(𝑁 − 1)))
Theorem	nprmdvdsfacm1 48109	A non-prime integer greater than 5 divides the factorial of the integer decreased by 1 (see remark in [Ribenboim] p. 181). Note: not valid for 𝑁 = 4, but for 𝑁 = 1! (Contributed by AV, 7-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∉ ℙ) → 𝑁 ∥ (!‘(𝑁 − 1)))
Theorem	ppivalnnprm 48110	Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a prime number. (Contributed by AV, 10-Apr-2026.)
⊢ (𝑃 ∈ ℙ → (⌊‘((((!‘(𝑃 − 1)) + 1) / 𝑃) − (⌊‘((!‘(𝑃 − 1)) / 𝑃)))) = 1)
Theorem	ppivalnnnprmge6 48111	Value of a term of the prime-counting function pi for positive integers, according to Ján Mináč, for a non-prime number greater than 4. (Contributed by AV, 4-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘6) ∧ 𝑁 ∉ ℙ) → (⌊‘((((!‘(𝑁 − 1)) + 1) / 𝑁) − (⌊‘((!‘(𝑁 − 1)) / 𝑁)))) = 0)
Theorem	ppivalnn4 48112	Value of the term of the prime-counting function pi for positive integers, according to Ján Mináč, for 4. (Contributed by AV, 8-Apr-2026.)
⊢ (⌊‘((((!‘(4 − 1)) + 1) / 4) − (⌊‘((!‘(4 − 1)) / 4)))) = 0
Theorem	ppivalnnnprm 48113	Value of a term of the prime-counting function pi for positive integers, according to Ján Miná&ccaron, for a non-prime number greater than 1. (Contributed by AV, 8-Apr-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘2) ∧ 𝑁 ∉ ℙ) → (⌊‘((((!‘(𝑁 − 1)) + 1) / 𝑁) − (⌊‘((!‘(𝑁 − 1)) / 𝑁)))) = 0)
Theorem	indprm 48114	An indicator function for prime numbers, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ ((𝟭‘(ℤ≥‘2))‘ℙ) = (𝑘 ∈ (ℤ≥‘2) ↦ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
Theorem	indprmfz 48115*	An indicator function for prime numbers in a finite interval of integers, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ 𝐼 = (2...𝐴)    ⇒   ⊢ ((𝟭‘𝐼)‘(𝐼 ∩ ℙ)) = (𝑘 ∈ 𝐼 ↦ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
Theorem	ppi1sum 48116	Value of the prime-counting function pi for 1, according to Ján Mináč. (Contributed by AV, 4-Apr-2026.)
⊢ (π‘1) = Σ𝑘 ∈ ∅ (⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘))))
Theorem	ppivalnn 48117*	Value of the prime-counting function pi for positive integers, according to Ján Mináč, see statement in [Ribenboim], p. 181. (Contributed by AV, 10-Apr-2026.)
⊢ (𝑁 ∈ ℕ → (π‘𝑁) = Σ𝑘 ∈ (2...𝑁)(⌊‘((((!‘(𝑘 − 1)) + 1) / 𝑘) − (⌊‘((!‘(𝑘 − 1)) / 𝑘)))))
21.48.12.6  Solutions of quadratic equations
Theorem	quad1 48118*	A condition for a quadratic equation with complex coefficients to have (exactly) one complex solution. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ ℂ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))
Theorem	requad01 48119*	A condition for a quadratic equation with real coefficients to have (at least) one real solution. (Contributed by AV, 23-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (∃𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 0 ≤ 𝐷))
Theorem	requad1 48120*	A condition for a quadratic equation with real coefficients to have (exactly) one real solution. (Contributed by AV, 26-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (∃!𝑥 ∈ ℝ ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0 ↔ 𝐷 = 0))
Theorem	requad2 48121*	A condition for a quadratic equation with real coefficients to have (exactly) two different real solutions. (Contributed by AV, 28-Jan-2023.)
⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝐴 ≠ 0)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    &   ⊢ (𝜑 → 𝐷 = ((𝐵↑2) − (4 · (𝐴 · 𝐶))))    ⇒   ⊢ (𝜑 → (∃!𝑝 ∈ 𝒫 ℝ((♯‘𝑝) = 2 ∧ ∀𝑥 ∈ 𝑝 ((𝐴 · (𝑥↑2)) + ((𝐵 · 𝑥) + 𝐶)) = 0) ↔ 0 < 𝐷))
21.48.13  Even and odd numbers Even and odd numbers can be characterized in many different ways. In the following, the definition of even and odd numbers is based on the fact that dividing an even number (resp. an odd number increased by 1) by 2 is an integer, see df-even 48124 and df-odd 48125. Alternate definitions resp. characterizations are provided in dfeven2 48147, dfeven3 48156, dfeven4 48136 and in dfodd2 48134, dfodd3 48148, dfodd4 48157, dfodd5 48158, dfodd6 48135. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 48135 in opoeALTV 48181 and dfodd3 48148 in oddprmALTV 48185. Having a fixed definition for even and odd numbers, and alternate characterizations as theorems, advanced theorems about even and/or odd numbers can be expressed more explicitly, and the appropriate characterization can be chosen for their proof, which may become clearer and sometimes also shorter (see, for example, divgcdoddALTV 48180 and divgcdodd 16678).
21.48.13.1  Definitions and basic properties
Syntax	ceven 48122	Extend the definition of a class to include the set of even numbers.
class Even
Syntax	codd 48123	Extend the definition of a class to include the set of odd numbers.
class Odd
Definition	df-even 48124	Define the set of even numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
Definition	df-odd 48125	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
Theorem	iseven 48126	The predicate "is an even number". An even number is an integer which is divisible by 2, i.e. the result of dividing the even integer by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Even ↔ (𝑍 ∈ ℤ ∧ (𝑍 / 2) ∈ ℤ))
Theorem	isodd 48127	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd integer increased by 1 and then divided by 2 is still an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 + 1) / 2) ∈ ℤ))
Theorem	evenz 48128	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)
Theorem	oddz 48129	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
Theorem	evendiv2z 48130	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ)
Theorem	oddp1div2z 48131	The result of dividing an odd number increased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Odd → ((𝑍 + 1) / 2) ∈ ℤ)
Theorem	oddm1div2z 48132	The result of dividing an odd number decreased by 1 and then divided by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Odd → ((𝑍 − 1) / 2) ∈ ℤ)
Theorem	isodd2 48133	The predicate "is an odd number". An odd number is an integer which is not divisible by 2, i.e. the result of dividing the odd number decreased by 1 and then divided by 2 is still an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Odd ↔ (𝑍 ∈ ℤ ∧ ((𝑍 − 1) / 2) ∈ ℤ))
Theorem	dfodd2 48134	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ}
Theorem	dfodd6 48135*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)}
Theorem	dfeven4 48136*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)}
Theorem	evenm1odd 48137	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd )
Theorem	evenp1odd 48138	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd )
Theorem	oddp1eveni 48139	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even )
Theorem	oddm1eveni 48140	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even )
Theorem	evennodd 48141	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd )
Theorem	oddneven 48142	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even )
Theorem	enege 48143	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even )
Theorem	onego 48144	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd )
Theorem	m1expevenALTV 48145	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 48146	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 48147	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}
Theorem	dfodd3 48148	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
Theorem	iseven2 48149	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 48150	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 48151	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)
Theorem	m2even 48152	A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )
Theorem	2ndvdsodd 48153	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)
Theorem	2dvdsoddp1 48154	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))
Theorem	2dvdsoddm1 48155	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 48156	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}
Theorem	dfodd4 48157	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1}
Theorem	dfodd5 48158	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0}
Theorem	zefldiv2ALTV 48159	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 48160	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 48161	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 48162	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 48163	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 48164	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2}
Theorem	dfodd7 48165	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1}
Theorem	gcd2odd1 48166	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 48165 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 48167	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 48168	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd ))
Theorem	zeo2ALTV 48169	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 48170	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 48171	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 48172*	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 48173	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 48174	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 48175	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 48176	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 48177	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd ))
Theorem	bits0eALTV 48178	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 48179	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 48180	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 48181	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 48182	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 48183	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 48184	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 48185	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 48186	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∈ Even
Theorem	0noddALTV 48187	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∉ Odd
Theorem	1oddALTV 48188	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∈ Odd
Theorem	1nevenALTV 48189	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∉ Even
Theorem	2evenALTV 48190	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∈ Even
Theorem	2noddALTV 48191	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∉ Odd
Theorem	nn0o1gt2ALTV 48192	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 48193	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 48194	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 48195	An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.)
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0)
Theorem	nneven 48196	An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.)
⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ)
Theorem	nn0onn0exALTV 48197*	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 48198*	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 48199*	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 48200	2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.)
⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ Even )