Theorem fzoval 13580

Description: Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015.)

Assertion

Ref	Expression
fzoval	⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Proof of Theorem fzoval

Dummy variables 𝑚 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 22	. . . 4 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
2		oveq1 7367	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7379	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13575	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7393	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7515	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13576	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6674	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7544	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13431	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6674	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7544	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2775	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 480	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 812	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∅c0 4286  𝒫 cpw 4555   × cxp 5623  (class class class)co 7360  1c1 11031   − cmin 11368  ℤcz 12492  ...cfz 13427  ..^cfzo 13574

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378  ax-un 7682  ax-cnex 11086  ax-resscn 11087

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-iun 4949  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-neg 11371  df-z 12493  df-uz 12756  df-fz 13428  df-fzo 13575

This theorem is referenced by:  elfzo  13581  fzon  13600  fzoss1  13606  fzoss2  13607  elfzolem1  13624  fz1fzo0m1  13630  fzval3  13654  fzo13pr  13669  fzo0to2pr  13670  fzo0to3tp  13672  fzo0to42pr  13673  fzo1to4tp  13674  fzoend  13677  fzofzp1b  13685  elfzom1b  13686  peano2fzor  13695  fzoshftral  13707  zmodfzo  13818  zmodidfzo  13824  fzofi  13901  hashfzo  14356  wrdffz  14462  revcl  14688  revlen  14689  revccat  14693  revrev  14694  revco  14761  fzosump1  15679  telfsumo  15729  fsumparts  15733  geoser  15794  pwdif  15795  pwm1geoser  15796  geo2sum2  15801  dfphi2  16705  reumodprminv  16736  gsumwsubmcl  18766  gsumsgrpccat  18769  gsumwmhm  18774  efgsdmi  19665  efgs1b  19669  efgredlemf  19674  efgredlemd  19677  efgredlemc  19678  efgredlem  19680  cpmadugsumlemF  22824  advlogexp  26624  dchrisumlem1  27460  redwlklem  29747  wlkiswwlks2lem3  29948  wlkiswwlksupgr2  29954  clwlkclwwlklem2a  30077  wlk2v2e  30236  eucrct2eupth  30324  gsummulsubdishift1  33153  cycpmco2  33217  submat1n  33964  eulerpartlemd  34525  fzssfzo  34698  signstfvn  34728  pthhashvtx  35324  remexz  42426  fzosumm1  42572  bccbc  44653  monoords  45612  stirlinglem12  46396  difltmodne  47655  iccpartiltu  47735  iccpartigtl  47736  iccpartgt  47740  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  nn0sumshdiglemA  48932  nn0sumshdiglemB  48933