Theorem fzoval 13748

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 7416	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7428	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13743	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7442	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7564	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 488	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13744	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6710	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7594	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 488	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13598	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6710	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7594	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2798	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 486	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 824	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∅c0 4279  𝒫 cpw 4557   × cxp 5646  (class class class)co 7409  1c1 11158   − cmin 11498  ℤcz 12648  ...cfz 13594  ..^cfzo 13742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7735  ax-cnex 11213  ax-resscn 11214

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7985  df-2nd 7986  df-neg 11501  df-z 12649  df-uz 12921  df-fz 13595  df-fzo 13743

This theorem is used by:  elfzo  13749  fzon  13769  fzoss1  13775  fzoss2  13776  elfzolem1  13793  fz1fzo0m1  13799  fzval3  13823  fzo13pr  13838  fzo0to2pr  13839  fzo0to3tp  13841  fzo0to42pr  13842  fzo1to4tp  13843  fzoend  13846  fzofzp1b  13854  elfzom1b  13855  peano2fzor  13864  fzoshftral  13876  zmodfzo  13988  zmodidfzo  13994  fzofi  14071  hashfzo  14527  wrdffz  14633  revcl  14863  revlen  14864  revccat  14868  revrev  14869  revco  14938  fzosump1  15871  telfsumo  15922  fsumparts  15926  geoser  15989  pwdif  15990  pwm1geoser  15991  geo2sum2  15996  dfphi2  16898  reumodprminv  16929  gsumwsubmcl  18980  gsumsgrpccat  18983  gsumwmhm  18988  efgsdmi  19893  efgs1b  19897  efgredlemf  19902  efgredlemd  19905  efgredlemc  19906  efgredlem  19908  cpmadugsumlemF  23141  advlogexp  26932  dchrisumlem1  27765  redwlklem  30169  pthhashvtx  30234  wlkiswwlks2lem3  30379  wlkiswwlksupgr2  30385  clwlkclwwlklem2a  30508  wlk2v2e  30677  eucrct2eupth  30765  gsummulsubdishift1  33548  cycpmco2  33613  submat1n  34356  eulerpartlemd  34918  fzssfzo  35091  signstfvn  35118  remexz  43068  fzosumm1  43215  bccbc  45267  monoords  46228  stirlinglem12  47011  difltmodne  48334  muldvdsfacm1  48373  iccpartiltu  48420  iccpartigtl  48421  iccpartgt  48425  nprmmul1  48525  nnsum4primeseven  48814  nnsum4primesevenALTV  48815  nn0sumshdiglemA  49647  nn0sumshdiglemB  49648