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

Theorem ltnled 10776
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 10709 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
41, 2, 3syl2anc 584 1 (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wcel 2105   class class class wbr 5058  cr 10525   < clt 10664  cle 10665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-xp 5555  df-cnv 5557  df-xr 10668  df-le 10670
This theorem is referenced by:  ltsub1  11125  ltsub2  11126  0mnnnnn0  11918  mul2lt0bi  12485  fzp1nel  12981  fzodisj  13061  elfznelfzob  13133  ccatsymb  13926  swrdnd  14006  cshwcsh2id  14180  sqrlem7  14598  sqrtlt  14611  lo1bdd2  14871  isercoll  15014  fprodntriv  15286  fzm1ndvds  15662  fzo0dvdseq  15663  bitsfzolem  15773  bitsfzo  15774  sadcaddlem  15796  smuval2  15821  bezoutlem3  15879  2mulprm  16027  isprm5  16041  odzdvds  16122  prm23ge5  16142  pc2dvds  16205  pockthg  16232  prmreclem1  16242  prmreclem5  16246  1arith  16253  4sqlem11  16281  vdwlem6  16312  vdwlem11  16317  ramlb  16345  oddvds  18606  gexdvds  18640  sylow1lem3  18656  coe1tmmul2  20374  zringlpirlem3  20563  iccntr  23358  icccmplem2  23360  reconnlem2  23364  evth  23492  lebnumlem3  23496  nmoleub2lem3  23648  minveclem3b  23960  minveclem4  23964  pmltpclem2  23979  ovolgelb  24010  ovolicc2lem2  24048  ovolicc2lem4  24050  mbfposr  24182  itg2const2  24271  itg2cnlem2  24292  itg2cn  24293  plyco0  24711  coeeulem  24743  dgradd2  24787  cxplt2  25208  fsumharmonic  25517  dmlogdmgm  25529  lgamgulmlem1  25534  lgamucov  25543  ftalem3  25580  ftalem5  25582  ftalem7  25584  ppiprm  25656  chtprm  25658  chpub  25724  perfectlem2  25734  bposlem1  25788  lgsdilem2  25837  lgsqrlem2  25851  lgsquadlem2  25885  2sqblem  25935  2sqmod  25940  2sqnn0  25942  pntpbnd1  26090  pntlem3  26113  nbusgrvtxm1  27089  crctcshwlkn0lem3  27518  frgrreggt1  28100  minvecolem4  28585  minvecolem5  28586  nndiffz1  30436  psgnfzto1stlem  30670  lmdvg  31096  eulerpartlems  31518  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemrv2  31679  signsply0  31721  reprinfz1  31793  lpadmax  31853  lpadright  31855  0nn0m1nnn0  32249  erdszelem8  32343  bccolsum  32869  unbdqndv2lem1  33746  unbdqndv2lem2  33747  poimirlem2  34776  poimirlem3  34777  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem23  34797  poimirlem26  34800  poimirlem31  34805  poimir  34807  mblfinlem2  34812  itg2addnclem  34825  itg2addnclem2  34826  itg2addnclem3  34827  iblabsnclem  34837  ftc1anclem5  34853  areacirclem4  34867  areacirclem5  34868  areacirc  34869  cntotbnd  34957  elpell1qr2  39349  pellfundglb  39362  pellfund14gap  39364  congabseq  39451  jm2.19  39470  jm2.26lem3  39478  dgraa0p  39629  dvgrat  40524  uzwo4  41195  divlt0gt0d  41432  supxrgere  41481  uzublem  41584  nleltd  41608  supminfxr  41620  xrpnf  41642  sqrlearg  41709  lptre2pt  41801  limsupubuzlem  41873  climxrrelem  41910  climxlim2lem  42006  icccncfext  42050  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  volioore  42156  voliooico  42158  voliccico  42165  stoweidlem26  42192  stoweidlem34  42200  stoweidlem59  42225  stirlinglem5  42244  dirkercncflem1  42269  fourierdlem10  42283  fourierdlem19  42292  fourierdlem25  42298  fourierdlem35  42308  fourierdlem40  42313  fourierdlem42  42315  fourierdlem64  42336  fourierdlem65  42337  fourierdlem74  42346  fourierdlem75  42347  fourierdlem78  42350  fourierdlem79  42351  fourierdlem104  42376  fourierswlem  42396  fouriersw  42397  elaa2lem  42399  etransclem32  42432  etransclem41  42441  hsphoidmvle2  42748  hoidmv1lelem1  42754  hoidmv1lelem2  42755  hoidmv1lelem3  42756  hoidmvlelem2  42759  hoidmvlelem4  42761  hoidmvlelem5  42762  hoiqssbllem3  42787  hspmbllem1  42789  hspmbllem2  42790  vonicc  42848  pimdecfgtioo  42876  pimincfltioo  42877  fmtno4prmfac  43581  requad01  43633  requad1  43634  perfectALTVlem2  43734  itsclc0yqsol  44649  aacllem  44800
  Copyright terms: Public domain W3C validator