Theorem ltnled 11382

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ wcel 2145   class class class wbr 5103  ℝcr 11124   < clt 11268   ≤ cle 11269

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5661  df-cnv 5663  df-xr 11272  df-le 11274

This theorem is used by:  ltsub1  11735  ltsub2  11736  0mnnnnn0  12561  0nn0m1nnn0  12676  mul2lt0bi  13151  fzp1nel  13667  fzodisj  13750  elfznelfzob  13831  ccatsymb  14649  swrdnd  14725  cshwcsh2id  14900  01sqrexlem7  15336  sqrtlt  15349  lo1bdd2  15612  isercoll  15756  fprodntriv  16030  fzm1ndvds  16413  fzo0dvdseq  16414  bitsfzolem  16525  bitsfzo  16526  sadcaddlem  16548  smuval2  16573  bezoutlem3  16632  2mulprm  16784  isprm5  16799  odzdvds  16888  prm23ge5  16908  pc2dvds  16972  pockthg  16999  prmreclem1  17009  prmreclem5  17013  1arith  17020  4sqlem11  17048  vdwlem6  17079  vdwlem11  17084  ramlb  17112  oddvds  19675  gexdvds  19712  sylow1lem3  19728  zringlpirlem3  21678  psdmul  22395  coe1tmmul2  22503  iccntr  25049  icccmplem2  25051  reconnlem2  25055  evth  25188  lebnumlem3  25192  nmoleub2lem3  25344  minveclem3b  25657  minveclem4  25661  pmltpclem2  25678  ovolgelb  25709  ovolicc2lem2  25747  ovolicc2lem4  25749  mbfposr  25881  itg2const2  25970  itg2cnlem2  25991  itg2cn  25992  plyco0  26418  coeeulem  26451  dgradd2  26495  cxplt2  26936  fsumharmonic  27249  dmlogdmgm  27261  lgamgulmlem1  27266  lgamucov  27275  ftalem3  27312  ftalem5  27314  ftalem7  27316  ppiprm  27388  chtprm  27390  chpub  27457  perfectlem2  27467  bposlem1  27521  lgsdilem2  27570  lgsqrlem2  27584  lgsquadlem2  27618  2sqblem  27668  2sqmod  27673  2sqnn0  27675  pntpbnd1  27823  pntlem3  27846  nbusgrvtxm1  29840  crctcshwlkn0lem3  30281  frgrreggt1  30874  minvecolem4  31362  minvecolem5  31363  nndiffz1  33258  psgnfzto1stlem  33541  exsslsb  34108  lmdvg  34464  eulerpartlems  34872  ballotlemfc0  35005  ballotlemfcc  35006  ballotlemrv2  35034  signsply0  35060  reprinfz1  35131  lpadmax  35194  lpadright  35196  erdszelem8  35778  bccolsum  36319  unbdqndv2lem1  37207  unbdqndv2lem2  37208  poimirlem2  38372  poimirlem3  38373  poimirlem6  38376  poimirlem7  38377  poimirlem8  38378  poimirlem16  38386  poimirlem17  38387  poimirlem19  38389  poimirlem20  38390  poimirlem21  38391  poimirlem22  38392  poimirlem23  38393  poimirlem26  38396  poimirlem31  38401  poimir  38403  mblfinlem2  38408  itg2addnclem  38421  itg2addnclem2  38422  itg2addnclem3  38423  iblabsnclem  38433  ftc1anclem5  38447  areacirclem4  38461  areacirclem5  38462  areacirc  38463  cntotbnd  38547  aks4d1p5  42947  aks4d1p8d2  42952  aks4d1p8  42954  aks4d1p9  42955  posbezout  42967  primrootlekpowne0  42972  hashnexinj  42995  sticksstones1  43013  sticksstones22  43035  unitscyglem2  43063  unitscyglem4  43065  infdesc  43490  elpell1qr2  43714  pellfundglb  43727  pellfund14gap  43729  congabseq  43816  jm2.19  43835  jm2.26lem3  43843  dgraa0p  43991  dvgrat  45137  uzwo4  45888  divlt0gt0d  46120  supxrgere  46164  uzublem  46259  nleltd  46281  supminfxr  46293  xrpnf  46314  sqrlearg  46384  lptre2pt  46469  limsupubuzlem  46541  climxrrelem  46578  climxlim2lem  46674  icccncfext  46716  ioodvbdlimc1lem2  46761  ioodvbdlimc2lem  46763  volioore  46819  voliooico  46821  voliccico  46828  stoweidlem26  46855  stoweidlem34  46863  stoweidlem59  46888  stirlinglem5  46907  dirkercncflem1  46932  fourierdlem10  46946  fourierdlem19  46955  fourierdlem25  46961  fourierdlem35  46971  fourierdlem40  46976  fourierdlem42  46978  fourierdlem64  46999  fourierdlem65  47000  fourierdlem74  47009  fourierdlem75  47010  fourierdlem78  47013  fourierdlem79  47014  fourierdlem104  47039  fourierswlem  47059  fouriersw  47060  elaa2lem  47062  etransclem32  47095  etransclem41  47104  hsphoidmvle2  47414  hoidmv1lelem1  47420  hoidmv1lelem2  47421  hoidmv1lelem3  47422  hoidmvlelem2  47425  hoidmvlelem4  47427  hoidmvlelem5  47428  hoiqssbllem3  47453  hspmbllem1  47455  hspmbllem2  47456  vonicc  47514  pimdecfgtioo  47546  pimincfltioo  47547  et-sqrtnegnre  47702  fmtno4prmfac  48476  requad01  48538  requad1  48539  perfectALTVlem2  48639  itsclc0yqsol  49695  aacllem  50773