Theorem ltle 11331

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1539   ∈ wcel 2107   class class class wbr 5123  ℝcr 11136   < clt 11277   ≤ cle 11278

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737  ax-resscn 11194  ax-pre-lttri 11211

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-er 8727  df-en 8968  df-dom 8969  df-sdom 8970  df-pnf 11279  df-mnf 11280  df-xr 11281  df-ltxr 11282  df-le 11283

This theorem is referenced by:  leltletr  11334  ltleletr  11336  letr  11337  letric  11343  ltlen  11344  ltlei  11365  ltled  11391  lt2add  11730  lep1  12090  lem1  12092  letrp1  12093  ltmul12a  12105  mulge0b  12120  lediv12a  12143  bndndx  12508  ltsubnn0  12560  uzind  12693  fnn0ind  12700  eluz2b2  12945  zmin  12968  rpnnen1lem2  13001  rpnnen1lem1  13002  rpnnen1lem3  13003  rpnnen1lem5  13005  rpge0  13030  rpneg  13049  iccsplit  13507  zltaddlt1le  13527  difelfznle  13664  fvffz0  13668  elfzouz2  13696  elfzo0le  13725  fzostep1  13804  fllep1  13823  fracle1  13825  expgt1  14123  expnbnd  14253  expnlbnd2  14255  faclbnd  14311  swrdnd0  14677  swrdsbslen  14684  swrdspsleq  14685  pfxccat3  14754  swrdccat  14755  repswswrd  14804  resqrex  15271  sqrtgt0  15279  absmax  15350  eqsqrt2d  15389  rlim2lt  15515  mulcn2  15614  rlimo1  15635  o1rlimmul  15637  climbdd  15690  caucvgrlem  15691  supcvg  15874  efcllem  16095  sin01bnd  16203  cos01bnd  16204  sin01gt0  16208  cos01gt0  16209  absef  16215  efieq1re  16217  ruclem11  16258  nn0o  16402  pythagtriplem12  16846  pythagtriplem13  16847  pythagtriplem14  16848  pythagtriplem16  16850  pclem  16858  prmgaplem4  17074  cshwshashlem2  17116  isabvd  20781  met2ndci  24479  blcvx  24755  iocopnst  24906  nmoleub2a  25086  nmoleub2b  25087  nmhmcn  25089  iscmet3lem2  25262  caubl  25278  ivthlem2  25423  ovolicc2lem4  25491  ioombl1lem4  25532  ioovolcl  25541  volsup2  25576  itg2monolem1  25721  itg2gt0  25731  itg2cnlem1  25732  dvne0  25986  ftc1lem4  26016  dgrlt  26242  aalioulem5  26314  ulmbdd  26377  iblulm  26386  radcnvlem1  26392  abelthlem5  26415  abelthlem7  26418  sincosq1lem  26475  tangtx  26483  tanabsge  26484  sinq12ge0  26486  sineq0  26502  tanord  26516  logcj  26584  argregt0  26588  argrege0  26589  argimgt0  26590  logdmnrp  26619  logcnlem3  26622  logf1o2  26628  cxpsqrtlem  26680  abscxpbnd  26732  logreclem  26741  asinneg  26865  atanlogsublem  26894  atanlogsub  26895  rlimcnp  26944  xrlimcnp  26947  basellem8  27067  chtub  27192  bposlem9  27272  chebbnd1  27452  chtppilimlem1  27453  dchrvmasumiflem1  27481  mulog2sumlem2  27515  pntrmax  27544  pntibndlem2  27571  pntibndlem3  27572  pntlemf  27585  axlowdimlem16  28902  pthdlem1  29714  crctcshwlkn0lem3  29760  crctcshwlkn0lem5  29762  crctcshwlkn0lem7  29764  crctcshwlkn0  29769  nmblolbii  30746  ubthlem1  30817  bcsiALT  31126  nmbdoplbi  31971  nmcexi  31973  nmcoplbi  31975  lnconi  31980  nmbdfnlbi  31996  nmcfnlbi  31999  nmopcoi  32042  branmfn  32052  leopmul  32081  nmopleid  32086  esumcvg  34046  ballotlemfrceq  34490  sinccvglem  35636  opnrebl2  36281  ivthALT  36295  dnibndlem12  36449  poimirlem15  37601  poimirlem31  37617  ftc1cnnclem  37657  ftc1anclem5  37663  incsequz2  37715  nnubfi  37716  bfplem2  37789  60gcd7e1  41965  lcmineqlem10  41998  factwoffsmonot  42202  3cubeslem1  42658  pell14qrgap  42849  pellfundre  42855  pellfundlb  42858  reabsifneg  43607  reabsifnpos  43608  reabsifpos  43609  reabsifnneg  43610  stoweidlem17  45989  stoweidlem34  46006  wallispilem1  46037  sqrtnegnre  47277  2elfz2melfz  47288  elfzelfzlble  47291  subsubelfzo0  47296  requad01  47566  requad2  47568  bgoldbtbnd  47754  bgoldbachlt  47758  tgblthelfgott  47760  m1modmmod  48400  nnolog2flm1  48469  itsclc0yqsol  48643