Theorem ltnled 10787

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   < clt 10675   ≤ cle 10676

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-xr 10679  df-le 10681

This theorem is referenced by:  ltsub1  11136  ltsub2  11137  0mnnnnn0  11930  mul2lt0bi  12496  fzp1nel  12992  fzodisj  13072  elfznelfzob  13144  ccatsymb  13936  swrdnd  14016  cshwcsh2id  14190  sqrlem7  14608  sqrtlt  14621  lo1bdd2  14881  isercoll  15024  fprodntriv  15296  fzm1ndvds  15672  fzo0dvdseq  15673  bitsfzolem  15783  bitsfzo  15784  sadcaddlem  15806  smuval2  15831  bezoutlem3  15889  2mulprm  16037  isprm5  16051  odzdvds  16132  prm23ge5  16152  pc2dvds  16215  pockthg  16242  prmreclem1  16252  prmreclem5  16256  1arith  16263  4sqlem11  16291  vdwlem6  16322  vdwlem11  16327  ramlb  16355  oddvds  18675  gexdvds  18709  sylow1lem3  18725  coe1tmmul2  20444  zringlpirlem3  20633  iccntr  23429  icccmplem2  23431  reconnlem2  23435  evth  23563  lebnumlem3  23567  nmoleub2lem3  23719  minveclem3b  24031  minveclem4  24035  pmltpclem2  24050  ovolgelb  24081  ovolicc2lem2  24119  ovolicc2lem4  24121  mbfposr  24253  itg2const2  24342  itg2cnlem2  24363  itg2cn  24364  plyco0  24782  coeeulem  24814  dgradd2  24858  cxplt2  25281  fsumharmonic  25589  dmlogdmgm  25601  lgamgulmlem1  25606  lgamucov  25615  ftalem3  25652  ftalem5  25654  ftalem7  25656  ppiprm  25728  chtprm  25730  chpub  25796  perfectlem2  25806  bposlem1  25860  lgsdilem2  25909  lgsqrlem2  25923  lgsquadlem2  25957  2sqblem  26007  2sqmod  26012  2sqnn0  26014  pntpbnd1  26162  pntlem3  26185  nbusgrvtxm1  27161  crctcshwlkn0lem3  27590  frgrreggt1  28172  minvecolem4  28657  minvecolem5  28658  nndiffz1  30509  psgnfzto1stlem  30742  lmdvg  31196  eulerpartlems  31618  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemrv2  31779  signsply0  31821  reprinfz1  31893  lpadmax  31953  lpadright  31955  0nn0m1nnn0  32351  erdszelem8  32445  bccolsum  32971  unbdqndv2lem1  33848  unbdqndv2lem2  33849  poimirlem2  34909  poimirlem3  34910  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem26  34933  poimirlem31  34938  poimir  34940  mblfinlem2  34945  itg2addnclem  34958  itg2addnclem2  34959  itg2addnclem3  34960  iblabsnclem  34970  ftc1anclem5  34986  areacirclem4  35000  areacirclem5  35001  areacirc  35002  cntotbnd  35089  elpell1qr2  39518  pellfundglb  39531  pellfund14gap  39533  congabseq  39620  jm2.19  39639  jm2.26lem3  39647  dgraa0p  39798  dvgrat  40693  uzwo4  41364  divlt0gt0d  41601  supxrgere  41650  uzublem  41753  nleltd  41777  supminfxr  41789  xrpnf  41811  sqrlearg  41878  lptre2pt  41970  limsupubuzlem  42042  climxrrelem  42079  climxlim2lem  42175  icccncfext  42219  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  volioore  42324  voliooico  42326  voliccico  42333  stoweidlem26  42360  stoweidlem34  42368  stoweidlem59  42393  stirlinglem5  42412  dirkercncflem1  42437  fourierdlem10  42451  fourierdlem19  42460  fourierdlem25  42466  fourierdlem35  42476  fourierdlem40  42481  fourierdlem42  42483  fourierdlem64  42504  fourierdlem65  42505  fourierdlem74  42514  fourierdlem75  42515  fourierdlem78  42518  fourierdlem79  42519  fourierdlem104  42544  fourierswlem  42564  fouriersw  42565  elaa2lem  42567  etransclem32  42600  etransclem41  42609  hsphoidmvle2  42916  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem2  42927  hoidmvlelem4  42929  hoidmvlelem5  42930  hoiqssbllem3  42955  hspmbllem1  42957  hspmbllem2  42958  vonicc  43016  pimdecfgtioo  43044  pimincfltioo  43045  fmtno4prmfac  43783  requad01  43835  requad1  43836  perfectALTVlem2  43936  itsclc0yqsol  44800  aacllem  44951