ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zltp1le GIF version

Theorem zltp1le 9239
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
StepHypRef Expression
1 nnge1 8874 . . . 4 ((𝑁𝑀) ∈ ℕ → 1 ≤ (𝑁𝑀))
21a1i 9 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁𝑀) ∈ ℕ → 1 ≤ (𝑁𝑀)))
3 znnsub 9236 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑁𝑀) ∈ ℕ))
4 zre 9189 . . . 4 (𝑀 ∈ ℤ → 𝑀 ∈ ℝ)
5 zre 9189 . . . 4 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
6 1re 7892 . . . . 5 1 ∈ ℝ
7 leaddsub2 8331 . . . . 5 ((𝑀 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑀)))
86, 7mp3an2 1314 . . . 4 ((𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑀)))
94, 5, 8syl2an 287 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁 ↔ 1 ≤ (𝑁𝑀)))
102, 3, 93imtr4d 202 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 → (𝑀 + 1) ≤ 𝑁))
114adantr 274 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℝ)
1211ltp1d 8819 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 < (𝑀 + 1))
13 peano2re 8028 . . . . 5 (𝑀 ∈ ℝ → (𝑀 + 1) ∈ ℝ)
1411, 13syl 14 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 1) ∈ ℝ)
155adantl 275 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈ ℝ)
16 ltletr 7982 . . . 4 ((𝑀 ∈ ℝ ∧ (𝑀 + 1) ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
1711, 14, 15, 16syl3anc 1227 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 < (𝑀 + 1) ∧ (𝑀 + 1) ≤ 𝑁) → 𝑀 < 𝑁))
1812, 17mpand 426 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 + 1) ≤ 𝑁𝑀 < 𝑁))
1910, 18impbid 128 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 < 𝑁 ↔ (𝑀 + 1) ≤ 𝑁))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wcel 2135   class class class wbr 3979  (class class class)co 5839  cr 7746  1c1 7748   + caddc 7750   < clt 7927  cle 7928  cmin 8063  cn 8851  cz 9185
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4097  ax-pow 4150  ax-pr 4184  ax-un 4408  ax-setind 4511  ax-cnex 7838  ax-resscn 7839  ax-1cn 7840  ax-1re 7841  ax-icn 7842  ax-addcl 7843  ax-addrcl 7844  ax-mulcl 7845  ax-addcom 7847  ax-addass 7849  ax-distr 7851  ax-i2m1 7852  ax-0lt1 7853  ax-0id 7855  ax-rnegex 7856  ax-cnre 7858  ax-pre-ltirr 7859  ax-pre-ltwlin 7860  ax-pre-lttrn 7861  ax-pre-ltadd 7863
This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2726  df-sbc 2950  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-pw 3558  df-sn 3579  df-pr 3580  df-op 3582  df-uni 3787  df-int 3822  df-br 3980  df-opab 4041  df-id 4268  df-xp 4607  df-rel 4608  df-cnv 4609  df-co 4610  df-dm 4611  df-iota 5150  df-fun 5187  df-fv 5193  df-riota 5795  df-ov 5842  df-oprab 5843  df-mpo 5844  df-pnf 7929  df-mnf 7930  df-xr 7931  df-ltxr 7932  df-le 7933  df-sub 8065  df-neg 8066  df-inn 8852  df-n0 9109  df-z 9186
This theorem is referenced by:  zleltp1  9240  zlem1lt  9241  zgt0ge1  9243  nnltp1le  9245  nn0ltp1le  9247  btwnnz  9279  uzind2  9297  fzind  9300  btwnapz  9315  eluzp1l  9484  eluz2b1  9533  zltaddlt1le  9937  fzsplit2  9979  m1modge3gt1  10300  seq3f1olemqsumkj  10427  seq3f1olemqsumk  10428  bcval5  10670  seq3coll  10749  cvgratnnlemseq  11461  nn0o1gt2  11836  divalglemnqt  11851  zsupcllemstep  11872  infssuzex  11876  suprzubdc  11879  isprm3  12044  dvdsnprmd  12051  prmgt1  12058  oddprmge3  12061  znege1  12104  hashdvds  12147
  Copyright terms: Public domain W3C validator