Theorem ltle 11349

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttri 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  leltletr  11352  ltleletr  11354  letr  11355  letric  11361  ltlen  11362  ltlei  11383  ltled  11409  lt2add  11748  lep1  12108  lem1  12110  letrp1  12111  ltmul12a  12123  mulge0b  12138  lediv12a  12161  bndndx  12525  ltsubnn0  12577  uzind  12710  fnn0ind  12717  eluz2b2  12963  zmin  12986  rpnnen1lem2  13019  rpnnen1lem1  13020  rpnnen1lem3  13021  rpnnen1lem5  13023  rpge0  13048  rpneg  13067  iccsplit  13525  zltaddlt1le  13545  difelfznle  13682  fvffz0  13686  elfzouz2  13714  elfzo0le  13743  fzostep1  13822  fllep1  13841  fracle1  13843  expgt1  14141  expnbnd  14271  expnlbnd2  14273  faclbnd  14329  swrdnd0  14695  swrdsbslen  14702  swrdspsleq  14703  pfxccat3  14772  swrdccat  14773  repswswrd  14822  resqrex  15289  sqrtgt0  15297  absmax  15368  eqsqrt2d  15407  rlim2lt  15533  mulcn2  15632  rlimo1  15653  o1rlimmul  15655  climbdd  15708  caucvgrlem  15709  supcvg  15892  efcllem  16113  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  cos01gt0  16227  absef  16233  efieq1re  16235  ruclem11  16276  nn0o  16420  pythagtriplem12  16864  pythagtriplem13  16865  pythagtriplem14  16866  pythagtriplem16  16868  pclem  16876  prmgaplem4  17092  cshwshashlem2  17134  isabvd  20813  met2ndci  24535  blcvx  24819  iocopnst  24970  nmoleub2a  25150  nmoleub2b  25151  nmhmcn  25153  iscmet3lem2  25326  caubl  25342  ivthlem2  25487  ovolicc2lem4  25555  ioombl1lem4  25596  ioovolcl  25605  volsup2  25640  itg2monolem1  25785  itg2gt0  25795  itg2cnlem1  25796  dvne0  26050  ftc1lem4  26080  dgrlt  26306  aalioulem5  26378  ulmbdd  26441  iblulm  26450  radcnvlem1  26456  abelthlem5  26479  abelthlem7  26482  sincosq1lem  26539  tangtx  26547  tanabsge  26548  sinq12ge0  26550  sineq0  26566  tanord  26580  logcj  26648  argregt0  26652  argrege0  26653  argimgt0  26654  logdmnrp  26683  logcnlem3  26686  logf1o2  26692  cxpsqrtlem  26744  abscxpbnd  26796  logreclem  26805  asinneg  26929  atanlogsublem  26958  atanlogsub  26959  rlimcnp  27008  xrlimcnp  27011  basellem8  27131  chtub  27256  bposlem9  27336  chebbnd1  27516  chtppilimlem1  27517  dchrvmasumiflem1  27545  mulog2sumlem2  27579  pntrmax  27608  pntibndlem2  27635  pntibndlem3  27636  pntlemf  27649  axlowdimlem16  28972  pthdlem1  29786  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  crctcshwlkn0lem7  29836  crctcshwlkn0  29841  nmblolbii  30818  ubthlem1  30889  bcsiALT  31198  nmbdoplbi  32043  nmcexi  32045  nmcoplbi  32047  lnconi  32052  nmbdfnlbi  32068  nmcfnlbi  32071  nmopcoi  32114  branmfn  32124  leopmul  32153  nmopleid  32158  esumcvg  34087  ballotlemfrceq  34531  sinccvglem  35677  opnrebl2  36322  ivthALT  36336  dnibndlem12  36490  poimirlem15  37642  poimirlem31  37658  ftc1cnnclem  37698  ftc1anclem5  37704  incsequz2  37756  nnubfi  37757  bfplem2  37830  60gcd7e1  42006  lcmineqlem10  42039  factwoffsmonot  42243  3cubeslem1  42695  pell14qrgap  42886  pellfundre  42892  pellfundlb  42895  reabsifneg  43645  reabsifnpos  43646  reabsifpos  43647  reabsifnneg  43648  stoweidlem17  46032  stoweidlem34  46049  wallispilem1  46080  sqrtnegnre  47319  2elfz2melfz  47330  elfzelfzlble  47333  subsubelfzo0  47338  requad01  47608  requad2  47610  bgoldbtbnd  47796  bgoldbachlt  47800  tgblthelfgott  47802  m1modmmod  48442  nnolog2flm1  48511  itsclc0yqsol  48685