Theorem ltnle 11224

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 11223	. . 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 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

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 5243  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  letric  11245  ltnled  11292  leaddsub  11625  mulge0b  12024  nnnle0  12190  nn0n0n1ge2b  12482  znnnlt1  12530  uzwo  12836  qsqueeze  13128  difreicc  13412  fzp1disj  13511  fzneuz  13536  fznuz  13537  uznfz  13538  difelfznle  13570  nelfzo  13592  ssfzoulel  13688  elfzonelfzo  13697  modfzo0difsn  13878  ssnn0fi  13920  discr1  14174  bcval5  14253  swrdnd  14590  swrdnnn0nd  14592  swrdnd0  14593  swrdsbslen  14600  swrdspsleq  14601  pfxnd0  14624  pfxccat3  14669  swrdccat  14670  pfxccat3a  14673  repswswrd  14719  cnpart  15175  absmax  15265  rlimrege0  15514  rpnnen2lem12  16162  alzdvds  16259  algcvgblem  16516  prmndvdsfaclt  16664  pcprendvds  16780  pcdvdsb  16809  pcmpt  16832  prmunb  16854  prmreclem2  16857  prmgaplem5  16995  prmgaplem6  16996  prmlem1  17047  prmlem2  17059  lt6abl  19836  metdseq0  24811  xrhmeo  24912  ovolicc2lem3  25488  itg2seq  25711  dvne0  25984  coeeulem  26197  radcnvlt1  26395  argimgt0  26589  cxple2  26674  ressatans  26912  eldmgm  27000  basellem2  27060  issqf  27114  bpos1  27262  bposlem3  27265  bposlem6  27268  2sqreulem1  27425  2sqreunnlem1  27428  pntpbnd2  27566  ostth2lem4  27615  crctcshwlkn0  29906  crctcsh  29909  eucrctshift  30330  ltflcei  37859  poimirlem4  37875  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  poimirlem31  37902  mblfinlem1  37908  mbfposadd  37918  itgaddnclem2  37930  ftc1anclem1  37944  ftc1anclem5  37948  dvasin  37955  reabsifnpos  43989  reabsifnneg  43991  icccncfext  46245  stoweidlem14  46372  stoweidlem34  46392  ltnltne  47659  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  ply1mulgsumlem2  48747