Home Intuitionistic Logic ExplorerTheorem List (p. 83 of 102) < 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 - 8201-8300   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theorem5nn0 8201 5 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
5 ∈ ℕ0

Theorem6nn0 8202 6 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
6 ∈ ℕ0

Theorem7nn0 8203 7 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
7 ∈ ℕ0

Theorem8nn0 8204 8 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
8 ∈ ℕ0

Theorem9nn0 8205 9 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
9 ∈ ℕ0

Theorem10nn0 8206 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
10 ∈ ℕ0

Theoremnn0ge0 8207 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 ≤ 𝑁)

Theoremnn0nlt0 8208 A nonnegative integer is not less than zero. (Contributed by NM, 9-May-2004.) (Revised by Mario Carneiro, 27-May-2016.)
(𝐴 ∈ ℕ0 → ¬ 𝐴 < 0)

Theoremnn0ge0i 8209 Nonnegative integers are nonnegative. (Contributed by Raph Levien, 10-Dec-2002.)
𝑁 ∈ ℕ0       0 ≤ 𝑁

Theoremnn0le0eq0 8210 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))

Theoremnn0p1gt0 8211 A nonnegative integer increased by 1 is greater than 0. (Contributed by Alexander van der Vekens, 3-Oct-2018.)
(𝑁 ∈ ℕ0 → 0 < (𝑁 + 1))

Theoremnnnn0addcl 8212 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) → (𝑀 + 𝑁) ∈ ℕ)

Theoremnn0nnaddcl 8213 A nonnegative integer plus a positive integer is a positive integer. (Contributed by NM, 22-Dec-2005.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℕ)

Theorem0mnnnnn0 8214 The result of subtracting a positive integer from 0 is not a nonnegative integer. (Contributed by Alexander van der Vekens, 19-Mar-2018.)
(𝑁 ∈ ℕ → (0 − 𝑁) ∉ ℕ0)

Theoremun0addcl 8215 If 𝑆 is closed under addition, then so is 𝑆 ∪ {0}. (Contributed by Mario Carneiro, 17-Jul-2014.)
(𝜑𝑆 ⊆ ℂ)    &   𝑇 = (𝑆 ∪ {0})    &   ((𝜑 ∧ (𝑀𝑆𝑁𝑆)) → (𝑀 + 𝑁) ∈ 𝑆)       ((𝜑 ∧ (𝑀𝑇𝑁𝑇)) → (𝑀 + 𝑁) ∈ 𝑇)

Theoremun0mulcl 8216 If 𝑆 is closed under multiplication, then so is 𝑆 ∪ {0}. (Contributed by Mario Carneiro, 17-Jul-2014.)
(𝜑𝑆 ⊆ ℂ)    &   𝑇 = (𝑆 ∪ {0})    &   ((𝜑 ∧ (𝑀𝑆𝑁𝑆)) → (𝑀 · 𝑁) ∈ 𝑆)       ((𝜑 ∧ (𝑀𝑇𝑁𝑇)) → (𝑀 · 𝑁) ∈ 𝑇)

Theoremnn0addcl 8217 Closure of addition of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0)

Theoremnn0mulcl 8218 Closure of multiplication of nonnegative integers. (Contributed by NM, 22-Jul-2004.) (Proof shortened by Mario Carneiro, 17-Jul-2014.)
((𝑀 ∈ ℕ0𝑁 ∈ ℕ0) → (𝑀 · 𝑁) ∈ ℕ0)

Theoremnn0addcli 8219 Closure of addition of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
𝑀 ∈ ℕ0    &   𝑁 ∈ ℕ0       (𝑀 + 𝑁) ∈ ℕ0

Theoremnn0mulcli 8220 Closure of multiplication of nonnegative integers, inference form. (Contributed by Raph Levien, 10-Dec-2002.)
𝑀 ∈ ℕ0    &   𝑁 ∈ ℕ0       (𝑀 · 𝑁) ∈ ℕ0

Theoremnn0p1nn 8221 A nonnegative integer plus 1 is a positive integer. (Contributed by Raph Levien, 30-Jun-2006.) (Revised by Mario Carneiro, 16-May-2014.)
(𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ)

Theorempeano2nn0 8222 Second Peano postulate for nonnegative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ∈ ℕ0 → (𝑁 + 1) ∈ ℕ0)

Theoremnnm1nn0 8223 A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007.) (Revised by Mario Carneiro, 16-May-2014.)
(𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)

Theoremelnn0nn 8224 The nonnegative integer property expressed in terms of positive integers. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
(𝑁 ∈ ℕ0 ↔ (𝑁 ∈ ℂ ∧ (𝑁 + 1) ∈ ℕ))

Theoremelnnnn0 8225 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-May-2004.)
(𝑁 ∈ ℕ ↔ (𝑁 ∈ ℂ ∧ (𝑁 − 1) ∈ ℕ0))

Theoremelnnnn0b 8226 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 1-Sep-2005.)
(𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 0 < 𝑁))

Theoremelnnnn0c 8227 The positive integer property expressed in terms of nonnegative integers. (Contributed by NM, 10-Jan-2006.)
(𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 1 ≤ 𝑁))

Theoremnn0addge1 8228 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝐴 + 𝑁))

Theoremnn0addge2 8229 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → 𝐴 ≤ (𝑁 + 𝐴))

Theoremnn0addge1i 8230 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
𝐴 ∈ ℝ    &   𝑁 ∈ ℕ0       𝐴 ≤ (𝐴 + 𝑁)

Theoremnn0addge2i 8231 A number is less than or equal to itself plus a nonnegative integer. (Contributed by NM, 10-Mar-2005.)
𝐴 ∈ ℝ    &   𝑁 ∈ ℕ0       𝐴 ≤ (𝑁 + 𝐴)

Theoremnn0le2xi 8232 A nonnegative integer is less than or equal to twice itself. (Contributed by Raph Levien, 10-Dec-2002.)
𝑁 ∈ ℕ0       𝑁 ≤ (2 · 𝑁)

Theoremnn0lele2xi 8233 '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 8234 Two ways to write the support of a function on 0. (Contributed by Mario Carneiro, 29-Dec-2014.)
(𝐹:𝐼⟶ℕ0 → (𝐹 “ (V ∖ {0})) = (𝐹 “ ℕ))

Theoremnnnn0d 8235 A positive integer is a nonnegative integer. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ)       (𝜑𝐴 ∈ ℕ0)

Theoremnn0red 8236 A nonnegative integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ0)       (𝜑𝐴 ∈ ℝ)

Theoremnn0cnd 8237 A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ0)       (𝜑𝐴 ∈ ℂ)

Theoremnn0ge0d 8238 A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ0)       (𝜑 → 0 ≤ 𝐴)

Theoremnn0addcld 8239 Closure of addition of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)       (𝜑 → (𝐴 + 𝐵) ∈ ℕ0)

Theoremnn0mulcld 8240 Closure of multiplication of nonnegative integers, inference form. (Contributed by Mario Carneiro, 27-May-2016.)
(𝜑𝐴 ∈ ℕ0)    &   (𝜑𝐵 ∈ ℕ0)       (𝜑 → (𝐴 · 𝐵) ∈ ℕ0)

Theoremnn0readdcl 8241 Closure law for addition of reals, restricted to nonnegative integers. (Contributed by Alexander van der Vekens, 6-Apr-2018.)
((𝐴 ∈ ℕ0𝐵 ∈ ℕ0) → (𝐴 + 𝐵) ∈ ℝ)

Theoremnn0ge2m1nn 8242 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 8243 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 8244 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 8245 Extend class notation to include the class of integers.
class

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

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

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

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

Theoremzrei 8251 An integer is a real number. (Contributed by NM, 14-Jul-2005.)
𝐴 ∈ ℤ       𝐴 ∈ ℝ

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

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

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

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

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

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

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

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

Theoremelznn0 8260 Integer property expressed in terms of nonnegative integers. (Contributed by NM, 9-May-2004.)
(𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))

Theoremelznn 8261 Integer property expressed in terms of positive integers and nonnegative integers. (Contributed by NM, 12-Jul-2005.)
(𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ0)))

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

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

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

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

Theoremnnzi 8266 A positive integer is an integer. (Contributed by Mario Carneiro, 18-Feb-2014.)
𝑁 ∈ ℕ       𝑁 ∈ ℤ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremzletric 8289 Trichotomy law. (Contributed by Jim Kingdon, 27-Mar-2020.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴𝐵𝐵𝐴))

Theoremzlelttric 8290 Trichotomy law. (Contributed by Jim Kingdon, 17-Apr-2020.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴𝐵𝐵 < 𝐴))

Theoremzltnle 8291 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Jim Kingdon, 14-Mar-2020.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Theoremzleloe 8292 Integer 'Less than or equal to' expressed in terms of 'less than' or 'equals'. (Contributed by Jim Kingdon, 8-Apr-2020.)
((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴𝐵 ↔ (𝐴 < 𝐵𝐴 = 𝐵)))

Theoremznnnlt1 8293 An integer is not a positive integer iff it is less than one. (Contributed by NM, 13-Jul-2005.)
(𝑁 ∈ ℤ → (¬ 𝑁 ∈ ℕ ↔ 𝑁 < 1))

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

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

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

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

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

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

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

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-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10124
 Copyright terms: Public domain < Previous  Next >