Theorem lensymd 11372

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2146   class class class wbr 5111  ℝcr 11110   < clt 11254   ≤ cle 11255

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11258  df-le 11260

This theorem is used by:  lbinf  12179  supaddc  12193  supmul1  12195  zsupss  12973  prodge0rd  13137  infmrp1  13383  fzdisj  13592  uzdisj  13638  fzouzdisj  13737  addmodlteq  13996  seqf1olem1  14091  seqf1olem2  14092  seqcoll  14515  seqcoll2  14516  ccatalpha  14646  rlimcld2  15649  rlimno1  15725  smupvallem  16559  lcmgcdlem  16682  4sqlem11  17033  ramcl2lem  17087  psdmul  22359  recld2  25003  nmoleub2lem3  25305  ivthlem3  25643  ovolicopnf  25714  dvferm1lem  26174  dvferm2lem  26176  dgrlb  26424  dgreq0  26453  aaliou3lem9  26544  radcnvle  26614  abelthlem2  26626  dvlog2lem  26848  lgsval2lem  27502  pntlem3  27804  irredminply  34146  unblimceq0lem  37128  unblimceq0  37129  mblfinlem2  38342  imo72b2  44931  climisp  46493  stoweidlem52  46799  fourierdlem10  46864  fourierdlem12  46866  fourierdlem20  46874  fourierdlem50  46903  fourierdlem54  46907  fourierdlem103  46956  fouriersw  46978  etransclem35  47016  etransc  47030