Theorem lensymd 10834

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2111   class class class wbr 5035  ℝcr 10579   < clt 10718   ≤ cle 10719

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5172  ax-nul 5179  ax-pr 5301

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-br 5036  df-opab 5098  df-xp 5533  df-cnv 5535  df-xr 10722  df-le 10724

This theorem is referenced by:  lbinf  11635  supaddc  11649  supmul1  11651  zsupss  12382  prodge0rd  12542  infmrp1  12783  fzdisj  12988  uzdisj  13034  fzouzdisj  13127  addmodlteq  13368  seqf1olem1  13464  seqf1olem2  13465  seqcoll  13879  seqcoll2  13880  ccatalpha  13999  rlimcld2  14988  rlimno1  15063  smupvallem  15887  lcmgcdlem  16007  4sqlem11  16351  ramcl2lem  16405  recld2  23520  nmoleub2lem3  23821  ivthlem3  24158  ovolicopnf  24229  dvferm1lem  24688  dvferm2lem  24690  dgrlb  24937  dgreq0  24966  aaliou3lem9  25050  radcnvle  25119  abelthlem2  25131  dvlog2lem  25347  lgsval2lem  25995  pntlem3  26297  unblimceq0lem  34261  unblimceq0  34262  mblfinlem2  35401  imo72b2  41279  climisp  42782  stoweidlem52  43088  fourierdlem10  43153  fourierdlem12  43155  fourierdlem20  43163  fourierdlem50  43192  fourierdlem54  43196  fourierdlem103  43245  fouriersw  43267  etransclem35  43305  etransc  43319