Theorem lensymd 11301

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  lbinf  12112  supaddc  12126  supmul1  12128  zsupss  12872  prodge0rd  13036  infmrp1  13281  fzdisj  13488  uzdisj  13534  fzouzdisj  13632  addmodlteq  13887  seqf1olem1  13982  seqf1olem2  13983  seqcoll  14405  seqcoll2  14406  ccatalpha  14534  rlimcld2  15520  rlimno1  15596  smupvallem  16429  lcmgcdlem  16552  4sqlem11  16902  ramcl2lem  16956  psdmul  22029  recld2  24679  nmoleub2lem3  24991  ivthlem3  25330  ovolicopnf  25401  dvferm1lem  25864  dvferm2lem  25866  dgrlb  26117  dgreq0  26147  aaliou3lem9  26234  radcnvle  26305  abelthlem2  26318  dvlog2lem  26537  lgsval2lem  27194  pntlem3  27496  irredminply  33679  unblimceq0lem  36467  unblimceq0  36468  mblfinlem2  37625  imo72b2  44134  climisp  45717  stoweidlem52  46023  fourierdlem10  46088  fourierdlem12  46090  fourierdlem20  46098  fourierdlem50  46127  fourierdlem54  46131  fourierdlem103  46180  fouriersw  46202  etransclem35  46240  etransc  46254