Theorem zltp1le 12555

Description: Integer ordering relation. (Contributed by NM, 10-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)

Assertion

Ref	Expression
zltp1le	⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

Proof of Theorem zltp1le

Step	Hyp	Ref	Expression
1		nnge1 12187	. . . 4 ⊢ ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀))
2	1	a1i 11	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀)))
3		znnsub 12551	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))
4		zre 12506	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 12506	. . . 4 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		1re 11146	. . . . 5 ⊢ 1 ∈ ℝ
7		leaddsub2 11628	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
8	6, 7	mp3an2 1452	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
9	4, 5, 8	syl2an 597	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
10	2, 3, 9	3imtr4d 294	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 → (𝑀 + 1) ≤ 𝑁))
11	4	adantr 480	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ)
12	11	ltp1d 12086	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 < (𝑀 + 1))
13		peano2re 11320	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
14	11, 13	syl 17	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 1) ∈ ℝ)
15	5	adantl 481	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
16		ltletr 11239	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
17	11, 14, 15, 16	syl3anc 1374	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
18	12, 17	mpand 696	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 → 𝑀 < 𝑁))
19	10, 18	impbid 212	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  (class class class)co 7370  ℝcr 11039  1c1 11041   + caddc 11043   < clt 11180   ≤ cle 11181   − cmin 11378  ℕcn 12159  ℤcz 12502

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-resscn 11097  ax-1cn 11098  ax-icn 11099  ax-addcl 11100  ax-addrcl 11101  ax-mulcl 11102  ax-mulrcl 11103  ax-mulcom 11104  ax-addass 11105  ax-mulass 11106  ax-distr 11107  ax-i2m1 11108  ax-1ne0 11109  ax-1rid 11110  ax-rnegex 11111  ax-rrecex 11112  ax-cnre 11113  ax-pre-lttri 11114  ax-pre-lttrn 11115  ax-pre-ltadd 11116  ax-pre-mulgt0 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-riota 7327  df-ov 7373  df-oprab 7374  df-mpo 7375  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-sub 11380  df-neg 11381  df-nn 12160  df-n0 12416  df-z 12503

This theorem is referenced by:  zleltp1  12556  zlem1lt  12557  zgt0ge1  12560  nnltp1le  12562  nn0ltp1le  12564  btwnnz  12582  uzind2  12599  fzind  12604  eluzp1l  12792  eluz2b1  12846  zltaddlt1le  13435  fzsplit2  13479  fzdif1  13535  elfzop1le2  13602  m1modge3gt1  13855  bcval5  14255  seqcoll  14401  hashge2el2dif  14417  hashge2el2difr  14418  swrd2lsw  14889  2swrd2eqwrdeq  14890  isercoll  15605  nn0o1gt2  16322  divalglem6  16339  isprm3  16624  dvdsnprmd  16631  2mulprm  16634  oddprmge3  16641  ge2nprmge4  16642  hashdvds  16716  prmreclem5  16862  prmgaplem3  16995  prmgaplem5  16997  prmgaplem6  16998  prmgaplem8  17000  chnccat  18563  sylow1lem3  19546  chfacfscmul0  22819  chfacfscmulfsupp  22820  chfacfpmmul0  22823  chfacfpmmulfsupp  22824  dyaddisjlem  25569  plyeq0lem  26188  basellem2  27065  chtub  27196  bposlem9  27276  lgsdilem2  27317  lgsquadlem1  27364  2lgslem1a  27375  pntpbnd1  27570  pntpbnd2  27571  tgldimor  28592  eucrct2eupth  30338  konigsberglem5  30349  nndiffz1  32883  ltesubnnd  32920  dp2ltc  32985  smatrcl  33980  breprexplemc  34816  zltp1ne  35332  dnibndlem13  36718  knoppndvlem6  36745  poimirlem3  37903  poimirlem4  37904  poimirlem15  37915  poimirlem17  37917  poimirlem28  37928  zltp1led  42378  lcmineqlem11  42438  lcmineqlem23  42450  lcmineqlem  42451  sticksstones10  42554  eluzp1  42706  ellz1  43153  lzunuz  43154  rmygeid  43350  jm3.1lem2  43404  fzuntgd  43843  bccbc  44730  monoords  45688  fmul01lt1lem1  45973  dvnxpaek  46329  iblspltprt  46360  itgspltprt  46366  fourierdlem6  46500  fourierdlem12  46506  fourierdlem19  46513  fourierdlem42  46536  fourierdlem48  46541  fourierdlem49  46542  fourierdlem79  46572  ormkglobd  47262  addmodne  47733  m1modnep2mod  47741  iccpartiltu  47811  iccpartgt  47816  icceuelpartlem  47824  iccpartnel  47827  lighneallem4b  47998  evenltle  48106  gbowge7  48152  gbege6  48154  stgoldbwt  48165  sbgoldbwt  48166  sbgoldbalt  48170  sbgoldbm  48173  bgoldbtbndlem1  48194  tgblthelfgott  48204  elfzolborelfzop1  48908