Theorem lensymd 11328

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2141   class class class wbr 5097  ℝcr 11066   < clt 11210   ≤ cle 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-cnv 5651  df-xr 11214  df-le 11216

This theorem is referenced by:  lbinf  12139  supaddc  12153  supmul1  12155  zsupss  12932  prodge0rd  13096  infmrp1  13342  fzdisj  13550  uzdisj  13596  fzouzdisj  13695  addmodlteq  13953  seqf1olem1  14048  seqf1olem2  14049  seqcoll  14471  seqcoll2  14472  ccatalpha  14601  rlimcld2  15596  rlimno1  15672  smupvallem  16508  lcmgcdlem  16631  4sqlem11  16982  ramcl2lem  17036  psdmul  22219  recld2  24863  nmoleub2lem3  25165  ivthlem3  25503  ovolicopnf  25574  dvferm1lem  26034  dvferm2lem  26036  dgrlb  26284  dgreq0  26313  aaliou3lem9  26402  radcnvle  26471  abelthlem2  26483  dvlog2lem  26705  lgsval2lem  27359  pntlem3  27661  irredminply  33974  unblimceq0lem  36905  unblimceq0  36906  mblfinlem2  38118  imo72b2  44709  climisp  46281  stoweidlem52  46587  fourierdlem10  46652  fourierdlem12  46654  fourierdlem20  46662  fourierdlem50  46691  fourierdlem54  46695  fourierdlem103  46744  fouriersw  46766  etransclem35  46804  etransc  46818