Theorem ltle 10718

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

Assertion

Ref	Expression
ltle	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Proof of Theorem ltle

Step	Hyp	Ref	Expression
1		orc 864	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		leloe 10716	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	syl5ibr 249	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   class class class wbr 5030  ℝcr 10525   < clt 10664   ≤ cle 10665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-resscn 10583  ax-pre-lttri 10600

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-er 8272  df-en 8493  df-dom 8494  df-sdom 8495  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670

This theorem is referenced by:  ltleletr  10722  letr  10723  letric  10729  ltlen  10730  ltlei  10751  ltled  10777  lt2add  11114  lep1  11470  lem1  11472  letrp1  11473  ltmul12a  11485  mulge0b  11499  lediv12a  11522  bndndx  11884  ltsubnn0  11936  uzind  12062  fnn0ind  12069  eluz2b2  12309  zmin  12332  rpnnen1lem2  12364  rpnnen1lem1  12365  rpnnen1lem3  12366  rpnnen1lem5  12368  rpge0  12390  rpneg  12409  iccsplit  12863  zltaddlt1le  12883  difelfznle  13016  fvffz0  13020  elfzouz2  13047  elfzo0le  13076  fzostep1  13148  fllep1  13166  fracle1  13168  expgt1  13463  expnbnd  13589  expnlbnd2  13591  faclbnd  13646  swrdnd0  14010  swrdsbslen  14017  swrdspsleq  14018  pfxccat3  14087  swrdccat  14088  repswswrd  14137  resqrex  14602  sqrtgt0  14610  absmax  14681  eqsqrt2d  14720  rlim2lt  14846  mulcn2  14944  rlimo1  14965  o1rlimmul  14967  climbdd  15020  caucvgrlem  15021  supcvg  15203  efcllem  15423  sin01bnd  15530  cos01bnd  15531  sin01gt0  15535  cos01gt0  15536  absef  15542  efieq1re  15544  ruclem11  15585  nn0o  15724  pythagtriplem12  16153  pythagtriplem13  16154  pythagtriplem14  16155  pythagtriplem16  16157  pclem  16165  prmgaplem4  16380  cshwshashlem2  16422  isabvd  19584  met2ndci  23129  blcvx  23403  iocopnst  23545  nmoleub2a  23722  nmoleub2b  23723  nmhmcn  23725  iscmet3lem2  23896  caubl  23912  ivthlem2  24056  ovolicc2lem4  24124  ioombl1lem4  24165  ioovolcl  24174  volsup2  24209  itg2monolem1  24354  itg2gt0  24364  itg2cnlem1  24365  dvne0  24614  ftc1lem4  24642  dgrlt  24863  aalioulem5  24932  ulmbdd  24993  iblulm  25002  radcnvlem1  25008  abelthlem5  25030  abelthlem7  25033  sincosq1lem  25090  tangtx  25098  tanabsge  25099  sinq12ge0  25101  sineq0  25116  tanord  25130  logcj  25197  argregt0  25201  argrege0  25202  argimgt0  25203  logdmnrp  25232  logcnlem3  25235  logf1o2  25241  cxpsqrtlem  25293  abscxpbnd  25342  logreclem  25348  asinneg  25472  atanlogsublem  25501  atanlogsub  25502  rlimcnp  25551  xrlimcnp  25554  basellem8  25673  chtub  25796  bposlem9  25876  chebbnd1  26056  chtppilimlem1  26057  dchrvmasumiflem1  26085  mulog2sumlem2  26119  pntrmax  26148  pntibndlem2  26175  pntibndlem3  26176  pntlemf  26189  axlowdimlem16  26751  pthdlem1  27555  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  crctcshwlkn0lem7  27602  crctcshwlkn0  27607  nmblolbii  28582  ubthlem1  28653  bcsiALT  28962  nmbdoplbi  29807  nmcexi  29809  nmcoplbi  29811  lnconi  29816  nmbdfnlbi  29832  nmcfnlbi  29835  nmopcoi  29878  branmfn  29888  leopmul  29917  nmopleid  29922  esumcvg  31455  ballotlemfrceq  31896  sinccvglem  33028  opnrebl2  33782  ivthALT  33796  dnibndlem12  33941  poimirlem15  35072  poimirlem31  35088  ftc1cnnclem  35128  ftc1anclem5  35134  incsequz2  35187  nnubfi  35188  bfplem2  35261  60gcd7e1  39293  lcmineqlem10  39326  factwoffsmonot  39388  3cubeslem1  39625  pell14qrgap  39816  pellfundre  39822  pellfundlb  39825  reabsifneg  40332  reabsifnpos  40333  reabsifpos  40334  reabsifnneg  40335  stoweidlem17  42659  stoweidlem34  42676  wallispilem1  42707  leltletr  43850  sqrtnegnre  43864  2elfz2melfz  43875  elfzelfzlble  43878  subsubelfzo0  43883  requad01  44139  requad2  44141  bgoldbtbnd  44327  bgoldbachlt  44331  tgblthelfgott  44333  m1modmmod  44935  nnolog2flm1  45004  itsclc0yqsol  45178