![]() |
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 7358 | . . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1)) | |
3 | 1, 2 | oveqan12d 7370 | . . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1))) |
4 | df-fzo 13522 | . . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1))) | |
5 | ovex 7384 | . . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V | |
6 | 3, 4, 5 | ovmpoa 7504 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
7 | simpl 483 | . . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ) | |
8 | fzof 13523 | . . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ | |
9 | 8 | fdmi 6677 | . . . . . 6 ⊢ dom ..^ = (ℤ × ℤ) |
10 | 9 | ndmov 7532 | . . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅) |
11 | 7, 10 | nsyl5 159 | . . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅) |
12 | simpl 483 | . . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ) | |
13 | fzf 13382 | . . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ | |
14 | 13 | fdmi 6677 | . . . . . 6 ⊢ dom ... = (ℤ × ℤ) |
15 | 14 | ndmov 7532 | . . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅) |
16 | 12, 15 | nsyl5 159 | . . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅) |
17 | 11, 16 | eqtr4d 2780 | . . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
18 | 17 | adantr 481 | . 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
19 | 6, 18 | pm2.61ian 810 | 1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ∅c0 4280 𝒫 cpw 4558 × cxp 5629 (class class class)co 7351 1c1 11010 − cmin 11343 ℤcz 12457 ...cfz 13378 ..^cfzo 13521 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2708 ax-sep 5254 ax-nul 5261 ax-pr 5382 ax-un 7664 ax-cnex 11065 ax-resscn 11066 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rab 3406 df-v 3445 df-sbc 3738 df-csb 3854 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4281 df-if 4485 df-pw 4560 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4864 df-iun 4954 df-br 5104 df-opab 5166 df-mpt 5187 df-id 5529 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6445 df-fun 6495 df-fn 6496 df-f 6497 df-fv 6501 df-ov 7354 df-oprab 7355 df-mpo 7356 df-1st 7913 df-2nd 7914 df-neg 11346 df-z 12458 df-uz 12722 df-fz 13379 df-fzo 13522 |
This theorem is referenced by: elfzo 13528 fzon 13547 fzoss1 13553 fzoss2 13554 fz1fzo0m1 13574 fzval3 13595 fzo13pr 13610 fzo0to2pr 13611 fzo0to3tp 13612 fzo0to42pr 13613 fzo1to4tp 13614 fzoend 13617 fzofzp1b 13624 elfzom1b 13625 peano2fzor 13633 fzoshftral 13643 zmodfzo 13753 zmodidfzo 13759 fzofi 13833 hashfzo 14283 wrdffz 14377 revcl 14607 revlen 14608 revccat 14612 revrev 14613 revco 14681 fzosump1 15597 telfsumo 15647 fsumparts 15651 geoser 15712 pwdif 15713 pwm1geoser 15714 geo2sum2 15719 dfphi2 16606 reumodprminv 16636 gsumwsubmcl 18607 gsumsgrpccat 18610 gsumwmhm 18615 efgsdmi 19473 efgs1b 19477 efgredlemf 19482 efgredlemd 19485 efgredlemc 19486 efgredlem 19488 cpmadugsumlemF 22177 advlogexp 25962 dchrisumlem1 26789 redwlklem 28448 wlkiswwlks2lem3 28645 wlkiswwlksupgr2 28651 clwlkclwwlklem2a 28771 wlk2v2e 28930 eucrct2eupth 29018 cycpmco2 31808 submat1n 32198 eulerpartlemd 32778 fzssfzo 32963 signstfvn 32993 pthhashvtx 33533 metakunt20 40534 fzosumm1 40603 bccbc 42536 monoords 43436 elfzolem1 43460 stirlinglem12 44227 iccpartiltu 45515 iccpartigtl 45516 iccpartgt 45520 nnsum4primeseven 45893 nnsum4primesevenALTV 45894 nn0sumshdiglemA 46606 nn0sumshdiglemB 46607 |
Copyright terms: Public domain | W3C validator |