Theorem ltle 11225

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  leltletr  11228  ltleletr  11230  letr  11231  letric  11237  ltlen  11238  ltlei  11259  ltled  11285  lt2add  11626  lep1  11987  lem1  11989  letrp1  11990  ltmul12a  12002  mulge0b  12017  lediv12a  12040  bndndx  12427  ltsubnn0  12479  uzind  12612  fnn0ind  12619  eluz2b2  12862  zmin  12885  rpnnen1lem2  12918  rpnnen1lem1  12919  rpnnen1lem3  12920  rpnnen1lem5  12922  rpge0  12947  rpneg  12967  iccsplit  13429  zltaddlt1le  13449  difelfznle  13587  fvffz0  13591  elfzouz2  13620  elfzo0le  13649  fzostep1  13732  fllep1  13751  fracle1  13753  expgt1  14053  expnbnd  14185  expnlbnd2  14187  faclbnd  14243  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  pfxccat3  14687  swrdccat  14688  repswswrd  14737  resqrex  15203  sqrtgt0  15211  absmax  15283  eqsqrt2d  15322  rlim2lt  15450  mulcn2  15549  rlimo1  15570  o1rlimmul  15572  climbdd  15625  caucvgrlem  15626  supcvg  15812  efcllem  16033  sin01bnd  16143  cos01bnd  16144  sin01gt0  16148  cos01gt0  16149  absef  16155  efieq1re  16157  ruclem11  16198  nn0o  16343  pythagtriplem12  16788  pythagtriplem13  16789  pythagtriplem14  16790  pythagtriplem16  16792  pclem  16800  prmgaplem4  17016  cshwshashlem2  17058  isabvd  20780  met2ndci  24497  blcvx  24773  iocopnst  24917  nmoleub2a  25094  nmoleub2b  25095  nmhmcn  25097  iscmet3lem2  25269  caubl  25285  ivthlem2  25429  ovolicc2lem4  25497  ioombl1lem4  25538  ioovolcl  25547  volsup2  25582  itg2monolem1  25727  itg2gt0  25737  itg2cnlem1  25738  dvne0  25988  ftc1lem4  26016  dgrlt  26241  aalioulem5  26313  ulmbdd  26376  iblulm  26385  radcnvlem1  26391  abelthlem5  26413  abelthlem7  26416  sincosq1lem  26474  tangtx  26482  tanabsge  26483  sinq12ge0  26485  sineq0  26501  tanord  26515  logcj  26583  argregt0  26587  argrege0  26588  argimgt0  26589  logdmnrp  26618  logcnlem3  26621  logf1o2  26627  cxpsqrtlem  26679  abscxpbnd  26730  logreclem  26739  asinneg  26863  atanlogsublem  26892  atanlogsub  26893  rlimcnp  26942  xrlimcnp  26945  basellem8  27065  chtub  27189  bposlem9  27269  chebbnd1  27449  chtppilimlem1  27450  dchrvmasumiflem1  27478  mulog2sumlem2  27512  pntrmax  27541  pntibndlem2  27568  pntibndlem3  27569  pntlemf  27582  axlowdimlem16  29040  pthdlem1  29849  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  crctcshwlkn0lem7  29899  crctcshwlkn0  29904  nmblolbii  30885  ubthlem1  30956  bcsiALT  31265  nmbdoplbi  32110  nmcexi  32112  nmcoplbi  32114  lnconi  32119  nmbdfnlbi  32135  nmcfnlbi  32138  nmopcoi  32181  branmfn  32191  leopmul  32220  nmopleid  32225  esumcvg  34246  ballotlemfrceq  34689  sinccvglem  35870  opnrebl2  36519  ivthALT  36533  dnibndlem12  36765  poimirlem15  37970  poimirlem31  37986  ftc1cnnclem  38026  ftc1anclem5  38032  incsequz2  38084  nnubfi  38085  bfplem2  38158  60gcd7e1  42458  lcmineqlem10  42491  3cubeslem1  43130  pell14qrgap  43321  pellfundre  43327  pellfundlb  43330  reabsifneg  44077  reabsifnpos  44078  reabsifpos  44079  reabsifnneg  44080  stoweidlem17  46463  stoweidlem34  46480  wallispilem1  46511  sqrtnegnre  47767  2elfz2melfz  47778  elfzelfzlble  47781  subsubelfzo0  47787  m1modmmod  47824  requad01  48109  requad2  48111  bgoldbtbnd  48297  bgoldbachlt  48301  tgblthelfgott  48303  nnolog2flm1  49078  itsclc0yqsol  49252