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.

Step	Hyp	Ref	Expression
1		elin 3964	. . . 4 ⊢ (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) ↔ (𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)))
2		elfzel1 13507	. . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ)
3	2	adantl 481	. . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ)
4	3	zred 12673	. . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ)
5		elfzel2 13506	. . . . . . 7 ⊢ (𝑥 ∈ (𝐽...𝐾) → 𝐾 ∈ ℤ)
6	5	adantr 480	. . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ)
7	6	zred 12673	. . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℝ)
8		elfzelz 13508	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ)
9	8	zred 12673	. . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ)
10	9	adantl 481	. . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ)
11		elfzle1 13511	. . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑥)
12	11	adantl 481	. . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑥)
13		elfzle2 13512	. . . . . . 7 ⊢ (𝑥 ∈ (𝐽...𝐾) → 𝑥 ≤ 𝐾)
14	13	adantr 480	. . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝐾)
15	4, 10, 7, 12, 14	letrd 11378	. . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝐾)
16	4, 7, 15	lensymd 11372	. . . 4 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
17	1, 16	sylbi 216	. . 3 ⊢ (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀)
18	17	con2i 139	. 2 ⊢ (𝐾 < 𝑀 → ¬ 𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)))
19	18	eq0rdv 4404	1 ⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅)

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