Theorem ltnle 11396

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∈ wcel 2144   class class class wbr 5102  ℝcr 11206   < clt 11350   ≤ cle 11351

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5657  df-cnv 5659  df-xr 11354  df-le 11356

This theorem is used by:  letric  11417  ltnled  11464  leaddsub  11799  mulge0b  12194  nnnle0  12378  nn0n0n1ge2b  12682  znnnlt1  12730  uzwo  13045  qsqueeze  13338  difreicc  13622  fzp1disj  13724  fzneuz  13749  fznuz  13750  uznfz  13751  difelfznle  13783  nelfzo  13806  ssfzoulel  13902  elfzonelfzo  13911  modfzo0difsn  14093  ssnn0fi  14135  discr1  14390  bcval5  14469  swrdnd  14812  swrdnnn0nd  14814  swrdnd0  14815  swrdsbslen  14822  swrdspsleq  14823  pfxnd0  14846  pfxccat3  14891  swrdccat  14892  pfxccat3a  14895  repswswrd  14943  cnpart  15416  absmax  15506  rlimrege0  15755  rpnnen2lem12  16402  alzdvds  16499  algcvgblem  16761  prmndvdsfaclt  16910  pcprendvds  17027  pcdvdsb  17056  pcmpt  17079  prmunb  17101  prmreclem2  17104  prmgaplem5  17242  prmgaplem6  17243  prmlem1  17294  prmlem2  17307  lt6abl  20118  metdseq0  25183  xrhmeo  25276  ovolicc2lem3  25849  itg2seq  26072  dvne0  26340  coeeulem  26552  radcnvlt1  26754  argimgt0  26949  cxple2  27034  ressatans  27271  eldmgm  27358  basellem2  27418  issqf  27472  bpos1  27619  bposlem3  27622  bposlem6  27625  2sqreulem1  27782  2sqreunnlem1  27785  pntpbnd2  27923  ostth2lem4  27972  crctcshwlkn0  30419  crctcsh  30422  eucrctshift  30853  ltflcei  38640  poimirlem4  38651  poimirlem13  38660  poimirlem14  38661  poimirlem15  38662  poimirlem31  38678  mblfinlem1  38684  mbfposadd  38694  itgaddnclem2  38706  ftc1anclem1  38720  ftc1anclem5  38724  dvasin  38731  reabsifnpos  44742  reabsifnneg  44744  icccncfext  47005  stoweidlem14  47132  stoweidlem34  47152  ltnltne  48477  nnsum4primeseven  49006  nnsum4primesevenALTV  49007  ply1mulgsumlem2  49607