P. 477 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 47601-47700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	139prmALT 47601	139 is a prime number. In contrast to 139prm 17101, the proof of this theorem uses 3dvds2dec 16310 for checking the divisibility by 3. Although the proof using 3dvds2dec 16310 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17101), the number of essential steps is smaller (301 compared with 327 for 139prm 17101). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ;;139 ∈ ℙ
Theorem	31prm 47602	31 is a prime number. In contrast to 37prm 17098, the proof of this theorem is not based on the "blanket" prmlem2 17097, but on isprm7 16685. Although the checks for non-divisibility by the primes 7 to 23 are not needed, the proof is much longer (regarding size) than the proof of 37prm 17098 (1810 characters compared with 1213 for 37prm 17098). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17098). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.)
⊢ ;31 ∈ ℙ
Theorem	m5prm 47603	The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.)
⊢ ((2↑5) − 1) ∈ ℙ
Theorem	127prm 47604	127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.)
⊢ ;;127 ∈ ℙ
Theorem	m7prm 47605	The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑7) − 1) ∈ ℙ
Theorem	m11nprm 47606	The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑;11) − 1) = (;89 · ;23)
Theorem	mod42tp1mod8 47607	If a number is 3 modulo 4, twice the number plus 1 is 7 modulo 8. (Contributed by AV, 19-Aug-2021.)
⊢ ((𝑁 ∈ ℤ ∧ (𝑁 mod 4) = 3) → (((2 · 𝑁) + 1) mod 8) = 7)
Theorem	sfprmdvdsmersenne 47608	If 𝑄 is a safe prime (i.e. 𝑄 = ((2 · 𝑃) + 1) for a prime 𝑃) with 𝑄≡7 (mod 8), then 𝑄 divides the 𝑃-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑄 ∈ ℙ ∧ (𝑄 mod 8) = 7 ∧ 𝑄 = ((2 · 𝑃) + 1))) → 𝑄 ∥ ((2↑𝑃) − 1))
Theorem	sgprmdvdsmersenne 47609	If 𝑃 is a Sophie Germain prime (i.e. 𝑄 = ((2 · 𝑃) + 1) is also prime) with 𝑃≡3 (mod 4), then 𝑄 divides the 𝑃-th Mersenne number MP. (Contributed by AV, 20-Aug-2021.)
⊢ (((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 3) ∧ (𝑄 = ((2 · 𝑃) + 1) ∧ 𝑄 ∈ ℙ)) → 𝑄 ∥ ((2↑𝑃) − 1))
Theorem	lighneallem1 47610	Lemma 1 for lighneal 47616. (Contributed by AV, 11-Aug-2021.)
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀))
Theorem	lighneallem2 47611	Lemma 2 for lighneal 47616. (Contributed by AV, 13-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem3 47612	Lemma 3 for lighneal 47616. (Contributed by AV, 11-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem4a 47613	Lemma 1 for lighneallem4 47615. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆)
Theorem	lighneallem4b 47614*	Lemma 2 for lighneallem4 47615. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2))
Theorem	lighneallem4 47615	Lemma 3 for lighneal 47616. (Contributed by AV, 16-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneal 47616	If a power of a prime 𝑃 (i.e. 𝑃↑𝑀) is of the form 2↑𝑁 − 1, then 𝑁 must be prime and 𝑀 must be 1. Generalization of mersenne 27145 (where 𝑀 = 1 is a prerequisite). Theorem of S. Ligh and L. Neal (1974) "A note on Mersenne mumbers", Mathematics Magazine, 47:4, 231-233. (Contributed by AV, 16-Aug-2021.)
⊢ (((𝑃 ∈ ℙ ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → (𝑀 = 1 ∧ 𝑁 ∈ ℙ))
21.48.12.3  Proth's theorem
Theorem	modexp2m1d 47617	The square of an integer which is -1 modulo a number greater than 1 is 1 modulo the same modulus. (Contributed by AV, 5-Jul-2020.)
⊢ (𝜑 → 𝐴 ∈ ℤ)    &   ⊢ (𝜑 → 𝐸 ∈ ℝ+)    &   ⊢ (𝜑 → 1 < 𝐸)    &   ⊢ (𝜑 → (𝐴 mod 𝐸) = (-1 mod 𝐸))    ⇒   ⊢ (𝜑 → ((𝐴↑2) mod 𝐸) = 1)
Theorem	proththdlem 47618	Lemma for proththd 47619. (Contributed by AV, 4-Jul-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))    ⇒   ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ))
Theorem	proththd 47619*	Proth's theorem (1878). If P is a Proth number, i.e. a number of the form k2^n+1 with k less than 2^n, and if there exists an integer x for which x^((P-1)/2) is -1 modulo P, then P is prime. Such a prime is called a Proth prime. Like Pocklington's theorem (see pockthg 16884), Proth's theorem allows for a convenient method for verifying large primes. (Contributed by AV, 5-Jul-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))    &   ⊢ (𝜑 → 𝐾 < (2↑𝑁))    &   ⊢ (𝜑 → ∃𝑥 ∈ ℤ ((𝑥↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ℙ)
Theorem	5tcu2e40 47620	5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.)
⊢ (5 · (2↑3)) = ;40
Theorem	3exp4mod41 47621	3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.)
⊢ ((3↑4) mod ;41) = (-1 mod ;41)
Theorem	41prothprmlem1 47622	Lemma 1 for 41prothprm 47624. (Contributed by AV, 4-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((𝑃 − 1) / 2) = ;20
Theorem	41prothprmlem2 47623	Lemma 2 for 41prothprm 47624. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)
Theorem	41prothprm 47624	41 is a Proth prime. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ)
21.48.12.4  Solutions of quadratic equations
Theorem	quad1 47625*	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 47626*	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 47627*	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 47628*	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 47631 and df-odd 47632. Alternate definitions resp. characterizations are provided in dfeven2 47654, dfeven3 47663, dfeven4 47643 and in dfodd2 47641, dfodd3 47655, dfodd4 47664, dfodd5 47665, dfodd6 47642. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 47642 in opoeALTV 47688 and dfodd3 47655 in oddprmALTV 47692. 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 47687 and divgcdodd 16687).
21.48.13.1  Definitions and basic properties
Syntax	ceven 47629	Extend the definition of a class to include the set of even numbers.
class Even
Syntax	codd 47630	Extend the definition of a class to include the set of odd numbers.
class Odd
Definition	df-even 47631	Define the set of even numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
Definition	df-odd 47632	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
Theorem	iseven 47633	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 47634	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 47635	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)
Theorem	oddz 47636	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
Theorem	evendiv2z 47637	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ)
Theorem	oddp1div2z 47638	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 47639	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 47640	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 47641	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ}
Theorem	dfodd6 47642*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)}
Theorem	dfeven4 47643*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)}
Theorem	evenm1odd 47644	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd )
Theorem	evenp1odd 47645	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd )
Theorem	oddp1eveni 47646	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even )
Theorem	oddm1eveni 47647	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even )
Theorem	evennodd 47648	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd )
Theorem	oddneven 47649	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even )
Theorem	enege 47650	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even )
Theorem	onego 47651	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd )
Theorem	m1expevenALTV 47652	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 47653	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 47654	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}
Theorem	dfodd3 47655	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
Theorem	iseven2 47656	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 47657	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 47658	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)
Theorem	m2even 47659	A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )
Theorem	2ndvdsodd 47660	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)
Theorem	2dvdsoddp1 47661	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))
Theorem	2dvdsoddm1 47662	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 47663	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}
Theorem	dfodd4 47664	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1}
Theorem	dfodd5 47665	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0}
Theorem	zefldiv2ALTV 47666	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 47667	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 47668	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 47669	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 47670	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 47671	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2}
Theorem	dfodd7 47672	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1}
Theorem	gcd2odd1 47673	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 47672 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 47674	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 47675	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd ))
Theorem	zeo2ALTV 47676	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 47677	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 47678	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 47679*	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 47680	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 47681	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 47682	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 47683	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 47684	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd ))
Theorem	bits0eALTV 47685	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 47686	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 47687	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 47688	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 47689	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 47690	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 47691	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 47692	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 47693	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∈ Even
Theorem	0noddALTV 47694	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∉ Odd
Theorem	1oddALTV 47695	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∈ Odd
Theorem	1nevenALTV 47696	1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∉ Even
Theorem	2evenALTV 47697	2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∈ Even
Theorem	2noddALTV 47698	2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 2 ∉ Odd
Theorem	nn0o1gt2ALTV 47699	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 47700	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) ∈ ℕ)