Theorem ltle 10994

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1539   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   < clt 10940   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  ltleletr  10998  letr  10999  letric  11005  ltlen  11006  ltlei  11027  ltled  11053  lt2add  11390  lep1  11746  lem1  11748  letrp1  11749  ltmul12a  11761  mulge0b  11775  lediv12a  11798  bndndx  12162  ltsubnn0  12214  uzind  12342  fnn0ind  12349  eluz2b2  12590  zmin  12613  rpnnen1lem2  12646  rpnnen1lem1  12647  rpnnen1lem3  12648  rpnnen1lem5  12650  rpge0  12672  rpneg  12691  iccsplit  13146  zltaddlt1le  13166  difelfznle  13299  fvffz0  13303  elfzouz2  13330  elfzo0le  13359  fzostep1  13431  fllep1  13449  fracle1  13451  expgt1  13749  expnbnd  13875  expnlbnd2  13877  faclbnd  13932  swrdnd0  14298  swrdsbslen  14305  swrdspsleq  14306  pfxccat3  14375  swrdccat  14376  repswswrd  14425  resqrex  14890  sqrtgt0  14898  absmax  14969  eqsqrt2d  15008  rlim2lt  15134  mulcn2  15233  rlimo1  15254  o1rlimmul  15256  climbdd  15311  caucvgrlem  15312  supcvg  15496  efcllem  15715  sin01bnd  15822  cos01bnd  15823  sin01gt0  15827  cos01gt0  15828  absef  15834  efieq1re  15836  ruclem11  15877  nn0o  16020  pythagtriplem12  16455  pythagtriplem13  16456  pythagtriplem14  16457  pythagtriplem16  16459  pclem  16467  prmgaplem4  16683  cshwshashlem2  16726  isabvd  19995  met2ndci  23584  blcvx  23867  iocopnst  24009  nmoleub2a  24186  nmoleub2b  24187  nmhmcn  24189  iscmet3lem2  24361  caubl  24377  ivthlem2  24521  ovolicc2lem4  24589  ioombl1lem4  24630  ioovolcl  24639  volsup2  24674  itg2monolem1  24820  itg2gt0  24830  itg2cnlem1  24831  dvne0  25080  ftc1lem4  25108  dgrlt  25332  aalioulem5  25401  ulmbdd  25462  iblulm  25471  radcnvlem1  25477  abelthlem5  25499  abelthlem7  25502  sincosq1lem  25559  tangtx  25567  tanabsge  25568  sinq12ge0  25570  sineq0  25585  tanord  25599  logcj  25666  argregt0  25670  argrege0  25671  argimgt0  25672  logdmnrp  25701  logcnlem3  25704  logf1o2  25710  cxpsqrtlem  25762  abscxpbnd  25811  logreclem  25817  asinneg  25941  atanlogsublem  25970  atanlogsub  25971  rlimcnp  26020  xrlimcnp  26023  basellem8  26142  chtub  26265  bposlem9  26345  chebbnd1  26525  chtppilimlem1  26526  dchrvmasumiflem1  26554  mulog2sumlem2  26588  pntrmax  26617  pntibndlem2  26644  pntibndlem3  26645  pntlemf  26658  axlowdimlem16  27228  pthdlem1  28035  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  crctcshwlkn0lem7  28082  crctcshwlkn0  28087  nmblolbii  29062  ubthlem1  29133  bcsiALT  29442  nmbdoplbi  30287  nmcexi  30289  nmcoplbi  30291  lnconi  30296  nmbdfnlbi  30312  nmcfnlbi  30315  nmopcoi  30358  branmfn  30368  leopmul  30397  nmopleid  30402  esumcvg  31954  ballotlemfrceq  32395  sinccvglem  33530  opnrebl2  34437  ivthALT  34451  dnibndlem12  34596  poimirlem15  35719  poimirlem31  35735  ftc1cnnclem  35775  ftc1anclem5  35781  incsequz2  35834  nnubfi  35835  bfplem2  35908  60gcd7e1  39941  lcmineqlem10  39974  factwoffsmonot  40091  3cubeslem1  40422  pell14qrgap  40613  pellfundre  40619  pellfundlb  40622  reabsifneg  41129  reabsifnpos  41130  reabsifpos  41131  reabsifnneg  41132  stoweidlem17  43448  stoweidlem34  43465  wallispilem1  43496  leltletr  44673  sqrtnegnre  44687  2elfz2melfz  44698  elfzelfzlble  44701  subsubelfzo0  44706  requad01  44961  requad2  44963  bgoldbtbnd  45149  bgoldbachlt  45153  tgblthelfgott  45155  m1modmmod  45755  nnolog2flm1  45824  itsclc0yqsol  45998