Theorem lensymd 11369

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106   class class class wbr 5148  ℝcr 11111   < clt 11252   ≤ cle 11253

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-xr 11256  df-le 11258

This theorem is referenced by:  lbinf  12171  supaddc  12185  supmul1  12187  zsupss  12925  prodge0rd  13085  infmrp1  13327  fzdisj  13532  uzdisj  13578  fzouzdisj  13672  addmodlteq  13915  seqf1olem1  14011  seqf1olem2  14012  seqcoll  14429  seqcoll2  14430  ccatalpha  14547  rlimcld2  15526  rlimno1  15604  smupvallem  16428  lcmgcdlem  16547  4sqlem11  16892  ramcl2lem  16946  recld2  24550  nmoleub2lem3  24855  ivthlem3  25194  ovolicopnf  25265  dvferm1lem  25725  dvferm2lem  25727  dgrlb  25974  dgreq0  26003  aaliou3lem9  26087  radcnvle  26156  abelthlem2  26168  dvlog2lem  26384  lgsval2lem  27034  pntlem3  27336  unblimceq0lem  35685  unblimceq0  35686  mblfinlem2  36829  imo72b2  43226  climisp  44761  stoweidlem52  45067  fourierdlem10  45132  fourierdlem12  45134  fourierdlem20  45142  fourierdlem50  45171  fourierdlem54  45175  fourierdlem103  45224  fouriersw  45246  etransclem35  45284  etransc  45298