Theorem ltle 11321

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   < clt 11267   ≤ cle 11268

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 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-pre-lttri 11201

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is referenced by:  leltletr  11324  ltleletr  11326  letr  11327  letric  11333  ltlen  11334  ltlei  11355  ltled  11381  lt2add  11720  lep1  12080  lem1  12082  letrp1  12083  ltmul12a  12095  mulge0b  12110  lediv12a  12133  bndndx  12498  ltsubnn0  12550  uzind  12683  fnn0ind  12690  eluz2b2  12935  zmin  12958  rpnnen1lem2  12991  rpnnen1lem1  12992  rpnnen1lem3  12993  rpnnen1lem5  12995  rpge0  13020  rpneg  13039  iccsplit  13500  zltaddlt1le  13520  difelfznle  13657  fvffz0  13661  elfzouz2  13689  elfzo0le  13718  fzostep1  13797  fllep1  13816  fracle1  13818  expgt1  14116  expnbnd  14248  expnlbnd2  14250  faclbnd  14306  swrdnd0  14673  swrdsbslen  14680  swrdspsleq  14681  pfxccat3  14750  swrdccat  14751  repswswrd  14800  resqrex  15267  sqrtgt0  15275  absmax  15346  eqsqrt2d  15385  rlim2lt  15511  mulcn2  15610  rlimo1  15631  o1rlimmul  15633  climbdd  15686  caucvgrlem  15687  supcvg  15870  efcllem  16091  sin01bnd  16201  cos01bnd  16202  sin01gt0  16206  cos01gt0  16207  absef  16213  efieq1re  16215  ruclem11  16256  nn0o  16400  pythagtriplem12  16844  pythagtriplem13  16845  pythagtriplem14  16846  pythagtriplem16  16848  pclem  16856  prmgaplem4  17072  cshwshashlem2  17114  isabvd  20770  met2ndci  24459  blcvx  24735  iocopnst  24886  nmoleub2a  25066  nmoleub2b  25067  nmhmcn  25069  iscmet3lem2  25242  caubl  25258  ivthlem2  25403  ovolicc2lem4  25471  ioombl1lem4  25512  ioovolcl  25521  volsup2  25556  itg2monolem1  25701  itg2gt0  25711  itg2cnlem1  25712  dvne0  25966  ftc1lem4  25996  dgrlt  26222  aalioulem5  26294  ulmbdd  26357  iblulm  26366  radcnvlem1  26372  abelthlem5  26395  abelthlem7  26398  sincosq1lem  26456  tangtx  26464  tanabsge  26465  sinq12ge0  26467  sineq0  26483  tanord  26497  logcj  26565  argregt0  26569  argrege0  26570  argimgt0  26571  logdmnrp  26600  logcnlem3  26603  logf1o2  26609  cxpsqrtlem  26661  abscxpbnd  26713  logreclem  26722  asinneg  26846  atanlogsublem  26875  atanlogsub  26876  rlimcnp  26925  xrlimcnp  26928  basellem8  27048  chtub  27173  bposlem9  27253  chebbnd1  27433  chtppilimlem1  27434  dchrvmasumiflem1  27462  mulog2sumlem2  27496  pntrmax  27525  pntibndlem2  27552  pntibndlem3  27553  pntlemf  27566  axlowdimlem16  28882  pthdlem1  29694  crctcshwlkn0lem3  29740  crctcshwlkn0lem5  29742  crctcshwlkn0lem7  29744  crctcshwlkn0  29749  nmblolbii  30726  ubthlem1  30797  bcsiALT  31106  nmbdoplbi  31951  nmcexi  31953  nmcoplbi  31955  lnconi  31960  nmbdfnlbi  31976  nmcfnlbi  31979  nmopcoi  32022  branmfn  32032  leopmul  32061  nmopleid  32066  esumcvg  34063  ballotlemfrceq  34507  sinccvglem  35640  opnrebl2  36285  ivthALT  36299  dnibndlem12  36453  poimirlem15  37605  poimirlem31  37621  ftc1cnnclem  37661  ftc1anclem5  37667  incsequz2  37719  nnubfi  37720  bfplem2  37793  60gcd7e1  41964  lcmineqlem10  41997  factwoffsmonot  42201  3cubeslem1  42654  pell14qrgap  42845  pellfundre  42851  pellfundlb  42854  reabsifneg  43603  reabsifnpos  43604  reabsifpos  43605  reabsifnneg  43606  stoweidlem17  45994  stoweidlem34  46011  wallispilem1  46042  sqrtnegnre  47284  2elfz2melfz  47295  elfzelfzlble  47298  subsubelfzo0  47303  requad01  47583  requad2  47585  bgoldbtbnd  47771  bgoldbachlt  47775  tgblthelfgott  47777  m1modmmod  48449  nnolog2flm1  48518  itsclc0yqsol  48692