Theorem fzoval 13818

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 7447	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7459	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13813	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7473	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7596	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 488	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13814	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6740	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7626	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 488	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13667	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6740	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7626	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 160	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2801	. . 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 2147  ∅c0 4281  𝒫 cpw 4560   × cxp 5653  (class class class)co 7440  1c1 11225   − cmin 11565  ℤcz 12717  ...cfz 13663  ..^cfzo 13812

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772  ax-cnex 11280  ax-resscn 11281

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-fv 6563  df-ov 7443  df-oprab 7444  df-mpo 7445  df-1st 8022  df-2nd 8023  df-neg 11568  df-z 12718  df-uz 12990  df-fz 13664  df-fzo 13813

This theorem is used by:  elfzo  13819  fzon  13839  fzoss1  13845  fzoss2  13846  elfzolem1  13863  fz1fzo0m1  13869  fzval3  13893  fzo13pr  13908  fzo0to2pr  13909  fzo0to3tp  13911  fzo0to42pr  13912  fzo1to4tp  13913  fzoend  13916  fzofzp1b  13924  elfzom1b  13925  peano2fzor  13934  fzoshftral  13946  zmodfzo  14058  zmodidfzo  14064  fzofi  14141  hashfzo  14598  wrdffz  14704  revcl  14935  revlen  14936  revccat  14940  revrev  14941  revco  15010  fzosump1  15944  telfsumo  15995  fsumparts  15999  geoser  16062  pwdif  16063  pwm1geoser  16064  geo2sum2  16069  dfphi2  16977  reumodprminv  17008  gsumwsubmcl  19059  gsumsgrpccat  19062  gsumwmhm  19067  efgsdmi  19973  efgs1b  19977  efgredlemf  19982  efgredlemd  19985  efgredlemc  19986  efgredlem  19988  cpmadugsumlemF  23221  advlogexp  27010  dchrisumlem1  27843  redwlklem  30277  pthhashvtx  30342  wlkiswwlks2lem3  30487  wlkiswwlksupgr2  30493  clwlkclwwlklem2a  30616  wlk2v2e  30785  eucrct2eupth  30873  gsummulsubdishift1  33696  cycpmco2  33761  submat1n  34504  eulerpartlemd  35065  fzssfzo  35238  signstfvn  35265  remexz  43345  fzosumm1  43492  bccbc  45519  monoords  46516  stirlinglem12  47298  difltmodne  48621  muldvdsfacm1  48660  iccpartiltu  48707  iccpartigtl  48708  iccpartgt  48712  nprmmul1  48812  nnsum4primeseven  49101  nnsum4primesevenALTV  49102  nn0sumshdiglemA  49934  nn0sumshdiglemB  49935