Theorem ltnle 11229

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-xp 5637  df-cnv 5639  df-xr 11188  df-le 11190

This theorem is referenced by:  letric  11250  ltnled  11297  leaddsub  11630  mulge0b  12029  nnnle0  12195  nn0n0n1ge2b  12487  znnnlt1  12536  uzwo  12846  qsqueeze  13137  difreicc  13421  fzp1disj  13520  fzneuz  13545  fznuz  13546  uznfz  13547  difelfznle  13579  nelfzo  13601  ssfzoulel  13697  elfzonelfzo  13706  modfzo0difsn  13884  ssnn0fi  13926  discr1  14180  bcval5  14259  swrdnd  14595  swrdnnn0nd  14597  swrdnd0  14598  swrdsbslen  14605  swrdspsleq  14606  pfxnd0  14629  pfxccat3  14675  swrdccat  14676  pfxccat3a  14679  repswswrd  14725  cnpart  15182  absmax  15272  rlimrege0  15521  rpnnen2lem12  16169  alzdvds  16266  algcvgblem  16523  prmndvdsfaclt  16671  pcprendvds  16787  pcdvdsb  16816  pcmpt  16839  prmunb  16861  prmreclem2  16864  prmgaplem5  17002  prmgaplem6  17003  prmlem1  17054  prmlem2  17066  lt6abl  19801  metdseq0  24719  xrhmeo  24820  ovolicc2lem3  25396  itg2seq  25619  dvne0  25892  coeeulem  26105  radcnvlt1  26303  argimgt0  26497  cxple2  26582  ressatans  26820  eldmgm  26908  basellem2  26968  issqf  27022  bpos1  27170  bposlem3  27173  bposlem6  27176  2sqreulem1  27333  2sqreunnlem1  27336  pntpbnd2  27474  ostth2lem4  27523  crctcshwlkn0  29724  crctcsh  29727  eucrctshift  30145  ltflcei  37575  poimirlem4  37591  poimirlem13  37600  poimirlem14  37601  poimirlem15  37602  poimirlem31  37618  mblfinlem1  37624  mbfposadd  37634  itgaddnclem2  37646  ftc1anclem1  37660  ftc1anclem5  37664  dvasin  37671  reabsifnpos  43595  reabsifnneg  43597  icccncfext  45858  stoweidlem14  45985  stoweidlem34  46005  ltnltne  47273  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  ply1mulgsumlem2  48349