Theorem ltle 11232

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 853   = wceq 1547   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035   < clt 11177   ≤ cle 11178

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685  ax-resscn 11093  ax-pre-lttri 11110

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-nel 3040  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11179  df-mnf 11180  df-xr 11181  df-ltxr 11182  df-le 11183

This theorem is referenced by:  leltletr  11235  ltleletr  11237  letr  11238  letric  11244  ltlen  11245  ltlei  11266  ltled  11292  lt2add  11633  lep1  11994  lem1  11996  letrp1  11997  ltmul12a  12009  mulge0b  12024  lediv12a  12047  bndndx  12434  ltsubnn0  12486  uzind  12619  fnn0ind  12626  eluz2b2  12869  zmin  12892  rpnnen1lem2  12925  rpnnen1lem1  12926  rpnnen1lem3  12927  rpnnen1lem5  12929  rpge0  12954  rpneg  12974  iccsplit  13436  zltaddlt1le  13456  difelfznle  13594  fvffz0  13598  elfzouz2  13627  elfzo0le  13656  fzostep1  13739  fllep1  13758  fracle1  13760  expgt1  14060  expnbnd  14192  expnlbnd2  14194  faclbnd  14250  swrdnd0  14618  swrdsbslen  14625  swrdspsleq  14626  pfxccat3  14694  swrdccat  14695  repswswrd  14744  resqrex  15210  sqrtgt0  15218  absmax  15290  eqsqrt2d  15329  rlim2lt  15457  mulcn2  15556  rlimo1  15577  o1rlimmul  15579  climbdd  15632  caucvgrlem  15633  supcvg  15819  efcllem  16040  sin01bnd  16150  cos01bnd  16151  sin01gt0  16155  cos01gt0  16156  absef  16162  efieq1re  16164  ruclem11  16205  nn0o  16350  pythagtriplem12  16795  pythagtriplem13  16796  pythagtriplem14  16797  pythagtriplem16  16799  pclem  16807  prmgaplem4  17023  cshwshashlem2  17065  isabvd  20791  met2ndci  24512  blcvx  24788  iocopnst  24932  nmoleub2a  25109  nmoleub2b  25110  nmhmcn  25112  iscmet3lem2  25284  caubl  25300  ivthlem2  25444  ovolicc2lem4  25512  ioombl1lem4  25553  ioovolcl  25562  volsup2  25597  itg2monolem1  25742  itg2gt0  25752  itg2cnlem1  25753  dvne0  26003  ftc1lem4  26031  dgrlt  26256  aalioulem5  26327  ulmbdd  26388  iblulm  26397  radcnvlem1  26403  abelthlem5  26425  abelthlem7  26428  sincosq1lem  26486  tangtx  26494  tanabsge  26495  sinq12ge0  26497  sineq0  26513  tanord  26527  logcj  26595  argregt0  26599  argrege0  26600  argimgt0  26601  logdmnrp  26630  logcnlem3  26633  logf1o2  26639  cxpsqrtlem  26691  abscxpbnd  26742  logreclem  26751  asinneg  26875  atanlogsublem  26904  atanlogsub  26905  rlimcnp  26954  xrlimcnp  26957  basellem8  27076  chtub  27200  bposlem9  27280  chebbnd1  27460  chtppilimlem1  27461  dchrvmasumiflem1  27489  mulog2sumlem2  27523  pntrmax  27552  pntibndlem2  27579  pntibndlem3  27580  pntlemf  27593  axlowdimlem16  29051  pthdlem1  29859  crctcshwlkn0lem3  29905  crctcshwlkn0lem5  29907  crctcshwlkn0lem7  29909  crctcshwlkn0  29914  nmblolbii  30895  ubthlem1  30966  bcsiALT  31275  nmbdoplbi  32120  nmcexi  32122  nmcoplbi  32124  lnconi  32129  nmbdfnlbi  32145  nmcfnlbi  32148  nmopcoi  32191  branmfn  32201  leopmul  32230  nmopleid  32235  esumcvg  34277  ballotlemfrceq  34720  sinccvglem  35907  opnrebl2  36556  ivthALT  36570  dnibndlem12  36802  poimirlem15  38009  poimirlem31  38025  ftc1cnnclem  38065  ftc1anclem5  38071  incsequz2  38123  nnubfi  38124  bfplem2  38197  60gcd7e1  42497  lcmineqlem10  42530  3cubeslem1  43140  pell14qrgap  43327  pellfundre  43333  pellfundlb  43336  reabsifneg  44083  reabsifnpos  44084  reabsifpos  44085  reabsifnneg  44086  stoweidlem17  46467  stoweidlem34  46484  wallispilem1  46515  sqrtnegnre  47777  2elfz2melfz  47788  elfzelfzlble  47791  subsubelfzo0  47797  m1modmmod  47834  requad01  48119  requad2  48121  bgoldbtbnd  48307  bgoldbachlt  48311  tgblthelfgott  48313  nnolog2flm1  49088  itsclc0yqsol  49262