Theorem zltp1le 11540

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 11159	. . . 4 ⊢ ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀))
2	1	a1i 11	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 − 𝑀) ∈ ℕ → 1 ≤ (𝑁 − 𝑀)))
3		znnsub 11536	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁 − 𝑀) ∈ ℕ))
4		zre 11494	. . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5		zre 11494	. . . 4 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6		1re 10152	. . . . 5 ⊢ 1 ∈ ℝ
7		leaddsub2 10618	. . . . 5 ⊢ ((𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
8	6, 7	mp3an2 1525	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
9	4, 5, 8	syl2an 495	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁 − 𝑀)))
10	2, 3, 9	3imtr4d 283	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 → (𝑀 + 1) ≤ 𝑁))
11	4	adantr 472	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ)
12	11	ltp1d 11067	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 < (𝑀 + 1))
13		peano2re 10322	. . . . 5 ⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
14	11, 13	syl 17	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 1) ∈ ℝ)
15	5	adantl 473	. . . 4 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
16		ltletr 10242	. . . 4 ⊢ ((𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
17	11, 14, 15, 16	syl3anc 1439	. . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
18	12, 17	mpand 713	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 → 𝑀 < 𝑁))
19	10, 18	impbid 202	1 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∈ wcel 2103   class class class wbr 4760  (class class class)co 6765  ℝcr 10048  1c1 10050   + caddc 10052   < clt 10187   ≤ cle 10188   − cmin 10379  ℕcn 11133  ℤcz 11490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-nn 11134  df-n0 11406  df-z 11491

This theorem is referenced by:  zleltp1  11541  zlem1lt  11542  zgt0ge1  11544  nnltp1le  11546  nn0ltp1le  11548  btwnnz  11566  uzind2  11583  fzind  11588  eluzp1l  11825  eluz2b1  11873  zltaddlt1le  12438  fzsplit2  12480  m1modge3gt1  12832  bcval5  13220  seqcoll  13361  hashge2el2dif  13375  hashge2el2difr  13376  swrd2lsw  13817  2swrd2eqwrdeq  13818  isercoll  14518  nn0o1gt2  15220  divalglem6  15244  isprm3  15519  dvdsnprmd  15526  prmgt1  15532  oddprmge3  15535  hashdvds  15603  prmreclem5  15747  prmgaplem3  15880  prmgaplem5  15882  prmgaplem6  15883  prmgaplem8  15885  sylow1lem3  18136  chfacfscmul0  20786  chfacfscmulfsupp  20787  chfacfpmmul0  20790  chfacfpmmulfsupp  20791  dyaddisjlem  23484  plyeq0lem  24086  basellem2  24928  chtub  25057  bposlem9  25137  lgsdilem2  25178  lgsquadlem1  25225  2lgslem1a  25236  pntpbnd1  25395  pntpbnd2  25396  tgldimor  25517  eucrct2eupth  27318  konigsberglem5  27329  nndiffz1  29778  ltesubnnd  29798  dp2ltc  29824  smatrcl  30092  breprexplemc  30940  dnibndlem13  32707  knoppndvlem6  32735  poimirlem3  33644  poimirlem4  33645  poimirlem15  33656  poimirlem17  33658  poimirlem28  33669  ellz1  37749  lzunuz  37750  rmygeid  37950  jm3.1lem2  38004  bccbc  38963  elfzop1le2  39918  monoords  39927  fmul01lt1lem1  40236  dvnxpaek  40577  iblspltprt  40609  itgspltprt  40615  fourierdlem6  40750  fourierdlem12  40756  fourierdlem19  40763  fourierdlem42  40786  fourierdlem48  40791  fourierdlem49  40792  fourierdlem79  40822  iccpartiltu  41785  iccpartgt  41790  icceuelpartlem  41798  iccpartnel  41801  lighneallem4b  41953  evenltle  42053  gbowge7  42078  gbege6  42080  stgoldbwt  42091  sbgoldbwt  42092  sbgoldbalt  42096  sbgoldbm  42099  bgoldbtbndlem1  42120  tgblthelfgott  42130  tgblthelfgottOLD  42136  elfzolborelfzop1  42736