Theorem ltnled 11457

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2145   class class class wbr 5103  ℝcr 11199   < clt 11343   ≤ cle 11344

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11347  df-le 11349

This theorem is used by:  ltsub1  11812  ltsub2  11813  0mnnnnn0  12638  0nn0m1nnn0  12753  mul2lt0bi  13228  fzp1nel  13745  fzodisj  13828  elfznelfzob  13909  ccatsymb  14728  swrdnd  14804  cshwcsh2id  14979  01sqrexlem7  15415  sqrtlt  15428  lo1bdd2  15691  isercoll  15835  fprodntriv  16109  fzm1ndvds  16492  fzo0dvdseq  16493  bitsfzolem  16604  bitsfzo  16605  sadcaddlem  16627  smuval2  16652  bezoutlem3  16714  2mulprm  16868  isprm5  16883  odzdvds  16973  prm23ge5  16993  pc2dvds  17057  pockthg  17084  prmreclem1  17094  prmreclem5  17098  1arith  17105  4sqlem11  17133  vdwlem6  17164  vdwlem11  17169  ramlb  17197  oddvds  19761  gexdvds  19798  sylow1lem3  19814  zringlpirlem3  21770  psdmul  22487  coe1tmmul2  22595  iccntr  25141  icccmplem2  25143  reconnlem2  25147  evth  25280  lebnumlem3  25284  nmoleub2lem3  25436  minveclem3b  25749  minveclem4  25753  pmltpclem2  25770  ovolgelb  25801  ovolicc2lem2  25839  ovolicc2lem4  25841  mbfposr  25973  itg2const2  26062  itg2cnlem2  26083  itg2cn  26084  plyco0  26510  coeeulem  26543  dgradd2  26587  cxplt2  27026  fsumharmonic  27339  dmlogdmgm  27351  lgamgulmlem1  27356  lgamucov  27365  ftalem3  27402  ftalem5  27404  ftalem7  27406  ppiprm  27478  chtprm  27480  chpub  27547  perfectlem2  27557  bposlem1  27611  lgsdilem2  27660  lgsqrlem2  27674  lgsquadlem2  27708  2sqblem  27758  2sqmod  27763  2sqnn0  27765  pntpbnd1  27913  pntlem3  27936  infdesc  27967  nbusgrvtxm1  29960  crctcshwlkn0lem3  30401  frgrreggt1  30994  minvecolem4  31482  minvecolem5  31483  nndiffz1  33378  psgnfzto1stlem  33661  exsslsb  34229  lmdvg  34585  eulerpartlems  34992  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemrv2  35154  signsply0  35180  reprinfz1  35251  lpadmax  35314  lpadright  35316  erdszelem8  35963  bccolsum  36504  unbdqndv2lem1  37375  unbdqndv2lem2  37376  poimirlem2  38540  poimirlem3  38541  poimirlem6  38544  poimirlem7  38545  poimirlem8  38546  poimirlem16  38554  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem21  38559  poimirlem22  38560  poimirlem23  38561  poimirlem26  38564  poimirlem31  38569  poimir  38571  mblfinlem2  38576  itg2addnclem  38589  itg2addnclem2  38590  itg2addnclem3  38591  iblabsnclem  38601  ftc1anclem5  38615  areacirclem4  38629  areacirclem5  38630  areacirc  38631  cntotbnd  38730  aks4d1p5  43130  aks4d1p8d2  43135  aks4d1p8  43137  aks4d1p9  43138  posbezout  43150  primrootlekpowne0  43155  hashnexinj  43178  sticksstones1  43196  sticksstones22  43218  unitscyglem2  43246  unitscyglem4  43248  elpell1qr2  43878  pellfundglb  43891  pellfund14gap  43893  congabseq  43980  jm2.19  43999  jm2.26lem3  44007  dgraa0p  44150  dvgrat  45295  uzwo4  46069  divlt0gt0d  46301  supxrgere  46344  uzublem  46439  nleltd  46461  supminfxr  46473  xrpnf  46494  sqrlearg  46564  lptre2pt  46649  limsupubuzlem  46721  climxrrelem  46758  climxlim2lem  46854  icccncfext  46896  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  volioore  46999  voliooico  47001  voliccico  47008  stoweidlem26  47035  stoweidlem34  47043  stoweidlem59  47068  stirlinglem5  47087  dirkercncflem1  47112  fourierdlem10  47126  fourierdlem19  47135  fourierdlem25  47141  fourierdlem35  47151  fourierdlem40  47156  fourierdlem42  47158  fourierdlem64  47179  fourierdlem65  47180  fourierdlem74  47189  fourierdlem75  47190  fourierdlem78  47193  fourierdlem79  47194  fourierdlem104  47219  fourierswlem  47239  fouriersw  47240  elaa2lem  47242  etransclem32  47275  etransclem41  47284  hsphoidmvle2  47594  hoidmv1lelem1  47600  hoidmv1lelem2  47601  hoidmv1lelem3  47602  hoidmvlelem2  47605  hoidmvlelem4  47607  hoidmvlelem5  47608  hoiqssbllem3  47633  hspmbllem1  47635  hspmbllem2  47636  vonicc  47694  pimdecfgtioo  47726  pimincfltioo  47727  et-sqrtnegnre  47882  fmtno4prmfac  48656  requad01  48718  requad1  48719  perfectALTVlem2  48819  itsclc0yqsol  49875  aacllem  50938