Theorem ltnled 11223

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2105   class class class wbr 5092  ℝcr 10971   < clt 11110   ≤ cle 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-br 5093  df-opab 5155  df-xp 5626  df-cnv 5628  df-xr 11114  df-le 11116

This theorem is referenced by:  ltsub1  11572  ltsub2  11573  0mnnnnn0  12366  mul2lt0bi  12937  fzp1nel  13441  fzodisj  13522  elfznelfzob  13594  ccatsymb  14386  swrdnd  14465  cshwcsh2id  14640  sqrlem7  15059  sqrtlt  15072  lo1bdd2  15332  isercoll  15478  fprodntriv  15751  fzm1ndvds  16130  fzo0dvdseq  16131  bitsfzolem  16240  bitsfzo  16241  sadcaddlem  16263  smuval2  16288  bezoutlem3  16348  2mulprm  16495  isprm5  16509  odzdvds  16593  prm23ge5  16613  pc2dvds  16677  pockthg  16704  prmreclem1  16714  prmreclem5  16718  1arith  16725  4sqlem11  16753  vdwlem6  16784  vdwlem11  16789  ramlb  16817  oddvds  19251  gexdvds  19285  sylow1lem3  19301  zringlpirlem3  20792  coe1tmmul2  21553  iccntr  24090  icccmplem2  24092  reconnlem2  24096  evth  24228  lebnumlem3  24232  nmoleub2lem3  24384  minveclem3b  24698  minveclem4  24702  pmltpclem2  24719  ovolgelb  24750  ovolicc2lem2  24788  ovolicc2lem4  24790  mbfposr  24922  itg2const2  25012  itg2cnlem2  25033  itg2cn  25034  plyco0  25459  coeeulem  25491  dgradd2  25535  cxplt2  25959  fsumharmonic  26267  dmlogdmgm  26279  lgamgulmlem1  26284  lgamucov  26293  ftalem3  26330  ftalem5  26332  ftalem7  26334  ppiprm  26406  chtprm  26408  chpub  26474  perfectlem2  26484  bposlem1  26538  lgsdilem2  26587  lgsqrlem2  26601  lgsquadlem2  26635  2sqblem  26685  2sqmod  26690  2sqnn0  26692  pntpbnd1  26840  pntlem3  26863  nbusgrvtxm1  28035  crctcshwlkn0lem3  28465  frgrreggt1  29045  minvecolem4  29530  minvecolem5  29531  nndiffz1  31394  psgnfzto1stlem  31654  lmdvg  32201  eulerpartlems  32627  ballotlemfc0  32759  ballotlemfcc  32760  ballotlemrv2  32788  signsply0  32830  reprinfz1  32902  lpadmax  32962  lpadright  32964  0nn0m1nnn0  33370  erdszelem8  33459  bccolsum  33995  unbdqndv2lem1  34785  unbdqndv2lem2  34786  poimirlem2  35884  poimirlem3  35885  poimirlem6  35888  poimirlem7  35889  poimirlem8  35890  poimirlem16  35898  poimirlem17  35899  poimirlem19  35901  poimirlem20  35902  poimirlem21  35903  poimirlem22  35904  poimirlem23  35905  poimirlem26  35908  poimirlem31  35913  poimir  35915  mblfinlem2  35920  itg2addnclem  35933  itg2addnclem2  35934  itg2addnclem3  35935  iblabsnclem  35945  ftc1anclem5  35959  areacirclem4  35973  areacirclem5  35974  areacirc  35975  cntotbnd  36059  aks4d1p5  40342  aks4d1p8d2  40347  aks4d1p8  40349  aks4d1p9  40350  sticksstones1  40359  sticksstones22  40381  metakunt29  40410  metakunt30  40411  infdesc  40742  elpell1qr2  40956  pellfundglb  40969  pellfund14gap  40971  congabseq  41059  jm2.19  41078  jm2.26lem3  41086  dgraa0p  41237  dvgrat  42251  uzwo4  42921  divlt0gt0d  43160  supxrgere  43207  uzublem  43305  nleltd  43327  supminfxr  43339  xrpnf  43361  sqrlearg  43427  lptre2pt  43517  limsupubuzlem  43589  climxrrelem  43626  climxlim2lem  43722  icccncfext  43764  ioodvbdlimc1lem2  43809  ioodvbdlimc2lem  43811  volioore  43867  voliooico  43869  voliccico  43876  stoweidlem26  43903  stoweidlem34  43911  stoweidlem59  43936  stirlinglem5  43955  dirkercncflem1  43980  fourierdlem10  43994  fourierdlem19  44003  fourierdlem25  44009  fourierdlem35  44019  fourierdlem40  44024  fourierdlem42  44026  fourierdlem64  44047  fourierdlem65  44048  fourierdlem74  44057  fourierdlem75  44058  fourierdlem78  44061  fourierdlem79  44062  fourierdlem104  44087  fourierswlem  44107  fouriersw  44108  elaa2lem  44110  etransclem32  44143  etransclem41  44152  hsphoidmvle2  44460  hoidmv1lelem1  44466  hoidmv1lelem2  44467  hoidmv1lelem3  44468  hoidmvlelem2  44471  hoidmvlelem4  44473  hoidmvlelem5  44474  hoiqssbllem3  44499  hspmbllem1  44501  hspmbllem2  44502  vonicc  44560  pimdecfgtioo  44592  pimincfltioo  44593  fmtno4prmfac  45375  requad01  45424  requad1  45425  perfectALTVlem2  45525  itsclc0yqsol  46461  aacllem  46856