Theorem ltle 10529

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

Syntax hints:   → wi 4   ∧ wa 387   ∨ wo 833   = wceq 1507   ∈ wcel 2050   class class class wbr 4929  ℝcr 10334   < clt 10474   ≤ cle 10475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pow 5119  ax-pr 5186  ax-un 7279  ax-resscn 10392  ax-pre-lttri 10409

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ne 2968  df-nel 3074  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3682  df-csb 3787  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-pw 4424  df-sn 4442  df-pr 4444  df-op 4448  df-uni 4713  df-br 4930  df-opab 4992  df-mpt 5009  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419  df-ima 5420  df-iota 6152  df-fun 6190  df-fn 6191  df-f 6192  df-f1 6193  df-fo 6194  df-f1o 6195  df-fv 6196  df-er 8089  df-en 8307  df-dom 8308  df-sdom 8309  df-pnf 10476  df-mnf 10477  df-xr 10478  df-ltxr 10479  df-le 10480

This theorem is referenced by:  ltleletr  10533  letr  10534  letric  10540  ltlen  10541  ltlei  10562  ltled  10588  lt2add  10926  lep1  11282  lem1  11284  letrp1  11285  ltmul12a  11297  mulge0b  11311  lediv12a  11334  bndndx  11706  ltsubnn0  11760  uzind  11887  fnn0ind  11894  eluz2b2  12135  zmin  12158  rpnnen1lem2  12191  rpnnen1lem1  12192  rpnnen1lem3  12193  rpnnen1lem5  12195  rpge0  12219  rpneg  12238  iccsplit  12687  zltaddlt1le  12706  difelfznle  12837  fvffz0  12841  elfzouz2  12868  elfzo0le  12896  fzostep1  12968  fllep1  12986  fracle1  12988  expgt1  13282  expnbnd  13408  expnlbnd2  13410  faclbnd  13465  swrdnd0  13825  swrdsbslen  13841  swrdspsleq  13842  pfxccat3  13936  swrdccat3OLD  13937  swrdccat  13938  repswswrd  14003  resqrex  14471  sqrtgt0  14479  absmax  14550  eqsqrt2d  14589  rlim2lt  14715  mulcn2  14813  rlimo1  14834  o1rlimmul  14836  climbdd  14889  caucvgrlem  14890  supcvg  15071  efcllem  15291  sin01bnd  15398  cos01bnd  15399  sin01gt0  15403  cos01gt0  15404  absef  15410  efieq1re  15412  ruclem11  15453  nn0o  15594  pythagtriplem12  16019  pythagtriplem13  16020  pythagtriplem14  16021  pythagtriplem16  16023  pclem  16031  prmgaplem4  16246  cshwshashlem2  16286  isabvd  19313  met2ndci  22835  blcvx  23109  iocopnst  23247  nmoleub2a  23424  nmoleub2b  23425  nmhmcn  23427  iscmet3lem2  23598  caubl  23614  ivthlem2  23756  ovolicc2lem4  23824  ioombl1lem4  23865  ioovolcl  23874  volsup2  23909  itg2monolem1  24054  itg2gt0  24064  itg2cnlem1  24065  dvne0  24311  ftc1lem4  24339  dgrlt  24559  aalioulem5  24628  ulmbdd  24689  iblulm  24698  radcnvlem1  24704  abelthlem5  24726  abelthlem7  24729  sincosq1lem  24786  tangtx  24794  tanabsge  24795  sinq12ge0  24797  sineq0  24812  tanord  24823  logcj  24890  argregt0  24894  argrege0  24895  argimgt0  24896  logdmnrp  24925  logcnlem3  24928  logf1o2  24934  cxpsqrtlem  24986  abscxpbnd  25035  logreclem  25041  asinneg  25165  atanlogsublem  25194  atanlogsub  25195  rlimcnp  25245  xrlimcnp  25248  basellem8  25367  chtub  25490  bposlem9  25570  chebbnd1  25750  chtppilimlem1  25751  dchrvmasumiflem1  25779  mulog2sumlem2  25813  pntrmax  25842  pntibndlem2  25869  pntibndlem3  25870  pntlemf  25883  axlowdimlem16  26446  pthdlem1  27255  crctcshwlkn0lem3  27298  crctcshwlkn0lem5  27300  crctcshwlkn0lem7  27302  crctcshwlkn0  27307  nmblolbii  28353  ubthlem1  28425  bcsiALT  28735  nmbdoplbi  29582  nmcexi  29584  nmcoplbi  29586  lnconi  29591  nmbdfnlbi  29607  nmcfnlbi  29610  nmopcoi  29653  branmfn  29663  leopmul  29692  nmopleid  29697  esumcvg  30995  ballotlemfrceq  31438  sinccvglem  32441  opnrebl2  33196  ivthALT  33210  dnibndlem12  33354  poimirlem15  34354  poimirlem31  34370  ftc1cnnclem  34412  ftc1anclem5  34418  incsequz2  34472  nnubfi  34473  bfplem2  34549  pell14qrgap  38874  pellfundre  38880  pellfundlb  38883  stoweidlem17  41739  stoweidlem34  41756  wallispilem1  41787  leltletr  42905  sqrtnegnre  42919  2elfz2melfz  42930  elfzelfzlble  42933  subsubelfzo0  42938  requad01  43160  requad2  43162  bgoldbtbnd  43348  bgoldbachlt  43352  tgblthelfgott  43354  m1modmmod  43955  nnolog2flm1  44024  itsclc0yqsol  44125