Theorem ltle 11322

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2145   class class class wbr 5103  ℝcr 11123   < clt 11267   ≤ cle 11268

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  leltletr  11325  ltleletr  11327  letr  11328  letric  11334  ltlen  11335  ltlei  11356  ltled  11382  lt2add  11723  lep1  12080  lem1  12082  letrp1  12083  ltmul12a  12095  mulge0b  12109  lediv12a  12132  bndndx  12527  ltsubnn0  12579  uzind  12713  fnn0ind  12720  eluz2b2  12970  zmin  12993  rpnnen1lem2  13027  rpnnen1lem1  13028  rpnnen1lem3  13029  rpnnen1lem5  13031  rpge0  13056  rpneg  13076  iccsplit  13538  zltaddlt1le  13558  difelfznle  13697  fvffz0  13701  elfzouz2  13730  elfzo0le  13759  fzostep1  13842  fllep1  13862  fracle1  13864  expgt1  14164  expnbnd  14296  expnlbnd2  14298  faclbnd  14354  swrdnd0  14727  swrdsbslen  14734  swrdspsleq  14735  pfxccat3  14803  swrdccat  14804  repswswrd  14855  resqrex  15337  sqrtgt0  15345  absmax  15417  eqsqrt2d  15456  rlim2lt  15584  mulcn2  15683  rlimo1  15704  o1rlimmul  15706  climbdd  15759  caucvgrlem  15760  supcvg  15945  efcllem  16163  sin01bnd  16273  cos01bnd  16274  sin01gt0  16278  cos01gt0  16279  absef  16285  efieq1re  16287  ruclem11  16328  nn0o  16473  pythagtriplem12  16918  pythagtriplem13  16919  pythagtriplem14  16920  pythagtriplem16  16922  pclem  16930  prmgaplem4  17146  cshwshashlem2  17188  isabvd  20978  met2ndci  24748  blcvx  25024  iocopnst  25168  nmoleub2a  25345  nmoleub2b  25346  nmhmcn  25348  iscmet3lem2  25520  caubl  25536  ivthlem2  25680  ovolicc2lem4  25748  ioombl1lem4  25789  ioovolcl  25798  volsup2  25833  itg2monolem1  25978  itg2gt0  25988  itg2cnlem1  25989  dvne0  26238  ftc1lem4  26266  dgrlt  26492  aalioulem5  26572  ulmbdd  26634  iblulm  26643  radcnvlem1  26649  abelthlem5  26671  abelthlem7  26674  sincosq1lem  26735  tangtx  26743  tanabsge  26744  sinq12ge0  26746  sineq0  26761  tanord  26775  logcj  26843  argregt0  26847  argrege0  26848  argimgt0  26849  logdmnrp  26878  logcnlem3  26881  logf1o2  26887  cxpsqrtlem  26939  abscxpbnd  26990  logreclem  26999  asinneg  27123  atanlogsublem  27152  atanlogsub  27153  rlimcnp  27202  xrlimcnp  27205  basellem8  27324  chtub  27448  bposlem9  27528  chebbnd1  27708  chtppilimlem1  27709  dchrvmasumiflem1  27737  mulog2sumlem2  27771  pntrmax  27800  pntibndlem2  27827  pntibndlem3  27828  pntlemf  27841  axlowdimlem16  29414  pthdlem1  30231  crctcshwlkn0lem3  30280  crctcshwlkn0lem5  30282  crctcshwlkn0lem7  30284  crctcshwlkn0  30289  nmblolbii  31280  ubthlem1  31351  bcsiALT  31660  nmbdoplbi  32505  nmcexi  32507  nmcoplbi  32509  lnconi  32514  nmbdfnlbi  32530  nmcfnlbi  32533  nmopcoi  32576  branmfn  32586  leopmul  32615  nmopleid  32620  esumcvg  34596  ballotlemfrceq  35040  sinccvglem  36251  opnrebl2  36940  ivthALT  36954  dnibndlem12  37186  poimirlem15  38384  poimirlem31  38400  ftc1cnnclem  38440  ftc1anclem5  38446  incsequz2  38499  nnubfi  38500  bfplem2  38573  60gcd7e1  42871  lcmineqlem10  42904  3cubeslem1  43529  pell14qrgap  43716  pellfundre  43722  pellfundlb  43725  reabsifneg  44472  reabsifnpos  44473  reabsifpos  44474  reabsifnneg  44475  stoweidlem17  46845  stoweidlem34  46862  wallispilem1  46893  sqrtnegnre  48195  2elfz2melfz  48206  elfzelfzlble  48209  subsubelfzo0  48215  m1modmmod  48252  requad01  48537  requad2  48539  bgoldbtbnd  48725  bgoldbachlt  48729  tgblthelfgott  48731  nnolog2flm1  49520  itsclc0yqsol  49694