Theorem ltnled 10583

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∈ wcel 2048   class class class wbr 4927  ℝcr 10330   < clt 10470   ≤ cle 10471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-sep 5058  ax-nul 5065  ax-pr 5184

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ral 3090  df-rex 3091  df-rab 3094  df-v 3414  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-nul 4178  df-if 4349  df-sn 4440  df-pr 4442  df-op 4446  df-br 4928  df-opab 4990  df-xp 5410  df-cnv 5412  df-xr 10474  df-le 10476

This theorem is referenced by:  ltsub1  10933  ltsub2  10934  0mnnnnn0  11738  mul2lt0bi  12309  fzp1nel  12804  fzodisj  12883  elfznelfzob  12955  swrdnd  13816  cshwcsh2id  14046  sqrlem7  14463  sqrtlt  14476  lo1bdd2  14736  isercoll  14879  fprodntriv  15150  fzm1ndvds  15526  fzo0dvdseq  15527  bitsfzolem  15637  bitsfzo  15638  sadcaddlem  15660  smuval2  15685  bezoutlem3  15739  2mulprm  15887  isprm5  15901  odzdvds  15982  prm23ge5  16002  pc2dvds  16065  pockthg  16092  prmreclem1  16102  prmreclem5  16106  1arith  16113  4sqlem11  16141  vdwlem6  16172  vdwlem11  16177  ramlb  16205  oddvds  18431  gexdvds  18464  sylow1lem3  18480  coe1tmmul2  20141  zringlpirlem3  20329  iccntr  23126  icccmplem2  23128  reconnlem2  23132  evth  23260  lebnumlem3  23264  nmoleub2lem3  23416  minveclem3b  23728  minveclem4  23732  pmltpclem2  23747  ovolgelb  23778  ovolicc2lem2  23816  ovolicc2lem4  23818  mbfposr  23950  itg2const2  24039  itg2cnlem2  24060  itg2cn  24061  plyco0  24479  coeeulem  24511  dgradd2  24555  cxplt2  24976  fsumharmonic  25285  dmlogdmgm  25297  lgamgulmlem1  25302  lgamucov  25311  ftalem3  25348  ftalem5  25350  ftalem7  25352  ppiprm  25424  chtprm  25426  chpub  25492  perfectlem2  25502  bposlem1  25556  lgsdilem2  25605  lgsqrlem2  25619  lgsquadlem2  25653  2sqblem  25703  2sqmod  25708  2sqnn0  25710  pntpbnd1  25858  pntlem3  25881  nbusgrvtxm1  26858  crctcshwlkn0lem3  27292  frgrreggt1  27944  minvecolem4  28429  minvecolem5  28430  nndiffz1  30255  psgnfzto1stlem  30682  lmdvg  30831  eulerpartlems  31254  ballotlemfc0  31387  ballotlemfcc  31388  ballotlemrv2  31416  signsply0  31458  reprinfz1  31532  lpadmax  31592  lpadright  31594  erdszelem8  32020  bccolsum  32461  unbdqndv2lem1  33338  unbdqndv2lem2  33339  poimirlem2  34313  poimirlem3  34314  poimirlem6  34317  poimirlem7  34318  poimirlem8  34319  poimirlem16  34327  poimirlem17  34328  poimirlem19  34330  poimirlem20  34331  poimirlem21  34332  poimirlem22  34333  poimirlem23  34334  poimirlem26  34337  poimirlem31  34342  poimir  34344  mblfinlem2  34349  itg2addnclem  34362  itg2addnclem2  34363  itg2addnclem3  34364  iblabsnclem  34374  ftc1anclem5  34390  areacirclem4  34404  areacirclem5  34405  areacirc  34406  cntotbnd  34494  elpell1qr2  38843  pellfundglb  38856  pellfund14gap  38858  congabseq  38945  jm2.19  38964  jm2.26lem3  38972  dgraa0p  39123  dvgrat  40037  uzwo4  40712  divlt0gt0d  40960  supxrgere  41009  uzublem  41114  nleltd  41138  supminfxr  41150  xrpnf  41172  sqrlearg  41239  lptre2pt  41331  limsupubuzlem  41403  climxrrelem  41440  climxlim2lem  41536  icccncfext  41579  ioodvbdlimc1lem2  41626  ioodvbdlimc2lem  41628  volioore  41685  voliooico  41687  voliccico  41694  stoweidlem26  41721  stoweidlem34  41729  stoweidlem59  41754  stirlinglem5  41773  dirkercncflem1  41798  fourierdlem10  41812  fourierdlem19  41821  fourierdlem25  41827  fourierdlem35  41837  fourierdlem40  41842  fourierdlem42  41844  fourierdlem64  41865  fourierdlem65  41866  fourierdlem74  41875  fourierdlem75  41876  fourierdlem78  41879  fourierdlem79  41880  fourierdlem104  41905  fourierswlem  41925  fouriersw  41926  elaa2lem  41928  etransclem32  41961  etransclem41  41970  hsphoidmvle2  42277  hoidmv1lelem1  42283  hoidmv1lelem2  42284  hoidmv1lelem3  42285  hoidmvlelem2  42288  hoidmvlelem4  42290  hoidmvlelem5  42291  hoiqssbllem3  42316  hspmbllem1  42318  hspmbllem2  42319  vonicc  42377  pimdecfgtioo  42405  pimincfltioo  42406  fmtno4prmfac  43076  requad01  43128  requad1  43129  perfectALTVlem2  43229  itsclc0yqsol  44093  aacllem  44243