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
21.48.12.2  Mersenne primes "In mathematics, a Mersenne prime is a prime number that is one less than a power of two. That is, it is a prime number of the form Mn = 2^n-1 for some integer n. They are named after Marin Mersenne ... If n is a composite number then so is 2^n-1. Therefore, an equivalent definition of the Mersenne primes is that they are the prime numbers of the form Mp = 2^p-1 for some prime p.", see Wikipedia "Mersenne prime", 16-Aug-2021, https://en.wikipedia.org/wiki/Mersenne_prime. See also definition in [ApostolNT] p. 4. This means that if Mn = 2^n-1 is prime, than n must be prime, too, see mersenne 27158. The reverse direction is not generally valid: If p is prime, then Mp = 2^p-1 needs not be prime, e.g. M11 = 2047 = 23 x 89, see m11nprm 47611. This is an example of sgprmdvdsmersenne 47614, stating that if p with p = 3 modulo 4 (here 11) and q=2p+1 (here 23) are prime, then q divides Mp. "In number theory, a prime number p is a Sophie Germain prime if 2p+1 is also prime. The number 2p+1 associated with a Sophie Germain prime is called a safe prime.", see Wikipedia "Safe and Sophie Germain primes", 21-Aug-2021, https://en.wikipedia.org/wiki/Safe_and_Sophie_Germain_primes 47614. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 47613, it is shown that if a safe prime q is congruent to 7 modulo 8, then it is a divisor of the Mersenne number with its matching Sophie Germain prime as exponent. The main result of this section, however, is the formal proof of a theorem of S. Ligh and L. Neal in "A note on Mersenne numbers", see lighneal 47621.
Theorem	m2prm 47601	The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑2) − 1) ∈ ℙ
Theorem	m3prm 47602	The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.)
⊢ ((2↑3) − 1) ∈ ℙ
Theorem	flsqrt 47603	A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.)
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2))))
Theorem	flsqrt5 47604	The floor of the square root of a nonnegative number is 5 iff the number is between 25 and 35. (Contributed by AV, 17-Aug-2021.)
⊢ ((𝑋 ∈ ℝ ∧ 0 ≤ 𝑋) → ((;25 ≤ 𝑋 ∧ 𝑋 < ;36) ↔ (⌊‘(√‘𝑋)) = 5))
Theorem	3ndvds4 47605	3 does not divide 4. (Contributed by AV, 18-Aug-2021.)
⊢ ¬ 3 ∥ 4
Theorem	139prmALT 47606	139 is a prime number. In contrast to 139prm 17027, the proof of this theorem uses 3dvds2dec 16236 for checking the divisibility by 3. Although the proof using 3dvds2dec 16236 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17027), the number of essential steps is smaller (301 compared with 327 for 139prm 17027). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ ;;139 ∈ ℙ
Theorem	31prm 47607	31 is a prime number. In contrast to 37prm 17024, the proof of this theorem is not based on the "blanket" prmlem2 17023, but on isprm7 16611. 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 17024 (1810 characters compared with 1213 for 37prm 17024). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17024). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.)
⊢ ;31 ∈ ℙ
Theorem	m5prm 47608	The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.)
⊢ ((2↑5) − 1) ∈ ℙ
Theorem	127prm 47609	127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.)
⊢ ;;127 ∈ ℙ
Theorem	m7prm 47610	The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑7) − 1) ∈ ℙ
Theorem	m11nprm 47611	The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.)
⊢ ((2↑;11) − 1) = (;89 · ;23)
Theorem	mod42tp1mod8 47612	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 47613	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 47614	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 47615	Lemma 1 for lighneal 47621. (Contributed by AV, 11-Aug-2021.)
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀))
Theorem	lighneallem2 47616	Lemma 2 for lighneal 47621. (Contributed by AV, 13-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem3 47617	Lemma 3 for lighneal 47621. (Contributed by AV, 11-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneallem4a 47618	Lemma 1 for lighneallem4 47620. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆)
Theorem	lighneallem4b 47619*	Lemma 2 for lighneallem4 47620. (Contributed by AV, 16-Aug-2021.)
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2))
Theorem	lighneallem4 47620	Lemma 3 for lighneal 47621. (Contributed by AV, 16-Aug-2021.)
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1)
Theorem	lighneal 47621	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 27158 (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 47622	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 47623	Lemma for proththd 47624. (Contributed by AV, 4-Jul-2020.)
⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → 𝐾 ∈ ℕ)    &   ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1))    ⇒   ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ))
Theorem	proththd 47624*	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 16810), 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 47625	5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.)
⊢ (5 · (2↑3)) = ;40
Theorem	3exp4mod41 47626	3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.)
⊢ ((3↑4) mod ;41) = (-1 mod ;41)
Theorem	41prothprmlem1 47627	Lemma 1 for 41prothprm 47629. (Contributed by AV, 4-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((𝑃 − 1) / 2) = ;20
Theorem	41prothprmlem2 47628	Lemma 2 for 41prothprm 47629. (Contributed by AV, 5-Jul-2020.)
⊢ 𝑃 = ;41    ⇒   ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃)
Theorem	41prothprm 47629	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 47630*	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 47631*	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 47632*	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 47633*	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 47636 and df-odd 47637. Alternate definitions resp. characterizations are provided in dfeven2 47659, dfeven3 47668, dfeven4 47648 and in dfodd2 47646, dfodd3 47660, dfodd4 47669, dfodd5 47670, dfodd6 47647. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 47647 in opoeALTV 47693 and dfodd3 47660 in oddprmALTV 47697. 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 47692 and divgcdodd 16613).
21.48.13.1  Definitions and basic properties
Syntax	ceven 47634	Extend the definition of a class to include the set of even numbers.
class Even
Syntax	codd 47635	Extend the definition of a class to include the set of odd numbers.
class Odd
Definition	df-even 47636	Define the set of even numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ}
Definition	df-odd 47637	Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ}
Theorem	iseven 47638	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 47639	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 47640	An even number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ)
Theorem	oddz 47641	An odd number is an integer. (Contributed by AV, 14-Jun-2020.)
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ)
Theorem	evendiv2z 47642	The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ)
Theorem	oddp1div2z 47643	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 47644	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 47645	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 47646	Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ}
Theorem	dfodd6 47647*	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)}
Theorem	dfeven4 47648*	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)}
Theorem	evenm1odd 47649	The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd )
Theorem	evenp1odd 47650	The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd )
Theorem	oddp1eveni 47651	The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even )
Theorem	oddm1eveni 47652	The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.)
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even )
Theorem	evennodd 47653	An even number is not an odd number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd )
Theorem	oddneven 47654	An odd number is not an even number. (Contributed by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even )
Theorem	enege 47655	The negative of an even number is even. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even )
Theorem	onego 47656	The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.)
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd )
Theorem	m1expevenALTV 47657	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 47658	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 47659	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧}
Theorem	dfodd3 47660	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧}
Theorem	iseven2 47661	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 47662	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 47663	2 divides an even number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍)
Theorem	m2even 47664	A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.)
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even )
Theorem	2ndvdsodd 47665	2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍)
Theorem	2dvdsoddp1 47666	2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.)
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1))
Theorem	2dvdsoddm1 47667	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 47668	Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0}
Theorem	dfodd4 47669	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1}
Theorem	dfodd5 47670	Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0}
Theorem	zefldiv2ALTV 47671	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 47672	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 47673	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 47674	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 47675	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 47676	Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2}
Theorem	dfodd7 47677	Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.)
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1}
Theorem	gcd2odd1 47678	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 47677 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 47679	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 47680	An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.)
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd ))
Theorem	zeo2ALTV 47681	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 47682	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 47683	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 47684*	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 47685	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 47686	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 47687	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 47688	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 47689	Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.)
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd ))
Theorem	bits0eALTV 47690	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 47691	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 47692	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 47693	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 47694	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 47695	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 47696	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 47697	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 47698	0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∈ Even
Theorem	0noddALTV 47699	0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.)
⊢ 0 ∉ Odd
Theorem	1oddALTV 47700	1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.)
⊢ 1 ∈ Odd