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

Theorem lenltd 10221
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 10154 . 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:  ltnsymd  10224  nltled  10225  lensymd  10226  dedekind  10238  leadd1  10534  leord1  10593  prodge0  10908  lediv1  10926  lemuldiv  10941  lerec  10944  le2msq  10961  suprub  11022  suprleub  11027  supaddc  11028  supmul1  11030  infregelb  11045  suprfinzcl  11530  uzinfi  11806  zsupss  11815  suprzub  11817  rpnnen1lem5  11856  rpnnen1lem5OLD  11862  fzdisj  12406  uzdisj  12451  nn0disj  12494  fzouzdisj  12543  fleqceilz  12693  modsumfzodifsn  12783  addmodlteq  12785  seqf1olem1  12880  seqf1olem2  12881  leexp2  12955  hashf1  13279  seqcoll  13286  seqcoll2  13287  ccatsymb  13400  swrdccatin2  13533  rlimcld2  14353  rlimno1  14428  isercoll  14442  ruclem3  15006  bitsfzolem  15203  bitsmod  15205  sadcaddlem  15226  smupvallem  15252  pcfac  15650  4sqlem11  15706  ramcl2lem  15760  sylow1lem1  18059  fvmptnn04if  20702  chfacfisf  20707  chfacfisfcpmat  20708  recld2  22664  reconnlem2  22677  ivthlem2  23267  ivthlem3  23268  ovolicopnf  23338  ioombl1lem4  23375  ioorcl2  23386  itg1ge0a  23523  mbfi1fseqlem4  23530  itg2monolem1  23562  itg2cnlem1  23573  dvferm1lem  23792  dvferm2lem  23794  mdegmullem  23883  dgrub  24035  dgrlb  24037  dgreq0  24066  quotcan  24109  aaliou3lem9  24150  radcnvle  24219  abelthlem2  24231  logdivle  24413  cxple  24486  lgsval2lem  25077  gausslemma2dlem1a  25135  padicabv  25364  pthdlem1  26718  ssnnssfz  29677  smattr  29993  smatbl  29994  smatbr  29995  esumpcvgval  30268  eulerpartlems  30550  dstfrvunirn  30664  ballotlemodife  30687  erdszelem7  31305  erdszelem8  31306  unblimceq0  32623  unbdqndv2lem1  32625  poimirlem2  33541  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  areacirc  33635  rencldnfilem  37701  irrapxlem1  37703  monotoddzzfi  37824  radcnvrat  38830  reclt0d  39920  reclt0  39927  sqrlearg  40098  dvnxpaek  40475  volico  40518  sublevolico  40519  fourierdlem12  40654  fourierdlem42  40684  elaa2lem  40768  iundjiun  40995  hoidmvval0  41122  hoidmv1lelem2  41127  hoidmv1lelem3  41128  hoidmvlelem4  41133  hspdifhsp  41151  volico2  41176  ovolval2lem  41178  vonioo  41217  smfconst  41279  fzopredsuc  41658  stgoldbwt  41989  nnsum3primesle9  42007  bgoldbtbndlem1  42018  ssnn0ssfz  42452
  Copyright terms: Public domain W3C validator