Theorem ltnled 11374

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2146   class class class wbr 5111  ℝcr 11116   < clt 11260   ≤ cle 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-xp 5669  df-cnv 5671  df-xr 11264  df-le 11266

This theorem is used by:  ltsub1  11727  ltsub2  11728  0mnnnnn0  12553  0nn0m1nnn0  12668  mul2lt0bi  13142  fzp1nel  13658  fzodisj  13741  elfznelfzob  13822  ccatsymb  14640  swrdnd  14716  cshwcsh2id  14891  01sqrexlem7  15325  sqrtlt  15338  lo1bdd2  15601  isercoll  15745  fprodntriv  16021  fzm1ndvds  16404  fzo0dvdseq  16405  bitsfzolem  16516  bitsfzo  16517  sadcaddlem  16539  smuval2  16564  bezoutlem3  16623  2mulprm  16775  isprm5  16790  odzdvds  16879  prm23ge5  16899  pc2dvds  16963  pockthg  16990  prmreclem1  17000  prmreclem5  17004  1arith  17011  4sqlem11  17039  vdwlem6  17070  vdwlem11  17075  ramlb  17103  oddvds  19663  gexdvds  19700  sylow1lem3  19716  zringlpirlem3  21666  psdmul  22381  coe1tmmul2  22489  iccntr  25032  icccmplem2  25034  reconnlem2  25038  evth  25171  lebnumlem3  25175  nmoleub2lem3  25327  minveclem3b  25640  minveclem4  25644  pmltpclem2  25661  ovolgelb  25692  ovolicc2lem2  25730  ovolicc2lem4  25732  mbfposr  25864  itg2const2  25953  itg2cnlem2  25974  itg2cn  25975  plyco0  26402  coeeulem  26434  dgradd2  26478  cxplt2  26916  fsumharmonic  27229  dmlogdmgm  27241  lgamgulmlem1  27246  lgamucov  27255  ftalem3  27292  ftalem5  27294  ftalem7  27296  ppiprm  27368  chtprm  27370  chpub  27437  perfectlem2  27447  bposlem1  27501  lgsdilem2  27550  lgsqrlem2  27564  lgsquadlem2  27598  2sqblem  27648  2sqmod  27653  2sqnn0  27655  pntpbnd1  27803  pntlem3  27826  nbusgrvtxm1  29789  crctcshwlkn0lem3  30230  frgrreggt1  30817  minvecolem4  31305  minvecolem5  31306  nndiffz1  33203  psgnfzto1stlem  33486  exsslsb  34053  lmdvg  34409  eulerpartlems  34817  ballotlemfc0  34950  ballotlemfcc  34951  ballotlemrv2  34979  signsply0  35005  reprinfz1  35076  lpadmax  35139  lpadright  35141  erdszelem8  35729  bccolsum  36270  unbdqndv2lem1  37157  unbdqndv2lem2  37158  poimirlem2  38332  poimirlem3  38333  poimirlem6  38336  poimirlem7  38337  poimirlem8  38338  poimirlem16  38346  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem21  38351  poimirlem22  38352  poimirlem23  38353  poimirlem26  38356  poimirlem31  38361  poimir  38363  mblfinlem2  38368  itg2addnclem  38381  itg2addnclem2  38382  itg2addnclem3  38383  iblabsnclem  38393  ftc1anclem5  38407  areacirclem4  38421  areacirclem5  38422  areacirc  38423  cntotbnd  38507  aks4d1p5  42907  aks4d1p8d2  42912  aks4d1p8  42914  aks4d1p9  42915  posbezout  42927  primrootlekpowne0  42932  hashnexinj  42955  sticksstones1  42973  sticksstones22  42995  unitscyglem2  43023  unitscyglem4  43025  infdesc  43435  elpell1qr2  43659  pellfundglb  43672  pellfund14gap  43674  congabseq  43761  jm2.19  43780  jm2.26lem3  43788  dgraa0p  43936  dvgrat  45082  uzwo4  45833  divlt0gt0d  46065  supxrgere  46109  uzublem  46204  nleltd  46226  supminfxr  46238  xrpnf  46259  sqrlearg  46329  lptre2pt  46414  limsupubuzlem  46486  climxrrelem  46523  climxlim2lem  46619  icccncfext  46661  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  volioore  46764  voliooico  46766  voliccico  46773  stoweidlem26  46800  stoweidlem34  46808  stoweidlem59  46833  stirlinglem5  46852  dirkercncflem1  46877  fourierdlem10  46891  fourierdlem19  46900  fourierdlem25  46906  fourierdlem35  46916  fourierdlem40  46921  fourierdlem42  46923  fourierdlem64  46944  fourierdlem65  46945  fourierdlem74  46954  fourierdlem75  46955  fourierdlem78  46958  fourierdlem79  46959  fourierdlem104  46984  fourierswlem  47004  fouriersw  47005  elaa2lem  47007  etransclem32  47040  etransclem41  47049  hsphoidmvle2  47359  hoidmv1lelem1  47365  hoidmv1lelem2  47366  hoidmv1lelem3  47367  hoidmvlelem2  47370  hoidmvlelem4  47372  hoidmvlelem5  47373  hoiqssbllem3  47398  hspmbllem1  47400  hspmbllem2  47401  vonicc  47459  pimdecfgtioo  47491  pimincfltioo  47492  et-sqrtnegnre  47647  fmtno4prmfac  48384  requad01  48446  requad1  48447  perfectALTVlem2  48547  itsclc0yqsol  49603  aacllem  50680