Theorem ltnled 11321

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   < clt 11208   ≤ cle 11209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-xr 11212  df-le 11214

This theorem is referenced by:  ltsub1  11674  ltsub2  11675  0mnnnnn0  12474  mul2lt0bi  13059  fzp1nel  13572  fzodisj  13654  elfznelfzob  13734  ccatsymb  14547  swrdnd  14619  cshwcsh2id  14794  01sqrexlem7  15214  sqrtlt  15227  lo1bdd2  15490  isercoll  15634  fprodntriv  15908  fzm1ndvds  16292  fzo0dvdseq  16293  bitsfzolem  16404  bitsfzo  16405  sadcaddlem  16427  smuval2  16452  bezoutlem3  16511  2mulprm  16663  isprm5  16677  odzdvds  16766  prm23ge5  16786  pc2dvds  16850  pockthg  16877  prmreclem1  16887  prmreclem5  16891  1arith  16898  4sqlem11  16926  vdwlem6  16957  vdwlem11  16962  ramlb  16990  oddvds  19477  gexdvds  19514  sylow1lem3  19530  zringlpirlem3  21374  psdmul  22053  coe1tmmul2  22162  iccntr  24710  icccmplem2  24712  reconnlem2  24716  evth  24858  lebnumlem3  24862  nmoleub2lem3  25015  minveclem3b  25328  minveclem4  25332  pmltpclem2  25350  ovolgelb  25381  ovolicc2lem2  25419  ovolicc2lem4  25421  mbfposr  25553  itg2const2  25642  itg2cnlem2  25663  itg2cn  25664  plyco0  26097  coeeulem  26129  dgradd2  26174  cxplt2  26607  fsumharmonic  26922  dmlogdmgm  26934  lgamgulmlem1  26939  lgamucov  26948  ftalem3  26985  ftalem5  26987  ftalem7  26989  ppiprm  27061  chtprm  27063  chpub  27131  perfectlem2  27141  bposlem1  27195  lgsdilem2  27244  lgsqrlem2  27258  lgsquadlem2  27292  2sqblem  27342  2sqmod  27347  2sqnn0  27349  pntpbnd1  27497  pntlem3  27520  nbusgrvtxm1  29306  crctcshwlkn0lem3  29742  frgrreggt1  30322  minvecolem4  30809  minvecolem5  30810  nndiffz1  32709  psgnfzto1stlem  33057  exsslsb  33592  lmdvg  33943  eulerpartlems  34351  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemrv2  34513  signsply0  34542  reprinfz1  34613  lpadmax  34673  lpadright  34675  0nn0m1nnn0  35100  erdszelem8  35185  bccolsum  35726  unbdqndv2lem1  36497  unbdqndv2lem2  36498  poimirlem2  37616  poimirlem3  37617  poimirlem6  37620  poimirlem7  37621  poimirlem8  37622  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem26  37640  poimirlem31  37645  poimir  37647  mblfinlem2  37652  itg2addnclem  37665  itg2addnclem2  37666  itg2addnclem3  37667  iblabsnclem  37677  ftc1anclem5  37691  areacirclem4  37705  areacirclem5  37706  areacirc  37707  cntotbnd  37790  aks4d1p5  42068  aks4d1p8d2  42073  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootlekpowne0  42093  hashnexinj  42116  sticksstones1  42134  sticksstones22  42156  unitscyglem2  42184  unitscyglem4  42186  infdesc  42631  elpell1qr2  42860  pellfundglb  42873  pellfund14gap  42875  congabseq  42963  jm2.19  42982  jm2.26lem3  42990  dgraa0p  43138  dvgrat  44301  uzwo4  45047  divlt0gt0d  45284  supxrgere  45329  uzublem  45426  nleltd  45448  supminfxr  45460  xrpnf  45481  sqrlearg  45551  lptre2pt  45638  limsupubuzlem  45710  climxrrelem  45747  climxlim2lem  45843  icccncfext  45885  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  volioore  45988  voliooico  45990  voliccico  45997  stoweidlem26  46024  stoweidlem34  46032  stoweidlem59  46057  stirlinglem5  46076  dirkercncflem1  46101  fourierdlem10  46115  fourierdlem19  46124  fourierdlem25  46130  fourierdlem35  46140  fourierdlem40  46145  fourierdlem42  46147  fourierdlem64  46168  fourierdlem65  46169  fourierdlem74  46178  fourierdlem75  46179  fourierdlem78  46182  fourierdlem79  46183  fourierdlem104  46208  fourierswlem  46228  fouriersw  46229  elaa2lem  46231  etransclem32  46264  etransclem41  46273  hsphoidmvle2  46583  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem2  46594  hoidmvlelem4  46596  hoidmvlelem5  46597  hoiqssbllem3  46622  hspmbllem1  46624  hspmbllem2  46625  vonicc  46683  pimdecfgtioo  46715  pimincfltioo  46716  et-sqrtnegnre  46871  fmtno4prmfac  47573  requad01  47622  requad1  47623  perfectALTVlem2  47723  itsclc0yqsol  48753  aacllem  49790