Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fzdisj | Structured version Visualization version GIF version |
Description: Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010.) |
Ref | Expression |
---|---|
fzdisj | ⊢ (𝐾 < 𝑀 → ((𝐽...𝐾) ∩ (𝑀...𝑁)) = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3887 | . . . 4 ⊢ (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) ↔ (𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁))) | |
2 | elfzel1 13116 | . . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑀 ∈ ℤ) | |
3 | 2 | adantl 485 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℤ) |
4 | 3 | zred 12287 | . . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ∈ ℝ) |
5 | elfzel2 13115 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐽...𝐾) → 𝐾 ∈ ℤ) | |
6 | 5 | adantr 484 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℤ) |
7 | 6 | zred 12287 | . . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝐾 ∈ ℝ) |
8 | elfzelz 13117 | . . . . . . . 8 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℤ) | |
9 | 8 | zred 12287 | . . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑥 ∈ ℝ) |
10 | 9 | adantl 485 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ∈ ℝ) |
11 | elfzle1 13120 | . . . . . . 7 ⊢ (𝑥 ∈ (𝑀...𝑁) → 𝑀 ≤ 𝑥) | |
12 | 11 | adantl 485 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝑥) |
13 | elfzle2 13121 | . . . . . . 7 ⊢ (𝑥 ∈ (𝐽...𝐾) → 𝑥 ≤ 𝐾) | |
14 | 13 | adantr 484 | . . . . . 6 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑥 ≤ 𝐾) |
15 | 4, 10, 7, 12, 14 | letrd 10994 | . . . . 5 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → 𝑀 ≤ 𝐾) |
16 | 4, 7, 15 | lensymd 10988 | . . . 4 ⊢ ((𝑥 ∈ (𝐽...𝐾) ∧ 𝑥 ∈ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀) |
17 | 1, 16 | sylbi 220 | . . 3 ⊢ (𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁)) → ¬ 𝐾 < 𝑀) |
18 | 17 | con2i 141 | . 2 ⊢ (𝐾 < 𝑀 → ¬ 𝑥 ∈ ((𝐽...𝐾) ∩ (𝑀...𝑁))) |
19 | 18 | eq0rdv 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 |