Theorem ltnled 10063

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-xp 5044  df-cnv 5046  df-xr 9957  df-le 9959

This theorem is referenced by:  ltsub1  10403  ltsub2  10404  0mnnnnn0  11202  mul2lt0bi  11812  fzp1nel  12293  fzodisj  12371  elfznelfzob  12440  swrdnd  13284  cshwcsh2id  13425  sqrlem7  13837  sqrtlt  13850  lo1bdd2  14103  isercoll  14246  fprodntriv  14511  fzm1ndvds  14882  fzo0dvdseq  14883  bitsfzolem  14994  bitsfzo  14995  sadcaddlem  15017  smuval2  15042  bezoutlem3  15096  isprm5  15257  odzdvds  15338  prm23ge5  15358  pc2dvds  15421  pockthg  15448  prmreclem1  15458  prmreclem5  15462  1arith  15469  4sqlem11  15497  vdwlem6  15528  vdwlem11  15533  ramlb  15561  oddvds  17789  gexdvds  17822  sylow1lem3  17838  coe1tmmul2  19467  zringlpirlem3  19653  iccntr  22432  icccmplem2  22434  reconnlem2  22438  evth  22566  lebnumlem3  22570  nmoleub2lem3  22723  minveclem3b  23007  minveclem4  23011  pmltpclem2  23025  ovolgelb  23055  ovolicc2lem2  23093  ovolicc2lem4  23095  mbfposr  23225  itg2const2  23314  itg2cnlem2  23335  itg2cn  23336  plyco0  23752  coeeulem  23784  dgradd2  23828  pilem3  24011  cxplt2  24244  fsumharmonic  24538  dmlogdmgm  24550  lgamgulmlem1  24555  lgamucov  24564  ftalem3  24601  ftalem5  24603  ftalem7  24605  ppiprm  24677  chtprm  24679  chpub  24745  perfectlem2  24755  bposlem1  24809  lgsdilem2  24858  lgsqrlem2  24872  lgsquadlem2  24906  2sqblem  24956  pntpbnd1  25075  pntlem3  25098  clwwlkgt0  26299  eupath2lem3  26506  frgrareggt1  26643  minvecolem4  27120  minvecolem5  27121  nndiffz1  28936  2sqmod  28979  psgnfzto1stlem  29181  lmdvg  29327  eulerpartlems  29749  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemrv2  29910  signsply0  29954  erdszelem8  30434  bccolsum  30878  unbdqndv2lem1  31670  unbdqndv2lem2  31671  poimirlem2  32581  poimirlem3  32582  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem26  32605  poimirlem31  32610  poimir  32612  mblfinlem2  32617  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  iblabsnclem  32643  ftc1anclem5  32659  areacirclem4  32673  areacirclem5  32674  areacirc  32675  cntotbnd  32765  elpell1qr2  36454  pellfundglb  36467  pellfund14gap  36469  congabseq  36559  jm2.19  36578  jm2.26lem3  36586  dgraa0p  36738  dvgrat  37533  uzwo4  38246  divlt0gt0d  38439  supxrgere  38490  sqrlearg  38627  lptre2pt  38707  icccncfext  38773  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  volioore  38883  voliooico  38885  voliccico  38892  stoweidlem26  38919  stoweidlem34  38927  stoweidlem59  38952  stirlinglem5  38971  dirkercncflem1  38996  fourierdlem10  39010  fourierdlem19  39019  fourierdlem25  39025  fourierdlem35  39035  fourierdlem40  39040  fourierdlem42  39042  fourierdlem64  39063  fourierdlem65  39064  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem104  39103  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem32  39159  etransclem41  39168  hsphoidmvle2  39475  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  hoidmvlelem2  39486  hoidmvlelem4  39488  hoidmvlelem5  39489  hoiqssbllem3  39514  hspmbllem1  39516  hspmbllem2  39517  vonicc  39576  pimdecfgtioo  39604  pimincfltioo  39605  fmtno4prmfac  40022  perfectALTVlem2  40165  nbusgrvtxm1  40607  crctcsh1wlkn0lem3  41015  av-frgrareggt1  41547  aacllem  42356