Theorem fzoval 13633

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 7416	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7428	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13628	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7442	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7563	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 484	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13629	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6730	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7591	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 484	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13488	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6730	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7591	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2776	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 482	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 811	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∅c0 4323  𝒫 cpw 4603   × cxp 5675  (class class class)co 7409  1c1 11111   − cmin 11444  ℤcz 12558  ...cfz 13484  ..^cfzo 13627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-neg 11447  df-z 12559  df-uz 12823  df-fz 13485  df-fzo 13628

This theorem is referenced by:  elfzo  13634  fzon  13653  fzoss1  13659  fzoss2  13660  fz1fzo0m1  13680  fzval3  13701  fzo13pr  13716  fzo0to2pr  13717  fzo0to3tp  13718  fzo0to42pr  13719  fzo1to4tp  13720  fzoend  13723  fzofzp1b  13730  elfzom1b  13731  peano2fzor  13739  fzoshftral  13749  zmodfzo  13859  zmodidfzo  13865  fzofi  13939  hashfzo  14389  wrdffz  14485  revcl  14711  revlen  14712  revccat  14716  revrev  14717  revco  14785  fzosump1  15698  telfsumo  15748  fsumparts  15752  geoser  15813  pwdif  15814  pwm1geoser  15815  geo2sum2  15820  dfphi2  16707  reumodprminv  16737  gsumwsubmcl  18718  gsumsgrpccat  18721  gsumwmhm  18726  efgsdmi  19600  efgs1b  19604  efgredlemf  19609  efgredlemd  19612  efgredlemc  19613  efgredlem  19615  cpmadugsumlemF  22378  advlogexp  26163  dchrisumlem1  26992  redwlklem  28928  wlkiswwlks2lem3  29125  wlkiswwlksupgr2  29131  clwlkclwwlklem2a  29251  wlk2v2e  29410  eucrct2eupth  29498  cycpmco2  32292  submat1n  32785  eulerpartlemd  33365  fzssfzo  33550  signstfvn  33580  pthhashvtx  34118  metakunt20  41004  fzosumm1  41068  bccbc  43104  monoords  44007  elfzolem1  44031  stirlinglem12  44801  iccpartiltu  46090  iccpartigtl  46091  iccpartgt  46095  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  nn0sumshdiglemA  47305  nn0sumshdiglemB  47306