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

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

Proof of Theorem lenltd
StepHypRef Expression
1 ltd.1 . 2 (𝜑𝐴 ∈ ℝ)
2 ltd.2 . 2 (𝜑𝐵 ∈ ℝ)
3 lenlt 11240 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2anc 585 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wcel 2107   class class class wbr 5110  cr 11057   < clt 11196  cle 11197
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-xr 11200  df-le 11202
This theorem is referenced by:  ltnsymd  11311  nltled  11312  lensymd  11313  leadd1  11630  leord1  11689  lediv1  12027  lemuldiv  12042  lerec  12045  le2msq  12062  suprleub  12128  infregelb  12146  suprfinzcl  12624  uzinfi  12860  rpnnen1lem5  12913  nn0disj  13564  fleqceilz  13766  modsumfzodifsn  13856  addmodlteq  13858  leexp2  14083  expnngt1  14151  hashf1  14363  swrdccatin2  14624  isercoll  15559  ruclem3  16122  sadcaddlem  16344  pcfac  16778  sylow1lem1  19387  fvmptnn04if  22214  chfacfisf  22219  chfacfisfcpmat  22220  ivthlem2  24832  ioorcl2  24952  itg1ge0a  25092  mbfi1fseqlem4  25099  itg2monolem1  25131  itg2cnlem1  25142  mdegmullem  25459  quotcan  25685  logdivle  25993  cxple  26066  gausslemma2dlem1a  26729  padicabv  26994  upgrewlkle2  28596  pthdlem1  28756  ssnnssfz  31732  smattr  32420  smatbl  32421  smatbr  32422  esumpcvgval  32717  eulerpartlems  33000  dstfrvunirn  33114  ballotlemodife  33137  erdszelem7  33831  erdszelem8  33832  unbdqndv2lem1  35001  poimirlem2  36109  poimirlem7  36114  poimirlem10  36117  poimirlem11  36118  areacirc  36200  aks4d1p1p7  40560  aks4d1p3  40564  aks4d1p5  40566  sticksstones22  40605  metakunt7  40612  metakunt12  40617  metakunt22  40627  metakunt28  40633  metakunt29  40634  metakunt30  40635  frlmvscadiccat  40710  rencldnfilem  41172  irrapxlem1  41174  monotoddzzfi  41295  sqrtcvallem1  41977  reabsifneg  41978  reabsifpos  41980  radcnvrat  42668  reclt0d  43695  reclt0  43700  sqrlearg  43865  dvnxpaek  44257  volico  44298  sublevolico  44299  fourierdlem12  44434  fourierdlem42  44464  elaa2lem  44548  iundjiun  44775  hoidmvval0  44902  hoidmv1lelem2  44907  hoidmv1lelem3  44908  hoidmvlelem4  44913  hspdifhsp  44931  volico2  44956  ovolval2lem  44958  vonioo  44997  smfconst  45064  fzopredsuc  45629  stgoldbwt  46042  nnsum3primesle9  46060  bgoldbtbndlem1  46071  ssnn0ssfz  46499
  Copyright terms: Public domain W3C validator