Theorem lensymd 11500

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   < clt 11382   ≤ cle 11383

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-xp 5664  df-cnv 5666  df-xr 11386  df-le 11388

This theorem is used by:  lbinf  12310  supaddc  12324  supmul1  12326  zsupss  13104  prodge0rd  13269  infmrp1  13515  fzdisj  13725  uzdisj  13771  fzouzdisj  13870  addmodlteq  14129  seqf1olem1  14224  seqf1olem2  14225  seqcoll  14650  seqcoll2  14651  ccatalpha  14781  rlimcld2  15789  rlimno1  15865  smupvallem  16697  lcmgcdlem  16825  4sqlem11  17177  ramcl2lem  17231  psdmul  22542  recld2  25189  nmoleub2lem3  25491  ivthlem3  25829  ovolicopnf  25900  dvferm1lem  26359  dvferm2lem  26361  dgrlb  26610  dgreq0  26639  aaliou3lem9  26734  radcnvle  26804  abelthlem2  26816  dvlog2lem  27037  lgsval2lem  27691  pntlem3  27993  irredminply  34459  unblimceq0lem  37587  unblimceq0  37588  mblfinlem2  38844  imo72b2  45433  climisp  47029  stoweidlem52  47335  fourierdlem10  47400  fourierdlem12  47402  fourierdlem20  47410  fourierdlem50  47439  fourierdlem54  47443  fourierdlem103  47492  fouriersw  47514  etransclem35  47552  etransc  47566