Theorem ltnle 10117

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∈ wcel 1990   class class class wbr 4653  ℝcr 9935   < clt 10074   ≤ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-xp 5120  df-cnv 5122  df-xr 10078  df-le 10080

This theorem is referenced by:  letric  10137  ltnled  10184  leaddsub  10504  mulge0b  10893  nnnle0  11051  nn0n0n1ge2b  11359  znnnlt1  11404  uzwo  11751  qsqueeze  12032  difreicc  12304  fzp1disj  12399  fzneuz  12421  fznuz  12422  uznfz  12423  difelfznle  12453  nelfzo  12475  ssfzoulel  12562  elfzonelfzo  12570  modfzo0difsn  12742  ssnn0fi  12784  discr1  13000  facdiv  13074  bcval5  13105  ccatsymb  13366  swrdnd  13432  swrdsbslen  13448  swrdspsleq  13449  swrdccat3  13492  repswswrd  13531  cnpart  13980  absmax  14069  rlimrege0  14310  znnenlem  14940  rpnnen2lem12  14954  alzdvds  15042  algcvgblem  15290  prmndvdsfaclt  15435  pcprendvds  15545  pcdvdsb  15573  pcmpt  15596  prmunb  15618  prmreclem2  15621  prmgaplem5  15759  prmgaplem6  15760  prmlem1  15814  prmlem2  15827  lt6abl  18296  metdseq0  22657  xrhmeo  22745  ovolicc2lem3  23287  itg2seq  23509  dvne0  23774  coeeulem  23980  radcnvlt1  24172  argimgt0  24358  cxple2  24443  ressatans  24661  eldmgm  24748  basellem2  24808  issqf  24862  bpos1  25008  bposlem3  25011  bposlem6  25014  pntpbnd2  25276  ostth2lem4  25325  crctcshwlkn0  26713  crctcsh  26716  eucrctshift  27103  ltflcei  33397  poimirlem4  33413  poimirlem13  33422  poimirlem14  33423  poimirlem15  33424  poimirlem31  33440  mblfinlem1  33446  mbfposadd  33457  itgaddnclem2  33469  ftc1anclem1  33485  ftc1anclem5  33489  dvasin  33496  icccncfext  40100  stoweidlem14  40231  stoweidlem34  40251  ltnltne  41313  pfxccat3  41426  pfxccat3a  41429  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  ply1mulgsumlem2  42175