Theorem ltle 11221

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1541   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttri 11100

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  leltletr  11224  ltleletr  11226  letr  11227  letric  11233  ltlen  11234  ltlei  11255  ltled  11281  lt2add  11622  lep1  11982  lem1  11984  letrp1  11985  ltmul12a  11997  mulge0b  12012  lediv12a  12035  bndndx  12400  ltsubnn0  12452  uzind  12584  fnn0ind  12591  eluz2b2  12834  zmin  12857  rpnnen1lem2  12890  rpnnen1lem1  12891  rpnnen1lem3  12892  rpnnen1lem5  12894  rpge0  12919  rpneg  12939  iccsplit  13401  zltaddlt1le  13421  difelfznle  13558  fvffz0  13562  elfzouz2  13590  elfzo0le  13619  fzostep1  13702  fllep1  13721  fracle1  13723  expgt1  14023  expnbnd  14155  expnlbnd2  14157  faclbnd  14213  swrdnd0  14581  swrdsbslen  14588  swrdspsleq  14589  pfxccat3  14657  swrdccat  14658  repswswrd  14707  resqrex  15173  sqrtgt0  15181  absmax  15253  eqsqrt2d  15292  rlim2lt  15420  mulcn2  15519  rlimo1  15540  o1rlimmul  15542  climbdd  15595  caucvgrlem  15596  supcvg  15779  efcllem  16000  sin01bnd  16110  cos01bnd  16111  sin01gt0  16115  cos01gt0  16116  absef  16122  efieq1re  16124  ruclem11  16165  nn0o  16310  pythagtriplem12  16754  pythagtriplem13  16755  pythagtriplem14  16756  pythagtriplem16  16758  pclem  16766  prmgaplem4  16982  cshwshashlem2  17024  isabvd  20745  met2ndci  24466  blcvx  24742  iocopnst  24893  nmoleub2a  25073  nmoleub2b  25074  nmhmcn  25076  iscmet3lem2  25248  caubl  25264  ivthlem2  25409  ovolicc2lem4  25477  ioombl1lem4  25518  ioovolcl  25527  volsup2  25562  itg2monolem1  25707  itg2gt0  25717  itg2cnlem1  25718  dvne0  25972  ftc1lem4  26002  dgrlt  26228  aalioulem5  26300  ulmbdd  26363  iblulm  26372  radcnvlem1  26378  abelthlem5  26401  abelthlem7  26404  sincosq1lem  26462  tangtx  26470  tanabsge  26471  sinq12ge0  26473  sineq0  26489  tanord  26503  logcj  26571  argregt0  26575  argrege0  26576  argimgt0  26577  logdmnrp  26606  logcnlem3  26609  logf1o2  26615  cxpsqrtlem  26667  abscxpbnd  26719  logreclem  26728  asinneg  26852  atanlogsublem  26881  atanlogsub  26882  rlimcnp  26931  xrlimcnp  26934  basellem8  27054  chtub  27179  bposlem9  27259  chebbnd1  27439  chtppilimlem1  27440  dchrvmasumiflem1  27468  mulog2sumlem2  27502  pntrmax  27531  pntibndlem2  27558  pntibndlem3  27559  pntlemf  27572  axlowdimlem16  29030  pthdlem1  29839  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  crctcshwlkn0lem7  29889  crctcshwlkn0  29894  nmblolbii  30874  ubthlem1  30945  bcsiALT  31254  nmbdoplbi  32099  nmcexi  32101  nmcoplbi  32103  lnconi  32108  nmbdfnlbi  32124  nmcfnlbi  32127  nmopcoi  32170  branmfn  32180  leopmul  32209  nmopleid  32214  esumcvg  34243  ballotlemfrceq  34686  sinccvglem  35866  opnrebl2  36515  ivthALT  36529  dnibndlem12  36689  poimirlem15  37836  poimirlem31  37852  ftc1cnnclem  37892  ftc1anclem5  37898  incsequz2  37950  nnubfi  37951  bfplem2  38024  60gcd7e1  42259  lcmineqlem10  42292  3cubeslem1  42926  pell14qrgap  43117  pellfundre  43123  pellfundlb  43126  reabsifneg  43873  reabsifnpos  43874  reabsifpos  43875  reabsifnneg  43876  stoweidlem17  46261  stoweidlem34  46278  wallispilem1  46309  sqrtnegnre  47553  2elfz2melfz  47564  elfzelfzlble  47567  subsubelfzo0  47572  m1modmmod  47604  requad01  47867  requad2  47869  bgoldbtbnd  48055  bgoldbachlt  48059  tgblthelfgott  48061  nnolog2flm1  48836  itsclc0yqsol  49010