Theorem lensymd 11454

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11340  df-le 11342

This theorem is used by:  lbinf  12263  supaddc  12277  supmul1  12279  zsupss  13057  prodge0rd  13222  infmrp1  13468  fzdisj  13678  uzdisj  13724  fzouzdisj  13823  addmodlteq  14082  seqf1olem1  14177  seqf1olem2  14178  seqcoll  14602  seqcoll2  14603  ccatalpha  14733  rlimcld2  15738  rlimno1  15814  smupvallem  16646  lcmgcdlem  16774  4sqlem11  17126  ramcl2lem  17180  psdmul  22480  recld2  25127  nmoleub2lem3  25429  ivthlem3  25767  ovolicopnf  25838  dvferm1lem  26297  dvferm2lem  26299  dgrlb  26548  dgreq0  26577  aaliou3lem9  26670  radcnvle  26740  abelthlem2  26752  dvlog2lem  26973  lgsval2lem  27627  pntlem3  27929  irredminply  34341  unblimceq0lem  37352  unblimceq0  37353  mblfinlem2  38556  imo72b2  45157  climisp  46725  stoweidlem52  47031  fourierdlem10  47096  fourierdlem12  47098  fourierdlem20  47106  fourierdlem50  47135  fourierdlem54  47139  fourierdlem103  47188  fouriersw  47210  etransclem35  47248  etransc  47262