 Home Intuitionistic Logic ExplorerTheorem 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

3.4.8  Integers (as a subset of complex numbers)

Syntaxcz 8001 Extend class notation to include the class of integers.
class

Definitiondf-z 8002 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 8003 Membership in the set of integers. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℤ ↔ (𝑁 (𝑁 = 0 𝑁 -𝑁 ℕ)))

Theoremnnnegz 8004 The negative of a positive integer is an integer. (Contributed by NM, 12-Jan-2002.)
(𝑁 ℕ → -𝑁 ℤ)

Theoremzre 8005 An integer is a real. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℤ → 𝑁 ℝ)

Theoremzcn 8006 An integer is a complex number. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ → 𝑁 ℂ)

Theoremzrei 8007 An integer is a real number. (Contributed by NM, 14-Jul-2005.)
A        A

Theoremzssre 8008 The integers are a subset of the reals. (Contributed by NM, 2-Aug-2004.)
ℤ ⊆ ℝ

Theoremzsscn 8009 The integers are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.)
ℤ ⊆ ℂ

Theoremzex 8010 The set of integers exists. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.)
V

Theoremelnnz 8011 Positive integer property expressed in terms of integers. (Contributed by NM, 8-Jan-2002.)
(𝑁 ℕ ↔ (𝑁 0 < 𝑁))

Theorem0z 8012 Zero is an integer. (Contributed by NM, 12-Jan-2002.)
0

Theorem0zd 8013 Zero is an integer, deductive form (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
(φ → 0 ℤ)

Theoremelnn0z 8014 Nonnegative integer property expressed in terms of integers. (Contributed by NM, 9-May-2004.)
(𝑁 0 ↔ (𝑁 0 ≤ 𝑁))

Theoremelznn0nn 8015 Integer property expressed in terms nonnegative integers and positive integers. (Contributed by NM, 10-May-2004.)
(𝑁 ℤ ↔ (𝑁 0 (𝑁 -𝑁 ℕ)))

Theoremelznn0 8016 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ ↔ (𝑁 (𝑁 0 -𝑁 0)))

Theoremelznn 8017 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
(𝑁 ℤ ↔ (𝑁 (𝑁 -𝑁 0)))

Theoremnnssz 8018 Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.)
ℕ ⊆ ℤ

Theoremnn0ssz 8019 Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004.)
0 ⊆ ℤ

Theoremnnz 8020 A positive integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 ℕ → 𝑁 ℤ)

Theoremnn0z 8021 A nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 0𝑁 ℤ)

Theoremnnzi 8022 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁        𝑁

Theoremnn0zi 8023 A nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁 0       𝑁

Theoremelnnz1 8024 Positive integer property expressed in terms of integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
(𝑁 ℕ ↔ (𝑁 1 ≤ 𝑁))

Theoremnnzrab 8025 Positive integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
ℕ = {x ℤ ∣ 1 ≤ x}

Theoremnn0zrab 8026 Nonnegative integers expressed as a subset of integers. (Contributed by NM, 3-Oct-2004.)
0 = {x ℤ ∣ 0 ≤ x}

Theorem1z 8027 One is an integer. (Contributed by NM, 10-May-2004.)
1

Theorem1zzd 8028 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
(φ → 1 ℤ)

Theorem2z 8029 Two is an integer. (Contributed by NM, 10-May-2004.)
2

Theorem3z 8030 3 is an integer. (Contributed by David A. Wheeler, 8-Dec-2018.)
3

Theorem4z 8031 4 is an integer. (Contributed by BJ, 26-Mar-2020.)
4

Theoremznegcl 8032 Closure law for negative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ℤ → -𝑁 ℤ)

Theoremneg1z 8033 -1 is an integer (common case). (Contributed by David A. Wheeler, 5-Dec-2018.)
-1

Theoremznegclb 8034 A number is an integer iff its negative is. (Contributed by Stefan O'Rear, 13-Sep-2014.)
(A ℂ → (A ℤ ↔ -A ℤ))

Theoremnn0negz 8035 The negative of a nonnegative integer is an integer. (Contributed by NM, 9-May-2004.)
(𝑁 0 → -𝑁 ℤ)

Theoremnn0negzi 8036 The negative of a nonnegative integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁 0       -𝑁

Theorempeano2z 8037 Second Peano postulate generalized to integers. (Contributed by NM, 13-Feb-2005.)
(𝑁 ℤ → (𝑁 + 1) ℤ)

Theoremzaddcllempos 8038 Lemma for zaddcl 8041. Special case in which 𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℕ) → (𝑀 + 𝑁) ℤ)

Theorempeano2zm 8039 "Reverse" second Peano postulate for integers. (Contributed by NM, 12-Sep-2005.)
(𝑁 ℤ → (𝑁 − 1) ℤ)

Theoremzaddcllemneg 8040 Lemma for zaddcl 8041. Special case in which -𝑁 is a positive integer. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 -𝑁 ℕ) → (𝑀 + 𝑁) ℤ)

Theoremzaddcl 8041 Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 𝑁 ℤ) → (𝑀 + 𝑁) ℤ)

Theoremzsubcl 8042 Closure of subtraction of integers. (Contributed by NM, 11-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁) ℤ)

Theoremztri3or0 8043 Integer trichotomy (with zero). (Contributed by Jim Kingdon, 14-Mar-2020.)
(𝑁 ℤ → (𝑁 < 0 𝑁 = 0 0 < 𝑁))

Theoremztri3or 8044 Integer trichotomy. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 𝑀 = 𝑁 𝑁 < 𝑀))

Theoremzletric 8045 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
((A B ℤ) → (AB BA))

Theoremzlelttric 8046 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
((A B ℤ) → (AB B < A))

Theoremzltnle 8047 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ ¬ BA))

Theoremzleloe 8048 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 8049 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
(𝑁 ℤ → (¬ 𝑁 ℕ ↔ 𝑁 < 1))

Theoremzletr 8050 Transitive law of ordering for integers. (Contributed by Alexander van der Vekens, 3-Apr-2018.)
((𝐽 𝐾 𝐿 ℤ) → ((𝐽𝐾 𝐾𝐿) → 𝐽𝐿))

Theoremzrevaddcl 8051 Reverse closure law for addition of integers. (Contributed by NM, 11-May-2004.)
(𝑁 ℤ → ((𝑀 (𝑀 + 𝑁) ℤ) ↔ 𝑀 ℤ))

Theoremznnsub 8052 The positive difference of unequal integers is a positive integer. (Generalization of nnsub 7713.) (Contributed by NM, 11-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 ↔ (𝑁𝑀) ℕ))

Theoremzmulcl 8053 Closure of multiplication of integers. (Contributed by NM, 30-Jul-2004.)
((𝑀 𝑁 ℤ) → (𝑀 · 𝑁) ℤ)

Theoremzltp1le 8054 Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

Theoremzleltp1 8055 Integer ordering relation. (Contributed by NM, 10-May-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁𝑀 < (𝑁 + 1)))

Theoremzlem1lt 8056 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
((𝑀 𝑁 ℤ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))

Theoremzltlem1 8057 Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
((𝑀 𝑁 ℤ) → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))

Theoremzgt0ge1 8058 An integer greater than 0 is greater than or equal to 1. (Contributed by AV, 14-Oct-2018.)
(𝑍 ℤ → (0 < 𝑍 ↔ 1 ≤ 𝑍))

Theoremnnleltp1 8059 Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((A B ℕ) → (ABA < (B + 1)))

Theoremnnltp1le 8060 Positive integer ordering relation. (Contributed by NM, 19-Aug-2001.)
((A B ℕ) → (A < B ↔ (A + 1) ≤ B))

Theoremnnaddm1cl 8061 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 8062 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 0 𝑁 0) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

Theoremnn0leltp1 8063 Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004.)
((𝑀 0 𝑁 0) → (𝑀𝑁𝑀 < (𝑁 + 1)))

Theoremnn0ltlem1 8064 Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
((𝑀 0 𝑁 0) → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))

Theoremznn0sub 8065 The nonnegative difference of integers is a nonnegative integer. (Generalization of nn0sub 8066.) (Contributed by NM, 14-Jul-2005.)
((𝑀 𝑁 ℤ) → (𝑀𝑁 ↔ (𝑁𝑀) 0))

Theoremnn0sub 8066 Subtraction of nonnegative integers. (Contributed by NM, 9-May-2004.)
((𝑀 0 𝑁 0) → (𝑀𝑁 ↔ (𝑁𝑀) 0))

Theoremnn0n0n1ge2 8067 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 8068* 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 8069 Alternative definition of the integers, based on elz2 8068. (Contributed by Mario Carneiro, 16-May-2014.)
ℤ = ( − “ (ℕ × ℕ))

Theoremnn0sub2 8070 Subtraction of nonnegative integers. (Contributed by NM, 4-Sep-2005.)
((𝑀 0 𝑁 0 𝑀𝑁) → (𝑁𝑀) 0)

Theoremzapne 8071 Apartness is equivalent to not equal for integers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝑀 𝑁 ℤ) → (𝑀 # 𝑁𝑀𝑁))

Theoremzdceq 8072 Equality of integers is decidable. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → DECID A = B)

Theoremzdcle 8073 Integer is decidable. (Contributed by Jim Kingdon, 7-Apr-2020.)
((A B ℤ) → DECID AB)

Theoremzdclt 8074 Integer < is decidable. (Contributed by Jim Kingdon, 1-Jun-2020.)
((A B ℤ) → DECID A < B)

Theoremzltlen 8075 Integer 'Less than' expressed in terms of 'less than or equal to'. Also see ltleap 7393 which is a similar result for complex numbers. (Contributed by Jim Kingdon, 14-Mar-2020.)
((A B ℤ) → (A < B ↔ (AB BA)))

Theoremnn0n0n1ge2b 8076 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 8077 A nonnegative integer less than 1 is 0. (Contributed by Paul Chapman, 22-Jun-2011.)
(𝑁 0 → (𝑁 < 1 ↔ 𝑁 = 0))

Theoremnn0lt2 8078 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 8079 Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005.)
((𝑀 0 𝑁 0) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))

Theoremnnlem1lt 8080 Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
((𝑀 𝑁 ℕ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))

Theoremnnltlem1 8081 Positive integer ordering relation. (Contributed by NM, 21-Jun-2005.)
((𝑀 𝑁 ℕ) → (𝑀 < 𝑁𝑀 ≤ (𝑁 − 1)))

Theoremnnm1ge0 8082 A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018.)
(𝑁 ℕ → 0 ≤ (𝑁 − 1))

Theoremnn0ge0div 8083 Division of a nonnegative integer by a positive number is not negative. (Contributed by Alexander van der Vekens, 14-Apr-2018.)
((𝐾 0 𝐿 ℕ) → 0 ≤ (𝐾 / 𝐿))

Theoremzdiv 8084* Two ways to express "𝑀 divides 𝑁. (Contributed by NM, 3-Oct-2008.)
((𝑀 𝑁 ℤ) → (𝑘 ℤ (𝑀 · 𝑘) = 𝑁 ↔ (𝑁 / 𝑀) ℤ))

Theoremzdivadd 8085 Property of divisibility: if 𝐷 divides A and B then it divides A + B. (Contributed by NM, 3-Oct-2008.)
(((𝐷 A B ℤ) ((A / 𝐷) (B / 𝐷) ℤ)) → ((A + B) / 𝐷) ℤ)

Theoremzdivmul 8086 Property of divisibility: if 𝐷 divides A then it divides B · A. (Contributed by NM, 3-Oct-2008.)
(((𝐷 A B ℤ) (A / 𝐷) ℤ) → ((B · A) / 𝐷) ℤ)

Theoremzextle 8087* An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
((𝑀 𝑁 𝑘 ℤ (𝑘𝑀𝑘𝑁)) → 𝑀 = 𝑁)

Theoremzextlt 8088* An extensionality-like property for integer ordering. (Contributed by NM, 29-Oct-2005.)
((𝑀 𝑁 𝑘 ℤ (𝑘 < 𝑀𝑘 < 𝑁)) → 𝑀 = 𝑁)

Theoremrecnz 8089 The reciprocal of a number greater than 1 is not an integer. (Contributed by NM, 3-May-2005.)
((A 1 < A) → ¬ (1 / A) ℤ)

Theorembtwnnz 8090 A number between an integer and its successor is not an integer. (Contributed by NM, 3-May-2005.)
((A A < B B < (A + 1)) → ¬ B ℤ)

Theoremgtndiv 8091 A larger number does not divide a smaller positive integer. (Contributed by NM, 3-May-2005.)
((A B B < A) → ¬ (B / A) ℤ)

Theoremhalfnz 8092 One-half is not an integer. (Contributed by NM, 31-Jul-2004.)
¬ (1 / 2)

Theoremprime 8093* Two ways to express "A is a prime number (or 1)." (Contributed by NM, 4-May-2005.)
(A ℕ → (x ℕ ((A / x) ℕ → (x = 1 x = A)) ↔ x ℕ ((1 < x xA (A / x) ℕ) → x = A)))

Theoremmsqznn 8094 The square of a nonzero integer is a positive integer. (Contributed by NM, 2-Aug-2004.)
((A A ≠ 0) → (A · A) ℕ)

Theoremzneo 8095 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.) (Proof shortened by Mario Carneiro, 18-May-2014.)
((A B ℤ) → (2 · A) ≠ ((2 · B) + 1))

Theoremnneoor 8096 A positive integer is even or odd. (Contributed by Jim Kingdon, 15-Mar-2020.)
(𝑁 ℕ → ((𝑁 / 2) ((𝑁 + 1) / 2) ℕ))

Theoremnneo 8097 A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006.) (Proof shortened by Mario Carneiro, 18-May-2014.)
(𝑁 ℕ → ((𝑁 / 2) ℕ ↔ ¬ ((𝑁 + 1) / 2) ℕ))

Theoremnneoi 8098 A positive integer is even or odd but not both. (Contributed by NM, 20-Aug-2001.)
𝑁        ((𝑁 / 2) ℕ ↔ ¬ ((𝑁 + 1) / 2) ℕ)

Theoremzeo 8099 An integer is even or odd. (Contributed by NM, 1-Jan-2006.)
(𝑁 ℤ → ((𝑁 / 2) ((𝑁 + 1) / 2) ℤ))

Theoremzeo2 8100 An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015.)
(𝑁 ℤ → ((𝑁 / 2) ℤ ↔ ¬ ((𝑁 + 1) / 2) ℤ))

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-9427
 Copyright terms: Public domain < Previous  Next >