Theorem ltnle 11216

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-xr 11174  df-le 11176

This theorem is referenced by:  letric  11237  ltnled  11284  leaddsub  11617  mulge0b  12017  nnnle0  12201  nn0n0n1ge2b  12497  znnnlt1  12545  uzwo  12852  qsqueeze  13144  difreicc  13428  fzp1disj  13528  fzneuz  13553  fznuz  13554  uznfz  13555  difelfznle  13587  nelfzo  13610  ssfzoulel  13706  elfzonelfzo  13715  modfzo0difsn  13896  ssnn0fi  13938  discr1  14192  bcval5  14271  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  swrdsbslen  14618  swrdspsleq  14619  pfxnd0  14642  pfxccat3  14687  swrdccat  14688  pfxccat3a  14691  repswswrd  14737  cnpart  15193  absmax  15283  rlimrege0  15532  rpnnen2lem12  16183  alzdvds  16280  algcvgblem  16537  prmndvdsfaclt  16686  pcprendvds  16802  pcdvdsb  16831  pcmpt  16854  prmunb  16876  prmreclem2  16879  prmgaplem5  17017  prmgaplem6  17018  prmlem1  17069  prmlem2  17081  lt6abl  19861  metdseq0  24838  xrhmeo  24931  ovolicc2lem3  25504  itg2seq  25727  dvne0  25996  coeeulem  26207  radcnvlt1  26401  argimgt0  26594  cxple2  26679  ressatans  26916  eldmgm  27003  basellem2  27063  issqf  27117  bpos1  27264  bposlem3  27267  bposlem6  27270  2sqreulem1  27427  2sqreunnlem1  27430  pntpbnd2  27568  ostth2lem4  27617  crctcshwlkn0  29907  crctcsh  29910  eucrctshift  30331  ltflcei  37975  poimirlem4  37991  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  poimirlem31  38018  mblfinlem1  38024  mbfposadd  38034  itgaddnclem2  38046  ftc1anclem1  38060  ftc1anclem5  38064  dvasin  38071  reabsifnpos  44077  reabsifnneg  44079  icccncfext  46330  stoweidlem14  46457  stoweidlem34  46477  ltnltne  47762  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  ply1mulgsumlem2  48878