MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zlem1lt Structured version   Visualization version   GIF version

Theorem zlem1lt 11675
Description: Integer ordering relation. (Contributed by NM, 13-Nov-2004.)
Assertion
Ref Expression
zlem1lt ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))

Proof of Theorem zlem1lt
StepHypRef Expression
1 peano2zm 11666 . . 3 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
2 zltp1le 11673 . . 3 (((𝑀 − 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 − 1) < 𝑁 ↔ ((𝑀 − 1) + 1) ≤ 𝑁))
31, 2sylan 575 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 − 1) < 𝑁 ↔ ((𝑀 − 1) + 1) ≤ 𝑁))
4 zcn 11628 . . . . 5 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
5 ax-1cn 10246 . . . . 5 1 ∈ ℂ
6 npcan 10543 . . . . 5 ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑀 − 1) + 1) = 𝑀)
74, 5, 6sylancl 580 . . . 4 (𝑀 ∈ ℤ → ((𝑀 − 1) + 1) = 𝑀)
87adantr 472 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 − 1) + 1) = 𝑀)
98breq1d 4818 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (((𝑀 − 1) + 1) ≤ 𝑁𝑀𝑁))
103, 9bitr2d 271 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀𝑁 ↔ (𝑀 − 1) < 𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155   class class class wbr 4808  (class class class)co 6841  cc 10186  1c1 10189   + caddc 10191   < clt 10327  cle 10328  cmin 10519  cz 11623
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-n0 11538  df-z 11624
This theorem is referenced by:  nn0lem1lt  11688  nnlem1lt  11689  zbtwnre  11986  uzdisj  12619  nn0disj  12662  fzon  12696  ssfzo12  12768  ceile  12855  cshwidxn  13838  bitsfzolem  15438  bitscmp  15442  bitsinv1lem  15445  hashdvds  15760  logf1o2  24686  ang180lem3  24831  lgsquadlem1  25395  fzsplit3  29936  ballotlemfc0  30936  ballotlemfcc  30937  ballotlemimin  30949  ballotlemfrceq  30972  ballotlemfrcn0  30973  poimirlem23  33788  poimirlem24  33789  irrapxlem3  37998  hashnzfz2  39126  fzdifsuc2  40095  stoweidlem26  40812  fourierdlem12  40905  fzoopth  42003  nnsum3primesle9  42290  evengpop3  42294  zgtp1leeq  42912  m1modmmod  42917  nnolog2flm1  42985
  Copyright terms: Public domain W3C validator