Theorem fzoval 13637

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 7418	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7430	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13632	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7444	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7565	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 483	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13633	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6729	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7593	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 483	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13492	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6729	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7593	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2775	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 481	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 810	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∅c0 4322  𝒫 cpw 4602   × cxp 5674  (class class class)co 7411  1c1 11113   − cmin 11448  ℤcz 12562  ...cfz 13488  ..^cfzo 13631

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7727  ax-cnex 11168  ax-resscn 11169

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7977  df-2nd 7978  df-neg 11451  df-z 12563  df-uz 12827  df-fz 13489  df-fzo 13632

This theorem is referenced by:  elfzo  13638  fzon  13657  fzoss1  13663  fzoss2  13664  fz1fzo0m1  13684  fzval3  13705  fzo13pr  13720  fzo0to2pr  13721  fzo0to3tp  13722  fzo0to42pr  13723  fzo1to4tp  13724  fzoend  13727  fzofzp1b  13734  elfzom1b  13735  peano2fzor  13743  fzoshftral  13753  zmodfzo  13863  zmodidfzo  13869  fzofi  13943  hashfzo  14393  wrdffz  14489  revcl  14715  revlen  14716  revccat  14720  revrev  14721  revco  14789  fzosump1  15702  telfsumo  15752  fsumparts  15756  geoser  15817  pwdif  15818  pwm1geoser  15819  geo2sum2  15824  dfphi2  16711  reumodprminv  16741  gsumwsubmcl  18754  gsumsgrpccat  18757  gsumwmhm  18762  efgsdmi  19641  efgs1b  19645  efgredlemf  19650  efgredlemd  19653  efgredlemc  19654  efgredlem  19656  cpmadugsumlemF  22598  advlogexp  26387  dchrisumlem1  27216  redwlklem  29183  wlkiswwlks2lem3  29380  wlkiswwlksupgr2  29386  clwlkclwwlklem2a  29506  wlk2v2e  29665  eucrct2eupth  29753  cycpmco2  32550  submat1n  33071  eulerpartlemd  33651  fzssfzo  33836  signstfvn  33866  pthhashvtx  34404  metakunt20  41310  fzosumm1  41374  bccbc  43406  monoords  44306  elfzolem1  44330  stirlinglem12  45100  iccpartiltu  46389  iccpartigtl  46390  iccpartgt  46394  nnsum4primeseven  46767  nnsum4primesevenALTV  46768  nn0sumshdiglemA  47393  nn0sumshdiglemB  47394