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

Theorem lenltd 10296
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 10229 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
41, 2, 3syl2anc 696 1 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wcel 2103   class class class wbr 4760  cr 10048   < clt 10187  cle 10188
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pr 5011
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-opab 4821  df-xp 5224  df-cnv 5226  df-xr 10191  df-le 10193
This theorem is referenced by:  ltnsymd  10299  nltled  10300  lensymd  10301  dedekind  10313  leadd1  10609  leord1  10668  prodge0  10983  lediv1  11001  lemuldiv  11016  lerec  11019  le2msq  11036  suprub  11097  suprleub  11102  supaddc  11103  supmul1  11105  infregelb  11120  suprfinzcl  11605  uzinfi  11882  zsupss  11891  suprzub  11893  rpnnen1lem5  11932  rpnnen1lem5OLD  11938  fzdisj  12482  uzdisj  12527  nn0disj  12570  fzouzdisj  12619  fleqceilz  12768  modsumfzodifsn  12858  addmodlteq  12860  seqf1olem1  12955  seqf1olem2  12956  leexp2  13030  hashf1  13354  seqcoll  13361  seqcoll2  13362  ccatsymb  13475  swrdccatin2  13608  rlimcld2  14429  rlimno1  14504  isercoll  14518  ruclem3  15082  bitsfzolem  15279  bitsmod  15281  sadcaddlem  15302  smupvallem  15328  pcfac  15726  4sqlem11  15782  ramcl2lem  15836  sylow1lem1  18134  fvmptnn04if  20777  chfacfisf  20782  chfacfisfcpmat  20783  recld2  22739  reconnlem2  22752  ivthlem2  23342  ivthlem3  23343  ovolicopnf  23413  ioombl1lem4  23450  ioorcl2  23461  itg1ge0a  23598  mbfi1fseqlem4  23605  itg2monolem1  23637  itg2cnlem1  23648  dvferm1lem  23867  dvferm2lem  23869  mdegmullem  23958  dgrub  24110  dgrlb  24112  dgreq0  24141  quotcan  24184  aaliou3lem9  24225  radcnvle  24294  abelthlem2  24306  logdivle  24488  cxple  24561  lgsval2lem  25152  gausslemma2dlem1a  25210  padicabv  25439  pthdlem1  26793  ssnnssfz  29779  smattr  30095  smatbl  30096  smatbr  30097  esumpcvgval  30370  eulerpartlems  30652  dstfrvunirn  30766  ballotlemodife  30789  erdszelem7  31407  erdszelem8  31408  unblimceq0  32725  unbdqndv2lem1  32727  poimirlem2  33643  poimirlem7  33648  poimirlem10  33651  poimirlem11  33652  areacirc  33737  rencldnfilem  37803  irrapxlem1  37805  monotoddzzfi  37926  radcnvrat  38932  reclt0d  40022  reclt0  40029  sqrlearg  40200  dvnxpaek  40577  volico  40620  sublevolico  40621  fourierdlem12  40756  fourierdlem42  40786  elaa2lem  40870  iundjiun  41097  hoidmvval0  41224  hoidmv1lelem2  41229  hoidmv1lelem3  41230  hoidmvlelem4  41235  hspdifhsp  41253  volico2  41278  ovolval2lem  41280  vonioo  41319  smfconst  41381  fzopredsuc  41760  stgoldbwt  42091  nnsum3primesle9  42109  bgoldbtbndlem1  42120  ssnn0ssfz  42554
  Copyright terms: Public domain W3C validator