Theorem ltnled 11383

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2099   class class class wbr 5142  ℝcr 11129   < clt 11270   ≤ cle 11271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-br 5143  df-opab 5205  df-xp 5678  df-cnv 5680  df-xr 11274  df-le 11276

This theorem is referenced by:  ltsub1  11732  ltsub2  11733  0mnnnnn0  12526  mul2lt0bi  13104  fzp1nel  13609  fzodisj  13690  elfznelfzob  13762  ccatsymb  14556  swrdnd  14628  cshwcsh2id  14803  01sqrexlem7  15219  sqrtlt  15232  lo1bdd2  15492  isercoll  15638  fprodntriv  15910  fzm1ndvds  16290  fzo0dvdseq  16291  bitsfzolem  16400  bitsfzo  16401  sadcaddlem  16423  smuval2  16448  bezoutlem3  16508  2mulprm  16655  isprm5  16669  odzdvds  16755  prm23ge5  16775  pc2dvds  16839  pockthg  16866  prmreclem1  16876  prmreclem5  16880  1arith  16887  4sqlem11  16915  vdwlem6  16946  vdwlem11  16951  ramlb  16979  oddvds  19493  gexdvds  19530  sylow1lem3  19546  zringlpirlem3  21377  psdmul  22077  coe1tmmul2  22182  iccntr  24724  icccmplem2  24726  reconnlem2  24730  evth  24872  lebnumlem3  24876  nmoleub2lem3  25029  minveclem3b  25343  minveclem4  25347  pmltpclem2  25365  ovolgelb  25396  ovolicc2lem2  25434  ovolicc2lem4  25436  mbfposr  25568  itg2const2  25658  itg2cnlem2  25679  itg2cn  25680  plyco0  26113  coeeulem  26145  dgradd2  26190  cxplt2  26619  fsumharmonic  26931  dmlogdmgm  26943  lgamgulmlem1  26948  lgamucov  26957  ftalem3  26994  ftalem5  26996  ftalem7  26998  ppiprm  27070  chtprm  27072  chpub  27140  perfectlem2  27150  bposlem1  27204  lgsdilem2  27253  lgsqrlem2  27267  lgsquadlem2  27301  2sqblem  27351  2sqmod  27356  2sqnn0  27358  pntpbnd1  27506  pntlem3  27529  nbusgrvtxm1  29179  crctcshwlkn0lem3  29610  frgrreggt1  30190  minvecolem4  30677  minvecolem5  30678  nndiffz1  32538  psgnfzto1stlem  32799  lmdvg  33490  eulerpartlems  33916  ballotlemfc0  34048  ballotlemfcc  34049  ballotlemrv2  34077  signsply0  34119  reprinfz1  34190  lpadmax  34250  lpadright  34252  0nn0m1nnn0  34658  erdszelem8  34744  bccolsum  35269  unbdqndv2lem1  35920  unbdqndv2lem2  35921  poimirlem2  37030  poimirlem3  37031  poimirlem6  37034  poimirlem7  37035  poimirlem8  37036  poimirlem16  37044  poimirlem17  37045  poimirlem19  37047  poimirlem20  37048  poimirlem21  37049  poimirlem22  37050  poimirlem23  37051  poimirlem26  37054  poimirlem31  37059  poimir  37061  mblfinlem2  37066  itg2addnclem  37079  itg2addnclem2  37080  itg2addnclem3  37081  iblabsnclem  37091  ftc1anclem5  37105  areacirclem4  37119  areacirclem5  37120  areacirc  37121  cntotbnd  37204  aks4d1p5  41488  aks4d1p8d2  41493  aks4d1p8  41495  aks4d1p9  41496  posbezout  41507  hashnexinj  41531  sticksstones1  41550  sticksstones22  41572  metakunt29  41605  metakunt30  41606  infdesc  41989  elpell1qr2  42214  pellfundglb  42227  pellfund14gap  42229  congabseq  42317  jm2.19  42336  jm2.26lem3  42344  dgraa0p  42495  dvgrat  43672  uzwo4  44340  divlt0gt0d  44591  supxrgere  44638  uzublem  44735  nleltd  44757  supminfxr  44769  xrpnf  44791  sqrlearg  44861  lptre2pt  44951  limsupubuzlem  45023  climxrrelem  45060  climxlim2lem  45156  icccncfext  45198  ioodvbdlimc1lem2  45243  ioodvbdlimc2lem  45245  volioore  45301  voliooico  45303  voliccico  45310  stoweidlem26  45337  stoweidlem34  45345  stoweidlem59  45370  stirlinglem5  45389  dirkercncflem1  45414  fourierdlem10  45428  fourierdlem19  45437  fourierdlem25  45443  fourierdlem35  45453  fourierdlem40  45458  fourierdlem42  45460  fourierdlem64  45481  fourierdlem65  45482  fourierdlem74  45491  fourierdlem75  45492  fourierdlem78  45495  fourierdlem79  45496  fourierdlem104  45521  fourierswlem  45541  fouriersw  45542  elaa2lem  45544  etransclem32  45577  etransclem41  45586  hsphoidmvle2  45896  hoidmv1lelem1  45902  hoidmv1lelem2  45903  hoidmv1lelem3  45904  hoidmvlelem2  45907  hoidmvlelem4  45909  hoidmvlelem5  45910  hoiqssbllem3  45935  hspmbllem1  45937  hspmbllem2  45938  vonicc  45996  pimdecfgtioo  46028  pimincfltioo  46029  et-sqrtnegnre  46184  fmtno4prmfac  46835  requad01  46884  requad1  46885  perfectALTVlem2  46985  itsclc0yqsol  47760  aacllem  48157