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

Theorem fzdisj 13535
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 3964 . . . 4 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) ↔ (𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)))
2 elfzel1 13507 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
32adantl 481 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
43zred 12673 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ)
5 elfzel2 13506 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝐾 ∈ ℤ)
65adantr 480 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
76zred 12673 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℝ)
8 elfzelz 13508 . . . . . . . 8 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
98zred 12673 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
109adantl 481 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
11 elfzle1 13511 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀𝑥)
1211adantl 481 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝑥)
13 elfzle2 13512 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝑥𝐾)
1413adantr 480 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥𝐾)
154, 10, 7, 12, 14letrd 11378 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝐾)
164, 7, 15lensymd 11372 . . . 4 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
171, 16sylbi 216 . . 3 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
1817con2i 139 . 2 (𝐾 < 𝑀 → ¬ 𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)))
1918eq0rdv 4404 1 (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395   = wceq 1540  wcel 2105  cin 3947  c0 4322   class class class wbr 5148  (class class class)co 7412  cr 11115   < clt 11255  cle 11256  cz 12565  ...cfz 13491
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-pre-lttri 11190  ax-pre-lttrn 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-neg 11454  df-z 12566  df-uz 12830  df-fz 13492
This theorem is referenced by:  fsumm1  15704  fsum1p  15706  o1fsum  15766  climcndslem1  15802  climcndslem2  15803  mertenslem1  15837  fprod1p  15919  fprodeq0  15926  fallfacval4  15994  prmreclem5  16860  strleun  17097  uniioombllem3  25347  mtest  26166  birthdaylem2  26708  fsumharmonic  26767  ftalem5  26832  chtdif  26913  ppidif  26918  gausslemma2dlem4  27123  gausslemma2dlem6  27126  lgsquadlem2  27135  dchrisum0lem1b  27269  dchrisum0lem3  27273  pntrsumbnd2  27321  pntrlog2bndlem6  27337  pntpbnd2  27341  pntlemf  27359  axlowdimlem2  28483  axlowdimlem16  28497  esumpmono  33390  ballotlemfrceq  33840  fsum2dsub  33932  poimirlem1  36805  poimirlem2  36806  poimirlem3  36807  poimirlem4  36808  poimirlem6  36810  poimirlem7  36811  poimirlem11  36815  poimirlem12  36816  poimirlem16  36820  poimirlem17  36821  poimirlem19  36823  poimirlem20  36824  poimirlem23  36827  poimirlem24  36828  poimirlem25  36829  poimirlem28  36832  poimirlem29  36833  poimirlem31  36835  sticksstones6  41286  sticksstones7  41287  metakunt18  41321  metakunt20  41323  prodsplit  41340  sumcubes  41526  eldioph2lem1  41813  stoweidlem11  45038
  Copyright terms: Public domain W3C validator