Theorem ltle 11402

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1569   ∈ wcel 2144   class class class wbr 5102  ℝcr 11203   < clt 11347   ≤ cle 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-pre-lttri 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353

This theorem is used by:  leltletr  11405  ltleletr  11407  letric  11414  ltlen  11415  ltlei  11436  ltled  11462  lt2add  11805  lep1  12162  lem1  12164  letrp1  12165  ltmul12a  12177  mulge0b  12191  lediv12a  12214  bndndx  12609  ltsubnn0  12661  uzind  12795  fnn0ind  12802  eluz2b2  13052  zmin  13075  rpnnen1lem2  13109  rpnnen1lem1  13110  rpnnen1lem3  13111  rpnnen1lem5  13113  rpge0  13138  rpneg  13158  iccsplit  13620  zltaddlt1le  13640  difelfznle  13780  fvffz0  13784  elfzouz2  13813  elfzo0le  13842  fzostep1  13925  fllep1  13945  fracle1  13947  expgt1  14247  expnbnd  14380  expnlbnd2  14382  faclbnd  14438  swrdnd0  14812  swrdsbslen  14819  swrdspsleq  14820  pfxccat3  14888  swrdccat  14889  repswswrd  14940  resqrex  15423  sqrtgt0  15431  absmax  15503  eqsqrt2d  15542  rlim2lt  15670  mulcn2  15769  rlimo1  15790  o1rlimmul  15792  climbdd  15845  caucvgrlem  15846  supcvg  16031  efcllem  16249  sin01bnd  16359  cos01bnd  16360  sin01gt0  16364  cos01gt0  16365  absef  16371  efieq1re  16373  ruclem11  16414  nn0o  16559  pythagtriplem12  17010  pythagtriplem13  17011  pythagtriplem14  17012  pythagtriplem16  17014  pclem  17022  prmgaplem4  17238  cshwshashlem2  17280  isabvd  21075  met2ndci  24847  blcvx  25123  iocopnst  25267  nmoleub2a  25444  nmoleub2b  25445  nmhmcn  25447  iscmet3lem2  25619  caubl  25635  ivthlem2  25779  ovolicc2lem4  25847  ioombl1lem4  25888  ioovolcl  25897  volsup2  25932  itg2monolem1  26077  itg2gt0  26087  itg2cnlem1  26088  dvne0  26337  ftc1lem4  26365  dgrlt  26591  aalioulem5  26669  ulmbdd  26731  iblulm  26740  radcnvlem1  26746  abelthlem5  26768  abelthlem7  26771  sincosq1lem  26832  tangtx  26840  tanabsge  26841  sinq12ge0  26843  sineq0  26858  tanord  26872  logcj  26940  argregt0  26944  argrege0  26945  argimgt0  26946  logdmnrp  26975  logcnlem3  26978  logf1o2  26984  cxpsqrtlem  27036  abscxpbnd  27087  logreclem  27096  asinneg  27220  atanlogsublem  27249  atanlogsub  27250  rlimcnp  27299  xrlimcnp  27302  basellem8  27421  chtub  27545  bposlem9  27625  chebbnd1  27805  chtppilimlem1  27806  dchrvmasumiflem1  27834  mulog2sumlem2  27868  pntrmax  27897  pntibndlem2  27924  pntibndlem3  27925  pntlemf  27938  axlowdimlem16  29541  pthdlem1  30358  crctcshwlkn0lem3  30407  crctcshwlkn0lem5  30409  crctcshwlkn0lem7  30411  crctcshwlkn0  30416  nmblolbii  31407  ubthlem1  31478  bcsiALT  31787  nmbdoplbi  32632  nmcexi  32634  nmcoplbi  32636  lnconi  32641  nmbdfnlbi  32657  nmcfnlbi  32660  nmopcoi  32703  branmfn  32713  leopmul  32742  nmopleid  32747  esumcvg  34765  ballotlemfrceq  35208  sinccvglem  36524  opnrebl2  37202  ivthALT  37216  dnibndlem12  37448  poimirlem15  38647  poimirlem31  38663  ftc1cnnclem  38703  ftc1anclem5  38709  incsequz2  38777  nnubfi  38778  bfplem2  38851  60gcd7e1  43149  lcmineqlem10  43182  3cubeslem1  43788  pell14qrgap  43976  pellfundre  43982  pellfundlb  43985  reabsifneg  44726  reabsifnpos  44727  reabsifpos  44728  reabsifnneg  44729  stoweidlem17  47121  stoweidlem34  47138  wallispilem1  47169  sqrtnegnre  48471  2elfz2melfz  48482  elfzelfzlble  48485  subsubelfzo0  48491  m1modmmod  48528  requad01  48813  requad2  48815  bgoldbtbnd  49001  bgoldbachlt  49005  tgblthelfgott  49007  nnolog2flm1  49796  itsclc0yqsol  49970