Theorem lensymd 11361

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

Step	Hyp	Ref	Expression
1		lensymd.3	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4	2, 3	lenltd 11356	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbid 231	1 ⊢ (𝜑 → ¬ 𝐵 < 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   class class class wbr 5147  ℝcr 11105   < clt 11244   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-xr 11248  df-le 11250

This theorem is referenced by:  lbinf  12163  supaddc  12177  supmul1  12179  zsupss  12917  prodge0rd  13077  infmrp1  13319  fzdisj  13524  uzdisj  13570  fzouzdisj  13664  addmodlteq  13907  seqf1olem1  14003  seqf1olem2  14004  seqcoll  14421  seqcoll2  14422  ccatalpha  14539  rlimcld2  15518  rlimno1  15596  smupvallem  16420  lcmgcdlem  16539  4sqlem11  16884  ramcl2lem  16938  recld2  24321  nmoleub2lem3  24622  ivthlem3  24961  ovolicopnf  25032  dvferm1lem  25492  dvferm2lem  25494  dgrlb  25741  dgreq0  25770  aaliou3lem9  25854  radcnvle  25923  abelthlem2  25935  dvlog2lem  26151  lgsval2lem  26799  pntlem3  27101  unblimceq0lem  35370  unblimceq0  35371  mblfinlem2  36514  imo72b2  42909  climisp  44448  stoweidlem52  44754  fourierdlem10  44819  fourierdlem12  44821  fourierdlem20  44829  fourierdlem50  44858  fourierdlem54  44862  fourierdlem103  44911  fouriersw  44933  etransclem35  44971  etransc  44985