HomeHome Intuitionistic Logic Explorer
Theorem List (p. 81 of 95)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremelnnnn0 8001 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)
(𝑁 ℕ ↔ (𝑁 (𝑁 − 1) 0))
 
Theoremelnnnn0b 8002 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)
(𝑁 ℕ ↔ (𝑁 0 0 < 𝑁))
 
Theoremelnnnn0c 8003 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)
(𝑁 ℕ ↔ (𝑁 0 1 ≤ 𝑁))
 
Theoremnn0addge1 8004 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
((A 𝑁 0) → A ≤ (A + 𝑁))
 
Theoremnn0addge2 8005 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
((A 𝑁 0) → A ≤ (𝑁 + A))
 
Theoremnn0addge1i 8006 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
A     &   𝑁 0       A ≤ (A + 𝑁)
 
Theoremnn0addge2i 8007 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
A     &   𝑁 0       A ≤ (𝑁 + A)
 
Theoremnn0le2xi 8008 A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
𝑁 0       𝑁 ≤ (2 · 𝑁)
 
Theoremnn0lele2xi 8009 'Less than or equal to' implies 'less than or equal to twice' for nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.)
𝑀 0    &   𝑁 0       (𝑁𝑀𝑁 ≤ (2 · 𝑀))
 
Theoremnn0supp 8010 Two ways to write the support of a function on 0. (Contributed by Mario Carneiro, 29-Dec-2014.)
(𝐹:𝐼⟶ℕ0 → (𝐹 “ (V ∖ {0})) = (𝐹 “ ℕ))
 
Theoremnnnn0d 8011 A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
(φA ℕ)       (φA 0)
 
Theoremnn0red 8012 A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
(φA 0)       (φA ℝ)
 
Theoremnn0cnd 8013 A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
(φA 0)       (φA ℂ)
 
Theoremnn0ge0d 8014 A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
(φA 0)       (φ → 0 ≤ A)
 
Theoremnn0addcld 8015 Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
(φA 0)    &   (φB 0)       (φ → (A + B) 0)
 
Theoremnn0mulcld 8016 Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
(φA 0)    &   (φB 0)       (φ → (A · B) 0)
 
Theoremnn0readdcl 8017 Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
((A 0 B 0) → (A + B) ℝ)
 
Theoremnn0ge2m1nn 8018 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (Revised by AV, 4-Jan-2020.)
((𝑁 0 2 ≤ 𝑁) → (𝑁 − 1) ℕ)
 
Theoremnn0ge2m1nn0 8019 If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018.)
((𝑁 0 2 ≤ 𝑁) → (𝑁 − 1) 0)
 
Theoremnn0nndivcl 8020 Closure law for dividing of a nonnegative integer by a positive integer. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
((𝐾 0 𝐿 ℕ) → (𝐾 / 𝐿) ℝ)
 
3.4.8  Integers (as a subset of complex numbers)
 
Syntaxcz 8021 Extend class notation to include the class of integers.
class
 
Definitiondf-z 8022 Define the set of integers, which are the positive and negative integers together with zero. Definition of integers in [Apostol] p. 22. The letter Z abbreviates the German word Zahlen meaning "numbers." (Contributed by NM, 8-Jan-2002.)
ℤ = {𝑛 ℝ ∣ (𝑛 = 0 𝑛 -𝑛 ℕ)}
 
Theoremelz 8023 Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℤ ↔ (𝑁 (𝑁 = 0 𝑁 -𝑁 ℕ)))
 
Theoremnnnegz 8024 The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
(𝑁 ℕ → -𝑁 ℤ)
 
Theoremzre 8025 An integer is a real. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℤ → 𝑁 ℝ)
 
Theoremzcn 8026 An integer is a complex number. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ → 𝑁 ℂ)
 
Theoremzrei 8027 An integer is a real number. (Contributed by NM, 14-Jul-2005.)
A        A
 
Theoremzssre 8028 The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
ℤ ⊆ ℝ
 
Theoremzsscn 8029 The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
ℤ ⊆ ℂ
 
Theoremzex 8030 The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
V
 
Theoremelnnz 8031 Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℕ ↔ (𝑁 0 < 𝑁))
 
Theorem0z 8032 Zero is an integer. (Contributed by NM, 12-Jan-2002.)
0
 
Theorem0zd 8033 Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(φ → 0 ℤ)
 
Theoremelnn0z 8034 Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
(𝑁 0 ↔ (𝑁 0 ≤ 𝑁))
 
Theoremelznn0nn 8035 Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
(𝑁 ℤ ↔ (𝑁 0 (𝑁 -𝑁 ℕ)))
 
Theoremelznn0 8036 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ ↔ (𝑁 (𝑁 0 -𝑁 0)))
 
Theoremelznn 8037 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
(𝑁 ℤ ↔ (𝑁 (𝑁 -𝑁 0)))
 
Theoremnnssz 8038 Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)
ℕ ⊆ ℤ
 
Theoremnn0ssz 8039 Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)
0 ⊆ ℤ
 
Theoremnnz 8040 A positive integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 ℕ → 𝑁 ℤ)
 
Theoremnn0z 8041 A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 0𝑁 ℤ)
 
Theoremnnzi 8042 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁        𝑁
 
Theoremnn0zi 8043 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁 0       𝑁
 
Theoremelnnz1 8044 Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
(𝑁 ℕ ↔ (𝑁 1 ≤ 𝑁))
 
Theoremnnzrab 8045 Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
ℕ = {x ℤ ∣ 1 ≤ x}
 
Theoremnn0zrab 8046 Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
0 = {x ℤ ∣ 0 ≤ x}
 
Theorem1z 8047 One is an integer. (Contributed by NM, 10-May-2004.)
1
 
Theorem1zzd 8048 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(φ → 1 ℤ)
 
Theorem2z 8049 Two is an integer. (Contributed by NM, 10-May-2004.)
2
 
Theorem3z 8050 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
3
 
Theorem4z 8051 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
4
 
Theoremznegcl 8052 Closure law for negative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ → -𝑁 ℤ)
 
Theoremneg1z 8053 -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
-1
 
Theoremznegclb 8054 A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
(A ℂ → (A ℤ ↔ -A ℤ))
 
Theoremnn0negz 8055 The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 0 → -𝑁 ℤ)
 
Theoremnn0negzi 8056 The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁 0       -𝑁
 
Theorempeano2z 8057 Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
(𝑁 ℤ → (𝑁 + 1) ℤ)
 
Theoremzaddcllempos 8058 Lemma for zaddcl 8061. Special case in which 𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℕ) → (𝑀 + 𝑁) ℤ)
 
Theorempeano2zm 8059 "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
(𝑁 ℤ → (𝑁 − 1) ℤ)
 
Theoremzaddcllemneg 8060 Lemma for zaddcl 8061. Special case in which -𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 -𝑁 ℕ) → (𝑀 + 𝑁) ℤ)
 
Theoremzaddcl 8061 Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 𝑁 ℤ) → (𝑀 + 𝑁) ℤ)
 
Theoremzsubcl 8062 Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁) ℤ)
 
Theoremztri3or0 8063 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
(𝑁 ℤ → (𝑁 < 0 𝑁 = 0 0 < 𝑁))
 
Theoremztri3or 8064 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 𝑀 = 𝑁 𝑁 < 𝑀))
 
Theoremzletric 8065 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
((A B ℤ) → (AB BA))
 
Theoremzlelttric 8066 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
((A B ℤ) → (AB B < A))
 
Theoremzltnle 8067 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ ¬ BA))
 
Theoremzleloe 8068 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
((A B ℤ) → (AB ↔ (A < B A = B)))
 
Theoremznnnlt1 8069 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
(𝑁 ℤ → (¬ 𝑁 ℕ ↔ 𝑁 < 1))
 
Theoremzletr 8070 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
((𝐽 𝐾 𝐿 ℤ) → ((𝐽𝐾 𝐾𝐿) → 𝐽𝐿))
 
Theoremzrevaddcl 8071 Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
(𝑁 ℤ → ((𝑀 (𝑀 + 𝑁) ℤ) ↔ 𝑀 ℤ))
 
Theoremznnsub 8072 The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7733.) (Contributed by NM, 11-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 ↔ (𝑁𝑀) ℕ))
 
Theoremzmulcl 8073 Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
((𝑀 𝑁 ℤ) → (𝑀 · 𝑁) ℤ)
 
Theoremzltp1le 8074 Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
 
Theoremzleltp1 8075 Integer ordering relation. (Contributed by NM, 10-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁𝑀 < (𝑁 + 1)))
 
Theoremzlem1lt 8076 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))
 
Theoremzltlem1 8077 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))
 
Theoremzgt0ge1 8078 An integer greater than 0 is greater than or equal to 1. (Contributed by AV, 14-Oct-2018.)
(𝑍 ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍))
 
Theoremnnleltp1 8079 Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((A B ℕ) → (ABA < (B + 1)))
 
Theoremnnltp1le 8080 Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
((A B ℕ) → (A < B ↔ (A + 1) ≤ B))
 
Theoremnnaddm1cl 8081 Closure of addition of positive integers minus one. (Contributed by NM, 6-Aug-2003.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((A B ℕ) → ((A + B) − 1) ℕ)
 
Theoremnn0ltp1le 8082 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 0 𝑁 0) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
 
Theoremnn0leltp1 8083 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
((𝑀 0 𝑁 0) → (𝑀𝑁𝑀 < (𝑁 + 1)))
 
Theoremnn0ltlem1 8084 Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 0 𝑁 0) → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))
 
Theoremznn0sub 8085 The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 8086.) (Contributed by NM, 14-Jul-2005.)
((𝑀 𝑁 ℤ) → (𝑀𝑁 ↔ (𝑁𝑀) 0))
 
Theoremnn0sub 8086 Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
((𝑀 0 𝑁 0) → (𝑀𝑁 ↔ (𝑁𝑀) 0))
 
Theoremnn0n0n1ge2 8087 A nonnegative integer which is neither 0 nor 1 is greater than or equal to 2. (Contributed by Alexander van der Vekens, 6-Dec-2017.)
((𝑁 0 𝑁 ≠ 0 𝑁 ≠ 1) → 2 ≤ 𝑁)
 
Theoremelz2 8088* Membership in the set of integers. Commonly used in constructions of the integers as equivalence classes under subtraction of the positive integers. (Contributed by Mario Carneiro, 16-May-2014.)
(𝑁 ℤ ↔ x y 𝑁 = (xy))
 
Theoremdfz2 8089 Alternative definition of the integers, based on elz2 8088. (Contributed by Mario Carneiro, 16-May-2014.)
ℤ = ( − “ (ℕ × ℕ))
 
Theoremnn0sub2 8090 Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
((𝑀 0 𝑁 0 𝑀𝑁) → (𝑁𝑀) 0)
 
Theoremzapne 8091 Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 # 𝑁𝑀𝑁))
 
Theoremzdceq 8092 Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → DECID A = B)
 
Theoremzdcle 8093 Integer is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
((A B ℤ) → DECID AB)
 
Theoremzdclt 8094 Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
((A B ℤ) → DECID A < B)
 
Theoremzltlen 8095 Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7413 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ (AB BA)))
 
Theoremnn0n0n1ge2b 8096 A nonnegative integer is neither 0 nor 1 if and only if it is greater than or equal to 2. (Contributed by Alexander van der Vekens, 17-Jan-2018.)
(𝑁 0 → ((𝑁 ≠ 0 𝑁 ≠ 1) ↔ 2 ≤ 𝑁))
 
Theoremnn0lt10b 8097 A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
(𝑁 0 → (𝑁 < 1 ↔ 𝑁 = 0))
 
Theoremnn0lt2 8098 A nonnegative integer less than 2 must be 0 or 1. (Contributed by Alexander van der Vekens, 16-Sep-2018.)
((𝑁 0 𝑁 < 2) → (𝑁 = 0 𝑁 = 1))
 
Theoremnn0lem1lt 8099 Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
((𝑀 0 𝑁 0) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))
 
Theoremnnlem1lt 8100 Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
((𝑀 𝑁 ℕ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9457
  Copyright terms: Public domain < Previous  Next >