Theorem ltle 11222

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 867	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		leloe 11220	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	imbitrrid 246	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027   < clt 11168   ≤ cle 11169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-pre-lttri 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  leltletr  11225  ltleletr  11227  letr  11228  letric  11234  ltlen  11235  ltlei  11256  ltled  11282  lt2add  11623  lep1  11983  lem1  11985  letrp1  11986  ltmul12a  11998  mulge0b  12013  lediv12a  12036  bndndx  12401  ltsubnn0  12453  uzind  12586  fnn0ind  12593  eluz2b2  12840  zmin  12863  rpnnen1lem2  12896  rpnnen1lem1  12897  rpnnen1lem3  12898  rpnnen1lem5  12900  rpge0  12925  rpneg  12945  iccsplit  13406  zltaddlt1le  13426  difelfznle  13563  fvffz0  13567  elfzouz2  13595  elfzo0le  13624  fzostep1  13704  fllep1  13723  fracle1  13725  expgt1  14025  expnbnd  14157  expnlbnd2  14159  faclbnd  14215  swrdnd0  14582  swrdsbslen  14589  swrdspsleq  14590  pfxccat3  14658  swrdccat  14659  repswswrd  14708  resqrex  15175  sqrtgt0  15183  absmax  15255  eqsqrt2d  15294  rlim2lt  15422  mulcn2  15521  rlimo1  15542  o1rlimmul  15544  climbdd  15597  caucvgrlem  15598  supcvg  15781  efcllem  16002  sin01bnd  16112  cos01bnd  16113  sin01gt0  16117  cos01gt0  16118  absef  16124  efieq1re  16126  ruclem11  16167  nn0o  16312  pythagtriplem12  16756  pythagtriplem13  16757  pythagtriplem14  16758  pythagtriplem16  16760  pclem  16768  prmgaplem4  16984  cshwshashlem2  17026  isabvd  20715  met2ndci  24426  blcvx  24702  iocopnst  24853  nmoleub2a  25033  nmoleub2b  25034  nmhmcn  25036  iscmet3lem2  25208  caubl  25224  ivthlem2  25369  ovolicc2lem4  25437  ioombl1lem4  25478  ioovolcl  25487  volsup2  25522  itg2monolem1  25667  itg2gt0  25677  itg2cnlem1  25678  dvne0  25932  ftc1lem4  25962  dgrlt  26188  aalioulem5  26260  ulmbdd  26323  iblulm  26332  radcnvlem1  26338  abelthlem5  26361  abelthlem7  26364  sincosq1lem  26422  tangtx  26430  tanabsge  26431  sinq12ge0  26433  sineq0  26449  tanord  26463  logcj  26531  argregt0  26535  argrege0  26536  argimgt0  26537  logdmnrp  26566  logcnlem3  26569  logf1o2  26575  cxpsqrtlem  26627  abscxpbnd  26679  logreclem  26688  asinneg  26812  atanlogsublem  26841  atanlogsub  26842  rlimcnp  26891  xrlimcnp  26894  basellem8  27014  chtub  27139  bposlem9  27219  chebbnd1  27399  chtppilimlem1  27400  dchrvmasumiflem1  27428  mulog2sumlem2  27462  pntrmax  27491  pntibndlem2  27518  pntibndlem3  27519  pntlemf  27532  axlowdimlem16  28920  pthdlem1  29729  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  crctcshwlkn0lem7  29779  crctcshwlkn0  29784  nmblolbii  30761  ubthlem1  30832  bcsiALT  31141  nmbdoplbi  31986  nmcexi  31988  nmcoplbi  31990  lnconi  31995  nmbdfnlbi  32011  nmcfnlbi  32014  nmopcoi  32057  branmfn  32067  leopmul  32096  nmopleid  32101  esumcvg  34055  ballotlemfrceq  34499  sinccvglem  35647  opnrebl2  36297  ivthALT  36311  dnibndlem12  36465  poimirlem15  37617  poimirlem31  37633  ftc1cnnclem  37673  ftc1anclem5  37679  incsequz2  37731  nnubfi  37732  bfplem2  37805  60gcd7e1  41981  lcmineqlem10  42014  3cubeslem1  42660  pell14qrgap  42851  pellfundre  42857  pellfundlb  42860  reabsifneg  43608  reabsifnpos  43609  reabsifpos  43610  reabsifnneg  43611  stoweidlem17  46002  stoweidlem34  46019  wallispilem1  46050  sqrtnegnre  47295  2elfz2melfz  47306  elfzelfzlble  47309  subsubelfzo0  47314  m1modmmod  47346  requad01  47609  requad2  47611  bgoldbtbnd  47797  bgoldbachlt  47801  tgblthelfgott  47803  nnolog2flm1  48579  itsclc0yqsol  48753