Theorem ltle 10723

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 863	. 2 ⊢ (𝐴 < 𝐵 → (𝐴 < 𝐵 ∨ 𝐴 = 𝐵))
2		leloe 10721	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3	1, 2	syl5ibr 248	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1533   ∈ wcel 2110   class class class wbr 5058  ℝcr 10530   < clt 10669   ≤ cle 10670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-resscn 10588  ax-pre-lttri 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675

This theorem is referenced by:  ltleletr  10727  letr  10728  letric  10734  ltlen  10735  ltlei  10756  ltled  10782  lt2add  11119  lep1  11475  lem1  11477  letrp1  11478  ltmul12a  11490  mulge0b  11504  lediv12a  11527  bndndx  11890  ltsubnn0  11942  uzind  12068  fnn0ind  12075  eluz2b2  12315  zmin  12338  rpnnen1lem2  12370  rpnnen1lem1  12371  rpnnen1lem3  12372  rpnnen1lem5  12374  rpge0  12396  rpneg  12415  iccsplit  12865  zltaddlt1le  12884  difelfznle  13015  fvffz0  13019  elfzouz2  13046  elfzo0le  13075  fzostep1  13147  fllep1  13165  fracle1  13167  expgt1  13461  expnbnd  13587  expnlbnd2  13589  faclbnd  13644  swrdnd0  14013  swrdsbslen  14020  swrdspsleq  14021  pfxccat3  14090  swrdccat  14091  repswswrd  14140  resqrex  14604  sqrtgt0  14612  absmax  14683  eqsqrt2d  14722  rlim2lt  14848  mulcn2  14946  rlimo1  14967  o1rlimmul  14969  climbdd  15022  caucvgrlem  15023  supcvg  15205  efcllem  15425  sin01bnd  15532  cos01bnd  15533  sin01gt0  15537  cos01gt0  15538  absef  15544  efieq1re  15546  ruclem11  15587  nn0o  15728  pythagtriplem12  16157  pythagtriplem13  16158  pythagtriplem14  16159  pythagtriplem16  16161  pclem  16169  prmgaplem4  16384  cshwshashlem2  16424  isabvd  19585  met2ndci  23126  blcvx  23400  iocopnst  23538  nmoleub2a  23715  nmoleub2b  23716  nmhmcn  23718  iscmet3lem2  23889  caubl  23905  ivthlem2  24047  ovolicc2lem4  24115  ioombl1lem4  24156  ioovolcl  24165  volsup2  24200  itg2monolem1  24345  itg2gt0  24355  itg2cnlem1  24356  dvne0  24602  ftc1lem4  24630  dgrlt  24850  aalioulem5  24919  ulmbdd  24980  iblulm  24989  radcnvlem1  24995  abelthlem5  25017  abelthlem7  25020  sincosq1lem  25077  tangtx  25085  tanabsge  25086  sinq12ge0  25088  sineq0  25103  tanord  25116  logcj  25183  argregt0  25187  argrege0  25188  argimgt0  25189  logdmnrp  25218  logcnlem3  25221  logf1o2  25227  cxpsqrtlem  25279  abscxpbnd  25328  logreclem  25334  asinneg  25458  atanlogsublem  25487  atanlogsub  25488  rlimcnp  25537  xrlimcnp  25540  basellem8  25659  chtub  25782  bposlem9  25862  chebbnd1  26042  chtppilimlem1  26043  dchrvmasumiflem1  26071  mulog2sumlem2  26105  pntrmax  26134  pntibndlem2  26161  pntibndlem3  26162  pntlemf  26175  axlowdimlem16  26737  pthdlem1  27541  crctcshwlkn0lem3  27584  crctcshwlkn0lem5  27586  crctcshwlkn0lem7  27588  crctcshwlkn0  27593  nmblolbii  28570  ubthlem1  28641  bcsiALT  28950  nmbdoplbi  29795  nmcexi  29797  nmcoplbi  29799  lnconi  29804  nmbdfnlbi  29820  nmcfnlbi  29823  nmopcoi  29866  branmfn  29876  leopmul  29905  nmopleid  29910  esumcvg  31340  ballotlemfrceq  31781  sinccvglem  32910  opnrebl2  33664  ivthALT  33678  dnibndlem12  33823  poimirlem15  34901  poimirlem31  34917  ftc1cnnclem  34959  ftc1anclem5  34965  incsequz2  35018  nnubfi  35019  bfplem2  35095  3cubeslem1  39274  pell14qrgap  39465  pellfundre  39471  pellfundlb  39474  stoweidlem17  42296  stoweidlem34  42313  wallispilem1  42344  leltletr  43487  sqrtnegnre  43501  2elfz2melfz  43512  elfzelfzlble  43515  subsubelfzo0  43520  requad01  43780  requad2  43782  bgoldbtbnd  43968  bgoldbachlt  43972  tgblthelfgott  43974  m1modmmod  44575  nnolog2flm1  44644  itsclc0yqsol  44745