Home | Metamath
Proof Explorer Theorem List (p. 112 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 6lt9 11101 | 6 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 6 < 9 | ||
Theorem | 5lt9 11102 | 5 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 5 < 9 | ||
Theorem | 4lt9 11103 | 4 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 4 < 9 | ||
Theorem | 3lt9 11104 | 3 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 3 < 9 | ||
Theorem | 2lt9 11105 | 2 is less than 9. (Contributed by Mario Carneiro, 9-Mar-2015.) |
⊢ 2 < 9 | ||
Theorem | 1lt9 11106 | 1 is less than 9. (Contributed by NM, 19-Oct-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) |
⊢ 1 < 9 | ||
Theorem | 9lt10OLD 11107 | 9 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) Obsolete version of 9lt10 11549 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 9 < 10 | ||
Theorem | 8lt10OLD 11108 | 8 is less than 10. (Contributed by Mario Carneiro, 8-Feb-2015.) Obsolete version of 8lt10 11550 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 8 < 10 | ||
Theorem | 7lt10OLD 11109 | 7 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 7lt10 11551 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 7 < 10 | ||
Theorem | 6lt10OLD 11110 | 6 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 6lt10 11552 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 6 < 10 | ||
Theorem | 5lt10OLD 11111 | 5 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 5lt10 11553 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 5 < 10 | ||
Theorem | 4lt10OLD 11112 | 4 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 4lt10 11554 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 4 < 10 | ||
Theorem | 3lt10OLD 11113 | 3 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 3lt10 11555 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 3 < 10 | ||
Theorem | 2lt10OLD 11114 | 2 is less than 10. (Contributed by Mario Carneiro, 10-Mar-2015.) Obsolete version of 2lt10 11556 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 2 < 10 | ||
Theorem | 1lt10OLD 11115 | 1 is less than 10. (Contributed by NM, 7-Nov-2012.) (Revised by Mario Carneiro, 9-Mar-2015.) Obsolete version of 1lt10 11557 as of 8-Sep-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 1 < 10 | ||
Theorem | 0ne2 11116 | 0 is not equal to 2. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 2 | ||
Theorem | 1ne2 11117 | 1 is not equal to 2. (Contributed by NM, 19-Oct-2012.) |
⊢ 1 ≠ 2 | ||
Theorem | 1le2 11118 | 1 is less than or equal to 2 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 ≤ 2 | ||
Theorem | 2cnne0 11119 | 2 is a nonzero complex number (common case). (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ (2 ∈ ℂ ∧ 2 ≠ 0) | ||
Theorem | 2rene0 11120 | 2 is a nonzero real number (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 ∈ ℝ ∧ 2 ≠ 0) | ||
Theorem | 1le3 11121 | 1 is less than or equal to 3. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 ≤ 3 | ||
Theorem | neg1mulneg1e1 11122 | -1 · -1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (-1 · -1) = 1 | ||
Theorem | halfre 11123 | One-half is real. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 / 2) ∈ ℝ | ||
Theorem | halfcn 11124 | One-half is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 / 2) ∈ ℂ | ||
Theorem | halfgt0 11125 | One-half is greater than zero. (Contributed by NM, 24-Feb-2005.) |
⊢ 0 < (1 / 2) | ||
Theorem | halfge0 11126 | One-half is not negative. (Contributed by AV, 7-Jun-2020.) |
⊢ 0 ≤ (1 / 2) | ||
Theorem | halflt1 11127 | One-half is less than one. (Contributed by NM, 24-Feb-2005.) |
⊢ (1 / 2) < 1 | ||
Theorem | 1mhlfehlf 11128 | Prove that 1 - 1/2 = 1/2. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (1 − (1 / 2)) = (1 / 2) | ||
Theorem | 8th4div3 11129 | An eighth of four thirds is a sixth. (Contributed by Paul Chapman, 24-Nov-2007.) |
⊢ ((1 / 8) · (4 / 3)) = (1 / 6) | ||
Theorem | halfpm6th 11130 | One half plus or minus one sixth. (Contributed by Paul Chapman, 17-Jan-2008.) |
⊢ (((1 / 2) − (1 / 6)) = (1 / 3) ∧ ((1 / 2) + (1 / 6)) = (2 / 3)) | ||
Theorem | it0e0 11131 | i times 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (i · 0) = 0 | ||
Theorem | 2mulicn 11132 | (2 · i) ∈ ℂ (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · i) ∈ ℂ | ||
Theorem | 2muline0 11133 | (2 · i) ≠ 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (2 · i) ≠ 0 | ||
Theorem | halfcl 11134 | Closure of half of a number (common case). (Contributed by NM, 1-Jan-2006.) |
⊢ (𝐴 ∈ ℂ → (𝐴 / 2) ∈ ℂ) | ||
Theorem | rehalfcl 11135 | Real closure of half. (Contributed by NM, 1-Jan-2006.) |
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈ ℝ) | ||
Theorem | half0 11136 | Half of a number is zero iff the number is zero. (Contributed by NM, 20-Apr-2006.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) = 0 ↔ 𝐴 = 0)) | ||
Theorem | 2halves 11137 | Two halves make a whole. (Contributed by NM, 11-Apr-2005.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) | ||
Theorem | halfpos2 11138 | A number is positive iff its half is positive. (Contributed by NM, 10-Apr-2005.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ 0 < (𝐴 / 2))) | ||
Theorem | halfpos 11139 | A positive number is greater than its half. (Contributed by NM, 28-Oct-2004.) (Proof shortened by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℝ → (0 < 𝐴 ↔ (𝐴 / 2) < 𝐴)) | ||
Theorem | halfnneg2 11140 | A number is nonnegative iff its half is nonnegative. (Contributed by NM, 9-Dec-2005.) |
⊢ (𝐴 ∈ ℝ → (0 ≤ 𝐴 ↔ 0 ≤ (𝐴 / 2))) | ||
Theorem | halfaddsubcl 11141 | Closure of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝐴 + 𝐵) / 2) ∈ ℂ ∧ ((𝐴 − 𝐵) / 2) ∈ ℂ)) | ||
Theorem | halfaddsub 11142 | Sum and difference of half-sum and half-difference. (Contributed by Paul Chapman, 12-Oct-2007.) |
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → ((((𝐴 + 𝐵) / 2) + ((𝐴 − 𝐵) / 2)) = 𝐴 ∧ (((𝐴 + 𝐵) / 2) − ((𝐴 − 𝐵) / 2)) = 𝐵)) | ||
Theorem | subhalfhalf 11143 | Subtracting the half of a number from the number yields the half of the number. (Contributed by AV, 28-Jun-2021.) |
⊢ (𝐴 ∈ ℂ → (𝐴 − (𝐴 / 2)) = (𝐴 / 2)) | ||
Theorem | lt2halves 11144 | A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < (𝐶 / 2) ∧ 𝐵 < (𝐶 / 2)) → (𝐴 + 𝐵) < 𝐶)) | ||
Theorem | addltmul 11145 | Sum is less than product for numbers greater than 2. (Contributed by Stefan Allan, 24-Sep-2010.) |
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (2 < 𝐴 ∧ 2 < 𝐵)) → (𝐴 + 𝐵) < (𝐴 · 𝐵)) | ||
Theorem | nominpos 11146* | There is no smallest positive real number. (Contributed by NM, 28-Oct-2004.) |
⊢ ¬ ∃𝑥 ∈ ℝ (0 < 𝑥 ∧ ¬ ∃𝑦 ∈ ℝ (0 < 𝑦 ∧ 𝑦 < 𝑥)) | ||
Theorem | avglt1 11147 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 𝐴 < ((𝐴 + 𝐵) / 2))) | ||
Theorem | avglt2 11148 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ((𝐴 + 𝐵) / 2) < 𝐵)) | ||
Theorem | avgle1 11149 | Ordering property for average. (Contributed by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ 𝐴 ≤ ((𝐴 + 𝐵) / 2))) | ||
Theorem | avgle2 11150 | Ordering property for average. (Contributed by Jeff Hankins, 15-Sep-2013.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ ((𝐴 + 𝐵) / 2) ≤ 𝐵)) | ||
Theorem | avgle 11151 | The average of two numbers is less than or equal to at least one of them. (Contributed by NM, 9-Dec-2005.) (Revised by Mario Carneiro, 28-May-2014.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (((𝐴 + 𝐵) / 2) ≤ 𝐴 ∨ ((𝐴 + 𝐵) / 2) ≤ 𝐵)) | ||
Theorem | 2timesd 11152 | Two times a number. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (2 · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | times2d 11153 | A number times 2. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 · 2) = (𝐴 + 𝐴)) | ||
Theorem | halfcld 11154 | Closure of half of a number (frequently used special case). (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℂ) | ||
Theorem | 2halvesd 11155 | Two halves make a whole. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℂ) ⇒ ⊢ (𝜑 → ((𝐴 / 2) + (𝐴 / 2)) = 𝐴) | ||
Theorem | rehalfcld 11156 | Real closure of half. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝐴 / 2) ∈ ℝ) | ||
Theorem | lt2halvesd 11157 | A sum is less than the whole if each term is less than half. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < (𝐶 / 2)) & ⊢ (𝜑 → 𝐵 < (𝐶 / 2)) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < 𝐶) | ||
Theorem | rehalfcli 11158 | Half a real number is real. Inference form. (Contributed by David Moews, 28-Feb-2017.) |
⊢ 𝐴 ∈ ℝ ⇒ ⊢ (𝐴 / 2) ∈ ℝ | ||
Theorem | lt2addmuld 11159 | If two real numbers are less than a third real number, the sum of the two real numbers is less than twice the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 𝐶 ∈ ℝ) & ⊢ (𝜑 → 𝐴 < 𝐶) & ⊢ (𝜑 → 𝐵 < 𝐶) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) < (2 · 𝐶)) | ||
Theorem | add1p1 11160 | Adding two times 1 to a number. (Contributed by AV, 22-Sep-2018.) |
⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) + 1) = (𝑁 + 2)) | ||
Theorem | sub1m1 11161 | Subtracting two times 1 from a number. (Contributed by AV, 23-Oct-2018.) |
⊢ (𝑁 ∈ ℂ → ((𝑁 − 1) − 1) = (𝑁 − 2)) | ||
Theorem | cnm2m1cnm3 11162 | Subtracting 2 and afterwards 1 from a number results in the difference between the number and 3. (Contributed by Alexander van der Vekens, 16-Sep-2018.) |
⊢ (𝐴 ∈ ℂ → ((𝐴 − 2) − 1) = (𝐴 − 3)) | ||
Theorem | xp1d2m1eqxm1d2 11163 | A complex number increased by 1, then divided by 2, then decreased by 1 equals the complex number decreased by 1 and then divided by 2. (Contributed by AV, 24-May-2020.) |
⊢ (𝑋 ∈ ℂ → (((𝑋 + 1) / 2) − 1) = ((𝑋 − 1) / 2)) | ||
Theorem | div4p1lem1div2 11164 | An integer greater than 5, divided by 4 and increased by 1, is less than or equal to the half of the integer minus 1. (Contributed by AV, 8-Jul-2021.) |
⊢ ((𝑁 ∈ ℝ ∧ 6 ≤ 𝑁) → ((𝑁 / 4) + 1) ≤ ((𝑁 − 1) / 2)) | ||
Theorem | nnunb 11165* | The set of positive integers is unbounded above. Theorem I.28 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.) |
⊢ ¬ ∃𝑥 ∈ ℝ ∀𝑦 ∈ ℕ (𝑦 < 𝑥 ∨ 𝑦 = 𝑥) | ||
Theorem | arch 11166* | Archimedean property of real numbers. For any real number, there is an integer greater than it. Theorem I.29 of [Apostol] p. 26. (Contributed by NM, 21-Jan-1997.) |
⊢ (𝐴 ∈ ℝ → ∃𝑛 ∈ ℕ 𝐴 < 𝑛) | ||
Theorem | nnrecl 11167* | There exists a positive integer whose reciprocal is less than a given positive real. Exercise 3 of [Apostol] p. 28. (Contributed by NM, 8-Nov-2004.) |
⊢ ((𝐴 ∈ ℝ ∧ 0 < 𝐴) → ∃𝑛 ∈ ℕ (1 / 𝑛) < 𝐴) | ||
Theorem | bndndx 11168* | A bounded real sequence 𝐴(𝑘) is less than or equal to at least one of its indices. (Contributed by NM, 18-Jan-2008.) |
⊢ (∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (𝐴 ∈ ℝ ∧ 𝐴 ≤ 𝑥) → ∃𝑘 ∈ ℕ 𝐴 ≤ 𝑘) | ||
Syntax | cn0 11169 | Extend class notation to include the class of nonnegative integers. |
class ℕ0 | ||
Definition | df-n0 11170 | Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ0 = (ℕ ∪ {0}) | ||
Theorem | elnn0 11171 | Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) | ||
Theorem | nnssnn0 11172 | Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ ⊆ ℕ0 | ||
Theorem | nn0ssre 11173 | Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ ℕ0 ⊆ ℝ | ||
Theorem | nn0sscn 11174 | Nonnegative integers are a subset of the complex numbers.) (Contributed by NM, 9-May-2004.) |
⊢ ℕ0 ⊆ ℂ | ||
Theorem | nn0ex 11175 | The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004.) |
⊢ ℕ0 ∈ V | ||
Theorem | nnnn0 11176 | A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ∈ ℕ0) | ||
Theorem | nnnn0i 11177 | A positive integer is a nonnegative integer. (Contributed by NM, 20-Jun-2005.) |
⊢ 𝑁 ∈ ℕ ⇒ ⊢ 𝑁 ∈ ℕ0 | ||
Theorem | nn0re 11178 | A nonnegative integer is a real number. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ) | ||
Theorem | nn0cn 11179 | A nonnegative integer is a complex number. (Contributed by NM, 9-May-2004.) |
⊢ (𝐴 ∈ ℕ0 → 𝐴 ∈ ℂ) | ||
Theorem | nn0rei 11180 | A nonnegative integer is a real number. (Contributed by NM, 14-May-2003.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 ∈ ℝ | ||
Theorem | nn0cni 11181 | A nonnegative integer is a complex number. (Contributed by NM, 14-May-2003.) |
⊢ 𝐴 ∈ ℕ0 ⇒ ⊢ 𝐴 ∈ ℂ | ||
Theorem | dfn2 11182 | The set of positive integers defined in terms of nonnegative integers. (Contributed by NM, 23-Sep-2007.) (Proof shortened by Mario Carneiro, 13-Feb-2013.) |
⊢ ℕ = (ℕ0 ∖ {0}) | ||
Theorem | elnnne0 11183 | The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) | ||
Theorem | 0nn0 11184 | 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 0 ∈ ℕ0 | ||
Theorem | 1nn0 11185 | 1 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 1 ∈ ℕ0 | ||
Theorem | 2nn0 11186 | 2 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 2 ∈ ℕ0 | ||
Theorem | 3nn0 11187 | 3 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 3 ∈ ℕ0 | ||
Theorem | 4nn0 11188 | 4 is a nonnegative integer. (Contributed by Mario Carneiro, 18-Feb-2014.) |
⊢ 4 ∈ ℕ0 | ||
Theorem | 5nn0 11189 | 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 5 ∈ ℕ0 | ||
Theorem | 6nn0 11190 | 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 6 ∈ ℕ0 | ||
Theorem | 7nn0 11191 | 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 7 ∈ ℕ0 | ||
Theorem | 8nn0 11192 | 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 8 ∈ ℕ0 | ||
Theorem | 9nn0 11193 | 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.) |
⊢ 9 ∈ ℕ0 | ||
Theorem | 10nn0OLD 11194 | Obsolete version of 10nn0 11392 as of 6-Sep-2021. (Contributed by Mario Carneiro, 19-Apr-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 10 ∈ ℕ0 | ||
Theorem | nn0ge0 11195 | A nonnegative integer is greater than or equal to zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ (𝑁 ∈ ℕ0 → 0 ≤ 𝑁) | ||
Theorem | nn0nlt0 11196 | A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ0 → ¬ 𝐴 < 0) | ||
Theorem | nn0ge0i 11197 | Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.) |
⊢ 𝑁 ∈ ℕ0 ⇒ ⊢ 0 ≤ 𝑁 | ||
Theorem | nn0le0eq0 11198 | A nonnegative integer is less than or equal to zero iff it is equal to zero. (Contributed by NM, 9-Dec-2005.) |
⊢ (𝑁 ∈ ℕ0 → (𝑁 ≤ 0 ↔ 𝑁 = 0)) | ||
Theorem | nn0p1gt0 11199 | A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
⊢ (𝑁 ∈ ℕ0 → 0 < (𝑁 + 1)) | ||
Theorem | nnnn0addcl 11200 | A positive integer plus a nonnegative integer is a positive integer. (Contributed by NM, 20-Apr-2005.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |