Theorem ltleii 10160

Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.)

Hypotheses

Ref	Expression
lt.1	|- A e. RR
lt.2	|- B e. RR
ltlei.1	|- A < B

Assertion

Ref	Expression
ltleii	|- A <_ B

Proof of Theorem ltleii

Step	Hyp	Ref	Expression
1		ltlei.1	. 2 |- A < B
2		lt.1	. . 3 |- A e. RR
3		lt.2	. . 3 |- B e. RR
4	2, 3	ltlei 10159	. 2 |- ( A < B -> A <_ B )
5	1, 4	ax-mp 5	1 |- A <_ B

Syntax hints:   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  0le1  10551  ledivp1i  10949  ltdivp1i  10950  1le2  11241  1le3  11244  halfge0  11249  decleh  11541  declecOLD  11544  uzuzle23  11729  fz0to4untppr  12442  fzo0to42pr  12555  faclbnd4lem1  13080  4bc2eq6  13116  sqrt9  14014  sqrt2gt1lt2  14015  absrdbnd  14081  sqrtpclii  14122  geo2lim  14606  0.999...  14612  0.999...OLD  14613  ef01bndlem  14914  sin01bnd  14915  cos01bnd  14916  cos2bnd  14918  rpnnen2lem3  14945  rpnnen2lem4  14946  rpnnen2lem9  14951  rpnnen2lem12  14954  flodddiv4  15137  bitsp1o  15155  strlemor1OLD  15969  strleun  15972  cnfldfun  19758  elii1  22734  htpycc  22779  pcoval1  22813  pco0  22814  pcoval2  22816  pcocn  22817  pcohtpylem  22819  pcopt  22822  pcopt2  22823  pcoass  22824  pcorevlem  22826  vitalilem4  23380  vitali  23382  mbfi1fseqlem6  23487  dveflem  23742  sinhalfpilem  24215  sincosq1lem  24249  sincos4thpi  24265  sincos6thpi  24267  tanregt0  24285  efif1olem4  24291  relogrn  24308  argregt0  24356  argrege0  24357  logneg2  24361  heron  24565  asin1  24621  reasinsin  24623  log2cnv  24671  log2tlbnd  24672  log2ub  24676  harmonicbnd3  24734  ppiublem1  24927  ppiub  24929  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem7  25015  bposlem8  25016  bposlem9  25017  lgsdir2lem1  25050  chebbnd1lem3  25160  dchrvmasumlema  25189  logdivsum  25222  mulog2sumlem2  25224  pntpbnd1a  25274  pntpbnd2  25276  pntlemk  25295  istrkg3ld  25360  axlowdimlem16  25837  axlowdimlem17  25838  axlowdim  25841  usgrexmplef  26151  upgr4cycl4dv4e  27045  konigsbergiedgw  27108  konigsbergiedgwOLD  27109  konigsberglem1  27114  konigsberglem2  27115  konigsberglem3  27116  ex-fl  27304  ex-sqrt  27311  ex-gcd  27314  normlem6  27972  sqsscirc1  29954  prodfzo03  30681  hgt750lemd  30726  hgt750lem  30729  hgt750lem2  30730  hgt750leme  30736  tgoldbachgnn  30737  logi  31620  dnizeq0  32465  cnndvlem1  32528  bj-pinftyccb  33108  bj-pinftynminfty  33114  tan2h  33401  fdc  33541  jm2.20nn  37564  areaquad  37802  sineq0ALT  39173  halffl  39510  itgsin0pilem1  40165  itgsinexplem1  40169  wallispilem2  40283  wallispilem4  40285  stirlinglem15  40305  stirlingr  40307  fourierdlem62  40385  fourierdlem77  40400  fourierdlem102  40425  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  fourierdlem112  40435  fourierdlem114  40437  sqwvfoura  40445  sqwvfourb  40446  fourierswlem  40447  fouriersw  40448  etransclem23  40474  etransclem46  40497  smfmullem4  41001  fmtnoprmfac2lem1  41478  fmtno4prmfac  41484  31prm  41512  mod42tp1mod8  41519  sbgoldbo  41675  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  tgblthelfgott  41703  tgblthelfgottOLD  41709