Theorem lensymd 11296

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  lbinf  12107  supaddc  12121  supmul1  12123  zsupss  12862  prodge0rd  13026  infmrp1  13272  fzdisj  13479  uzdisj  13525  fzouzdisj  13623  addmodlteq  13881  seqf1olem1  13976  seqf1olem2  13977  seqcoll  14399  seqcoll2  14400  ccatalpha  14529  rlimcld2  15513  rlimno1  15589  smupvallem  16422  lcmgcdlem  16545  4sqlem11  16895  ramcl2lem  16949  psdmul  22121  recld2  24771  nmoleub2lem3  25083  ivthlem3  25422  ovolicopnf  25493  dvferm1lem  25956  dvferm2lem  25958  dgrlb  26209  dgreq0  26239  aaliou3lem9  26326  radcnvle  26397  abelthlem2  26410  dvlog2lem  26629  lgsval2lem  27286  pntlem3  27588  irredminply  33894  unblimceq0lem  36728  unblimceq0  36729  mblfinlem2  37909  imo72b2  44528  climisp  46104  stoweidlem52  46410  fourierdlem10  46475  fourierdlem12  46477  fourierdlem20  46485  fourierdlem50  46514  fourierdlem54  46518  fourierdlem103  46567  fouriersw  46589  etransclem35  46627  etransc  46641