Theorem fzoval 13695

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 23	. . . 4 ⊢ (𝑚 = 𝑀 → 𝑚 = 𝑀)
2		oveq1 7419	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7431	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13690	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7445	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7567	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 487	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13691	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6717	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7596	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 487	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13545	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6717	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7596	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2800	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 485	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 823	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1569   ∈ wcel 2142  ∅c0 4285  𝒫 cpw 4561   × cxp 5658  (class class class)co 7412  1c1 11107   − cmin 11447  ℤcz 12597  ...cfz 13541  ..^cfzo 13689

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734  ax-cnex 11162  ax-resscn 11163

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1103  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-neg 11450  df-z 12598  df-uz 12869  df-fz 13542  df-fzo 13690

This theorem is used by:  elfzo  13696  fzon  13716  fzoss1  13722  fzoss2  13723  elfzolem1  13740  fz1fzo0m1  13746  fzval3  13770  fzo13pr  13785  fzo0to2pr  13786  fzo0to3tp  13788  fzo0to42pr  13789  fzo1to4tp  13790  fzoend  13793  fzofzp1b  13801  elfzom1b  13802  peano2fzor  13811  fzoshftral  13823  zmodfzo  13934  zmodidfzo  13940  fzofi  14017  hashfzo  14473  wrdffz  14579  revcl  14805  revlen  14806  revccat  14810  revrev  14811  revco  14878  fzosump1  15810  telfsumo  15861  fsumparts  15865  geoser  15928  pwdif  15929  pwm1geoser  15930  geo2sum2  15935  dfphi2  16839  reumodprminv  16870  gsumwsubmcl  18902  gsumsgrpccat  18905  gsumwmhm  18910  efgsdmi  19808  efgs1b  19812  efgredlemf  19817  efgredlemd  19820  efgredlemc  19821  efgredlem  19823  cpmadugsumlemF  23044  advlogexp  26831  dchrisumlem1  27664  redwlklem  30030  wlkiswwlks2lem3  30231  wlkiswwlksupgr2  30237  clwlkclwwlklem2a  30360  wlk2v2e  30519  eucrct2eupth  30607  gsummulsubdishift1  33397  cycpmco2  33462  submat1n  34204  eulerpartlemd  34765  fzssfzo  34938  signstfvn  34965  pthhashvtx  35628  remexz  42899  fzosumm1  43046  bccbc  45083  monoords  46044  stirlinglem12  46827  difltmodne  48113  muldvdsfacm1  48152  iccpartiltu  48199  iccpartigtl  48200  iccpartgt  48204  nprmmul1  48304  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  nn0sumshdiglemA  49427  nn0sumshdiglemB  49428