MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltnled Structured version   Visualization version   GIF version

Theorem ltnled 10222
Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
Assertion
Ref Expression
ltnled (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))

Proof of Theorem ltnled
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 ltnle 10155 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2anc 694 1 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112  cle 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-cnv 5151  df-xr 10116  df-le 10118
This theorem is referenced by:  ltsub1  10562  ltsub2  10563  0mnnnnn0  11363  mul2lt0bi  11974  fzp1nel  12462  fzodisj  12541  elfznelfzob  12614  swrdnd  13478  cshwcsh2id  13620  sqrlem7  14033  sqrtlt  14046  lo1bdd2  14299  isercoll  14442  fprodntriv  14716  fzm1ndvds  15091  fzo0dvdseq  15092  bitsfzolem  15203  bitsfzo  15204  sadcaddlem  15226  smuval2  15251  bezoutlem3  15305  isprm5  15466  odzdvds  15547  prm23ge5  15567  pc2dvds  15630  pockthg  15657  prmreclem1  15667  prmreclem5  15671  1arith  15678  4sqlem11  15706  vdwlem6  15737  vdwlem11  15742  ramlb  15770  oddvds  18012  gexdvds  18045  sylow1lem3  18061  coe1tmmul2  19694  zringlpirlem3  19882  iccntr  22671  icccmplem2  22673  reconnlem2  22677  evth  22805  lebnumlem3  22809  nmoleub2lem3  22961  minveclem3b  23245  minveclem4  23249  pmltpclem2  23264  ovolgelb  23294  ovolicc2lem2  23332  ovolicc2lem4  23334  mbfposr  23464  itg2const2  23553  itg2cnlem2  23574  itg2cn  23575  plyco0  23993  coeeulem  24025  dgradd2  24069  pilem3  24252  cxplt2  24489  fsumharmonic  24783  dmlogdmgm  24795  lgamgulmlem1  24800  lgamucov  24809  ftalem3  24846  ftalem5  24848  ftalem7  24850  ppiprm  24922  chtprm  24924  chpub  24990  perfectlem2  25000  bposlem1  25054  lgsdilem2  25103  lgsqrlem2  25117  lgsquadlem2  25151  2sqblem  25201  pntpbnd1  25320  pntlem3  25343  nbusgrvtxm1  26325  crctcshwlkn0lem3  26760  frgrreggt1  27380  minvecolem4  27864  minvecolem5  27865  nndiffz1  29676  2sqmod  29776  psgnfzto1stlem  29978  lmdvg  30127  eulerpartlems  30550  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemrv2  30711  signsply0  30756  reprinfz1  30828  erdszelem8  31306  bccolsum  31751  unbdqndv2lem1  32625  unbdqndv2lem2  32626  poimirlem2  33541  poimirlem3  33542  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem21  33560  poimirlem22  33561  poimirlem23  33562  poimirlem26  33565  poimirlem31  33570  poimir  33572  mblfinlem2  33577  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  iblabsnclem  33603  ftc1anclem5  33619  areacirclem4  33633  areacirclem5  33634  areacirc  33635  cntotbnd  33725  elpell1qr2  37753  pellfundglb  37766  pellfund14gap  37768  congabseq  37858  jm2.19  37877  jm2.26lem3  37885  dgraa0p  38036  dvgrat  38828  uzwo4  39535  divlt0gt0d  39812  supxrgere  39862  uzublem  39970  nleltd  39994  supminfxr  40007  xrpnf  40029  sqrlearg  40098  lptre2pt  40190  limsupubuzlem  40262  climxrrelem  40299  climxlim2lem  40389  icccncfext  40418  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  volioore  40525  voliooico  40527  voliccico  40534  stoweidlem26  40561  stoweidlem34  40569  stoweidlem59  40594  stirlinglem5  40613  dirkercncflem1  40638  fourierdlem10  40652  fourierdlem19  40661  fourierdlem25  40667  fourierdlem35  40677  fourierdlem40  40682  fourierdlem42  40684  fourierdlem64  40705  fourierdlem65  40706  fourierdlem74  40715  fourierdlem75  40716  fourierdlem78  40719  fourierdlem79  40720  fourierdlem104  40745  fourierswlem  40765  fouriersw  40766  elaa2lem  40768  etransclem32  40801  etransclem41  40810  hsphoidmvle2  41120  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem2  41131  hoidmvlelem4  41133  hoidmvlelem5  41134  hoiqssbllem3  41159  hspmbllem1  41161  hspmbllem2  41162  vonicc  41220  pimdecfgtioo  41248  pimincfltioo  41249  fmtno4prmfac  41809  perfectALTVlem2  41956  aacllem  42875
  Copyright terms: Public domain W3C validator