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

Theorem lensymd 10173
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 10168 . 2 (𝜑 → (𝐴𝐵 ↔ ¬ 𝐵 < 𝐴))
51, 4mpbid 222 1 (𝜑 → ¬ 𝐵 < 𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1988   class class class wbr 4644  cr 9920   < clt 10059  cle 10060
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-br 4645  df-opab 4704  df-xp 5110  df-cnv 5112  df-xr 10063  df-le 10065
This theorem is referenced by:  lbinf  10961  infmrp1  12159  addmodlteq  12728  ccatalpha  13358  lcmgcdlem  15300  nmoleub2lem3  22896  pntlem3  25279  unblimceq0lem  32472  mblfinlem2  33418  imo72b2  38295  stoweidlem52  40032  fourierdlem10  40097  fourierdlem12  40099  fourierdlem20  40107  fourierdlem50  40136  fourierdlem54  40140  fourierdlem103  40189  fouriersw  40211  etransclem35  40249  etransc  40263
  Copyright terms: Public domain W3C validator