![]() |
Intuitionistic Logic Explorer Theorem List (p. 83 of 111) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nngt0 8201 | A positive integer is positive. (Contributed by NM, 26-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < 𝐴) | ||
Theorem | nnnlt1 8202 | A positive integer is not less than one. (Contributed by NM, 18-Jan-2004.) (Revised by Mario Carneiro, 27-May-2016.) |
⊢ (𝐴 ∈ ℕ → ¬ 𝐴 < 1) | ||
Theorem | 0nnn 8203 | Zero is not a positive integer. (Contributed by NM, 25-Aug-1999.) |
⊢ ¬ 0 ∈ ℕ | ||
Theorem | nnne0 8204 | A positive integer is nonzero. (Contributed by NM, 27-Sep-1999.) |
⊢ (𝐴 ∈ ℕ → 𝐴 ≠ 0) | ||
Theorem | nnap0 8205 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 8-Mar-2020.) |
⊢ (𝐴 ∈ ℕ → 𝐴 # 0) | ||
Theorem | nngt0i 8206 | A positive integer is positive (inference version). (Contributed by NM, 17-Sep-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 0 < 𝐴 | ||
Theorem | nnne0i 8207 | A positive integer is nonzero (inference version). (Contributed by NM, 25-Aug-1999.) |
⊢ 𝐴 ∈ ℕ ⇒ ⊢ 𝐴 ≠ 0 | ||
Theorem | nn2ge 8208* | There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ (𝐴 ≤ 𝑥 ∧ 𝐵 ≤ 𝑥)) | ||
Theorem | nn1gt1 8209 | A positive integer is either one or greater than one. This is for ℕ; 0elnn 4386 is a similar theorem for ω (the natural numbers as ordinals). (Contributed by Jim Kingdon, 7-Mar-2020.) |
⊢ (𝐴 ∈ ℕ → (𝐴 = 1 ∨ 1 < 𝐴)) | ||
Theorem | nngt1ne1 8210 | A positive integer is greater than one iff it is not equal to one. (Contributed by NM, 7-Oct-2004.) |
⊢ (𝐴 ∈ ℕ → (1 < 𝐴 ↔ 𝐴 ≠ 1)) | ||
Theorem | nndivre 8211 | The quotient of a real and a positive integer is real. (Contributed by NM, 28-Nov-2008.) |
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ) → (𝐴 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecre 8212 | The reciprocal of a positive integer is real. (Contributed by NM, 8-Feb-2008.) |
⊢ (𝑁 ∈ ℕ → (1 / 𝑁) ∈ ℝ) | ||
Theorem | nnrecgt0 8213 | The reciprocal of a positive integer is positive. (Contributed by NM, 25-Aug-1999.) |
⊢ (𝐴 ∈ ℕ → 0 < (1 / 𝐴)) | ||
Theorem | nnsub 8214 | Subtraction of positive integers. (Contributed by NM, 20-Aug-2001.) (Revised by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ)) | ||
Theorem | nnsubi 8215 | Subtraction of positive integers. (Contributed by NM, 19-Aug-2001.) |
⊢ 𝐴 ∈ ℕ & ⊢ 𝐵 ∈ ℕ ⇒ ⊢ (𝐴 < 𝐵 ↔ (𝐵 − 𝐴) ∈ ℕ) | ||
Theorem | nndiv 8216* | Two ways to express "𝐴 divides 𝐵 " for positive integers. (Contributed by NM, 3-Feb-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.) |
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (∃𝑥 ∈ ℕ (𝐴 · 𝑥) = 𝐵 ↔ (𝐵 / 𝐴) ∈ ℕ)) | ||
Theorem | nndivtr 8217 | Transitive property of divisibility: if 𝐴 divides 𝐵 and 𝐵 divides 𝐶, then 𝐴 divides 𝐶. Typically, 𝐶 would be an integer, although the theorem holds for complex 𝐶. (Contributed by NM, 3-May-2005.) |
⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℂ) ∧ ((𝐵 / 𝐴) ∈ ℕ ∧ (𝐶 / 𝐵) ∈ ℕ)) → (𝐶 / 𝐴) ∈ ℕ) | ||
Theorem | nnge1d 8218 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 1 ≤ 𝐴) | ||
Theorem | nngt0d 8219 | A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 0 < 𝐴) | ||
Theorem | nnne0d 8220 | A positive integer is nonzero. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 ≠ 0) | ||
Theorem | nnap0d 8221 | A positive integer is apart from zero. (Contributed by Jim Kingdon, 25-Aug-2021.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → 𝐴 # 0) | ||
Theorem | nnrecred 8222 | The reciprocal of a positive integer is real. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) ⇒ ⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) | ||
Theorem | nnaddcld 8223 | Closure of addition of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℕ) | ||
Theorem | nnmulcld 8224 | Closure of multiplication of positive integers. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 · 𝐵) ∈ ℕ) | ||
Theorem | nndivred 8225 | A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.) |
⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐴 / 𝐵) ∈ ℝ) | ||
The decimal representation of numbers/integers is based on the decimal digits 0 through 9 (df-0 7120 through df-9 8242), which are explicitly defined in the following. Note that the numbers 0 and 1 are constants defined as primitives of the complex number axiom system (see df-0 7120 and df-1 7121). Integers can also be exhibited as sums of powers of 10 (e.g. the number 103 can be expressed as ((;10↑2) + 3)) or as some other expression built from operations on the numbers 0 through 9. For example, the prime number 823541 can be expressed as (7↑7) − 2. Most abstract math rarely requires numbers larger than 4. Even in Wiles' proof of Fermat's Last Theorem, the largest number used appears to be 12. | ||
Syntax | c2 8226 | Extend class notation to include the number 2. |
class 2 | ||
Syntax | c3 8227 | Extend class notation to include the number 3. |
class 3 | ||
Syntax | c4 8228 | Extend class notation to include the number 4. |
class 4 | ||
Syntax | c5 8229 | Extend class notation to include the number 5. |
class 5 | ||
Syntax | c6 8230 | Extend class notation to include the number 6. |
class 6 | ||
Syntax | c7 8231 | Extend class notation to include the number 7. |
class 7 | ||
Syntax | c8 8232 | Extend class notation to include the number 8. |
class 8 | ||
Syntax | c9 8233 | Extend class notation to include the number 9. |
class 9 | ||
Syntax | c10 8234 | Extend class notation to include the number 10. |
class 10 | ||
Definition | df-2 8235 | Define the number 2. (Contributed by NM, 27-May-1999.) |
⊢ 2 = (1 + 1) | ||
Definition | df-3 8236 | Define the number 3. (Contributed by NM, 27-May-1999.) |
⊢ 3 = (2 + 1) | ||
Definition | df-4 8237 | Define the number 4. (Contributed by NM, 27-May-1999.) |
⊢ 4 = (3 + 1) | ||
Definition | df-5 8238 | Define the number 5. (Contributed by NM, 27-May-1999.) |
⊢ 5 = (4 + 1) | ||
Definition | df-6 8239 | Define the number 6. (Contributed by NM, 27-May-1999.) |
⊢ 6 = (5 + 1) | ||
Definition | df-7 8240 | Define the number 7. (Contributed by NM, 27-May-1999.) |
⊢ 7 = (6 + 1) | ||
Definition | df-8 8241 | Define the number 8. (Contributed by NM, 27-May-1999.) |
⊢ 8 = (7 + 1) | ||
Definition | df-9 8242 | Define the number 9. (Contributed by NM, 27-May-1999.) |
⊢ 9 = (8 + 1) | ||
Theorem | 0ne1 8243 | 0 ≠ 1 (common case). See aso 1ap0 7827. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 0 ≠ 1 | ||
Theorem | 1ne0 8244 | 1 ≠ 0. See aso 1ap0 7827. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 1 ≠ 0 | ||
Theorem | 1m1e0 8245 | (1 − 1) = 0 (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (1 − 1) = 0 | ||
Theorem | 2re 8246 | The number 2 is real. (Contributed by NM, 27-May-1999.) |
⊢ 2 ∈ ℝ | ||
Theorem | 2cn 8247 | The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.) |
⊢ 2 ∈ ℂ | ||
Theorem | 2ex 8248 | 2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 2 ∈ V | ||
Theorem | 2cnd 8249 | 2 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (𝜑 → 2 ∈ ℂ) | ||
Theorem | 3re 8250 | The number 3 is real. (Contributed by NM, 27-May-1999.) |
⊢ 3 ∈ ℝ | ||
Theorem | 3cn 8251 | The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.) |
⊢ 3 ∈ ℂ | ||
Theorem | 3ex 8252 | 3 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 3 ∈ V | ||
Theorem | 4re 8253 | The number 4 is real. (Contributed by NM, 27-May-1999.) |
⊢ 4 ∈ ℝ | ||
Theorem | 4cn 8254 | The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 4 ∈ ℂ | ||
Theorem | 5re 8255 | The number 5 is real. (Contributed by NM, 27-May-1999.) |
⊢ 5 ∈ ℝ | ||
Theorem | 5cn 8256 | The number 5 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 5 ∈ ℂ | ||
Theorem | 6re 8257 | The number 6 is real. (Contributed by NM, 27-May-1999.) |
⊢ 6 ∈ ℝ | ||
Theorem | 6cn 8258 | The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 6 ∈ ℂ | ||
Theorem | 7re 8259 | The number 7 is real. (Contributed by NM, 27-May-1999.) |
⊢ 7 ∈ ℝ | ||
Theorem | 7cn 8260 | The number 7 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 7 ∈ ℂ | ||
Theorem | 8re 8261 | The number 8 is real. (Contributed by NM, 27-May-1999.) |
⊢ 8 ∈ ℝ | ||
Theorem | 8cn 8262 | The number 8 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 8 ∈ ℂ | ||
Theorem | 9re 8263 | The number 9 is real. (Contributed by NM, 27-May-1999.) |
⊢ 9 ∈ ℝ | ||
Theorem | 9cn 8264 | The number 9 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 9 ∈ ℂ | ||
Theorem | 0le0 8265 | Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ 0 ≤ 0 | ||
Theorem | 0le2 8266 | 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018.) |
⊢ 0 ≤ 2 | ||
Theorem | 2pos 8267 | The number 2 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 2 | ||
Theorem | 2ne0 8268 | The number 2 is nonzero. (Contributed by NM, 9-Nov-2007.) |
⊢ 2 ≠ 0 | ||
Theorem | 2ap0 8269 | The number 2 is apart from zero. (Contributed by Jim Kingdon, 9-Mar-2020.) |
⊢ 2 # 0 | ||
Theorem | 3pos 8270 | The number 3 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 3 | ||
Theorem | 3ne0 8271 | The number 3 is nonzero. (Contributed by FL, 17-Oct-2010.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
⊢ 3 ≠ 0 | ||
Theorem | 3ap0 8272 | The number 3 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 3 # 0 | ||
Theorem | 4pos 8273 | The number 4 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 4 | ||
Theorem | 4ne0 8274 | The number 4 is nonzero. (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ 4 ≠ 0 | ||
Theorem | 4ap0 8275 | The number 4 is apart from zero. (Contributed by Jim Kingdon, 10-Oct-2021.) |
⊢ 4 # 0 | ||
Theorem | 5pos 8276 | The number 5 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 5 | ||
Theorem | 6pos 8277 | The number 6 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 6 | ||
Theorem | 7pos 8278 | The number 7 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 7 | ||
Theorem | 8pos 8279 | The number 8 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 8 | ||
Theorem | 9pos 8280 | The number 9 is positive. (Contributed by NM, 27-May-1999.) |
⊢ 0 < 9 | ||
This includes adding two pairs of values 1..10 (where the right is less than the left) and where the left is less than the right for the values 1..10. | ||
Theorem | neg1cn 8281 | -1 is a complex number (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ -1 ∈ ℂ | ||
Theorem | neg1rr 8282 | -1 is a real number (common case). (Contributed by David A. Wheeler, 5-Dec-2018.) |
⊢ -1 ∈ ℝ | ||
Theorem | neg1ne0 8283 | -1 is nonzero (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 ≠ 0 | ||
Theorem | neg1lt0 8284 | -1 is less than 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ -1 < 0 | ||
Theorem | neg1ap0 8285 | -1 is apart from zero. (Contributed by Jim Kingdon, 9-Jun-2020.) |
⊢ -1 # 0 | ||
Theorem | negneg1e1 8286 | --1 is 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ --1 = 1 | ||
Theorem | 1pneg1e0 8287 | 1 + -1 is 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + -1) = 0 | ||
Theorem | 0m0e0 8288 | 0 minus 0 equals 0 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (0 − 0) = 0 | ||
Theorem | 1m0e1 8289 | 1 - 0 = 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 − 0) = 1 | ||
Theorem | 0p1e1 8290 | 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
⊢ (0 + 1) = 1 | ||
Theorem | 1p0e1 8291 | 1 + 0 = 1. (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ (1 + 0) = 1 | ||
Theorem | 1p1e2 8292 | 1 + 1 = 2. (Contributed by NM, 1-Apr-2008.) |
⊢ (1 + 1) = 2 | ||
Theorem | 2m1e1 8293 | 2 - 1 = 1. The result is on the right-hand-side to be consistent with similar proofs like 4p4e8 8314. (Contributed by David A. Wheeler, 4-Jan-2017.) |
⊢ (2 − 1) = 1 | ||
Theorem | 1e2m1 8294 | 1 = 2 - 1 (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
⊢ 1 = (2 − 1) | ||
Theorem | 3m1e2 8295 | 3 - 1 = 2. (Contributed by FL, 17-Oct-2010.) (Revised by NM, 10-Dec-2017.) |
⊢ (3 − 1) = 2 | ||
Theorem | 2p2e4 8296 | Two plus two equals four. For more information, see "2+2=4 Trivia" on the Metamath Proof Explorer Home Page: http://us.metamath.org/mpeuni/mmset.html#trivia. (Contributed by NM, 27-May-1999.) |
⊢ (2 + 2) = 4 | ||
Theorem | 2times 8297 | Two times a number. (Contributed by NM, 10-Oct-2004.) (Revised by Mario Carneiro, 27-May-2016.) (Proof shortened by AV, 26-Feb-2020.) |
⊢ (𝐴 ∈ ℂ → (2 · 𝐴) = (𝐴 + 𝐴)) | ||
Theorem | times2 8298 | A number times 2. (Contributed by NM, 16-Oct-2007.) |
⊢ (𝐴 ∈ ℂ → (𝐴 · 2) = (𝐴 + 𝐴)) | ||
Theorem | 2timesi 8299 | Two times a number. (Contributed by NM, 1-Aug-1999.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (2 · 𝐴) = (𝐴 + 𝐴) | ||
Theorem | times2i 8300 | A number times 2. (Contributed by NM, 11-May-2004.) |
⊢ 𝐴 ∈ ℂ ⇒ ⊢ (𝐴 · 2) = (𝐴 + 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |