Theorem ltnle 11262

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 11261	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
2	1	ancoms 462	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ≤ 𝐴 ↔ ¬ 𝐴 < 𝐵))
3	2	con2bid 356	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∈ 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:  letric  11283  ltnled  11330  leaddsub  11663  mulge0b  12062  nnnle0  12246  nn0n0n1ge2b  12550  znnnlt1  12598  uzwo  12912  qsqueeze  13204  difreicc  13488  fzp1disj  13588  fzneuz  13613  fznuz  13614  uznfz  13615  difelfznle  13647  nelfzo  13670  ssfzoulel  13766  elfzonelfzo  13775  modfzo0difsn  13956  ssnn0fi  13998  discr1  14252  bcval5  14331  swrdnd  14668  swrdnnn0nd  14670  swrdnd0  14671  swrdsbslen  14678  swrdspsleq  14679  pfxnd0  14702  pfxccat3  14747  swrdccat  14748  pfxccat3a  14751  repswswrd  14797  cnpart  15267  absmax  15357  rlimrege0  15606  rpnnen2lem12  16257  alzdvds  16354  algcvgblem  16611  prmndvdsfaclt  16760  pcprendvds  16876  pcdvdsb  16905  pcmpt  16928  prmunb  16950  prmreclem2  16953  prmgaplem5  17091  prmgaplem6  17092  prmlem1  17143  prmlem2  17156  lt6abl  19935  metdseq0  24915  xrhmeo  25008  ovolicc2lem3  25581  itg2seq  25804  dvne0  26073  coeeulem  26284  radcnvlt1  26481  argimgt0  26677  cxple2  26762  ressatans  26999  eldmgm  27086  basellem2  27146  issqf  27200  bpos1  27347  bposlem3  27350  bposlem6  27353  2sqreulem1  27510  2sqreunnlem1  27513  pntpbnd2  27651  ostth2lem4  27700  crctcshwlkn0  30021  crctcsh  30024  eucrctshift  30445  ltflcei  38107  poimirlem4  38123  poimirlem13  38132  poimirlem14  38133  poimirlem15  38134  poimirlem31  38150  mblfinlem1  38156  mbfposadd  38166  itgaddnclem2  38178  ftc1anclem1  38192  ftc1anclem5  38196  dvasin  38203  reabsifnpos  44209  reabsifnneg  44211  icccncfext  46461  stoweidlem14  46588  stoweidlem34  46608  ltnltne  47893  nnsum4primeseven  48422  nnsum4primesevenALTV  48423  ply1mulgsumlem2  49009