Theorem lensymd 11288

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 11283	. 2 ⊢ (𝜑 → (𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴))
5	1, 4	mpbid 232	1 ⊢ (𝜑 → ¬ 𝐵 < 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170   ≤ cle 11171

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-xr 11174  df-le 11176

This theorem is referenced by:  lbinf  12100  supaddc  12114  supmul1  12116  zsupss  12878  prodge0rd  13042  infmrp1  13288  fzdisj  13496  uzdisj  13542  fzouzdisj  13641  addmodlteq  13899  seqf1olem1  13994  seqf1olem2  13995  seqcoll  14417  seqcoll2  14418  ccatalpha  14547  rlimcld2  15531  rlimno1  15607  smupvallem  16443  lcmgcdlem  16566  4sqlem11  16917  ramcl2lem  16971  psdmul  22142  recld2  24790  nmoleub2lem3  25092  ivthlem3  25430  ovolicopnf  25501  dvferm1lem  25961  dvferm2lem  25963  dgrlb  26211  dgreq0  26240  aaliou3lem9  26327  radcnvle  26398  abelthlem2  26410  dvlog2lem  26629  lgsval2lem  27284  pntlem3  27586  irredminply  33876  unblimceq0lem  36782  unblimceq0  36783  mblfinlem2  37993  imo72b2  44617  climisp  46192  stoweidlem52  46498  fourierdlem10  46563  fourierdlem12  46565  fourierdlem20  46573  fourierdlem50  46602  fourierdlem54  46606  fourierdlem103  46655  fouriersw  46677  etransclem35  46715  etransc  46729