Theorem lensymd 11332

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   class class class wbr 5110  ℝcr 11074   < clt 11215   ≤ cle 11216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-xr 11219  df-le 11221

This theorem is referenced by:  lbinf  12143  supaddc  12157  supmul1  12159  zsupss  12903  prodge0rd  13067  infmrp1  13312  fzdisj  13519  uzdisj  13565  fzouzdisj  13663  addmodlteq  13918  seqf1olem1  14013  seqf1olem2  14014  seqcoll  14436  seqcoll2  14437  ccatalpha  14565  rlimcld2  15551  rlimno1  15627  smupvallem  16460  lcmgcdlem  16583  4sqlem11  16933  ramcl2lem  16987  psdmul  22060  recld2  24710  nmoleub2lem3  25022  ivthlem3  25361  ovolicopnf  25432  dvferm1lem  25895  dvferm2lem  25897  dgrlb  26148  dgreq0  26178  aaliou3lem9  26265  radcnvle  26336  abelthlem2  26349  dvlog2lem  26568  lgsval2lem  27225  pntlem3  27527  irredminply  33713  unblimceq0lem  36501  unblimceq0  36502  mblfinlem2  37659  imo72b2  44168  climisp  45751  stoweidlem52  46057  fourierdlem10  46122  fourierdlem12  46124  fourierdlem20  46132  fourierdlem50  46161  fourierdlem54  46165  fourierdlem103  46214  fouriersw  46236  etransclem35  46274  etransc  46288