Theorem ltle 11234

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-pre-lttri 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185

This theorem is referenced by:  leltletr  11237  ltleletr  11239  letr  11240  letric  11246  ltlen  11247  ltlei  11268  ltled  11294  lt2add  11635  lep1  11996  lem1  11998  letrp1  11999  ltmul12a  12011  mulge0b  12026  lediv12a  12049  bndndx  12436  ltsubnn0  12488  uzind  12621  fnn0ind  12628  eluz2b2  12871  zmin  12894  rpnnen1lem2  12927  rpnnen1lem1  12928  rpnnen1lem3  12929  rpnnen1lem5  12931  rpge0  12956  rpneg  12976  iccsplit  13438  zltaddlt1le  13458  difelfznle  13596  fvffz0  13600  elfzouz2  13629  elfzo0le  13658  fzostep1  13741  fllep1  13760  fracle1  13762  expgt1  14062  expnbnd  14194  expnlbnd2  14196  faclbnd  14252  swrdnd0  14620  swrdsbslen  14627  swrdspsleq  14628  pfxccat3  14696  swrdccat  14697  repswswrd  14746  resqrex  15212  sqrtgt0  15220  absmax  15292  eqsqrt2d  15331  rlim2lt  15459  mulcn2  15558  rlimo1  15579  o1rlimmul  15581  climbdd  15634  caucvgrlem  15635  supcvg  15821  efcllem  16042  sin01bnd  16152  cos01bnd  16153  sin01gt0  16157  cos01gt0  16158  absef  16164  efieq1re  16166  ruclem11  16207  nn0o  16352  pythagtriplem12  16797  pythagtriplem13  16798  pythagtriplem14  16799  pythagtriplem16  16801  pclem  16809  prmgaplem4  17025  cshwshashlem2  17067  isabvd  20789  met2ndci  24487  blcvx  24763  iocopnst  24907  nmoleub2a  25084  nmoleub2b  25085  nmhmcn  25087  iscmet3lem2  25259  caubl  25275  ivthlem2  25419  ovolicc2lem4  25487  ioombl1lem4  25528  ioovolcl  25537  volsup2  25572  itg2monolem1  25717  itg2gt0  25727  itg2cnlem1  25728  dvne0  25978  ftc1lem4  26006  dgrlt  26231  aalioulem5  26302  ulmbdd  26363  iblulm  26372  radcnvlem1  26378  abelthlem5  26400  abelthlem7  26403  sincosq1lem  26461  tangtx  26469  tanabsge  26470  sinq12ge0  26472  sineq0  26488  tanord  26502  logcj  26570  argregt0  26574  argrege0  26575  argimgt0  26576  logdmnrp  26605  logcnlem3  26608  logf1o2  26614  cxpsqrtlem  26666  abscxpbnd  26717  logreclem  26726  asinneg  26850  atanlogsublem  26879  atanlogsub  26880  rlimcnp  26929  xrlimcnp  26932  basellem8  27051  chtub  27175  bposlem9  27255  chebbnd1  27435  chtppilimlem1  27436  dchrvmasumiflem1  27464  mulog2sumlem2  27498  pntrmax  27527  pntibndlem2  27554  pntibndlem3  27555  pntlemf  27568  axlowdimlem16  29026  pthdlem1  29834  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  crctcshwlkn0lem7  29884  crctcshwlkn0  29889  nmblolbii  30870  ubthlem1  30941  bcsiALT  31250  nmbdoplbi  32095  nmcexi  32097  nmcoplbi  32099  lnconi  32104  nmbdfnlbi  32120  nmcfnlbi  32123  nmopcoi  32166  branmfn  32176  leopmul  32205  nmopleid  32210  esumcvg  34230  ballotlemfrceq  34673  sinccvglem  35854  opnrebl2  36503  ivthALT  36517  dnibndlem12  36749  poimirlem15  37956  poimirlem31  37972  ftc1cnnclem  38012  ftc1anclem5  38018  incsequz2  38070  nnubfi  38071  bfplem2  38144  60gcd7e1  42444  lcmineqlem10  42477  3cubeslem1  43116  pell14qrgap  43303  pellfundre  43309  pellfundlb  43312  reabsifneg  44059  reabsifnpos  44060  reabsifpos  44061  reabsifnneg  44062  stoweidlem17  46445  stoweidlem34  46462  wallispilem1  46493  sqrtnegnre  47755  2elfz2melfz  47766  elfzelfzlble  47769  subsubelfzo0  47775  m1modmmod  47812  requad01  48097  requad2  48099  bgoldbtbnd  48285  bgoldbachlt  48289  tgblthelfgott  48291  nnolog2flm1  49066  itsclc0yqsol  49240