Theorem ltle 11309

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   class class class wbr 5111  ℝcr 11110   < clt 11254   ≤ cle 11255

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-pre-lttri 11185

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260

This theorem is used by:  leltletr  11312  ltleletr  11314  letr  11315  letric  11321  ltlen  11322  ltlei  11343  ltled  11369  lt2add  11710  lep1  12067  lem1  12069  letrp1  12070  ltmul12a  12082  mulge0b  12096  lediv12a  12119  bndndx  12514  ltsubnn0  12566  uzind  12699  fnn0ind  12706  eluz2b2  12956  zmin  12979  rpnnen1lem2  13012  rpnnen1lem1  13013  rpnnen1lem3  13014  rpnnen1lem5  13016  rpge0  13041  rpneg  13061  iccsplit  13523  zltaddlt1le  13543  difelfznle  13682  fvffz0  13686  elfzouz2  13715  elfzo0le  13744  fzostep1  13827  fllep1  13847  fracle1  13849  expgt1  14149  expnbnd  14281  expnlbnd2  14283  faclbnd  14339  swrdnd0  14712  swrdsbslen  14719  swrdspsleq  14720  pfxccat3  14788  swrdccat  14789  repswswrd  14840  resqrex  15320  sqrtgt0  15328  absmax  15400  eqsqrt2d  15439  rlim2lt  15567  mulcn2  15666  rlimo1  15687  o1rlimmul  15689  climbdd  15742  caucvgrlem  15743  supcvg  15928  efcllem  16148  sin01bnd  16258  cos01bnd  16259  sin01gt0  16263  cos01gt0  16264  absef  16270  efieq1re  16272  ruclem11  16313  nn0o  16458  pythagtriplem12  16903  pythagtriplem13  16904  pythagtriplem14  16905  pythagtriplem16  16907  pclem  16915  prmgaplem4  17131  cshwshashlem2  17173  isabvd  20944  met2ndci  24708  blcvx  24984  iocopnst  25128  nmoleub2a  25305  nmoleub2b  25306  nmhmcn  25308  iscmet3lem2  25480  caubl  25496  ivthlem2  25640  ovolicc2lem4  25708  ioombl1lem4  25749  ioovolcl  25758  volsup2  25793  itg2monolem1  25938  itg2gt0  25948  itg2cnlem1  25949  dvne0  26199  ftc1lem4  26227  dgrlt  26452  aalioulem5  26528  ulmbdd  26590  iblulm  26599  radcnvlem1  26605  abelthlem5  26627  abelthlem7  26630  sincosq1lem  26691  tangtx  26699  tanabsge  26700  sinq12ge0  26702  sineq0  26718  tanord  26732  logcj  26800  argregt0  26804  argrege0  26805  argimgt0  26806  logdmnrp  26835  logcnlem3  26838  logf1o2  26844  cxpsqrtlem  26896  abscxpbnd  26947  logreclem  26956  asinneg  27080  atanlogsublem  27109  atanlogsub  27110  rlimcnp  27159  xrlimcnp  27162  basellem8  27281  chtub  27405  bposlem9  27485  chebbnd1  27665  chtppilimlem1  27666  dchrvmasumiflem1  27694  mulog2sumlem2  27728  pntrmax  27757  pntibndlem2  27784  pntibndlem3  27785  pntlemf  27798  axlowdimlem16  29336  pthdlem1  30144  crctcshwlkn0lem3  30190  crctcshwlkn0lem5  30192  crctcshwlkn0lem7  30194  crctcshwlkn0  30199  nmblolbii  31180  ubthlem1  31251  bcsiALT  31560  nmbdoplbi  32405  nmcexi  32407  nmcoplbi  32409  lnconi  32414  nmbdfnlbi  32430  nmcfnlbi  32433  nmopcoi  32476  branmfn  32486  leopmul  32515  nmopleid  32520  esumcvg  34499  ballotlemfrceq  34943  sinccvglem  36177  opnrebl2  36865  ivthALT  36879  dnibndlem12  37111  poimirlem15  38319  poimirlem31  38335  ftc1cnnclem  38375  ftc1anclem5  38381  incsequz2  38433  nnubfi  38434  bfplem2  38507  60gcd7e1  42805  lcmineqlem10  42838  3cubeslem1  43448  pell14qrgap  43635  pellfundre  43641  pellfundlb  43644  reabsifneg  44391  reabsifnpos  44392  reabsifpos  44393  reabsifnneg  44394  stoweidlem17  46764  stoweidlem34  46781  wallispilem1  46812  sqrtnegnre  48077  2elfz2melfz  48088  elfzelfzlble  48091  subsubelfzo0  48097  m1modmmod  48134  requad01  48419  requad2  48421  bgoldbtbnd  48607  bgoldbachlt  48611  tgblthelfgott  48613  nnolog2flm1  49403  itsclc0yqsol  49577