Theorem lensymd 11466

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11204   < clt 11348   ≤ cle 11349

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-xr 11352  df-le 11354

This theorem is used by:  lbinf  12275  supaddc  12289  supmul1  12291  zsupss  13069  prodge0rd  13234  infmrp1  13480  fzdisj  13690  uzdisj  13736  fzouzdisj  13835  addmodlteq  14094  seqf1olem1  14189  seqf1olem2  14190  seqcoll  14614  seqcoll2  14615  ccatalpha  14745  rlimcld2  15752  rlimno1  15828  smupvallem  16660  lcmgcdlem  16788  4sqlem11  17140  ramcl2lem  17194  psdmul  22494  recld2  25141  nmoleub2lem3  25443  ivthlem3  25781  ovolicopnf  25852  dvferm1lem  26311  dvferm2lem  26313  dgrlb  26562  dgreq0  26591  aaliou3lem9  26684  radcnvle  26754  abelthlem2  26766  dvlog2lem  26987  lgsval2lem  27641  pntlem3  27943  irredminply  34396  unblimceq0lem  37466  unblimceq0  37467  mblfinlem2  38683  imo72b2  45279  climisp  46863  stoweidlem52  47169  fourierdlem10  47234  fourierdlem12  47236  fourierdlem20  47244  fourierdlem50  47273  fourierdlem54  47277  fourierdlem103  47326  fouriersw  47348  etransclem35  47386  etransc  47400