Theorem ltnled 11297

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  ltsub1  11650  ltsub2  11651  0mnnnnn0  12450  mul2lt0bi  13035  fzp1nel  13548  fzodisj  13630  elfznelfzob  13710  ccatsymb  14523  swrdnd  14595  cshwcsh2id  14770  01sqrexlem7  15190  sqrtlt  15203  lo1bdd2  15466  isercoll  15610  fprodntriv  15884  fzm1ndvds  16268  fzo0dvdseq  16269  bitsfzolem  16380  bitsfzo  16381  sadcaddlem  16403  smuval2  16428  bezoutlem3  16487  2mulprm  16639  isprm5  16653  odzdvds  16742  prm23ge5  16762  pc2dvds  16826  pockthg  16853  prmreclem1  16863  prmreclem5  16867  1arith  16874  4sqlem11  16902  vdwlem6  16933  vdwlem11  16938  ramlb  16966  oddvds  19453  gexdvds  19490  sylow1lem3  19506  zringlpirlem3  21350  psdmul  22029  coe1tmmul2  22138  iccntr  24686  icccmplem2  24688  reconnlem2  24692  evth  24834  lebnumlem3  24838  nmoleub2lem3  24991  minveclem3b  25304  minveclem4  25308  pmltpclem2  25326  ovolgelb  25357  ovolicc2lem2  25395  ovolicc2lem4  25397  mbfposr  25529  itg2const2  25618  itg2cnlem2  25639  itg2cn  25640  plyco0  26073  coeeulem  26105  dgradd2  26150  cxplt2  26583  fsumharmonic  26898  dmlogdmgm  26910  lgamgulmlem1  26915  lgamucov  26924  ftalem3  26961  ftalem5  26963  ftalem7  26965  ppiprm  27037  chtprm  27039  chpub  27107  perfectlem2  27117  bposlem1  27171  lgsdilem2  27220  lgsqrlem2  27234  lgsquadlem2  27268  2sqblem  27318  2sqmod  27323  2sqnn0  27325  pntpbnd1  27473  pntlem3  27496  nbusgrvtxm1  29282  crctcshwlkn0lem3  29715  frgrreggt1  30295  minvecolem4  30782  minvecolem5  30783  nndiffz1  32682  psgnfzto1stlem  33030  exsslsb  33565  lmdvg  33916  eulerpartlems  34324  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemrv2  34486  signsply0  34515  reprinfz1  34586  lpadmax  34646  lpadright  34648  0nn0m1nnn0  35073  erdszelem8  35158  bccolsum  35699  unbdqndv2lem1  36470  unbdqndv2lem2  36471  poimirlem2  37589  poimirlem3  37590  poimirlem6  37593  poimirlem7  37594  poimirlem8  37595  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem21  37608  poimirlem22  37609  poimirlem23  37610  poimirlem26  37613  poimirlem31  37618  poimir  37620  mblfinlem2  37625  itg2addnclem  37638  itg2addnclem2  37639  itg2addnclem3  37640  iblabsnclem  37650  ftc1anclem5  37664  areacirclem4  37678  areacirclem5  37679  areacirc  37680  cntotbnd  37763  aks4d1p5  42041  aks4d1p8d2  42046  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  primrootlekpowne0  42066  hashnexinj  42089  sticksstones1  42107  sticksstones22  42129  unitscyglem2  42157  unitscyglem4  42159  infdesc  42604  elpell1qr2  42833  pellfundglb  42846  pellfund14gap  42848  congabseq  42936  jm2.19  42955  jm2.26lem3  42963  dgraa0p  43111  dvgrat  44274  uzwo4  45020  divlt0gt0d  45257  supxrgere  45302  uzublem  45399  nleltd  45421  supminfxr  45433  xrpnf  45454  sqrlearg  45524  lptre2pt  45611  limsupubuzlem  45683  climxrrelem  45720  climxlim2lem  45816  icccncfext  45858  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  volioore  45961  voliooico  45963  voliccico  45970  stoweidlem26  45997  stoweidlem34  46005  stoweidlem59  46030  stirlinglem5  46049  dirkercncflem1  46074  fourierdlem10  46088  fourierdlem19  46097  fourierdlem25  46103  fourierdlem35  46113  fourierdlem40  46118  fourierdlem42  46120  fourierdlem64  46141  fourierdlem65  46142  fourierdlem74  46151  fourierdlem75  46152  fourierdlem78  46155  fourierdlem79  46156  fourierdlem104  46181  fourierswlem  46201  fouriersw  46202  elaa2lem  46204  etransclem32  46237  etransclem41  46246  hsphoidmvle2  46556  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmvlelem2  46567  hoidmvlelem4  46569  hoidmvlelem5  46570  hoiqssbllem3  46595  hspmbllem1  46597  hspmbllem2  46598  vonicc  46656  pimdecfgtioo  46688  pimincfltioo  46689  et-sqrtnegnre  46844  fmtno4prmfac  47546  requad01  47595  requad1  47596  perfectALTVlem2  47696  itsclc0yqsol  48726  aacllem  49763