Theorem ltnled 11356

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 11288	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))
4	1, 2, 3	syl2anc 595	1 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2149   class class class wbr 5113  ℝcr 11098   < clt 11242   ≤ cle 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-xp 5668  df-cnv 5670  df-xr 11246  df-le 11248

This theorem is referenced by:  ltsub1  11709  ltsub2  11710  0mnnnnn0  12535  mul2lt0bi  13123  fzp1nel  13638  fzodisj  13721  elfznelfzob  13802  ccatsymb  14619  swrdnd  14691  cshwcsh2id  14864  01sqrexlem7  15298  sqrtlt  15311  lo1bdd2  15574  isercoll  15718  fprodntriv  15995  fzm1ndvds  16379  fzo0dvdseq  16380  bitsfzolem  16491  bitsfzo  16492  sadcaddlem  16514  smuval2  16539  bezoutlem3  16598  2mulprm  16750  isprm5  16765  odzdvds  16854  prm23ge5  16874  pc2dvds  16938  pockthg  16965  prmreclem1  16975  prmreclem5  16979  1arith  16986  4sqlem11  17014  vdwlem6  17045  vdwlem11  17050  ramlb  17078  oddvds  19616  gexdvds  19653  sylow1lem3  19669  zringlpirlem3  21582  psdmul  22297  coe1tmmul2  22405  iccntr  24947  icccmplem2  24949  reconnlem2  24953  evth  25086  lebnumlem3  25090  nmoleub2lem3  25242  minveclem3b  25555  minveclem4  25559  pmltpclem2  25576  ovolgelb  25607  ovolicc2lem2  25645  ovolicc2lem4  25647  mbfposr  25779  itg2const2  25868  itg2cnlem2  25889  itg2cn  25890  plyco0  26317  coeeulem  26349  dgradd2  26393  cxplt2  26828  fsumharmonic  27141  dmlogdmgm  27153  lgamgulmlem1  27158  lgamucov  27167  ftalem3  27204  ftalem5  27206  ftalem7  27208  ppiprm  27280  chtprm  27282  chpub  27349  perfectlem2  27359  bposlem1  27413  lgsdilem2  27462  lgsqrlem2  27476  lgsquadlem2  27510  2sqblem  27560  2sqmod  27565  2sqnn0  27567  pntpbnd1  27715  pntlem3  27738  nbusgrvtxm1  29669  crctcshwlkn0lem3  30101  frgrreggt1  30684  minvecolem4  31172  minvecolem5  31173  nndiffz1  33071  psgnfzto1stlem  33360  exsslsb  33931  lmdvg  34287  eulerpartlems  34694  ballotlemfc0  34827  ballotlemfcc  34828  ballotlemrv2  34856  signsply0  34882  reprinfz1  34953  lpadmax  35016  lpadright  35018  0nn0m1nnn0  35502  erdszelem8  35588  bccolsum  36129  unbdqndv2lem1  36986  unbdqndv2lem2  36987  poimirlem2  38160  poimirlem3  38161  poimirlem6  38164  poimirlem7  38165  poimirlem8  38166  poimirlem16  38174  poimirlem17  38175  poimirlem19  38177  poimirlem20  38178  poimirlem21  38179  poimirlem22  38180  poimirlem23  38181  poimirlem26  38184  poimirlem31  38189  poimir  38191  mblfinlem2  38196  itg2addnclem  38209  itg2addnclem2  38210  itg2addnclem3  38211  iblabsnclem  38221  ftc1anclem5  38235  areacirclem4  38249  areacirclem5  38250  areacirc  38251  cntotbnd  38334  aks4d1p5  42736  aks4d1p8d2  42741  aks4d1p8  42743  aks4d1p9  42744  posbezout  42756  primrootlekpowne0  42761  hashnexinj  42784  sticksstones1  42802  sticksstones22  42824  unitscyglem2  42852  unitscyglem4  42854  infdesc  43266  elpell1qr2  43490  pellfundglb  43503  pellfund14gap  43505  congabseq  43592  jm2.19  43611  jm2.26lem3  43619  dgraa0p  43767  dvgrat  44913  uzwo4  45664  divlt0gt0d  45896  supxrgere  45940  uzublem  46035  nleltd  46057  supminfxr  46069  xrpnf  46090  sqrlearg  46160  lptre2pt  46245  limsupubuzlem  46317  climxrrelem  46354  climxlim2lem  46450  icccncfext  46492  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  volioore  46595  voliooico  46597  voliccico  46604  stoweidlem26  46631  stoweidlem34  46639  stoweidlem59  46664  stirlinglem5  46683  dirkercncflem1  46708  fourierdlem10  46722  fourierdlem19  46731  fourierdlem25  46737  fourierdlem35  46747  fourierdlem40  46752  fourierdlem42  46754  fourierdlem64  46775  fourierdlem65  46776  fourierdlem74  46785  fourierdlem75  46786  fourierdlem78  46789  fourierdlem79  46790  fourierdlem104  46815  fourierswlem  46835  fouriersw  46836  elaa2lem  46838  etransclem32  46871  etransclem41  46880  hsphoidmvle2  47190  hoidmv1lelem1  47196  hoidmv1lelem2  47197  hoidmv1lelem3  47198  hoidmvlelem2  47201  hoidmvlelem4  47203  hoidmvlelem5  47204  hoiqssbllem3  47229  hspmbllem1  47231  hspmbllem2  47232  vonicc  47290  pimdecfgtioo  47322  pimincfltioo  47323  et-sqrtnegnre  47478  fmtno4prmfac  48212  requad01  48274  requad1  48275  perfectALTVlem2  48375  itsclc0yqsol  49428  aacllem  50474