Theorem ltnle 11219

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031   < clt 11173   ≤ cle 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5631  df-cnv 5633  df-xr 11177  df-le 11179

This theorem is referenced by:  letric  11240  ltnled  11287  leaddsub  11620  mulge0b  12020  nnnle0  12204  nn0n0n1ge2b  12500  znnnlt1  12548  uzwo  12855  qsqueeze  13147  difreicc  13431  fzp1disj  13531  fzneuz  13556  fznuz  13557  uznfz  13558  difelfznle  13590  nelfzo  13613  ssfzoulel  13709  elfzonelfzo  13718  modfzo0difsn  13899  ssnn0fi  13941  discr1  14195  bcval5  14274  swrdnd  14611  swrdnnn0nd  14613  swrdnd0  14614  swrdsbslen  14621  swrdspsleq  14622  pfxnd0  14645  pfxccat3  14690  swrdccat  14691  pfxccat3a  14694  repswswrd  14740  cnpart  15196  absmax  15286  rlimrege0  15535  rpnnen2lem12  16186  alzdvds  16283  algcvgblem  16540  prmndvdsfaclt  16689  pcprendvds  16805  pcdvdsb  16834  pcmpt  16857  prmunb  16879  prmreclem2  16882  prmgaplem5  17020  prmgaplem6  17021  prmlem1  17072  prmlem2  17084  lt6abl  19864  metdseq0  24833  xrhmeo  24926  ovolicc2lem3  25499  itg2seq  25722  dvne0  25991  coeeulem  26202  radcnvlt1  26399  argimgt0  26592  cxple2  26677  ressatans  26914  eldmgm  27002  basellem2  27062  issqf  27116  bpos1  27263  bposlem3  27266  bposlem6  27269  2sqreulem1  27426  2sqreunnlem1  27429  pntpbnd2  27567  ostth2lem4  27616  crctcshwlkn0  29907  crctcsh  29910  eucrctshift  30331  ltflcei  37946  poimirlem4  37962  poimirlem13  37971  poimirlem14  37972  poimirlem15  37973  poimirlem31  37989  mblfinlem1  37995  mbfposadd  38005  itgaddnclem2  38017  ftc1anclem1  38031  ftc1anclem5  38035  dvasin  38042  reabsifnpos  44081  reabsifnneg  44083  icccncfext  46336  stoweidlem14  46463  stoweidlem34  46483  ltnltne  47762  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  ply1mulgsumlem2  48878