Theorem ltnled 11293

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-xr 11183  df-le 11185

This theorem is referenced by:  ltsub1  11646  ltsub2  11647  0mnnnnn0  12469  mul2lt0bi  13050  fzp1nel  13565  fzodisj  13648  elfznelfzob  13729  ccatsymb  14545  swrdnd  14617  cshwcsh2id  14790  01sqrexlem7  15210  sqrtlt  15223  lo1bdd2  15486  isercoll  15630  fprodntriv  15907  fzm1ndvds  16291  fzo0dvdseq  16292  bitsfzolem  16403  bitsfzo  16404  sadcaddlem  16426  smuval2  16451  bezoutlem3  16510  2mulprm  16662  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  19522  gexdvds  19559  sylow1lem3  19575  zringlpirlem3  21444  psdmul  22132  coe1tmmul2  22241  iccntr  24787  icccmplem2  24789  reconnlem2  24793  evth  24926  lebnumlem3  24930  nmoleub2lem3  25082  minveclem3b  25395  minveclem4  25399  pmltpclem2  25416  ovolgelb  25447  ovolicc2lem2  25485  ovolicc2lem4  25487  mbfposr  25619  itg2const2  25708  itg2cnlem2  25729  itg2cn  25730  plyco0  26157  coeeulem  26189  dgradd2  26233  cxplt2  26662  fsumharmonic  26975  dmlogdmgm  26987  lgamgulmlem1  26992  lgamucov  27001  ftalem3  27038  ftalem5  27040  ftalem7  27042  ppiprm  27114  chtprm  27116  chpub  27183  perfectlem2  27193  bposlem1  27247  lgsdilem2  27296  lgsqrlem2  27310  lgsquadlem2  27344  2sqblem  27394  2sqmod  27399  2sqnn0  27401  pntpbnd1  27549  pntlem3  27572  nbusgrvtxm1  29448  crctcshwlkn0lem3  29880  frgrreggt1  30463  minvecolem4  30951  minvecolem5  30952  nndiffz1  32859  psgnfzto1stlem  33161  exsslsb  33741  lmdvg  34097  eulerpartlems  34504  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemrv2  34666  signsply0  34695  reprinfz1  34766  lpadmax  34826  lpadright  34828  0nn0m1nnn0  35295  erdszelem8  35380  bccolsum  35921  unbdqndv2lem1  36769  unbdqndv2lem2  36770  poimirlem2  37943  poimirlem3  37944  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem31  37972  poimir  37974  mblfinlem2  37979  itg2addnclem  37992  itg2addnclem2  37993  itg2addnclem3  37994  iblabsnclem  38004  ftc1anclem5  38018  areacirclem4  38032  areacirclem5  38033  areacirc  38034  cntotbnd  38117  aks4d1p5  42519  aks4d1p8d2  42524  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootlekpowne0  42544  hashnexinj  42567  sticksstones1  42585  sticksstones22  42607  unitscyglem2  42635  unitscyglem4  42637  infdesc  43076  elpell1qr2  43300  pellfundglb  43313  pellfund14gap  43315  congabseq  43402  jm2.19  43421  jm2.26lem3  43429  dgraa0p  43577  dvgrat  44739  uzwo4  45484  divlt0gt0d  45719  supxrgere  45763  uzublem  45858  nleltd  45880  supminfxr  45892  xrpnf  45913  sqrlearg  45983  lptre2pt  46068  limsupubuzlem  46140  climxrrelem  46177  climxlim2lem  46273  icccncfext  46315  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  volioore  46418  voliooico  46420  voliccico  46427  stoweidlem26  46454  stoweidlem34  46462  stoweidlem59  46487  stirlinglem5  46506  dirkercncflem1  46531  fourierdlem10  46545  fourierdlem19  46554  fourierdlem25  46560  fourierdlem35  46570  fourierdlem40  46575  fourierdlem42  46577  fourierdlem64  46598  fourierdlem65  46599  fourierdlem74  46608  fourierdlem75  46609  fourierdlem78  46612  fourierdlem79  46613  fourierdlem104  46638  fourierswlem  46658  fouriersw  46659  elaa2lem  46661  etransclem32  46694  etransclem41  46703  hsphoidmvle2  47013  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  hoidmvlelem2  47024  hoidmvlelem4  47026  hoidmvlelem5  47027  hoiqssbllem3  47052  hspmbllem1  47054  hspmbllem2  47055  vonicc  47113  pimdecfgtioo  47145  pimincfltioo  47146  et-sqrtnegnre  47301  fmtno4prmfac  48035  requad01  48097  requad1  48098  perfectALTVlem2  48198  itsclc0yqsol  49240  aacllem  50276