Theorem ltnled 11280

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-xr 11170  df-le 11172

This theorem is referenced by:  ltsub1  11633  ltsub2  11634  0mnnnnn0  12433  mul2lt0bi  13013  fzp1nel  13527  fzodisj  13609  elfznelfzob  13690  ccatsymb  14506  swrdnd  14578  cshwcsh2id  14751  01sqrexlem7  15171  sqrtlt  15184  lo1bdd2  15447  isercoll  15591  fprodntriv  15865  fzm1ndvds  16249  fzo0dvdseq  16250  bitsfzolem  16361  bitsfzo  16362  sadcaddlem  16384  smuval2  16409  bezoutlem3  16468  2mulprm  16620  isprm5  16634  odzdvds  16723  prm23ge5  16743  pc2dvds  16807  pockthg  16834  prmreclem1  16844  prmreclem5  16848  1arith  16855  4sqlem11  16883  vdwlem6  16914  vdwlem11  16919  ramlb  16947  oddvds  19476  gexdvds  19513  sylow1lem3  19529  zringlpirlem3  21419  psdmul  22109  coe1tmmul2  22218  iccntr  24766  icccmplem2  24768  reconnlem2  24772  evth  24914  lebnumlem3  24918  nmoleub2lem3  25071  minveclem3b  25384  minveclem4  25388  pmltpclem2  25406  ovolgelb  25437  ovolicc2lem2  25475  ovolicc2lem4  25477  mbfposr  25609  itg2const2  25698  itg2cnlem2  25719  itg2cn  25720  plyco0  26153  coeeulem  26185  dgradd2  26230  cxplt2  26663  fsumharmonic  26978  dmlogdmgm  26990  lgamgulmlem1  26995  lgamucov  27004  ftalem3  27041  ftalem5  27043  ftalem7  27045  ppiprm  27117  chtprm  27119  chpub  27187  perfectlem2  27197  bposlem1  27251  lgsdilem2  27300  lgsqrlem2  27314  lgsquadlem2  27348  2sqblem  27398  2sqmod  27403  2sqnn0  27405  pntpbnd1  27553  pntlem3  27576  nbusgrvtxm1  29452  crctcshwlkn0lem3  29885  frgrreggt1  30468  minvecolem4  30955  minvecolem5  30956  nndiffz1  32866  psgnfzto1stlem  33182  exsslsb  33753  lmdvg  34110  eulerpartlems  34517  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemrv2  34679  signsply0  34708  reprinfz1  34779  lpadmax  34839  lpadright  34841  0nn0m1nnn0  35307  erdszelem8  35392  bccolsum  35933  unbdqndv2lem1  36709  unbdqndv2lem2  36710  poimirlem2  37823  poimirlem3  37824  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem26  37847  poimirlem31  37852  poimir  37854  mblfinlem2  37859  itg2addnclem  37872  itg2addnclem2  37873  itg2addnclem3  37874  iblabsnclem  37884  ftc1anclem5  37898  areacirclem4  37912  areacirclem5  37913  areacirc  37914  cntotbnd  37997  aks4d1p5  42334  aks4d1p8d2  42339  aks4d1p8  42341  aks4d1p9  42342  posbezout  42354  primrootlekpowne0  42359  hashnexinj  42382  sticksstones1  42400  sticksstones22  42422  unitscyglem2  42450  unitscyglem4  42452  infdesc  42886  elpell1qr2  43114  pellfundglb  43127  pellfund14gap  43129  congabseq  43216  jm2.19  43235  jm2.26lem3  43243  dgraa0p  43391  dvgrat  44553  uzwo4  45298  divlt0gt0d  45534  supxrgere  45578  uzublem  45674  nleltd  45696  supminfxr  45708  xrpnf  45729  sqrlearg  45799  lptre2pt  45884  limsupubuzlem  45956  climxrrelem  45993  climxlim2lem  46089  icccncfext  46131  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  volioore  46234  voliooico  46236  voliccico  46243  stoweidlem26  46270  stoweidlem34  46278  stoweidlem59  46303  stirlinglem5  46322  dirkercncflem1  46347  fourierdlem10  46361  fourierdlem19  46370  fourierdlem25  46376  fourierdlem35  46386  fourierdlem40  46391  fourierdlem42  46393  fourierdlem64  46414  fourierdlem65  46415  fourierdlem74  46424  fourierdlem75  46425  fourierdlem78  46428  fourierdlem79  46429  fourierdlem104  46454  fourierswlem  46474  fouriersw  46475  elaa2lem  46477  etransclem32  46510  etransclem41  46519  hsphoidmvle2  46829  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmv1lelem3  46837  hoidmvlelem2  46840  hoidmvlelem4  46842  hoidmvlelem5  46843  hoiqssbllem3  46868  hspmbllem1  46870  hspmbllem2  46871  vonicc  46929  pimdecfgtioo  46961  pimincfltioo  46962  et-sqrtnegnre  47117  fmtno4prmfac  47818  requad01  47867  requad1  47868  perfectALTVlem2  47968  itsclc0yqsol  49010  aacllem  50046