Home | Metamath
Proof Explorer Theorem List (p. 439 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44955) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 2pwp1prmfmtno 43801* | Every prime number of the form ((2↑𝑘) + 1) must be a Fermat number. (Contributed by AV, 7-Aug-2021.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝑃 = ((2↑𝐾) + 1) ∧ 𝑃 ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝑃 = (FermatNo‘𝑛)) | ||
"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 25803. 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 43815. This is an example of sgprmdvdsmersenne 43818, 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 43818. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 43817, 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 43825. | ||
Theorem | m2prm 43802 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑2) − 1) ∈ ℙ | ||
Theorem | m3prm 43803 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑3) − 1) ∈ ℙ | ||
Theorem | 2exp5 43804 | Two to the fifth power is 32. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑5) = ;32 | ||
Theorem | flsqrt 43805 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
Theorem | flsqrt5 43806 | 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 43807 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
⊢ ¬ 3 ∥ 4 | ||
Theorem | 139prmALT 43808 | 139 is a prime number. In contrast to 139prm 16457, the proof of this theorem uses 3dvds2dec 15682 for checking the divisibility by 3. Although the proof using 3dvds2dec 15682 is longer (regarding size: 1849 characters compared with 1809 for 139prm 16457), the number of essential steps is smaller (301 compared with 327 for 139prm 16457). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 31prm 43809 | 31 is a prime number. In contrast to 37prm 16454, the proof of this theorem is not based on the "blanket" prmlem2 16453, but on isprm7 16052. 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 16454 (1810 characters compared with 1213 for 37prm 16454). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 16454). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
⊢ ;31 ∈ ℙ | ||
Theorem | m5prm 43810 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
⊢ ((2↑5) − 1) ∈ ℙ | ||
Theorem | 2exp7 43811 | Two to the seventh power is 128. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑7) = ;;128 | ||
Theorem | 127prm 43812 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ ;;127 ∈ ℙ | ||
Theorem | m7prm 43813 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑7) − 1) ∈ ℙ | ||
Theorem | 2exp11 43814 | Two to the eleventh power is 2048. (Contributed by AV, 16-Aug-2021.) |
⊢ (2↑;11) = ;;;2048 | ||
Theorem | m11nprm 43815 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
Theorem | mod42tp1mod8 43816 | 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 43817 | 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 43818 | 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 43819 | Lemma 1 for lighneal 43825. (Contributed by AV, 11-Aug-2021.) |
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
Theorem | lighneallem2 43820 | Lemma 2 for lighneal 43825. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem3 43821 | Lemma 3 for lighneal 43825. (Contributed by AV, 11-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem4a 43822 | Lemma 1 for lighneallem4 43824. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
Theorem | lighneallem4b 43823* | Lemma 2 for lighneallem4 43824. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
Theorem | lighneallem4 43824 | Lemma 3 for lighneal 43825. (Contributed by AV, 16-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneal 43825 | 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 25803 (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 ∧ 𝑁 ∈ ℙ)) | ||
Theorem | modexp2m1d 43826 | 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 43827 | Lemma for proththd 43828. (Contributed by AV, 4-Jul-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
Theorem | proththd 43828* | 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 16242), 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 43829 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
⊢ (5 · (2↑3)) = ;40 | ||
Theorem | 3exp4mod41 43830 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 43831 | Lemma 1 for 41prothprm 43833. (Contributed by AV, 4-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 43832 | Lemma 2 for 41prothprm 43833. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
Theorem | 41prothprm 43833 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
Theorem | quad1 43834* | 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 43835* | 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 43836* | 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 43837* | 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 < 𝐷)) | ||
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 43840 and df-odd 43841. Alternate definitions resp. characterizations are provided in dfeven2 43863, dfeven3 43872, dfeven4 43852 and in dfodd2 43850, dfodd3 43864, dfodd4 43873, dfodd5 43874, dfodd6 43851. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 43851 in opoeALTV 43897 and dfodd3 43864 in oddprmALTV 43901. 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 43896 and divgcdodd 16054). | ||
Syntax | ceven 43838 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 43839 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 43840 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
Definition | df-odd 43841 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
Theorem | iseven 43842 | 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 43843 | 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 43844 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
Theorem | oddz 43845 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
Theorem | evendiv2z 43846 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
Theorem | oddp1div2z 43847 | 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 43848 | 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 43849 | 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 43850 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
Theorem | dfodd6 43851* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
Theorem | dfeven4 43852* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
Theorem | evenm1odd 43853 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
Theorem | evenp1odd 43854 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
Theorem | oddp1eveni 43855 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
Theorem | oddm1eveni 43856 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
Theorem | evennodd 43857 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
Theorem | oddneven 43858 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
Theorem | enege 43859 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
Theorem | onego 43860 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
Theorem | m1expevenALTV 43861 | 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 43862 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
Theorem | dfeven2 43863 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} | ||
Theorem | dfodd3 43864 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
Theorem | iseven2 43865 | 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 43866 | 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 43867 | 2 divides an even number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍) | ||
Theorem | m2even 43868 | A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.) |
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even ) | ||
Theorem | 2ndvdsodd 43869 | 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍) | ||
Theorem | 2dvdsoddp1 43870 | 2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1)) | ||
Theorem | 2dvdsoddm1 43871 | 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1)) | ||
Theorem | dfeven3 43872 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0} | ||
Theorem | dfodd4 43873 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1} | ||
Theorem | dfodd5 43874 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0} | ||
Theorem | zefldiv2ALTV 43875 | 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 43876 | 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 43877 | 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)) | ||
Theorem | iseven5 43878 | 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 43879 | 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 43880 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2} | ||
Theorem | dfodd7 43881 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1} | ||
Theorem | gcd2odd1 43882 | 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 43881 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.) |
⊢ (𝑍 ∈ Odd → (𝑍 gcd 2) = 1) | ||
Theorem | zneoALTV 43883 | 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 43884 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd )) | ||
Theorem | zeo2ALTV 43885 | 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 43886 | 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 43887 | A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.) (Revised by AV, 19-Jun-2020.) |
⊢ 𝑁 ∈ ℕ ⇒ ⊢ (𝑁 ∈ Even ↔ ¬ 𝑁 ∈ Odd ) | ||
Theorem | odd2np1ALTV 43888* | 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 43889 | 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 43890 | 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 43891 | 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 43892 | 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 43893 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd )) | ||
Theorem | bits0eALTV 43894 | 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 43895 | 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 43896 | 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 43897 | 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 43898 | 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 43899 | 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 43900 | 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 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |