Theorem lensymd 11259

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   class class class wbr 5086  ℝcr 11000   < clt 11141   ≤ cle 11142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-cnv 5619  df-xr 11145  df-le 11147

This theorem is referenced by:  lbinf  12070  supaddc  12084  supmul1  12086  zsupss  12830  prodge0rd  12994  infmrp1  13239  fzdisj  13446  uzdisj  13492  fzouzdisj  13590  addmodlteq  13848  seqf1olem1  13943  seqf1olem2  13944  seqcoll  14366  seqcoll2  14367  ccatalpha  14496  rlimcld2  15480  rlimno1  15556  smupvallem  16389  lcmgcdlem  16512  4sqlem11  16862  ramcl2lem  16916  psdmul  22076  recld2  24725  nmoleub2lem3  25037  ivthlem3  25376  ovolicopnf  25447  dvferm1lem  25910  dvferm2lem  25912  dgrlb  26163  dgreq0  26193  aaliou3lem9  26280  radcnvle  26351  abelthlem2  26364  dvlog2lem  26583  lgsval2lem  27240  pntlem3  27542  irredminply  33721  unblimceq0lem  36540  unblimceq0  36541  mblfinlem2  37698  imo72b2  44205  climisp  45784  stoweidlem52  46090  fourierdlem10  46155  fourierdlem12  46157  fourierdlem20  46165  fourierdlem50  46194  fourierdlem54  46198  fourierdlem103  46247  fouriersw  46269  etransclem35  46307  etransc  46321