Theorem ltle 11233

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  leltletr  11236  ltleletr  11238  letr  11239  letric  11245  ltlen  11246  ltlei  11267  ltled  11293  lt2add  11634  lep1  11994  lem1  11996  letrp1  11997  ltmul12a  12009  mulge0b  12024  lediv12a  12047  bndndx  12412  ltsubnn0  12464  uzind  12596  fnn0ind  12603  eluz2b2  12846  zmin  12869  rpnnen1lem2  12902  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  rpge0  12931  rpneg  12951  iccsplit  13413  zltaddlt1le  13433  difelfznle  13570  fvffz0  13574  elfzouz2  13602  elfzo0le  13631  fzostep1  13714  fllep1  13733  fracle1  13735  expgt1  14035  expnbnd  14167  expnlbnd2  14169  faclbnd  14225  swrdnd0  14593  swrdsbslen  14600  swrdspsleq  14601  pfxccat3  14669  swrdccat  14670  repswswrd  14719  resqrex  15185  sqrtgt0  15193  absmax  15265  eqsqrt2d  15304  rlim2lt  15432  mulcn2  15531  rlimo1  15552  o1rlimmul  15554  climbdd  15607  caucvgrlem  15608  supcvg  15791  efcllem  16012  sin01bnd  16122  cos01bnd  16123  sin01gt0  16127  cos01gt0  16128  absef  16134  efieq1re  16136  ruclem11  16177  nn0o  16322  pythagtriplem12  16766  pythagtriplem13  16767  pythagtriplem14  16768  pythagtriplem16  16770  pclem  16778  prmgaplem4  16994  cshwshashlem2  17036  isabvd  20757  met2ndci  24478  blcvx  24754  iocopnst  24905  nmoleub2a  25085  nmoleub2b  25086  nmhmcn  25088  iscmet3lem2  25260  caubl  25276  ivthlem2  25421  ovolicc2lem4  25489  ioombl1lem4  25530  ioovolcl  25539  volsup2  25574  itg2monolem1  25719  itg2gt0  25729  itg2cnlem1  25730  dvne0  25984  ftc1lem4  26014  dgrlt  26240  aalioulem5  26312  ulmbdd  26375  iblulm  26384  radcnvlem1  26390  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  26731  logreclem  26740  asinneg  26864  atanlogsublem  26893  atanlogsub  26894  rlimcnp  26943  xrlimcnp  26946  basellem8  27066  chtub  27191  bposlem9  27271  chebbnd1  27451  chtppilimlem1  27452  dchrvmasumiflem1  27480  mulog2sumlem2  27514  pntrmax  27543  pntibndlem2  27570  pntibndlem3  27571  pntlemf  27584  axlowdimlem16  29042  pthdlem1  29851  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  crctcshwlkn0lem7  29901  crctcshwlkn0  29906  nmblolbii  30886  ubthlem1  30957  bcsiALT  31266  nmbdoplbi  32111  nmcexi  32113  nmcoplbi  32115  lnconi  32120  nmbdfnlbi  32136  nmcfnlbi  32139  nmopcoi  32182  branmfn  32192  leopmul  32221  nmopleid  32226  esumcvg  34263  ballotlemfrceq  34706  sinccvglem  35885  opnrebl2  36534  ivthALT  36548  dnibndlem12  36708  poimirlem15  37883  poimirlem31  37899  ftc1cnnclem  37939  ftc1anclem5  37945  incsequz2  37997  nnubfi  37998  bfplem2  38071  60gcd7e1  42372  lcmineqlem10  42405  3cubeslem1  43038  pell14qrgap  43229  pellfundre  43235  pellfundlb  43238  reabsifneg  43985  reabsifnpos  43986  reabsifpos  43987  reabsifnneg  43988  stoweidlem17  46372  stoweidlem34  46389  wallispilem1  46420  sqrtnegnre  47664  2elfz2melfz  47675  elfzelfzlble  47678  subsubelfzo0  47683  m1modmmod  47715  requad01  47978  requad2  47980  bgoldbtbnd  48166  bgoldbachlt  48170  tgblthelfgott  48172  nnolog2flm1  48947  itsclc0yqsol  49121