Theorem ltnled 11464

Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
ltnled	⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Proof of Theorem ltnled

Step	Hyp	Ref	Expression
1		ltd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltd.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℝ)
3		ltnle 11396	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2144   class class class wbr 5102  ℝcr 11206   < clt 11350   ≤ cle 11351

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 5391

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 5657  df-cnv 5659  df-xr 11354  df-le 11356

This theorem is used by:  ltsub1  11819  ltsub2  11820  0mnnnnn0  12645  0nn0m1nnn0  12760  mul2lt0bi  13235  fzp1nel  13752  fzodisj  13835  elfznelfzob  13916  ccatsymb  14735  swrdnd  14812  cshwcsh2id  14987  01sqrexlem7  15424  sqrtlt  15437  lo1bdd2  15700  isercoll  15844  fprodntriv  16118  fzm1ndvds  16501  fzo0dvdseq  16502  bitsfzolem  16613  bitsfzo  16614  sadcaddlem  16636  smuval2  16661  bezoutlem3  16723  2mulprm  16877  isprm5  16892  odzdvds  16982  prm23ge5  17002  pc2dvds  17066  pockthg  17093  prmreclem1  17103  prmreclem5  17107  1arith  17114  4sqlem11  17142  vdwlem6  17173  vdwlem11  17178  ramlb  17206  oddvds  19770  gexdvds  19807  sylow1lem3  19823  zringlpirlem3  21779  psdmul  22496  coe1tmmul2  22604  iccntr  25150  icccmplem2  25152  reconnlem2  25156  evth  25289  lebnumlem3  25293  nmoleub2lem3  25445  minveclem3b  25758  minveclem4  25762  pmltpclem2  25779  ovolgelb  25810  ovolicc2lem2  25848  ovolicc2lem4  25850  mbfposr  25982  itg2const2  26071  itg2cnlem2  26092  itg2cn  26093  plyco0  26519  coeeulem  26552  dgradd2  26596  cxplt2  27035  fsumharmonic  27348  dmlogdmgm  27360  lgamgulmlem1  27365  lgamucov  27374  ftalem3  27411  ftalem5  27413  ftalem7  27415  ppiprm  27487  chtprm  27489  chpub  27556  perfectlem2  27566  bposlem1  27620  lgsdilem2  27669  lgsqrlem2  27683  lgsquadlem2  27717  2sqblem  27767  2sqmod  27772  2sqnn0  27774  pntpbnd1  27922  pntlem3  27945  infdesc  27976  nbusgrvtxm1  29969  crctcshwlkn0lem3  30410  frgrreggt1  31003  minvecolem4  31491  minvecolem5  31492  nndiffz1  33428  psgnfzto1stlem  33711  exsslsb  34279  lmdvg  34635  eulerpartlems  35042  ballotlemfc0  35175  ballotlemfcc  35176  ballotlemrv2  35204  signsply0  35230  reprinfz1  35301  lpadmax  35364  lpadright  35366  erdszelem8  36081  bccolsum  36628  unbdqndv2lem1  37499  unbdqndv2lem2  37500  poimirlem2  38677  poimirlem3  38678  poimirlem6  38681  poimirlem7  38682  poimirlem8  38683  poimirlem16  38691  poimirlem17  38692  poimirlem19  38694  poimirlem20  38695  poimirlem21  38696  poimirlem22  38697  poimirlem23  38698  poimirlem26  38701  poimirlem31  38706  poimir  38708  mblfinlem2  38713  itg2addnclem  38726  itg2addnclem2  38727  itg2addnclem3  38728  iblabsnclem  38738  ftc1anclem5  38752  areacirclem4  38766  areacirclem5  38767  areacirc  38768  cntotbnd  38867  aks4d1p5  43267  aks4d1p8d2  43272  aks4d1p8  43274  aks4d1p9  43275  posbezout  43287  primrootlekpowne0  43292  hashnexinj  43315  sticksstones1  43333  sticksstones22  43355  unitscyglem2  43383  unitscyglem4  43385  elpell1qr2  44016  pellfundglb  44029  pellfund14gap  44031  congabseq  44118  jm2.19  44137  jm2.26lem3  44145  dgraa0p  44288  dvgrat  45433  uzwo4  46206  divlt0gt0d  46438  supxrgere  46481  uzublem  46576  nleltd  46598  supminfxr  46610  xrpnf  46631  sqrlearg  46701  lptre2pt  46786  limsupubuzlem  46858  climxrrelem  46895  climxlim2lem  46991  icccncfext  47033  ioodvbdlimc1lem2  47078  ioodvbdlimc2lem  47080  volioore  47136  voliooico  47138  voliccico  47145  stoweidlem26  47172  stoweidlem34  47180  stoweidlem59  47205  stirlinglem5  47224  dirkercncflem1  47249  fourierdlem10  47263  fourierdlem19  47272  fourierdlem25  47278  fourierdlem35  47288  fourierdlem40  47293  fourierdlem42  47295  fourierdlem64  47316  fourierdlem65  47317  fourierdlem74  47326  fourierdlem75  47327  fourierdlem78  47330  fourierdlem79  47331  fourierdlem104  47356  fourierswlem  47376  fouriersw  47377  elaa2lem  47379  etransclem32  47412  etransclem41  47421  hsphoidmvle2  47731  hoidmv1lelem1  47737  hoidmv1lelem2  47738  hoidmv1lelem3  47739  hoidmvlelem2  47742  hoidmvlelem4  47744  hoidmvlelem5  47745  hoiqssbllem3  47770  hspmbllem1  47772  hspmbllem2  47773  vonicc  47831  pimdecfgtioo  47863  pimincfltioo  47864  et-sqrtnegnre  48019  fmtno4prmfac  48793  requad01  48855  requad1  48856  perfectALTVlem2  48956  itsclc0yqsol  50012  aacllem  51150