Theorem ltnle 11225

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 11224	. . 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 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-xr 11183  df-le 11185

This theorem is referenced by:  letric  11246  ltnled  11293  leaddsub  11626  mulge0b  12026  nnnle0  12210  nn0n0n1ge2b  12506  znnnlt1  12554  uzwo  12861  qsqueeze  13153  difreicc  13437  fzp1disj  13537  fzneuz  13562  fznuz  13563  uznfz  13564  difelfznle  13596  nelfzo  13619  ssfzoulel  13715  elfzonelfzo  13724  modfzo0difsn  13905  ssnn0fi  13947  discr1  14201  bcval5  14280  swrdnd  14617  swrdnnn0nd  14619  swrdnd0  14620  swrdsbslen  14627  swrdspsleq  14628  pfxnd0  14651  pfxccat3  14696  swrdccat  14697  pfxccat3a  14700  repswswrd  14746  cnpart  15202  absmax  15292  rlimrege0  15541  rpnnen2lem12  16192  alzdvds  16289  algcvgblem  16546  prmndvdsfaclt  16695  pcprendvds  16811  pcdvdsb  16840  pcmpt  16863  prmunb  16885  prmreclem2  16888  prmgaplem5  17026  prmgaplem6  17027  prmlem1  17078  prmlem2  17090  lt6abl  19870  metdseq0  24820  xrhmeo  24913  ovolicc2lem3  25486  itg2seq  25709  dvne0  25978  coeeulem  26189  radcnvlt1  26383  argimgt0  26576  cxple2  26661  ressatans  26898  eldmgm  26985  basellem2  27045  issqf  27099  bpos1  27246  bposlem3  27249  bposlem6  27252  2sqreulem1  27409  2sqreunnlem1  27412  pntpbnd2  27550  ostth2lem4  27599  crctcshwlkn0  29889  crctcsh  29892  eucrctshift  30313  ltflcei  37929  poimirlem4  37945  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem31  37972  mblfinlem1  37978  mbfposadd  37988  itgaddnclem2  38000  ftc1anclem1  38014  ftc1anclem5  38018  dvasin  38025  reabsifnpos  44060  reabsifnneg  44062  icccncfext  46315  stoweidlem14  46442  stoweidlem34  46462  ltnltne  47747  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  ply1mulgsumlem2  48863