Theorem ltle 11269

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  leltletr  11272  ltleletr  11274  letr  11275  letric  11281  ltlen  11282  ltlei  11303  ltled  11329  lt2add  11670  lep1  12030  lem1  12032  letrp1  12033  ltmul12a  12045  mulge0b  12060  lediv12a  12083  bndndx  12448  ltsubnn0  12500  uzind  12633  fnn0ind  12640  eluz2b2  12887  zmin  12910  rpnnen1lem2  12943  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  rpge0  12972  rpneg  12992  iccsplit  13453  zltaddlt1le  13473  difelfznle  13610  fvffz0  13614  elfzouz2  13642  elfzo0le  13671  fzostep1  13751  fllep1  13770  fracle1  13772  expgt1  14072  expnbnd  14204  expnlbnd2  14206  faclbnd  14262  swrdnd0  14629  swrdsbslen  14636  swrdspsleq  14637  pfxccat3  14706  swrdccat  14707  repswswrd  14756  resqrex  15223  sqrtgt0  15231  absmax  15303  eqsqrt2d  15342  rlim2lt  15470  mulcn2  15569  rlimo1  15590  o1rlimmul  15592  climbdd  15645  caucvgrlem  15646  supcvg  15829  efcllem  16050  sin01bnd  16160  cos01bnd  16161  sin01gt0  16165  cos01gt0  16166  absef  16172  efieq1re  16174  ruclem11  16215  nn0o  16360  pythagtriplem12  16804  pythagtriplem13  16805  pythagtriplem14  16806  pythagtriplem16  16808  pclem  16816  prmgaplem4  17032  cshwshashlem2  17074  isabvd  20728  met2ndci  24417  blcvx  24693  iocopnst  24844  nmoleub2a  25024  nmoleub2b  25025  nmhmcn  25027  iscmet3lem2  25199  caubl  25215  ivthlem2  25360  ovolicc2lem4  25428  ioombl1lem4  25469  ioovolcl  25478  volsup2  25513  itg2monolem1  25658  itg2gt0  25668  itg2cnlem1  25669  dvne0  25923  ftc1lem4  25953  dgrlt  26179  aalioulem5  26251  ulmbdd  26314  iblulm  26323  radcnvlem1  26329  abelthlem5  26352  abelthlem7  26355  sincosq1lem  26413  tangtx  26421  tanabsge  26422  sinq12ge0  26424  sineq0  26440  tanord  26454  logcj  26522  argregt0  26526  argrege0  26527  argimgt0  26528  logdmnrp  26557  logcnlem3  26560  logf1o2  26566  cxpsqrtlem  26618  abscxpbnd  26670  logreclem  26679  asinneg  26803  atanlogsublem  26832  atanlogsub  26833  rlimcnp  26882  xrlimcnp  26885  basellem8  27005  chtub  27130  bposlem9  27210  chebbnd1  27390  chtppilimlem1  27391  dchrvmasumiflem1  27419  mulog2sumlem2  27453  pntrmax  27482  pntibndlem2  27509  pntibndlem3  27510  pntlemf  27523  axlowdimlem16  28891  pthdlem1  29703  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  crctcshwlkn0lem7  29753  crctcshwlkn0  29758  nmblolbii  30735  ubthlem1  30806  bcsiALT  31115  nmbdoplbi  31960  nmcexi  31962  nmcoplbi  31964  lnconi  31969  nmbdfnlbi  31985  nmcfnlbi  31988  nmopcoi  32031  branmfn  32041  leopmul  32070  nmopleid  32075  esumcvg  34083  ballotlemfrceq  34527  sinccvglem  35666  opnrebl2  36316  ivthALT  36330  dnibndlem12  36484  poimirlem15  37636  poimirlem31  37652  ftc1cnnclem  37692  ftc1anclem5  37698  incsequz2  37750  nnubfi  37751  bfplem2  37824  60gcd7e1  42000  lcmineqlem10  42033  3cubeslem1  42679  pell14qrgap  42870  pellfundre  42876  pellfundlb  42879  reabsifneg  43628  reabsifnpos  43629  reabsifpos  43630  reabsifnneg  43631  stoweidlem17  46022  stoweidlem34  46039  wallispilem1  46070  sqrtnegnre  47312  2elfz2melfz  47323  elfzelfzlble  47326  subsubelfzo0  47331  m1modmmod  47363  requad01  47626  requad2  47628  bgoldbtbnd  47814  bgoldbachlt  47818  tgblthelfgott  47820  nnolog2flm1  48583  itsclc0yqsol  48757