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

Theorem nnleltp1 10427
Description: Positive integer ordering relation. (Contributed by NM, 13-Aug-2001.) (Proof shortened by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
nnleltp1 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴𝐵𝐴 < (𝐵 + 1)))

Proof of Theorem nnleltp1
StepHypRef Expression
1 nnz 10401 . 2 (𝐴 ∈ ℕ → 𝐴 ∈ ℤ)
2 nnz 10401 . 2 (𝐵 ∈ ℕ → 𝐵 ∈ ℤ)
3 zleltp1 10424 . 2 ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (𝐴𝐵𝐴 < (𝐵 + 1)))
41, 2, 3syl2an 465 1 ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (𝐴𝐵𝐴 < (𝐵 + 1)))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 178  wa 360  wcel 1734   class class class wbr 4293  (class class class)co 6181  1c1 9088   + caddc 9090   < clt 9217  cle 9218  cn 10098  cz 10380
This theorem is referenced by:  eftlub  12830  eirrlem  12923  sqr2irr  12968  pcmpt  13381  infpnlem2  13399  prmreclem5  13408  ovolicc2lem3  19547  voliunlem1  19576  lgsquadlem2  21271  lgamcvg2  25305  wallispilem3  28310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1562  ax-5 1573  ax-17 1636  ax-9 1677  ax-8 1698  ax-13 1736  ax-14 1738  ax-6 1753  ax-7 1758  ax-11 1770  ax-12 1963  ax-ext 2460  ax-sep 4414  ax-nul 4422  ax-pow 4467  ax-pr 4493  ax-un 4793  ax-resscn 9144  ax-1cn 9145  ax-icn 9146  ax-addcl 9147  ax-addrcl 9148  ax-mulcl 9149  ax-mulrcl 9150  ax-mulcom 9151  ax-addass 9152  ax-mulass 9153  ax-distr 9154  ax-i2m1 9155  ax-1ne0 9156  ax-1rid 9157  ax-rnegex 9158  ax-rrecex 9159  ax-cnre 9160  ax-pre-lttri 9161  ax-pre-lttrn 9162  ax-pre-ltadd 9163  ax-pre-mulgt0 9164
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 939  df-3an 940  df-tru 1334  df-ex 1558  df-nf 1561  df-sb 1669  df-eu 2325  df-mo 2326  df-clab 2466  df-cleq 2472  df-clel 2475  df-nfc 2604  df-ne 2644  df-nel 2645  df-ral 2753  df-rex 2754  df-reu 2755  df-rab 2757  df-v 3005  df-sbc 3210  df-csb 3311  df-dif 3353  df-un 3355  df-in 3357  df-ss 3364  df-pss 3366  df-nul 3658  df-if 3810  df-pw 3875  df-sn 3894  df-pr 3895  df-tp 3896  df-op 3897  df-uni 4094  df-iun 4174  df-br 4294  df-opab 4352  df-mpt 4353  df-tr 4387  df-eprel 4586  df-id 4590  df-po 4595  df-so 4596  df-fr 4633  df-we 4635  df-ord 4676  df-on 4677  df-lim 4678  df-suc 4679  df-om 4938  df-xp 4976  df-rel 4977  df-cnv 4978  df-co 4979  df-dm 4980  df-rn 4981  df-res 4982  df-ima 4983  df-iota 5516  df-fun 5555  df-fn 5556  df-f 5557  df-f1 5558  df-fo 5559  df-f1o 5560  df-fv 5561  df-ov 6184  df-oprab 6185  df-mpt2 6186  df-riota 6654  df-recs 6728  df-rdg 6763  df-er 7000  df-en 7205  df-dom 7206  df-sdom 7207  df-pnf 9219  df-mnf 9220  df-xr 9221  df-ltxr 9222  df-le 9223  df-sub 9391  df-neg 9392  df-nn 10099  df-n0 10320  df-z 10381
  Copyright terms: Public domain W3C validator