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

Theorem lensymd 11313
Description: 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
lensymd.3 (𝜑𝐴𝐵)
Assertion
Ref Expression
lensymd (𝜑 → ¬ 𝐵 < 𝐴)

Proof of Theorem lensymd
StepHypRef Expression
1 lensymd.3 . 2 (𝜑𝐴𝐵)
2 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
3 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
42, 3lenltd 11308 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
51, 4mpbid 231 1 (𝜑 → ¬ 𝐵 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  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:  lbinf  12115  supaddc  12129  supmul1  12131  zsupss  12869  prodge0rd  13029  infmrp1  13270  fzdisj  13475  uzdisj  13521  fzouzdisj  13615  addmodlteq  13858  seqf1olem1  13954  seqf1olem2  13955  seqcoll  14370  seqcoll2  14371  ccatalpha  14488  rlimcld2  15467  rlimno1  15545  smupvallem  16370  lcmgcdlem  16489  4sqlem11  16834  ramcl2lem  16888  recld2  24193  nmoleub2lem3  24494  ivthlem3  24833  ovolicopnf  24904  dvferm1lem  25364  dvferm2lem  25366  dgrlb  25613  dgreq0  25642  aaliou3lem9  25726  radcnvle  25795  abelthlem2  25807  dvlog2lem  26023  lgsval2lem  26671  pntlem3  26973  unblimceq0lem  34998  unblimceq0  34999  mblfinlem2  36145  imo72b2  42519  climisp  44061  stoweidlem52  44367  fourierdlem10  44432  fourierdlem12  44434  fourierdlem20  44442  fourierdlem50  44471  fourierdlem54  44475  fourierdlem103  44524  fouriersw  44546  etransclem35  44584  etransc  44598
  Copyright terms: Public domain W3C validator