Theorem ltle 11435

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   class class class wbr 5106  ℝcr 11236   < clt 11380   ≤ cle 11381

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-resscn 11294  ax-pre-lttri 11311

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-er 8753  df-en 9010  df-dom 9011  df-sdom 9012  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386

This theorem is used by:  leltletr  11438  ltleletr  11440  letric  11447  ltlen  11448  ltlei  11469  ltled  11495  lt2add  11839  lep1  12196  lem1  12198  letrp1  12199  ltmul12a  12211  mulge0b  12225  lediv12a  12248  bndndx  12643  ltsubnn0  12695  uzind  12829  fnn0ind  12836  eluz2b2  13086  zmin  13109  rpnnen1lem2  13143  rpnnen1lem1  13144  rpnnen1lem3  13145  rpnnen1lem5  13147  rpge0  13172  rpneg  13192  iccsplit  13654  zltaddlt1le  13674  difelfznle  13814  fvffz0  13818  elfzouz2  13847  elfzo0le  13876  fzostep1  13959  fllep1  13979  fracle1  13981  expgt1  14281  expnbnd  14415  expnlbnd2  14417  faclbnd  14473  swrdnd0  14847  swrdsbslen  14854  swrdspsleq  14855  pfxccat3  14923  swrdccat  14924  repswswrd  14975  resqrex  15458  sqrtgt0  15466  absmax  15538  eqsqrt2d  15577  rlim2lt  15705  mulcn2  15804  rlimo1  15825  o1rlimmul  15827  climbdd  15880  caucvgrlem  15881  supcvg  16066  efcllem  16284  sin01bnd  16394  cos01bnd  16395  sin01gt0  16399  cos01gt0  16400  absef  16406  efieq1re  16408  ruclem11  16449  nn0o  16594  pythagtriplem12  17045  pythagtriplem13  17046  pythagtriplem14  17047  pythagtriplem16  17049  pclem  17057  prmgaplem4  17273  cshwshashlem2  17315  isabvd  21111  met2ndci  24885  blcvx  25161  iocopnst  25305  nmoleub2a  25482  nmoleub2b  25483  nmhmcn  25485  iscmet3lem2  25657  caubl  25673  ivthlem2  25817  ovolicc2lem4  25885  ioombl1lem4  25926  ioovolcl  25935  volsup2  25970  itg2monolem1  26115  itg2gt0  26125  itg2cnlem1  26126  dvne0  26375  ftc1lem4  26403  dgrlt  26629  aalioulem5  26709  ulmbdd  26771  iblulm  26780  radcnvlem1  26786  abelthlem5  26808  abelthlem7  26811  sincosq1lem  26872  tangtx  26880  tanabsge  26881  sinq12ge0  26883  sineq0  26898  tanord  26912  logcj  26980  argregt0  26984  argrege0  26985  argimgt0  26986  logdmnrp  27015  logcnlem3  27018  logf1o2  27024  cxpsqrtlem  27076  abscxpbnd  27127  logreclem  27136  asinneg  27260  atanlogsublem  27289  atanlogsub  27290  rlimcnp  27339  xrlimcnp  27342  basellem8  27461  chtub  27585  bposlem9  27665  chebbnd1  27845  chtppilimlem1  27846  dchrvmasumiflem1  27874  mulog2sumlem2  27908  pntrmax  27937  pntibndlem2  27964  pntibndlem3  27965  pntlemf  27978  axlowdimlem16  29581  pthdlem1  30398  crctcshwlkn0lem3  30447  crctcshwlkn0lem5  30449  crctcshwlkn0lem7  30451  crctcshwlkn0  30456  nmblolbii  31447  ubthlem1  31518  bcsiALT  31827  nmbdoplbi  32672  nmcexi  32674  nmcoplbi  32676  lnconi  32681  nmbdfnlbi  32697  nmcfnlbi  32700  nmopcoi  32743  branmfn  32753  leopmul  32782  nmopleid  32787  esumcvg  34822  ballotlemfrceq  35265  sinccvglem  36638  opnrebl2  37317  ivthALT  37331  dnibndlem12  37563  poimirlem15  38814  poimirlem31  38830  ftc1cnnclem  38870  ftc1anclem5  38876  incsequz2  38942  nnubfi  38943  bfplem2  39016  60gcd7e1  43314  lcmineqlem10  43347  3cubeslem1  43954  pell14qrgap  44142  pellfundre  44148  pellfundlb  44151  reabsifneg  44887  reabsifnpos  44888  reabsifpos  44889  reabsifnneg  44890  stoweidlem17  47294  stoweidlem34  47311  wallispilem1  47342  sqrtnegnre  48644  2elfz2melfz  48655  elfzelfzlble  48658  subsubelfzo0  48664  m1modmmod  48701  requad01  48986  requad2  48988  bgoldbtbnd  49174  bgoldbachlt  49178  tgblthelfgott  49180  nnolog2flm1  50027  itsclc0yqsol  50201