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

Theorem fzdisj 13144
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 3887 . . . 4 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) ↔ (𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)))
2 elfzel1 13116 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
32adantl 485 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
43zred 12287 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ)
5 elfzel2 13115 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝐾 ∈ ℤ)
65adantr 484 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
76zred 12287 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℝ)
8 elfzelz 13117 . . . . . . . 8 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
98zred 12287 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
109adantl 485 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
11 elfzle1 13120 . . . . . . 7 (𝑥 ∈ (𝑀...𝑁) → 𝑀𝑥)
1211adantl 485 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝑥)
13 elfzle2 13121 . . . . . . 7 (𝑥 ∈ (𝐽...𝐾) → 𝑥𝐾)
1413adantr 484 . . . . . 6 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥𝐾)
154, 10, 7, 12, 14letrd 10994 . . . . 5 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀𝐾)
164, 7, 15lensymd 10988 . . . 4 ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
171, 16sylbi 220 . . 3 (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
1817con2i 141 . 2 (𝐾 < 𝑀 → ¬ 𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)))
1918eq0rdv 4324 1 (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1543  wcel 2110  cin 3870  c0 4242   class class class wbr 5058  (class class class)co 7218  cr 10733   < clt 10872  cle 10873  cz 12181  ...cfz 13100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-pre-lttri 10808  ax-pre-lttrn 10809
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-ov 7221  df-oprab 7222  df-mpo 7223  df-1st 7766  df-2nd 7767  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-neg 11070  df-z 12182  df-uz 12444  df-fz 13101
This theorem is referenced by:  fsumm1  15320  fsum1p  15322  o1fsum  15382  climcndslem1  15418  climcndslem2  15419  mertenslem1  15453  fprod1p  15535  fprodeq0  15542  fallfacval4  15610  prmreclem5  16478  strleun  16715  uniioombllem3  24487  mtest  25301  birthdaylem2  25840  fsumharmonic  25899  ftalem5  25964  chtdif  26045  ppidif  26050  gausslemma2dlem4  26255  gausslemma2dlem6  26258  lgsquadlem2  26267  dchrisum0lem1b  26401  dchrisum0lem3  26405  pntrsumbnd2  26453  pntrlog2bndlem6  26469  pntpbnd2  26473  pntlemf  26491  axlowdimlem2  27039  axlowdimlem16  27053  esumpmono  31764  ballotlemfrceq  32212  fsum2dsub  32304  poimirlem1  35520  poimirlem2  35521  poimirlem3  35522  poimirlem4  35523  poimirlem6  35525  poimirlem7  35526  poimirlem11  35530  poimirlem12  35531  poimirlem16  35535  poimirlem17  35536  poimirlem19  35538  poimirlem20  35539  poimirlem23  35542  poimirlem24  35543  poimirlem25  35544  poimirlem28  35547  poimirlem29  35548  poimirlem31  35550  sticksstones6  39837  sticksstones7  39838  metakunt18  39872  metakunt20  39874  prodsplit  39891  eldioph2lem1  40293  stoweidlem11  43235
  Copyright terms: Public domain W3C validator