Theorem ltnled 11330

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2142   class class class wbr 5100  ℝcr 11072   < clt 11216   ≤ cle 11217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5653  df-cnv 5655  df-xr 11220  df-le 11222

This theorem is referenced by:  ltsub1  11683  ltsub2  11684  0mnnnnn0  12513  mul2lt0bi  13101  fzp1nel  13616  fzodisj  13699  elfznelfzob  13780  ccatsymb  14596  swrdnd  14668  cshwcsh2id  14841  01sqrexlem7  15275  sqrtlt  15288  lo1bdd2  15551  isercoll  15695  fprodntriv  15972  fzm1ndvds  16356  fzo0dvdseq  16357  bitsfzolem  16468  bitsfzo  16469  sadcaddlem  16491  smuval2  16516  bezoutlem3  16575  2mulprm  16727  isprm5  16742  odzdvds  16831  prm23ge5  16851  pc2dvds  16915  pockthg  16942  prmreclem1  16952  prmreclem5  16956  1arith  16963  4sqlem11  16991  vdwlem6  17022  vdwlem11  17027  ramlb  17055  oddvds  19587  gexdvds  19624  sylow1lem3  19640  zringlpirlem3  21516  psdmul  22231  coe1tmmul2  22339  iccntr  24882  icccmplem2  24884  reconnlem2  24888  evth  25021  lebnumlem3  25025  nmoleub2lem3  25177  minveclem3b  25490  minveclem4  25494  pmltpclem2  25511  ovolgelb  25542  ovolicc2lem2  25580  ovolicc2lem4  25582  mbfposr  25714  itg2const2  25803  itg2cnlem2  25824  itg2cn  25825  plyco0  26252  coeeulem  26284  dgradd2  26328  cxplt2  26763  fsumharmonic  27076  dmlogdmgm  27088  lgamgulmlem1  27093  lgamucov  27102  ftalem3  27139  ftalem5  27141  ftalem7  27143  ppiprm  27215  chtprm  27217  chpub  27284  perfectlem2  27294  bposlem1  27348  lgsdilem2  27397  lgsqrlem2  27411  lgsquadlem2  27445  2sqblem  27495  2sqmod  27500  2sqnn0  27502  pntpbnd1  27650  pntlem3  27673  nbusgrvtxm1  29580  crctcshwlkn0lem3  30012  frgrreggt1  30595  minvecolem4  31083  minvecolem5  31084  nndiffz1  32988  psgnfzto1stlem  33280  exsslsb  33894  lmdvg  34250  eulerpartlems  34657  ballotlemfc0  34790  ballotlemfcc  34791  ballotlemrv2  34819  signsply0  34845  reprinfz1  34916  lpadmax  34979  lpadright  34981  0nn0m1nnn0  35463  erdszelem8  35548  bccolsum  36089  unbdqndv2lem1  36947  unbdqndv2lem2  36948  poimirlem2  38121  poimirlem3  38122  poimirlem6  38125  poimirlem7  38126  poimirlem8  38127  poimirlem16  38135  poimirlem17  38136  poimirlem19  38138  poimirlem20  38139  poimirlem21  38140  poimirlem22  38141  poimirlem23  38142  poimirlem26  38145  poimirlem31  38150  poimir  38152  mblfinlem2  38157  itg2addnclem  38170  itg2addnclem2  38171  itg2addnclem3  38172  iblabsnclem  38182  ftc1anclem5  38196  areacirclem4  38210  areacirclem5  38211  areacirc  38212  cntotbnd  38295  aks4d1p5  42697  aks4d1p8d2  42702  aks4d1p8  42704  aks4d1p9  42705  posbezout  42717  primrootlekpowne0  42722  hashnexinj  42745  sticksstones1  42763  sticksstones22  42785  unitscyglem2  42813  unitscyglem4  42815  infdesc  43225  elpell1qr2  43449  pellfundglb  43462  pellfund14gap  43464  congabseq  43551  jm2.19  43570  jm2.26lem3  43578  dgraa0p  43726  dvgrat  44888  uzwo4  45633  divlt0gt0d  45865  supxrgere  45909  uzublem  46004  nleltd  46026  supminfxr  46038  xrpnf  46059  sqrlearg  46129  lptre2pt  46214  limsupubuzlem  46286  climxrrelem  46323  climxlim2lem  46419  icccncfext  46461  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  volioore  46564  voliooico  46566  voliccico  46573  stoweidlem26  46600  stoweidlem34  46608  stoweidlem59  46633  stirlinglem5  46652  dirkercncflem1  46677  fourierdlem10  46691  fourierdlem19  46700  fourierdlem25  46706  fourierdlem35  46716  fourierdlem40  46721  fourierdlem42  46723  fourierdlem64  46744  fourierdlem65  46745  fourierdlem74  46754  fourierdlem75  46755  fourierdlem78  46758  fourierdlem79  46759  fourierdlem104  46784  fourierswlem  46804  fouriersw  46805  elaa2lem  46807  etransclem32  46840  etransclem41  46849  hsphoidmvle2  47159  hoidmv1lelem1  47165  hoidmv1lelem2  47166  hoidmv1lelem3  47167  hoidmvlelem2  47170  hoidmvlelem4  47172  hoidmvlelem5  47173  hoiqssbllem3  47198  hspmbllem1  47200  hspmbllem2  47201  vonicc  47259  pimdecfgtioo  47291  pimincfltioo  47292  et-sqrtnegnre  47447  fmtno4prmfac  48181  requad01  48243  requad1  48244  perfectALTVlem2  48344  itsclc0yqsol  49386  aacllem  50422