Theorem ltnled 11437

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   < clt 11324   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-xp 5706  df-cnv 5708  df-xr 11328  df-le 11330

This theorem is referenced by:  ltsub1  11786  ltsub2  11787  0mnnnnn0  12585  mul2lt0bi  13163  fzp1nel  13668  fzodisj  13750  elfznelfzob  13823  ccatsymb  14630  swrdnd  14702  cshwcsh2id  14877  01sqrexlem7  15297  sqrtlt  15310  lo1bdd2  15570  isercoll  15716  fprodntriv  15990  fzm1ndvds  16370  fzo0dvdseq  16371  bitsfzolem  16480  bitsfzo  16481  sadcaddlem  16503  smuval2  16528  bezoutlem3  16588  2mulprm  16740  isprm5  16754  odzdvds  16842  prm23ge5  16862  pc2dvds  16926  pockthg  16953  prmreclem1  16963  prmreclem5  16967  1arith  16974  4sqlem11  17002  vdwlem6  17033  vdwlem11  17038  ramlb  17066  oddvds  19589  gexdvds  19626  sylow1lem3  19642  zringlpirlem3  21498  psdmul  22193  coe1tmmul2  22300  iccntr  24862  icccmplem2  24864  reconnlem2  24868  evth  25010  lebnumlem3  25014  nmoleub2lem3  25167  minveclem3b  25481  minveclem4  25485  pmltpclem2  25503  ovolgelb  25534  ovolicc2lem2  25572  ovolicc2lem4  25574  mbfposr  25706  itg2const2  25796  itg2cnlem2  25817  itg2cn  25818  plyco0  26251  coeeulem  26283  dgradd2  26328  cxplt2  26758  fsumharmonic  27073  dmlogdmgm  27085  lgamgulmlem1  27090  lgamucov  27099  ftalem3  27136  ftalem5  27138  ftalem7  27140  ppiprm  27212  chtprm  27214  chpub  27282  perfectlem2  27292  bposlem1  27346  lgsdilem2  27395  lgsqrlem2  27409  lgsquadlem2  27443  2sqblem  27493  2sqmod  27498  2sqnn0  27500  pntpbnd1  27648  pntlem3  27671  nbusgrvtxm1  29414  crctcshwlkn0lem3  29845  frgrreggt1  30425  minvecolem4  30912  minvecolem5  30913  nndiffz1  32791  psgnfzto1stlem  33093  lmdvg  33899  eulerpartlems  34325  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemrv2  34486  signsply0  34528  reprinfz1  34599  lpadmax  34659  lpadright  34661  0nn0m1nnn0  35080  erdszelem8  35166  bccolsum  35701  unbdqndv2lem1  36475  unbdqndv2lem2  36476  poimirlem2  37582  poimirlem3  37583  poimirlem6  37586  poimirlem7  37587  poimirlem8  37588  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem21  37601  poimirlem22  37602  poimirlem23  37603  poimirlem26  37606  poimirlem31  37611  poimir  37613  mblfinlem2  37618  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  iblabsnclem  37643  ftc1anclem5  37657  areacirclem4  37671  areacirclem5  37672  areacirc  37673  cntotbnd  37756  aks4d1p5  42037  aks4d1p8d2  42042  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootlekpowne0  42062  hashnexinj  42085  sticksstones1  42103  sticksstones22  42125  unitscyglem2  42153  unitscyglem4  42155  metakunt29  42190  metakunt30  42191  infdesc  42598  elpell1qr2  42828  pellfundglb  42841  pellfund14gap  42843  congabseq  42931  jm2.19  42950  jm2.26lem3  42958  dgraa0p  43106  dvgrat  44281  uzwo4  44955  divlt0gt0d  45201  supxrgere  45248  uzublem  45345  nleltd  45367  supminfxr  45379  xrpnf  45401  sqrlearg  45471  lptre2pt  45561  limsupubuzlem  45633  climxrrelem  45670  climxlim2lem  45766  icccncfext  45808  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  volioore  45911  voliooico  45913  voliccico  45920  stoweidlem26  45947  stoweidlem34  45955  stoweidlem59  45980  stirlinglem5  45999  dirkercncflem1  46024  fourierdlem10  46038  fourierdlem19  46047  fourierdlem25  46053  fourierdlem35  46063  fourierdlem40  46068  fourierdlem42  46070  fourierdlem64  46091  fourierdlem65  46092  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem79  46106  fourierdlem104  46131  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem32  46187  etransclem41  46196  hsphoidmvle2  46506  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem2  46517  hoidmvlelem4  46519  hoidmvlelem5  46520  hoiqssbllem3  46545  hspmbllem1  46547  hspmbllem2  46548  vonicc  46606  pimdecfgtioo  46638  pimincfltioo  46639  et-sqrtnegnre  46794  fmtno4prmfac  47446  requad01  47495  requad1  47496  perfectALTVlem2  47596  itsclc0yqsol  48498  aacllem  48895