Theorem fzoval 12298

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 6534	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 6546	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 12293	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 6555	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpt2a 6667	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 472	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8	7	con3i 149	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		fzof 12294	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
10	9	fdmi 5951	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
11	10	ndmov 6694	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
12	8, 11	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
13		simpl 472	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
14	13	con3i 149	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
15		fzf 12159	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
16	15	fdmi 5951	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
17	16	ndmov 6694	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
18	14, 17	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
19	12, 18	eqtr4d 2647	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
20	19	adantr 480	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
21	6, 20	pm2.61ian 827	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∅c0 3874  𝒫 cpw 4108   × cxp 5026  (class class class)co 6527  1c1 9794   − cmin 10118  ℤcz 11213  ...cfz 12155  ..^cfzo 12292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4704  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4368  df-iun 4452  df-br 4579  df-opab 4639  df-mpt 4640  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-fv 5798  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-1st 7037  df-2nd 7038  df-neg 10121  df-z 11214  df-uz 11523  df-fz 12156  df-fzo 12293

This theorem is referenced by:  elfzo  12299  fzon  12316  fzoss1  12322  fzoss2  12323  fz1fzo0m1  12341  fzval3  12362  fzo13pr  12377  fzo0to2pr  12378  fzo0to3tp  12379  fzo0to42pr  12380  fzo1to4tp  12381  fzoend  12383  fzofzp1b  12390  elfzom1b  12391  peano2fzor  12399  fzoshftral  12405  zmodfzo  12513  zmodidfzo  12519  fzofi  12593  hashfzo  13031  wrdffz  13130  revcl  13310  revlen  13311  revccat  13315  revrev  13316  revco  13380  fzosump1  14274  telfsumo  14324  fsumparts  14328  geoser  14387  geo2sum2  14393  dfphi2  15266  reumodprminv  15296  gsumwsubmcl  17147  gsumccat  17150  gsumwmhm  17154  efgsdmi  17917  efgs1b  17921  efgredlemf  17926  efgredlemd  17929  efgredlemc  17930  efgredlem  17932  cpmadugsumlemF  20448  advlogexp  24146  dchrisumlem1  24923  wlkntrllem2  25884  redwlk  25930  constr3pthlem1  25977  constr3pthlem3  25979  wlkiswwlk2lem3  26015  clwlkisclwwlklem2a  26107  submat1n  28993  eulerpartlemd  29549  fzssfzo  29734  signstfvn  29766  bccbc  37360  monoords  38246  elfzolem1  38272  stirlinglem12  38772  iccpartiltu  39755  iccpartigtl  39756  iccpartgt  39760  pwdif  39834  pwm1geoserALT  39835  nnsum4primeseven  40011  nnsum4primesevenALTV  40012  red1wlklem  40872  1wlkiswwlks2lem3  41060  1wlkiswwlksupgr2  41066  clwlkclwwlklem2a  41199  1wlk2v2e  41316  eucrct2eupth  41405  nn0sumshdiglemA  42203  nn0sumshdiglemB  42204