Theorem ltnled 11393

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2098   class class class wbr 5149  ℝcr 11139   < clt 11280   ≤ cle 11281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5150  df-opab 5212  df-xp 5684  df-cnv 5686  df-xr 11284  df-le 11286

This theorem is referenced by:  ltsub1  11742  ltsub2  11743  0mnnnnn0  12537  mul2lt0bi  13115  fzp1nel  13620  fzodisj  13701  elfznelfzob  13774  ccatsymb  14568  swrdnd  14640  cshwcsh2id  14815  01sqrexlem7  15231  sqrtlt  15244  lo1bdd2  15504  isercoll  15650  fprodntriv  15922  fzm1ndvds  16302  fzo0dvdseq  16303  bitsfzolem  16412  bitsfzo  16413  sadcaddlem  16435  smuval2  16460  bezoutlem3  16520  2mulprm  16667  isprm5  16681  odzdvds  16767  prm23ge5  16787  pc2dvds  16851  pockthg  16878  prmreclem1  16888  prmreclem5  16892  1arith  16899  4sqlem11  16927  vdwlem6  16958  vdwlem11  16963  ramlb  16991  oddvds  19514  gexdvds  19551  sylow1lem3  19567  zringlpirlem3  21407  psdmul  22113  coe1tmmul2  22220  iccntr  24781  icccmplem2  24783  reconnlem2  24787  evth  24929  lebnumlem3  24933  nmoleub2lem3  25086  minveclem3b  25400  minveclem4  25404  pmltpclem2  25422  ovolgelb  25453  ovolicc2lem2  25491  ovolicc2lem4  25493  mbfposr  25625  itg2const2  25715  itg2cnlem2  25736  itg2cn  25737  plyco0  26171  coeeulem  26203  dgradd2  26248  cxplt2  26677  fsumharmonic  26989  dmlogdmgm  27001  lgamgulmlem1  27006  lgamucov  27015  ftalem3  27052  ftalem5  27054  ftalem7  27056  ppiprm  27128  chtprm  27130  chpub  27198  perfectlem2  27208  bposlem1  27262  lgsdilem2  27311  lgsqrlem2  27325  lgsquadlem2  27359  2sqblem  27409  2sqmod  27414  2sqnn0  27416  pntpbnd1  27564  pntlem3  27587  nbusgrvtxm1  29264  crctcshwlkn0lem3  29695  frgrreggt1  30275  minvecolem4  30762  minvecolem5  30763  nndiffz1  32636  psgnfzto1stlem  32913  lmdvg  33682  eulerpartlems  34108  ballotlemfc0  34240  ballotlemfcc  34241  ballotlemrv2  34269  signsply0  34311  reprinfz1  34382  lpadmax  34442  lpadright  34444  0nn0m1nnn0  34850  erdszelem8  34936  bccolsum  35461  unbdqndv2lem1  36112  unbdqndv2lem2  36113  poimirlem2  37223  poimirlem3  37224  poimirlem6  37227  poimirlem7  37228  poimirlem8  37229  poimirlem16  37237  poimirlem17  37238  poimirlem19  37240  poimirlem20  37241  poimirlem21  37242  poimirlem22  37243  poimirlem23  37244  poimirlem26  37247  poimirlem31  37252  poimir  37254  mblfinlem2  37259  itg2addnclem  37272  itg2addnclem2  37273  itg2addnclem3  37274  iblabsnclem  37284  ftc1anclem5  37298  areacirclem4  37312  areacirclem5  37313  areacirc  37314  cntotbnd  37397  aks4d1p5  41680  aks4d1p8d2  41685  aks4d1p8  41687  aks4d1p9  41688  posbezout  41700  primrootlekpowne0  41705  hashnexinj  41728  sticksstones1  41746  sticksstones22  41768  metakunt29  41816  metakunt30  41817  infdesc  42199  elpell1qr2  42431  pellfundglb  42444  pellfund14gap  42446  congabseq  42534  jm2.19  42553  jm2.26lem3  42561  dgraa0p  42712  dvgrat  43888  uzwo4  44556  divlt0gt0d  44803  supxrgere  44850  uzublem  44947  nleltd  44969  supminfxr  44981  xrpnf  45003  sqrlearg  45073  lptre2pt  45163  limsupubuzlem  45235  climxrrelem  45272  climxlim2lem  45368  icccncfext  45410  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  volioore  45513  voliooico  45515  voliccico  45522  stoweidlem26  45549  stoweidlem34  45557  stoweidlem59  45582  stirlinglem5  45601  dirkercncflem1  45626  fourierdlem10  45640  fourierdlem19  45649  fourierdlem25  45655  fourierdlem35  45665  fourierdlem40  45670  fourierdlem42  45672  fourierdlem64  45693  fourierdlem65  45694  fourierdlem74  45703  fourierdlem75  45704  fourierdlem78  45707  fourierdlem79  45708  fourierdlem104  45733  fourierswlem  45753  fouriersw  45754  elaa2lem  45756  etransclem32  45789  etransclem41  45798  hsphoidmvle2  46108  hoidmv1lelem1  46114  hoidmv1lelem2  46115  hoidmv1lelem3  46116  hoidmvlelem2  46119  hoidmvlelem4  46121  hoidmvlelem5  46122  hoiqssbllem3  46147  hspmbllem1  46149  hspmbllem2  46150  vonicc  46208  pimdecfgtioo  46240  pimincfltioo  46241  et-sqrtnegnre  46396  fmtno4prmfac  47046  requad01  47095  requad1  47096  perfectALTVlem2  47196  itsclc0yqsol  48020  aacllem  48417