| Metamath
Proof Explorer Theorem List (p. 477 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | proththd 47601* | 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 16944), 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 47602 | 5 times the cube of 2 is 40. (Contributed by AV, 4-Jul-2020.) |
| ⊢ (5 · (2↑3)) = ;40 | ||
| Theorem | 3exp4mod41 47603 | 3 to the fourth power is -1 modulo 41. (Contributed by AV, 5-Jul-2020.) |
| ⊢ ((3↑4) mod ;41) = (-1 mod ;41) | ||
| Theorem | 41prothprmlem1 47604 | Lemma 1 for 41prothprm 47606. (Contributed by AV, 4-Jul-2020.) |
| ⊢ 𝑃 = ;41 ⇒ ⊢ ((𝑃 − 1) / 2) = ;20 | ||
| Theorem | 41prothprmlem2 47605 | Lemma 2 for 41prothprm 47606. (Contributed by AV, 5-Jul-2020.) |
| ⊢ 𝑃 = ;41 ⇒ ⊢ ((3↑((𝑃 − 1) / 2)) mod 𝑃) = (-1 mod 𝑃) | ||
| Theorem | 41prothprm 47606 | 41 is a Proth prime. (Contributed by AV, 5-Jul-2020.) |
| ⊢ 𝑃 = ;41 ⇒ ⊢ (𝑃 = ((5 · (2↑3)) + 1) ∧ 𝑃 ∈ ℙ) | ||
| Theorem | quad1 47607* | 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 47608* | 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 47609* | 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 47610* | 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 47613 and df-odd 47614. Alternate definitions resp. characterizations are provided in dfeven2 47636, dfeven3 47645, dfeven4 47625 and in dfodd2 47623, dfodd3 47637, dfodd4 47646, dfodd5 47647, dfodd6 47624. Each characterization can be useful (and used) in an appropriate context, e.g. dfodd6 47624 in opoeALTV 47670 and dfodd3 47637 in oddprmALTV 47674. 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 47669 and divgcdodd 16747). | ||
| Syntax | ceven 47611 | Extend the definition of a class to include the set of even numbers. |
| class Even | ||
| Syntax | codd 47612 | Extend the definition of a class to include the set of odd numbers. |
| class Odd | ||
| Definition | df-even 47613 | Define the set of even numbers. (Contributed by AV, 14-Jun-2020.) |
| ⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 / 2) ∈ ℤ} | ||
| Definition | df-odd 47614 | Define the set of odd numbers. (Contributed by AV, 14-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 + 1) / 2) ∈ ℤ} | ||
| Theorem | iseven 47615 | 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 47616 | 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 47617 | An even number is an integer. (Contributed by AV, 14-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → 𝑍 ∈ ℤ) | ||
| Theorem | oddz 47618 | An odd number is an integer. (Contributed by AV, 14-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → 𝑍 ∈ ℤ) | ||
| Theorem | evendiv2z 47619 | The result of dividing an even number by 2 is an integer. (Contributed by AV, 15-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → (𝑍 / 2) ∈ ℤ) | ||
| Theorem | oddp1div2z 47620 | 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 47621 | 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 47622 | 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 47623 | Alternate definition for odd numbers. (Contributed by AV, 15-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ ((𝑧 − 1) / 2) ∈ ℤ} | ||
| Theorem | dfodd6 47624* | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = ((2 · 𝑖) + 1)} | ||
| Theorem | dfeven4 47625* | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Even = {𝑧 ∈ ℤ ∣ ∃𝑖 ∈ ℤ 𝑧 = (2 · 𝑖)} | ||
| Theorem | evenm1odd 47626 | The predecessor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → (𝑍 − 1) ∈ Odd ) | ||
| Theorem | evenp1odd 47627 | The successor of an even number is odd. (Contributed by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → (𝑍 + 1) ∈ Odd ) | ||
| Theorem | oddp1eveni 47628 | The successor of an odd number is even. (Contributed by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → (𝑍 + 1) ∈ Even ) | ||
| Theorem | oddm1eveni 47629 | The predecessor of an odd number is even. (Contributed by AV, 6-Jul-2020.) |
| ⊢ (𝑍 ∈ Odd → (𝑍 − 1) ∈ Even ) | ||
| Theorem | evennodd 47630 | An even number is not an odd number. (Contributed by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → ¬ 𝑍 ∈ Odd ) | ||
| Theorem | oddneven 47631 | An odd number is not an even number. (Contributed by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → ¬ 𝑍 ∈ Even ) | ||
| Theorem | enege 47632 | The negative of an even number is even. (Contributed by AV, 20-Jun-2020.) |
| ⊢ (𝐴 ∈ Even → -𝐴 ∈ Even ) | ||
| Theorem | onego 47633 | The negative of an odd number is odd. (Contributed by AV, 20-Jun-2020.) |
| ⊢ (𝐴 ∈ Odd → -𝐴 ∈ Odd ) | ||
| Theorem | m1expevenALTV 47634 | 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 47635 | Exponentiation of -1 by an odd power. (Contributed by AV, 6-Jul-2020.) |
| ⊢ (𝑁 ∈ Odd → (-1↑𝑁) = -1) | ||
| Theorem | dfeven2 47636 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Even = {𝑧 ∈ ℤ ∣ 2 ∥ 𝑧} | ||
| Theorem | dfodd3 47637 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ ¬ 2 ∥ 𝑧} | ||
| Theorem | iseven2 47638 | 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 47639 | 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 47640 | 2 divides an even number. (Contributed by AV, 18-Jun-2020.) |
| ⊢ (𝑍 ∈ Even → 2 ∥ 𝑍) | ||
| Theorem | m2even 47641 | A multiple of 2 is an even number. (Contributed by AV, 5-Jun-2023.) |
| ⊢ (𝑍 ∈ ℤ → (2 · 𝑍) ∈ Even ) | ||
| Theorem | 2ndvdsodd 47642 | 2 does not divide an odd number. (Contributed by AV, 18-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → ¬ 2 ∥ 𝑍) | ||
| Theorem | 2dvdsoddp1 47643 | 2 divides an odd number increased by 1. (Contributed by AV, 18-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 + 1)) | ||
| Theorem | 2dvdsoddm1 47644 | 2 divides an odd number decreased by 1. (Contributed by AV, 18-Jun-2020.) |
| ⊢ (𝑍 ∈ Odd → 2 ∥ (𝑍 − 1)) | ||
| Theorem | dfeven3 47645 | Alternate definition for even numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Even = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 0} | ||
| Theorem | dfodd4 47646 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) = 1} | ||
| Theorem | dfodd5 47647 | Alternate definition for odd numbers. (Contributed by AV, 18-Jun-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ (𝑧 mod 2) ≠ 0} | ||
| Theorem | zefldiv2ALTV 47648 | 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 47649 | 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 47650 | 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 47651 | 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 47652 | 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 47653 | Alternate definition for even numbers. (Contributed by AV, 1-Jul-2020.) |
| ⊢ Even = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 2} | ||
| Theorem | dfodd7 47654 | Alternate definition for odd numbers. (Contributed by AV, 1-Jul-2020.) |
| ⊢ Odd = {𝑧 ∈ ℤ ∣ (2 gcd 𝑧) = 1} | ||
| Theorem | gcd2odd1 47655 | 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 47654 is longer (see proof in comment)! (Contributed by AV, 5-Jun-2023.) |
| ⊢ (𝑍 ∈ Odd → (𝑍 gcd 2) = 1) | ||
| Theorem | zneoALTV 47656 | 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 47657 | An integer is even or odd. (Contributed by NM, 1-Jan-2006.) (Revised by AV, 16-Jun-2020.) |
| ⊢ (𝑍 ∈ ℤ → (𝑍 ∈ Even ∨ 𝑍 ∈ Odd )) | ||
| Theorem | zeo2ALTV 47658 | 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 47659 | 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 47660 | 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 47661* | 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 47662 | 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 47663 | 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 47664 | 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 47665 | 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 47666 | Value of the zeroth bit. (Contributed by Mario Carneiro, 5-Sep-2016.) (Revised by AV, 19-Jun-2020.) |
| ⊢ (𝑁 ∈ ℤ → (0 ∈ (bits‘𝑁) ↔ 𝑁 ∈ Odd )) | ||
| Theorem | bits0eALTV 47667 | 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 47668 | 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 47669 | 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 47670 | 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 47671 | 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 47672 | 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 47673 | 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 47674 | A prime not equal to 2 is odd. (Contributed by Mario Carneiro, 4-Feb-2015.) (Revised by AV, 21-Jun-2020.) |
| ⊢ (𝑁 ∈ (ℙ ∖ {2}) → 𝑁 ∈ Odd ) | ||
| Theorem | 0evenALTV 47675 | 0 is an even number. (Contributed by AV, 11-Feb-2020.) (Revised by AV, 17-Jun-2020.) |
| ⊢ 0 ∈ Even | ||
| Theorem | 0noddALTV 47676 | 0 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 17-Jun-2020.) |
| ⊢ 0 ∉ Odd | ||
| Theorem | 1oddALTV 47677 | 1 is an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
| ⊢ 1 ∈ Odd | ||
| Theorem | 1nevenALTV 47678 | 1 is not an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
| ⊢ 1 ∉ Even | ||
| Theorem | 2evenALTV 47679 | 2 is an even number. (Contributed by AV, 12-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
| ⊢ 2 ∈ Even | ||
| Theorem | 2noddALTV 47680 | 2 is not an odd number. (Contributed by AV, 3-Feb-2020.) (Revised by AV, 18-Jun-2020.) |
| ⊢ 2 ∉ Odd | ||
| Theorem | nn0o1gt2ALTV 47681 | 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 47682 | 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 47683 | 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 47684 | An alternate characterization of an even nonnegative integer. (Contributed by AV, 22-Jun-2020.) |
| ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ0) | ||
| Theorem | nneven 47685 | An alternate characterization of an even positive integer. (Contributed by AV, 5-Jun-2023.) |
| ⊢ ((𝑁 ∈ ℕ ∧ 𝑁 ∈ Even ) → (𝑁 / 2) ∈ ℕ) | ||
| Theorem | nn0onn0exALTV 47686* | 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 47687* | 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 47688* | 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 47689 | 2 to the power of a positive integer is even. (Contributed by AV, 2-Jun-2020.) (Revised by AV, 20-Jun-2020.) |
| ⊢ (𝑁 ∈ ℕ → (2↑𝑁) ∈ Even ) | ||
| Theorem | epoo 47690 | The sum of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) |
| ⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 + 𝐵) ∈ Odd ) | ||
| Theorem | emoo 47691 | The difference of an even and an odd is odd. (Contributed by AV, 24-Jul-2020.) |
| ⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Odd ) → (𝐴 − 𝐵) ∈ Odd ) | ||
| Theorem | epee 47692 | The sum of two even numbers is even. (Contributed by AV, 21-Jul-2020.) |
| ⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 + 𝐵) ∈ Even ) | ||
| Theorem | emee 47693 | The difference of two even numbers is even. (Contributed by AV, 21-Jul-2020.) |
| ⊢ ((𝐴 ∈ Even ∧ 𝐵 ∈ Even ) → (𝐴 − 𝐵) ∈ Even ) | ||
| Theorem | evensumeven 47694 | If a summand is even, the other summand is even iff the sum is even. (Contributed by AV, 21-Jul-2020.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ Even ) → (𝐴 ∈ Even ↔ (𝐴 + 𝐵) ∈ Even )) | ||
| Theorem | 3odd 47695 | 3 is an odd number. (Contributed by AV, 20-Jul-2020.) |
| ⊢ 3 ∈ Odd | ||
| Theorem | 4even 47696 | 4 is an even number. (Contributed by AV, 23-Jul-2020.) |
| ⊢ 4 ∈ Even | ||
| Theorem | 5odd 47697 | 5 is an odd number. (Contributed by AV, 23-Jul-2020.) |
| ⊢ 5 ∈ Odd | ||
| Theorem | 6even 47698 | 6 is an even number. (Contributed by AV, 20-Jul-2020.) |
| ⊢ 6 ∈ Even | ||
| Theorem | 7odd 47699 | 7 is an odd number. (Contributed by AV, 20-Jul-2020.) |
| ⊢ 7 ∈ Odd | ||
| Theorem | 8even 47700 | 8 is an even number. (Contributed by AV, 23-Jul-2020.) |
| ⊢ 8 ∈ Even | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |