Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzdisj Structured version   Visualization version   GIF version

Theorem fzdisj 12918
 Description: Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.)
Assertion
Ref Expression
fzdisj (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)

Proof of Theorem fzdisj
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elin 3929 . . . 4 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) ↔ (𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)))
2 elfzel1 12891 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
32adantl 484 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
43zred 12066 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ)
5 elfzel2 12890 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝐾 ∈ ℤ)
65adantr 483 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
76zred 12066 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℝ)
8 elfzelz 12892 . . . . . . . 8 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
98zred 12066 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
109adantl 484 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
11 elfzle1 12894 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀𝑥)
1211adantl 484 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝑥)
13 elfzle2 12895 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝑥𝐾)
1413adantr 483 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥𝐾)
154, 10, 7, 12, 14letrd 10775 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝐾)
164, 7, 15lensymd 10769 . . . 4 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
171, 16sylbi 219 . . 3 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
1817con2i 141 . 2 (𝐾 < 𝑀 → ¬ 𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)))
1918eq0rdv 4333 1 (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114   ∩ cin 3912  ∅c0 4269   class class class wbr 5042  (class class class)co 7133  ℝcr 10514   < clt 10653   ≤ cle 10654  ℤcz 11960  ...cfz 12876 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572  ax-pre-lttri 10589  ax-pre-lttrn 10590 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-1st 7667  df-2nd 7668  df-er 8267  df-en 8488  df-dom 8489  df-sdom 8490  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-neg 10851  df-z 11961  df-uz 12223  df-fz 12877 This theorem is referenced by:  fsumm1  15086  fsum1p  15088  o1fsum  15148  climcndslem1  15184  climcndslem2  15185  mertenslem1  15220  fprod1p  15302  fprodeq0  15309  fallfacval4  15377  prmreclem5  16234  strleun  16570  uniioombllem3  24168  mtest  24978  birthdaylem2  25517  fsumharmonic  25576  ftalem5  25641  chtdif  25722  ppidif  25727  gausslemma2dlem4  25932  gausslemma2dlem6  25935  lgsquadlem2  25944  dchrisum0lem1b  26078  dchrisum0lem3  26082  pntrsumbnd2  26130  pntrlog2bndlem6  26146  pntpbnd2  26150  pntlemf  26168  axlowdimlem2  26716  axlowdimlem16  26730  esumpmono  31346  ballotlemfrceq  31794  fsum2dsub  31886  poimirlem1  34934  poimirlem2  34935  poimirlem3  34936  poimirlem4  34937  poimirlem6  34939  poimirlem7  34940  poimirlem11  34944  poimirlem12  34945  poimirlem16  34949  poimirlem17  34950  poimirlem19  34952  poimirlem20  34953  poimirlem23  34956  poimirlem24  34957  poimirlem25  34958  poimirlem28  34961  poimirlem29  34962  poimirlem31  34964  prodsplit  39208  eldioph2lem1  39494  stoweidlem11  42444
 Copyright terms: Public domain W3C validator