Theorem ltnled 11408

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-xr 11299  df-le 11301

This theorem is referenced by:  ltsub1  11759  ltsub2  11760  0mnnnnn0  12558  mul2lt0bi  13141  fzp1nel  13651  fzodisj  13733  elfznelfzob  13812  ccatsymb  14620  swrdnd  14692  cshwcsh2id  14867  01sqrexlem7  15287  sqrtlt  15300  lo1bdd2  15560  isercoll  15704  fprodntriv  15978  fzm1ndvds  16359  fzo0dvdseq  16360  bitsfzolem  16471  bitsfzo  16472  sadcaddlem  16494  smuval2  16519  bezoutlem3  16578  2mulprm  16730  isprm5  16744  odzdvds  16833  prm23ge5  16853  pc2dvds  16917  pockthg  16944  prmreclem1  16954  prmreclem5  16958  1arith  16965  4sqlem11  16993  vdwlem6  17024  vdwlem11  17029  ramlb  17057  oddvds  19565  gexdvds  19602  sylow1lem3  19618  zringlpirlem3  21475  psdmul  22170  coe1tmmul2  22279  iccntr  24843  icccmplem2  24845  reconnlem2  24849  evth  24991  lebnumlem3  24995  nmoleub2lem3  25148  minveclem3b  25462  minveclem4  25466  pmltpclem2  25484  ovolgelb  25515  ovolicc2lem2  25553  ovolicc2lem4  25555  mbfposr  25687  itg2const2  25776  itg2cnlem2  25797  itg2cn  25798  plyco0  26231  coeeulem  26263  dgradd2  26308  cxplt2  26740  fsumharmonic  27055  dmlogdmgm  27067  lgamgulmlem1  27072  lgamucov  27081  ftalem3  27118  ftalem5  27120  ftalem7  27122  ppiprm  27194  chtprm  27196  chpub  27264  perfectlem2  27274  bposlem1  27328  lgsdilem2  27377  lgsqrlem2  27391  lgsquadlem2  27425  2sqblem  27475  2sqmod  27480  2sqnn0  27482  pntpbnd1  27630  pntlem3  27653  nbusgrvtxm1  29396  crctcshwlkn0lem3  29832  frgrreggt1  30412  minvecolem4  30899  minvecolem5  30900  nndiffz1  32788  psgnfzto1stlem  33120  exsslsb  33647  lmdvg  33952  eulerpartlems  34362  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemrv2  34524  signsply0  34566  reprinfz1  34637  lpadmax  34697  lpadright  34699  0nn0m1nnn0  35118  erdszelem8  35203  bccolsum  35739  unbdqndv2lem1  36510  unbdqndv2lem2  36511  poimirlem2  37629  poimirlem3  37630  poimirlem6  37633  poimirlem7  37634  poimirlem8  37635  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem26  37653  poimirlem31  37658  poimir  37660  mblfinlem2  37665  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  iblabsnclem  37690  ftc1anclem5  37704  areacirclem4  37718  areacirclem5  37719  areacirc  37720  cntotbnd  37803  aks4d1p5  42081  aks4d1p8d2  42086  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootlekpowne0  42106  hashnexinj  42129  sticksstones1  42147  sticksstones22  42169  unitscyglem2  42197  unitscyglem4  42199  metakunt29  42234  metakunt30  42235  infdesc  42653  elpell1qr2  42883  pellfundglb  42896  pellfund14gap  42898  congabseq  42986  jm2.19  43005  jm2.26lem3  43013  dgraa0p  43161  dvgrat  44331  uzwo4  45058  divlt0gt0d  45298  supxrgere  45344  uzublem  45441  nleltd  45463  supminfxr  45475  xrpnf  45496  sqrlearg  45566  lptre2pt  45655  limsupubuzlem  45727  climxrrelem  45764  climxlim2lem  45860  icccncfext  45902  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  volioore  46005  voliooico  46007  voliccico  46014  stoweidlem26  46041  stoweidlem34  46049  stoweidlem59  46074  stirlinglem5  46093  dirkercncflem1  46118  fourierdlem10  46132  fourierdlem19  46141  fourierdlem25  46147  fourierdlem35  46157  fourierdlem40  46162  fourierdlem42  46164  fourierdlem64  46185  fourierdlem65  46186  fourierdlem74  46195  fourierdlem75  46196  fourierdlem78  46199  fourierdlem79  46200  fourierdlem104  46225  fourierswlem  46245  fouriersw  46246  elaa2lem  46248  etransclem32  46281  etransclem41  46290  hsphoidmvle2  46600  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  hoidmvlelem2  46611  hoidmvlelem4  46613  hoidmvlelem5  46614  hoiqssbllem3  46639  hspmbllem1  46641  hspmbllem2  46642  vonicc  46700  pimdecfgtioo  46732  pimincfltioo  46733  et-sqrtnegnre  46888  fmtno4prmfac  47559  requad01  47608  requad1  47609  perfectALTVlem2  47709  itsclc0yqsol  48685  aacllem  49320