Theorem lensymd 11284

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

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 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  lbinf  12095  supaddc  12109  supmul1  12111  zsupss  12850  prodge0rd  13014  infmrp1  13260  fzdisj  13467  uzdisj  13513  fzouzdisj  13611  addmodlteq  13869  seqf1olem1  13964  seqf1olem2  13965  seqcoll  14387  seqcoll2  14388  ccatalpha  14517  rlimcld2  15501  rlimno1  15577  smupvallem  16410  lcmgcdlem  16533  4sqlem11  16883  ramcl2lem  16937  psdmul  22109  recld2  24759  nmoleub2lem3  25071  ivthlem3  25410  ovolicopnf  25481  dvferm1lem  25944  dvferm2lem  25946  dgrlb  26197  dgreq0  26227  aaliou3lem9  26314  radcnvle  26385  abelthlem2  26398  dvlog2lem  26617  lgsval2lem  27274  pntlem3  27576  irredminply  33873  unblimceq0lem  36706  unblimceq0  36707  mblfinlem2  37859  imo72b2  44413  climisp  45990  stoweidlem52  46296  fourierdlem10  46361  fourierdlem12  46363  fourierdlem20  46371  fourierdlem50  46400  fourierdlem54  46404  fourierdlem103  46453  fouriersw  46475  etransclem35  46513  etransc  46527