Theorem ltnle 11343

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394   ∈ wcel 2099   class class class wbr 5153  ℝcr 11157   < clt 11298   ≤ cle 11299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3464  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-br 5154  df-opab 5216  df-xp 5688  df-cnv 5690  df-xr 11302  df-le 11304

This theorem is referenced by:  letric  11364  ltnled  11411  leaddsub  11740  mulge0b  12136  nnnle0  12297  nn0n0n1ge2b  12592  znnnlt1  12641  uzwo  12947  qsqueeze  13234  difreicc  13515  fzp1disj  13614  fzneuz  13636  fznuz  13637  uznfz  13638  difelfznle  13669  nelfzo  13691  ssfzoulel  13780  elfzonelfzo  13789  modfzo0difsn  13963  ssnn0fi  14005  discr1  14256  bcval5  14335  swrdnd  14662  swrdnnn0nd  14664  swrdnd0  14665  swrdsbslen  14672  swrdspsleq  14673  pfxnd0  14696  pfxccat3  14742  swrdccat  14743  pfxccat3a  14746  repswswrd  14792  cnpart  15245  absmax  15334  rlimrege0  15581  rpnnen2lem12  16227  alzdvds  16322  algcvgblem  16578  prmndvdsfaclt  16727  pcprendvds  16842  pcdvdsb  16871  pcmpt  16894  prmunb  16916  prmreclem2  16919  prmgaplem5  17057  prmgaplem6  17058  prmlem1  17110  prmlem2  17122  lt6abl  19893  metdseq0  24861  xrhmeo  24962  ovolicc2lem3  25539  itg2seq  25763  dvne0  26035  coeeulem  26251  radcnvlt1  26447  argimgt0  26639  cxple2  26724  ressatans  26962  eldmgm  27050  basellem2  27110  issqf  27164  bpos1  27312  bposlem3  27315  bposlem6  27318  2sqreulem1  27475  2sqreunnlem1  27478  pntpbnd2  27616  ostth2lem4  27665  crctcshwlkn0  29755  crctcsh  29758  eucrctshift  30176  ltflcei  37309  poimirlem4  37325  poimirlem13  37334  poimirlem14  37335  poimirlem15  37336  poimirlem31  37352  mblfinlem1  37358  mbfposadd  37368  itgaddnclem2  37380  ftc1anclem1  37394  ftc1anclem5  37398  dvasin  37405  reabsifnpos  43300  reabsifnneg  43302  icccncfext  45508  stoweidlem14  45635  stoweidlem34  45655  ltnltne  46912  nnsum4primeseven  47372  nnsum4primesevenALTV  47373  ply1mulgsumlem2  47770