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 233	1 ⊢ (𝜑 → ¬ 𝐵 < 𝐴)

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2119   class class class wbr 5072  ℝ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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  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  22154  recld2  24798  nmoleub2lem3  25100  ivthlem3  25438  ovolicopnf  25509  dvferm1lem  25969  dvferm2lem  25971  dgrlb  26219  dgreq0  26248  aaliou3lem9  26334  radcnvle  26403  abelthlem2  26415  dvlog2lem  26634  lgsval2lem  27288  pntlem3  27590  irredminply  33900  unblimceq0lem  36812  unblimceq0  36813  mblfinlem2  38025  imo72b2  44616  climisp  46189  stoweidlem52  46495  fourierdlem10  46560  fourierdlem12  46562  fourierdlem20  46570  fourierdlem50  46599  fourierdlem54  46603  fourierdlem103  46652  fouriersw  46674  etransclem35  46712  etransc  46726