Theorem lensymd 11126

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   class class class wbr 5074  ℝcr 10870   < clt 11009   ≤ cle 11010

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-xp 5595  df-cnv 5597  df-xr 11013  df-le 11015

This theorem is referenced by:  lbinf  11928  supaddc  11942  supmul1  11944  zsupss  12677  prodge0rd  12837  infmrp1  13078  fzdisj  13283  uzdisj  13329  fzouzdisj  13423  addmodlteq  13666  seqf1olem1  13762  seqf1olem2  13763  seqcoll  14178  seqcoll2  14179  ccatalpha  14298  rlimcld2  15287  rlimno1  15365  smupvallem  16190  lcmgcdlem  16311  4sqlem11  16656  ramcl2lem  16710  recld2  23977  nmoleub2lem3  24278  ivthlem3  24617  ovolicopnf  24688  dvferm1lem  25148  dvferm2lem  25150  dgrlb  25397  dgreq0  25426  aaliou3lem9  25510  radcnvle  25579  abelthlem2  25591  dvlog2lem  25807  lgsval2lem  26455  pntlem3  26757  unblimceq0lem  34686  unblimceq0  34687  mblfinlem2  35815  imo72b2  41783  climisp  43287  stoweidlem52  43593  fourierdlem10  43658  fourierdlem12  43660  fourierdlem20  43668  fourierdlem50  43697  fourierdlem54  43701  fourierdlem103  43750  fouriersw  43772  etransclem35  43810  etransc  43824