Theorem fzoval 13578

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 7365	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7377	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13573	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7391	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7513	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13574	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6672	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7542	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13429	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6672	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7542	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2773	. . 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 4284  𝒫 cpw 4553   × cxp 5621  (class class class)co 7358  1c1 11029   − cmin 11366  ℤcz 12490  ...cfz 13425  ..^cfzo 13572

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-neg 11369  df-z 12491  df-uz 12754  df-fz 13426  df-fzo 13573

This theorem is referenced by:  elfzo  13579  fzon  13598  fzoss1  13604  fzoss2  13605  elfzolem1  13622  fz1fzo0m1  13628  fzval3  13652  fzo13pr  13667  fzo0to2pr  13668  fzo0to3tp  13670  fzo0to42pr  13671  fzo1to4tp  13672  fzoend  13675  fzofzp1b  13683  elfzom1b  13684  peano2fzor  13693  fzoshftral  13705  zmodfzo  13816  zmodidfzo  13822  fzofi  13899  hashfzo  14354  wrdffz  14460  revcl  14686  revlen  14687  revccat  14691  revrev  14692  revco  14759  fzosump1  15677  telfsumo  15727  fsumparts  15731  geoser  15792  pwdif  15793  pwm1geoser  15794  geo2sum2  15799  dfphi2  16703  reumodprminv  16734  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  efgsdmi  19663  efgs1b  19667  efgredlemf  19672  efgredlemd  19675  efgredlemc  19676  efgredlem  19678  cpmadugsumlemF  22822  advlogexp  26622  dchrisumlem1  27458  redwlklem  29724  wlkiswwlks2lem3  29925  wlkiswwlksupgr2  29931  clwlkclwwlklem2a  30054  wlk2v2e  30213  eucrct2eupth  30301  gsummulsubdishift1  33130  cycpmco2  33194  submat1n  33941  eulerpartlemd  34502  fzssfzo  34675  signstfvn  34705  pthhashvtx  35301  remexz  42393  fzosumm1  42542  bccbc  44623  monoords  45582  stirlinglem12  46366  difltmodne  47625  iccpartiltu  47705  iccpartigtl  47706  iccpartgt  47710  nnsum4primeseven  48083  nnsum4primesevenALTV  48084  nn0sumshdiglemA  48902  nn0sumshdiglemB  48903