Theorem lensymd 11385

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 11380	. 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 11123   < clt 11267   ≤ cle 11268

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 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5661  df-cnv 5663  df-xr 11271  df-le 11273

This theorem is used by:  lbinf  12192  supaddc  12206  supmul1  12208  zsupss  12986  prodge0rd  13151  infmrp1  13397  fzdisj  13606  uzdisj  13652  fzouzdisj  13751  addmodlteq  14010  seqf1olem1  14105  seqf1olem2  14106  seqcoll  14529  seqcoll2  14530  ccatalpha  14660  rlimcld2  15665  rlimno1  15741  smupvallem  16573  lcmgcdlem  16696  4sqlem11  17047  ramcl2lem  17101  psdmul  22394  recld2  25041  nmoleub2lem3  25343  ivthlem3  25681  ovolicopnf  25752  dvferm1lem  26211  dvferm2lem  26213  dgrlb  26462  dgreq0  26491  aaliou3lem9  26586  radcnvle  26656  abelthlem2  26668  dvlog2lem  26889  lgsval2lem  27543  pntlem3  27845  irredminply  34226  unblimceq0lem  37203  unblimceq0  37204  mblfinlem2  38407  imo72b2  45012  climisp  46574  stoweidlem52  46880  fourierdlem10  46945  fourierdlem12  46947  fourierdlem20  46955  fourierdlem50  46984  fourierdlem54  46988  fourierdlem103  47037  fouriersw  47059  etransclem35  47097  etransc  47111