Theorem ltnle 10519

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)

Assertion

Ref	Expression
ltnle	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Proof of Theorem ltnle

Step	Hyp	Ref	Expression
1		lenlt 10518	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 451	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 347	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387   ∈ wcel 2051   class class class wbr 4926  ℝcr 10333   < clt 10473   ≤ cle 10474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-br 4927  df-opab 4989  df-xp 5410  df-cnv 5412  df-xr 10477  df-le 10479

This theorem is referenced by:  letric  10539  ltnled  10586  leaddsub  10916  mulge0b  11310  nnnle0  11472  nn0n0n1ge2b  11774  znnnlt1  11821  uzwo  12124  qsqueeze  12410  difreicc  12685  fzp1disj  12781  fzneuz  12803  fznuz  12804  uznfz  12805  difelfznle  12836  nelfzo  12858  ssfzoulel  12945  elfzonelfzo  12953  modfzo0difsn  13125  ssnn0fi  13167  discr1  13414  bcval5  13492  ccatsymb  13744  swrdnd  13821  swrdnnn0nd  13823  swrdnd0  13824  swrdsbslen  13840  swrdspsleq  13841  pfxnd0  13869  pfxccat3  13935  swrdccat3OLD  13936  swrdccat  13937  pfxccat3a  13941  repswswrd  14002  cnpart  14459  absmax  14549  rlimrege0  14796  rpnnen2lem12  15437  alzdvds  15529  algcvgblem  15776  prmndvdsfaclt  15922  pcprendvds  16032  pcdvdsb  16060  pcmpt  16083  prmunb  16105  prmreclem2  16108  prmgaplem5  16246  prmgaplem6  16247  prmlem1  16296  prmlem2  16308  lt6abl  18782  metdseq0  23181  xrhmeo  23269  ovolicc2lem3  23839  itg2seq  24062  dvne0  24327  coeeulem  24533  radcnvlt1  24725  argimgt0  24912  cxple2  24997  ressatans  25229  eldmgm  25317  basellem2  25377  issqf  25431  bpos1  25577  bposlem3  25580  bposlem6  25583  2sqreulem1  25740  2sqreunnlem1  25743  pntpbnd2  25881  ostth2lem4  25930  crctcshwlkn0  27323  crctcsh  27326  eucrctshift  27789  ltflcei  34354  poimirlem4  34370  poimirlem13  34379  poimirlem14  34380  poimirlem15  34381  poimirlem31  34397  mblfinlem1  34403  mbfposadd  34413  itgaddnclem2  34425  ftc1anclem1  34441  ftc1anclem5  34445  dvasin  34452  icccncfext  41630  stoweidlem14  41760  stoweidlem34  41780  ltnltne  42935  nnsum4primeseven  43363  nnsum4primesevenALTV  43364  ply1mulgsumlem2  43838