Theorem zltp1le 12693

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 12313	. . . 4 ⊢ ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀))
2	1	a1i 11	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀)))
3		znnsub 12689	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))
4		zre 12644	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 12644	. . . 4 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		1re 11257	. . . . 5 ⊢ 1 ∈ ℝ
7		leaddsub2 11740	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
8	6, 7	mp3an2 1478	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
9	4, 5, 8	syl2an 608	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
10	2, 3, 9	3imtr4d 297	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 → (𝑀 + 1) ≤ 𝑁))
11	4	adantr 486	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ)
12	11	ltp1d 12194	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 < (𝑀 + 1))
13		peano2re 11432	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
14	11, 13	syl 18	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 1) ∈ ℝ)
15	5	adantl 487	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
16		ltletr 11351	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
17	11, 14, 15, 16	syl3anc 1398	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
18	12, 17	mpand 708	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 → 𝑀 < 𝑁))
19	10, 18	impbid 215	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  (class class class)co 7416  ℝcr 11148  1c1 11150   + caddc 11152   < clt 11292   ≤ cle 11293   − cmin 11490  ℕcn 12282  ℤcz 12640

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7742  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6301  df-ord 6362  df-on 6363  df-lim 6364  df-suc 6365  df-iota 6491  df-fun 6537  df-fn 6538  df-f 6539  df-f1 6540  df-fo 6541  df-f1o 6542  df-fv 6543  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8365  df-rdg 8404  df-er 8703  df-en 8960  df-dom 8961  df-sdom 8962  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11492  df-neg 11493  df-nn 12283  df-n0 12554  df-z 12641

This theorem is used by:  zleltp1  12694  zlem1lt  12695  zltp1led  12698  zgt0ge1  12699  nnltp1le  12702  nn0ltp1le  12704  btwnnz  12722  uzind2  12739  fzind  12744  eluzp1l  12939  eluz2b1  12993  zltaddlt1le  13583  fzsplit2  13629  fzdif1  13685  elfzop1le2  13753  m1modge3gt1  14007  bcval5  14407  seqcoll  14554  hashge2el2dif  14570  hashge2el2difr  14571  swrd2lsw  15050  2swrd2eqwrdeq  15051  isercoll  15780  nn0o1gt2  16496  divalglem6  16513  isprm3  16798  dvdsnprmd  16805  2mulprm  16808  oddprmge3  16816  ge2nprmge4  16817  hashdvds  16891  prmreclem5  17037  prmgaplem3  17170  prmgaplem5  17172  prmgaplem6  17173  prmgaplem8  17175  chnccat  18739  sylow1lem3  19753  chfacfscmul0  23115  chfacfscmulfsupp  23116  chfacfpmmul0  23119  chfacfpmmulfsupp  23120  dyaddisjlem  25855  plyeq0lem  26468  basellem2  27350  chtub  27480  bposlem9  27560  lgsdilem2  27601  lgsquadlem1  27648  2lgslem1a  27659  pntpbnd1  27854  pntpbnd2  27855  tgldimor  28876  eucrct2eupth  30757  konigsberglem5  30768  nndiffz1  33289  ltesubnnd  33325  dp2ltc  33364  smatrcl  34339  breprexplemc  35173  zltp1ne  35797  dnibndlem13  37254  knoppndvlem6  37281  poimirlem3  38437  poimirlem4  38438  poimirlem15  38449  poimirlem17  38451  poimirlem28  38462  lcmineqlem11  42970  lcmineqlem23  42982  lcmineqlem  42983  sticksstones10  43086  eluzp1  43247  ellz1  43677  lzunuz  43678  rmygeid  43870  jm3.1lem2  43924  fzuntgd  44363  bccbc  45234  monoords  46195  fmul01lt1lem1  46479  dvnxpaek  46835  iblspltprt  46866  itgspltprt  46872  fourierdlem6  47006  fourierdlem12  47012  fourierdlem19  47019  fourierdlem42  47042  fourierdlem79  47078  addmodne  48303  m1modnep2mod  48311  iccpartiltu  48387  iccpartgt  48392  icceuelpartlem  48400  iccpartnel  48403  lighneallem4b  48577  evenltle  48698  gbowge7  48744  gbege6  48746  stgoldbwt  48757  sbgoldbwt  48758  sbgoldbalt  48762  sbgoldbm  48765  bgoldbtbndlem1  48786  tgblthelfgott  48796  elfzolborelfzop1  49514