Theorem ltle 11047

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1541   ∈ wcel 2109   class class class wbr 5078  ℝcr 10854   < clt 10993   ≤ cle 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-pre-lttri 10929

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999

This theorem is referenced by:  ltleletr  11051  letr  11052  letric  11058  ltlen  11059  ltlei  11080  ltled  11106  lt2add  11443  lep1  11799  lem1  11801  letrp1  11802  ltmul12a  11814  mulge0b  11828  lediv12a  11851  bndndx  12215  ltsubnn0  12267  uzind  12395  fnn0ind  12402  eluz2b2  12643  zmin  12666  rpnnen1lem2  12699  rpnnen1lem1  12700  rpnnen1lem3  12701  rpnnen1lem5  12703  rpge0  12725  rpneg  12744  iccsplit  13199  zltaddlt1le  13219  difelfznle  13352  fvffz0  13356  elfzouz2  13383  elfzo0le  13412  fzostep1  13484  fllep1  13502  fracle1  13504  expgt1  13802  expnbnd  13928  expnlbnd2  13930  faclbnd  13985  swrdnd0  14351  swrdsbslen  14358  swrdspsleq  14359  pfxccat3  14428  swrdccat  14429  repswswrd  14478  resqrex  14943  sqrtgt0  14951  absmax  15022  eqsqrt2d  15061  rlim2lt  15187  mulcn2  15286  rlimo1  15307  o1rlimmul  15309  climbdd  15364  caucvgrlem  15365  supcvg  15549  efcllem  15768  sin01bnd  15875  cos01bnd  15876  sin01gt0  15880  cos01gt0  15881  absef  15887  efieq1re  15889  ruclem11  15930  nn0o  16073  pythagtriplem12  16508  pythagtriplem13  16509  pythagtriplem14  16510  pythagtriplem16  16512  pclem  16520  prmgaplem4  16736  cshwshashlem2  16779  isabvd  20061  met2ndci  23659  blcvx  23942  iocopnst  24084  nmoleub2a  24261  nmoleub2b  24262  nmhmcn  24264  iscmet3lem2  24437  caubl  24453  ivthlem2  24597  ovolicc2lem4  24665  ioombl1lem4  24706  ioovolcl  24715  volsup2  24750  itg2monolem1  24896  itg2gt0  24906  itg2cnlem1  24907  dvne0  25156  ftc1lem4  25184  dgrlt  25408  aalioulem5  25477  ulmbdd  25538  iblulm  25547  radcnvlem1  25553  abelthlem5  25575  abelthlem7  25578  sincosq1lem  25635  tangtx  25643  tanabsge  25644  sinq12ge0  25646  sineq0  25661  tanord  25675  logcj  25742  argregt0  25746  argrege0  25747  argimgt0  25748  logdmnrp  25777  logcnlem3  25780  logf1o2  25786  cxpsqrtlem  25838  abscxpbnd  25887  logreclem  25893  asinneg  26017  atanlogsublem  26046  atanlogsub  26047  rlimcnp  26096  xrlimcnp  26099  basellem8  26218  chtub  26341  bposlem9  26421  chebbnd1  26601  chtppilimlem1  26602  dchrvmasumiflem1  26630  mulog2sumlem2  26664  pntrmax  26693  pntibndlem2  26720  pntibndlem3  26721  pntlemf  26734  axlowdimlem16  27306  pthdlem1  28113  crctcshwlkn0lem3  28156  crctcshwlkn0lem5  28158  crctcshwlkn0lem7  28160  crctcshwlkn0  28165  nmblolbii  29140  ubthlem1  29211  bcsiALT  29520  nmbdoplbi  30365  nmcexi  30367  nmcoplbi  30369  lnconi  30374  nmbdfnlbi  30390  nmcfnlbi  30393  nmopcoi  30436  branmfn  30446  leopmul  30475  nmopleid  30480  esumcvg  32033  ballotlemfrceq  32474  sinccvglem  33609  opnrebl2  34489  ivthALT  34503  dnibndlem12  34648  poimirlem15  35771  poimirlem31  35787  ftc1cnnclem  35827  ftc1anclem5  35833  incsequz2  35886  nnubfi  35887  bfplem2  35960  60gcd7e1  39993  lcmineqlem10  40026  factwoffsmonot  40143  3cubeslem1  40486  pell14qrgap  40677  pellfundre  40683  pellfundlb  40686  reabsifneg  41193  reabsifnpos  41194  reabsifpos  41195  reabsifnneg  41196  stoweidlem17  43512  stoweidlem34  43529  wallispilem1  43560  leltletr  44737  sqrtnegnre  44751  2elfz2melfz  44762  elfzelfzlble  44765  subsubelfzo0  44770  requad01  45025  requad2  45027  bgoldbtbnd  45213  bgoldbachlt  45217  tgblthelfgott  45219  m1modmmod  45819  nnolog2flm1  45888  itsclc0yqsol  46062