Theorem ltnled 11365

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∈ wcel 2104   class class class wbr 5147  ℝcr 11111   < clt 11252   ≤ cle 11253

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-xr 11256  df-le 11258

This theorem is referenced by:  ltsub1  11714  ltsub2  11715  0mnnnnn0  12508  mul2lt0bi  13084  fzp1nel  13589  fzodisj  13670  elfznelfzob  13742  ccatsymb  14536  swrdnd  14608  cshwcsh2id  14783  01sqrexlem7  15199  sqrtlt  15212  lo1bdd2  15472  isercoll  15618  fprodntriv  15890  fzm1ndvds  16269  fzo0dvdseq  16270  bitsfzolem  16379  bitsfzo  16380  sadcaddlem  16402  smuval2  16427  bezoutlem3  16487  2mulprm  16634  isprm5  16648  odzdvds  16732  prm23ge5  16752  pc2dvds  16816  pockthg  16843  prmreclem1  16853  prmreclem5  16857  1arith  16864  4sqlem11  16892  vdwlem6  16923  vdwlem11  16928  ramlb  16956  oddvds  19456  gexdvds  19493  sylow1lem3  19509  zringlpirlem3  21235  coe1tmmul2  22018  iccntr  24557  icccmplem2  24559  reconnlem2  24563  evth  24705  lebnumlem3  24709  nmoleub2lem3  24862  minveclem3b  25176  minveclem4  25180  pmltpclem2  25198  ovolgelb  25229  ovolicc2lem2  25267  ovolicc2lem4  25269  mbfposr  25401  itg2const2  25491  itg2cnlem2  25512  itg2cn  25513  plyco0  25941  coeeulem  25973  dgradd2  26018  cxplt2  26442  fsumharmonic  26752  dmlogdmgm  26764  lgamgulmlem1  26769  lgamucov  26778  ftalem3  26815  ftalem5  26817  ftalem7  26819  ppiprm  26891  chtprm  26893  chpub  26959  perfectlem2  26969  bposlem1  27023  lgsdilem2  27072  lgsqrlem2  27086  lgsquadlem2  27120  2sqblem  27170  2sqmod  27175  2sqnn0  27177  pntpbnd1  27325  pntlem3  27348  nbusgrvtxm1  28903  crctcshwlkn0lem3  29333  frgrreggt1  29913  minvecolem4  30400  minvecolem5  30401  nndiffz1  32264  psgnfzto1stlem  32529  lmdvg  33231  eulerpartlems  33657  ballotlemfc0  33789  ballotlemfcc  33790  ballotlemrv2  33818  signsply0  33860  reprinfz1  33932  lpadmax  33992  lpadright  33994  0nn0m1nnn0  34400  erdszelem8  34487  bccolsum  35013  unbdqndv2lem1  35688  unbdqndv2lem2  35689  poimirlem2  36793  poimirlem3  36794  poimirlem6  36797  poimirlem7  36798  poimirlem8  36799  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem21  36812  poimirlem22  36813  poimirlem23  36814  poimirlem26  36817  poimirlem31  36822  poimir  36824  mblfinlem2  36829  itg2addnclem  36842  itg2addnclem2  36843  itg2addnclem3  36844  iblabsnclem  36854  ftc1anclem5  36868  areacirclem4  36882  areacirclem5  36883  areacirc  36884  cntotbnd  36967  aks4d1p5  41251  aks4d1p8d2  41256  aks4d1p8  41258  aks4d1p9  41259  sticksstones1  41268  sticksstones22  41290  metakunt29  41319  metakunt30  41320  infdesc  41687  elpell1qr2  41912  pellfundglb  41925  pellfund14gap  41927  congabseq  42015  jm2.19  42034  jm2.26lem3  42042  dgraa0p  42193  dvgrat  43373  uzwo4  44041  divlt0gt0d  44294  supxrgere  44341  uzublem  44438  nleltd  44460  supminfxr  44472  xrpnf  44494  sqrlearg  44564  lptre2pt  44654  limsupubuzlem  44726  climxrrelem  44763  climxlim2lem  44859  icccncfext  44901  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  volioore  45004  voliooico  45006  voliccico  45013  stoweidlem26  45040  stoweidlem34  45048  stoweidlem59  45073  stirlinglem5  45092  dirkercncflem1  45117  fourierdlem10  45131  fourierdlem19  45140  fourierdlem25  45146  fourierdlem35  45156  fourierdlem40  45161  fourierdlem42  45163  fourierdlem64  45184  fourierdlem65  45185  fourierdlem74  45194  fourierdlem75  45195  fourierdlem78  45198  fourierdlem79  45199  fourierdlem104  45224  fourierswlem  45244  fouriersw  45245  elaa2lem  45247  etransclem32  45280  etransclem41  45289  hsphoidmvle2  45599  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmv1lelem3  45607  hoidmvlelem2  45610  hoidmvlelem4  45612  hoidmvlelem5  45613  hoiqssbllem3  45638  hspmbllem1  45640  hspmbllem2  45641  vonicc  45699  pimdecfgtioo  45731  pimincfltioo  45732  et-sqrtnegnre  45887  fmtno4prmfac  46538  requad01  46587  requad1  46588  perfectALTVlem2  46688  itsclc0yqsol  47537  aacllem  47935