![]() |
Metamath
Proof Explorer Theorem List (p. 476 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | fmtnofz04prm 47501 | The first five Fermat numbers are prime, see remark in [ApostolNT] p. 7. (Contributed by AV, 28-Jul-2021.) |
⊢ (𝑁 ∈ (0...4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtnole4prm 47502 | The first five Fermat numbers are prime. (Contributed by AV, 28-Jul-2021.) |
⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ≤ 4) → (FermatNo‘𝑁) ∈ ℙ) | ||
Theorem | fmtno5faclem1 47503 | Lemma 1 for fmtno5fac 47506. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 4) = ;;;;;;;26801668 | ||
Theorem | fmtno5faclem2 47504 | Lemma 2 for fmtno5fac 47506. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;6700417 · 6) = ;;;;;;;40202502 | ||
Theorem | fmtno5faclem3 47505 | Lemma 3 for fmtno5fac 47506. (Contributed by AV, 22-Jul-2021.) |
⊢ (;;;;;;;;402025020 + ;;;;;;;26801668) = ;;;;;;;;428826688 | ||
Theorem | fmtno5fac 47506 | The factorization of the 5 th Fermat number, see remark in [ApostolNT] p. 7. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) = (;;;;;;6700417 · ;;641) | ||
Theorem | fmtno5nprm 47507 | The 5 th Fermat number is a not a prime. (Contributed by AV, 22-Jul-2021.) |
⊢ (FermatNo‘5) ∉ ℙ | ||
Theorem | prmdvdsfmtnof1lem1 47508* | Lemma 1 for prmdvdsfmtnof1 47511. (Contributed by AV, 3-Aug-2021.) |
⊢ 𝐼 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐹}, ℝ, < ) & ⊢ 𝐽 = inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝐺}, ℝ, < ) ⇒ ⊢ ((𝐹 ∈ (ℤ≥‘2) ∧ 𝐺 ∈ (ℤ≥‘2)) → (𝐼 = 𝐽 → (𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺))) | ||
Theorem | prmdvdsfmtnof1lem2 47509 | Lemma 2 for prmdvdsfmtnof1 47511. (Contributed by AV, 3-Aug-2021.) |
⊢ ((𝐹 ∈ ran FermatNo ∧ 𝐺 ∈ ran FermatNo) → ((𝐼 ∈ ℙ ∧ 𝐼 ∥ 𝐹 ∧ 𝐼 ∥ 𝐺) → 𝐹 = 𝐺)) | ||
Theorem | prmdvdsfmtnof 47510* | The mapping of a Fermat number to its smallest prime factor is a function. (Contributed by AV, 4-Aug-2021.) (Proof shortened by II, 16-Feb-2023.) |
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < )) ⇒ ⊢ 𝐹:ran FermatNo⟶ℙ | ||
Theorem | prmdvdsfmtnof1 47511* | The mapping of a Fermat number to its smallest prime factor is a one-to-one function. (Contributed by AV, 4-Aug-2021.) |
⊢ 𝐹 = (𝑓 ∈ ran FermatNo ↦ inf({𝑝 ∈ ℙ ∣ 𝑝 ∥ 𝑓}, ℝ, < )) ⇒ ⊢ 𝐹:ran FermatNo–1-1→ℙ | ||
Theorem | prminf2 47512 | The set of prime numbers is infinite. The proof of this variant of prminf 16948 is based on Goldbach's theorem goldbachth 47471 (via prmdvdsfmtnof1 47511 and prmdvdsfmtnof1lem2 47509), see Wikipedia "Fermat number", 4-Aug-2021, https://en.wikipedia.org/wiki/Fermat_number#Basic_properties 47509. (Contributed by AV, 4-Aug-2021.) |
⊢ ℙ ∉ Fin | ||
Theorem | 2pwp1prm 47513* | For ((2↑𝑘) + 1) to be prime, 𝑘 must be a power of 2, see Wikipedia "Fermat number", section "Other theorms about Fermat numbers", https://en.wikipedia.org/wiki/Fermat_number, 5-Aug-2021. (Contributed by AV, 7-Aug-2021.) |
⊢ ((𝐾 ∈ ℕ ∧ ((2↑𝐾) + 1) ∈ ℙ) → ∃𝑛 ∈ ℕ0 𝐾 = (2↑𝑛)) | ||
Theorem | 2pwp1prmfmtno 47514* | 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 27285. 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 47525. This is an example of sgprmdvdsmersenne 47528, 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 47528. Hence, 11 is a Sophie Germain prime and 2x11+1=23 is its associated safe prime. By sfprmdvdsmersenne 47527, 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 47535. | ||
Theorem | m2prm 47515 | The second Mersenne number M2 = 3 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑2) − 1) ∈ ℙ | ||
Theorem | m3prm 47516 | The third Mersenne number M3 = 7 is a prime number. (Contributed by AV, 16-Aug-2021.) |
⊢ ((2↑3) − 1) ∈ ℙ | ||
Theorem | flsqrt 47517 | A condition equivalent to the floor of a square root. (Contributed by AV, 17-Aug-2021.) |
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ 𝐵 ∈ ℕ0) → ((⌊‘(√‘𝐴)) = 𝐵 ↔ ((𝐵↑2) ≤ 𝐴 ∧ 𝐴 < ((𝐵 + 1)↑2)))) | ||
Theorem | flsqrt5 47518 | 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 47519 | 3 does not divide 4. (Contributed by AV, 18-Aug-2021.) |
⊢ ¬ 3 ∥ 4 | ||
Theorem | 139prmALT 47520 | 139 is a prime number. In contrast to 139prm 17157, the proof of this theorem uses 3dvds2dec 16366 for checking the divisibility by 3. Although the proof using 3dvds2dec 16366 is longer (regarding size: 1849 characters compared with 1809 for 139prm 17157), the number of essential steps is smaller (301 compared with 327 for 139prm 17157). (Contributed by Mario Carneiro, 19-Feb-2014.) (Revised by AV, 18-Aug-2021.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ ;;139 ∈ ℙ | ||
Theorem | 31prm 47521 | 31 is a prime number. In contrast to 37prm 17154, the proof of this theorem is not based on the "blanket" prmlem2 17153, but on isprm7 16741. 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 17154 (1810 characters compared with 1213 for 37prm 17154). The number of essential steps, however, is much smaller (138 compared with 213 for 37prm 17154). (Contributed by AV, 17-Aug-2021.) (Proof modification is discouraged.) |
⊢ ;31 ∈ ℙ | ||
Theorem | m5prm 47522 | The fifth Mersenne number M5 = 31 is a prime number. (Contributed by AV, 17-Aug-2021.) |
⊢ ((2↑5) − 1) ∈ ℙ | ||
Theorem | 127prm 47523 | 127 is a prime number. (Contributed by AV, 16-Aug-2021.) (Proof shortened by AV, 16-Sep-2021.) |
⊢ ;;127 ∈ ℙ | ||
Theorem | m7prm 47524 | The seventh Mersenne number M7 = 127 is a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑7) − 1) ∈ ℙ | ||
Theorem | m11nprm 47525 | The eleventh Mersenne number M11 = 2047 is not a prime number. (Contributed by AV, 18-Aug-2021.) |
⊢ ((2↑;11) − 1) = (;89 · ;23) | ||
Theorem | mod42tp1mod8 47526 | 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 47527 | 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 47528 | 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 47529 | Lemma 1 for lighneal 47535. (Contributed by AV, 11-Aug-2021.) |
⊢ ((𝑃 = 2 ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) → ((2↑𝑁) − 1) ≠ (𝑃↑𝑀)) | ||
Theorem | lighneallem2 47530 | Lemma 2 for lighneal 47535. (Contributed by AV, 13-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ 2 ∥ 𝑁 ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem3 47531 | Lemma 3 for lighneal 47535. (Contributed by AV, 11-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneallem4a 47532 | Lemma 1 for lighneallem4 47534. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘3) ∧ 𝑆 = (((𝐴↑𝑀) + 1) / (𝐴 + 1))) → 2 ≤ 𝑆) | ||
Theorem | lighneallem4b 47533* | Lemma 2 for lighneallem4 47534. (Contributed by AV, 16-Aug-2021.) |
⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ (ℤ≥‘2) ∧ ¬ 2 ∥ 𝑀) → Σ𝑘 ∈ (0...(𝑀 − 1))((-1↑𝑘) · (𝐴↑𝑘)) ∈ (ℤ≥‘2)) | ||
Theorem | lighneallem4 47534 | Lemma 3 for lighneal 47535. (Contributed by AV, 16-Aug-2021.) |
⊢ (((𝑃 ∈ (ℙ ∖ {2}) ∧ 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (¬ 2 ∥ 𝑁 ∧ ¬ 2 ∥ 𝑀) ∧ ((2↑𝑁) − 1) = (𝑃↑𝑀)) → 𝑀 = 1) | ||
Theorem | lighneal 47535 | 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 27285 (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 47536 | 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 47537 | Lemma for proththd 47538. (Contributed by AV, 4-Jul-2020.) |
⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 = ((𝐾 · (2↑𝑁)) + 1)) ⇒ ⊢ (𝜑 → (𝑃 ∈ ℕ ∧ 1 < 𝑃 ∧ ((𝑃 − 1) / 2) ∈ ℕ)) | ||
Theorem | proththd 47538* | 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 16939), 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 47539 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
⊢ (5 · (2↑3)) = ;40 | ||
Theorem | 3exp4mod41 47540 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
Theorem | 41prothprmlem1 47541 | Lemma 1 for 41prothprm 47543. (Contributed by AV, 4-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
Theorem | 41prothprmlem2 47542 | Lemma 2 for 41prothprm 47543. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
Theorem | 41prothprm 47543 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
Theorem | quad1 47544* | 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 47545* | 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 47546* | 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 47547* | 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 47550 and df-odd 47551. Alternate definitions resp. characterizations are provided in dfeven2 47573, dfeven3 47582, dfeven4 47562 and in dfodd2 47560, dfodd3 47574, dfodd4 47583, dfodd5 47584, dfodd6 47561. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 47561 in opoeALTV 47607 and dfodd3 47574 in oddprmALTV 47611. 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 47606 and divgcdodd 16743). | ||
Syntax | ceven 47548 | Extend the definition of a class to include the set of even numbers. |
class Even | ||
Syntax | codd 47549 | Extend the definition of a class to include the set of odd numbers. |
class Odd | ||
Definition | df-even 47550 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
Definition | df-odd 47551 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
Theorem | iseven 47552 | 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 47553 | 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 47554 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
Theorem | oddz 47555 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
Theorem | evendiv2z 47556 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
Theorem | oddp1div2z 47557 | 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 47558 | 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 47559 | 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 47560 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
Theorem | dfodd6 47561* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
Theorem | dfeven4 47562* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
Theorem | evenm1odd 47563 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
Theorem | evenp1odd 47564 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
Theorem | oddp1eveni 47565 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
Theorem | oddm1eveni 47566 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
Theorem | evennodd 47567 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
Theorem | oddneven 47568 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
Theorem | enege 47569 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
Theorem | onego 47570 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
Theorem | m1expevenALTV 47571 | 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 47572 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
Theorem | dfeven2 47573 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} | ||
Theorem | dfodd3 47574 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
Theorem | iseven2 47575 | 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 47576 | 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 47577 | 2 divides an even number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Even → 2 ∥ 𝑍) | ||
Theorem | m2even 47578 | A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.) |
⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even ) | ||
Theorem | 2ndvdsodd 47579 | 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍) | ||
Theorem | 2dvdsoddp1 47580 | 2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1)) | ||
Theorem | 2dvdsoddm1 47581 | 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.) |
⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1)) | ||
Theorem | dfeven3 47582 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0} | ||
Theorem | dfodd4 47583 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1} | ||
Theorem | dfodd5 47584 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0} | ||
Theorem | zefldiv2ALTV 47585 | 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 47586 | 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 47587 | 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 47588 | 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 47589 | 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 47590 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2} | ||
Theorem | dfodd7 47591 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) |
⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1} | ||
Theorem | gcd2odd1 47592 | 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 47591 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.) |
⊢ (𝑍 ∈ Odd → (𝑍 gcd 2) = 1) | ||
Theorem | zneoALTV 47593 | 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 47594 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) |
⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd )) | ||
Theorem | zeo2ALTV 47595 | 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 47596 | 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 47597 | 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 47598* | 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 47599 | 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 47600 | 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 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |