![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fzoval | Structured version Visualization version GIF version |
Description: Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.) |
Ref | Expression |
---|---|
fzoval | ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . . 4 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀) | |
2 | oveq1 6697 | . . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) | |
3 | 1, 2 | oveqan12d 6709 | . . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1))) |
4 | df-fzo 12505 | . . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | |
5 | ovex 6718 | . . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V | |
6 | 3, 4, 5 | ovmpt2a 6833 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
7 | simpl 472 | . . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ) | |
8 | 7 | con3i 150 | . . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) |
9 | fzof 12506 | . . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | |
10 | 9 | fdmi 6090 | . . . . . 6 ⊢ dom ..^ = (ℤ × ℤ) |
11 | 10 | ndmov 6860 | . . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅) |
12 | 8, 11 | syl 17 | . . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅) |
13 | simpl 472 | . . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ) | |
14 | 13 | con3i 150 | . . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ)) |
15 | fzf 12368 | . . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ | |
16 | 15 | fdmi 6090 | . . . . . 6 ⊢ dom ... = (ℤ × ℤ) |
17 | 16 | ndmov 6860 | . . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅) |
18 | 14, 17 | syl 17 | . . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅) |
19 | 12, 18 | eqtr4d 2688 | . . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
20 | 19 | adantr 480 | . 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
21 | 6, 20 | pm2.61ian 848 | 1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 = wceq 1523 ∈ wcel 2030 ∅c0 3948 𝒫 cpw 4191 × cxp 5141 (class class class)co 6690 1c1 9975 − cmin 10304 ℤcz 11415 ...cfz 12364 ..^cfzo 12504 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 ax-cnex 10030 ax-resscn 10031 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1055 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-csb 3567 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-iun 4554 df-br 4686 df-opab 4746 df-mpt 4763 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-rn 5154 df-res 5155 df-ima 5156 df-iota 5889 df-fun 5928 df-fn 5929 df-f 5930 df-fv 5934 df-ov 6693 df-oprab 6694 df-mpt2 6695 df-1st 7210 df-2nd 7211 df-neg 10307 df-z 11416 df-uz 11726 df-fz 12365 df-fzo 12505 |
This theorem is referenced by: elfzo 12511 fzon 12528 fzoss1 12534 fzoss2 12535 fz1fzo0m1 12555 fzval3 12576 fzo13pr 12592 fzo0to2pr 12593 fzo0to3tp 12594 fzo0to42pr 12595 fzo1to4tp 12596 fzoend 12599 fzofzp1b 12606 elfzom1b 12607 peano2fzor 12615 fzoshftral 12625 zmodfzo 12733 zmodidfzo 12739 fzofi 12813 hashfzo 13254 wrdffz 13358 revcl 13556 revlen 13557 revccat 13561 revrev 13562 revco 13626 fzosump1 14525 telfsumo 14578 fsumparts 14582 geoser 14643 geo2sum2 14649 dfphi2 15526 reumodprminv 15556 gsumwsubmcl 17422 gsumccat 17425 gsumwmhm 17429 efgsdmi 18191 efgs1b 18195 efgredlemf 18200 efgredlemd 18203 efgredlemc 18204 efgredlem 18206 cpmadugsumlemF 20729 advlogexp 24446 dchrisumlem1 25223 redwlklem 26624 wlkiswwlks2lem3 26825 wlkiswwlksupgr2 26831 clwlkclwwlklem2a 26964 wlk2v2e 27135 eucrct2eupth 27223 submat1n 29999 eulerpartlemd 30556 fzssfzo 30741 signstfvn 30774 bccbc 38861 monoords 39825 elfzolem1 39850 stirlinglem12 40620 iccpartiltu 41683 iccpartigtl 41684 iccpartgt 41688 pwdif 41826 pwm1geoserALT 41827 nnsum4primeseven 42013 nnsum4primesevenALTV 42014 nn0sumshdiglemA 42738 nn0sumshdiglemB 42739 |
Copyright terms: Public domain | W3C validator |