Theorem ltle 11264

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

Syntax hints:   → wi 4   ∧ wa 399   ∨ wo 858   = wceq 1559   ∈ wcel 2141   class class class wbr 5097  ℝcr 11065   < clt 11209   ≤ cle 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-pre-lttri 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215

This theorem is referenced by:  leltletr  11267  ltleletr  11269  letr  11270  letric  11276  ltlen  11277  ltlei  11298  ltled  11324  lt2add  11665  lep1  12025  lem1  12027  letrp1  12028  ltmul12a  12040  mulge0b  12055  lediv12a  12078  bndndx  12473  ltsubnn0  12525  uzind  12658  fnn0ind  12665  eluz2b2  12915  zmin  12938  rpnnen1lem2  12971  rpnnen1lem1  12972  rpnnen1lem3  12973  rpnnen1lem5  12975  rpge0  13000  rpneg  13020  iccsplit  13482  zltaddlt1le  13502  difelfznle  13640  fvffz0  13644  elfzouz2  13673  elfzo0le  13702  fzostep1  13785  fllep1  13804  fracle1  13806  expgt1  14106  expnbnd  14238  expnlbnd2  14240  faclbnd  14296  swrdnd0  14664  swrdsbslen  14671  swrdspsleq  14672  pfxccat3  14740  swrdccat  14741  repswswrd  14790  resqrex  15267  sqrtgt0  15275  absmax  15347  eqsqrt2d  15386  rlim2lt  15514  mulcn2  15613  rlimo1  15634  o1rlimmul  15636  climbdd  15689  caucvgrlem  15690  supcvg  15876  efcllem  16097  sin01bnd  16207  cos01bnd  16208  sin01gt0  16212  cos01gt0  16213  absef  16219  efieq1re  16221  ruclem11  16262  nn0o  16407  pythagtriplem12  16852  pythagtriplem13  16853  pythagtriplem14  16854  pythagtriplem16  16856  pclem  16864  prmgaplem4  17080  cshwshashlem2  17122  isabvd  20848  met2ndci  24569  blcvx  24845  iocopnst  24989  nmoleub2a  25166  nmoleub2b  25167  nmhmcn  25169  iscmet3lem2  25341  caubl  25357  ivthlem2  25501  ovolicc2lem4  25569  ioombl1lem4  25610  ioovolcl  25619  volsup2  25654  itg2monolem1  25799  itg2gt0  25809  itg2cnlem1  25810  dvne0  26060  ftc1lem4  26088  dgrlt  26313  aalioulem5  26387  ulmbdd  26448  iblulm  26457  radcnvlem1  26463  abelthlem5  26485  abelthlem7  26488  sincosq1lem  26549  tangtx  26557  tanabsge  26558  sinq12ge0  26560  sineq0  26576  tanord  26590  logcj  26658  argregt0  26662  argrege0  26663  argimgt0  26664  logdmnrp  26693  logcnlem3  26696  logf1o2  26702  cxpsqrtlem  26754  abscxpbnd  26805  logreclem  26814  asinneg  26938  atanlogsublem  26967  atanlogsub  26968  rlimcnp  27017  xrlimcnp  27020  basellem8  27139  chtub  27263  bposlem9  27343  chebbnd1  27523  chtppilimlem1  27524  dchrvmasumiflem1  27552  mulog2sumlem2  27586  pntrmax  27615  pntibndlem2  27642  pntibndlem3  27643  pntlemf  27656  axlowdimlem16  29114  pthdlem1  29922  crctcshwlkn0lem3  29968  crctcshwlkn0lem5  29970  crctcshwlkn0lem7  29972  crctcshwlkn0  29977  nmblolbii  30958  ubthlem1  31029  bcsiALT  31338  nmbdoplbi  32183  nmcexi  32185  nmcoplbi  32187  lnconi  32192  nmbdfnlbi  32208  nmcfnlbi  32211  nmopcoi  32254  branmfn  32264  leopmul  32293  nmopleid  32298  esumcvg  34343  ballotlemfrceq  34786  sinccvglem  35982  opnrebl2  36641  ivthALT  36655  dnibndlem12  36887  poimirlem15  38094  poimirlem31  38110  ftc1cnnclem  38150  ftc1anclem5  38156  incsequz2  38208  nnubfi  38209  bfplem2  38282  60gcd7e1  42582  lcmineqlem10  42615  3cubeslem1  43225  pell14qrgap  43412  pellfundre  43418  pellfundlb  43421  reabsifneg  44168  reabsifnpos  44169  reabsifpos  44170  reabsifnneg  44171  stoweidlem17  46551  stoweidlem34  46568  wallispilem1  46599  sqrtnegnre  47861  2elfz2melfz  47872  elfzelfzlble  47875  subsubelfzo0  47881  m1modmmod  47918  requad01  48203  requad2  48205  bgoldbtbnd  48391  bgoldbachlt  48395  tgblthelfgott  48397  nnolog2flm1  49172  itsclc0yqsol  49346