Theorem fzoval 12848

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 6977	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 6989	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 12843	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7002	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7115	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 475	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8	7	con3i 152	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		fzof 12844	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
10	9	fdmi 6348	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
11	10	ndmov 7142	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
12	8, 11	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
13		simpl 475	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
14	13	con3i 152	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
15		fzf 12705	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
16	15	fdmi 6348	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
17	16	ndmov 7142	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
18	14, 17	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
19	12, 18	eqtr4d 2811	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
20	19	adantr 473	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
21	6, 20	pm2.61ian 799	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2048  ∅c0 4173  𝒫 cpw 4416   × cxp 5398  (class class class)co 6970  1c1 10328   − cmin 10662  ℤcz 11786  ...cfz 12701  ..^cfzo 12842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5305  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-fv 6190  df-ov 6973  df-oprab 6974  df-mpo 6975  df-1st 7494  df-2nd 7495  df-neg 10665  df-z 11787  df-uz 12052  df-fz 12702  df-fzo 12843

This theorem is referenced by:  elfzo  12849  fzon  12866  fzoss1  12872  fzoss2  12873  fz1fzo0m1  12893  fzval3  12914  fzo13pr  12929  fzo0to2pr  12930  fzo0to3tp  12931  fzo0to42pr  12932  fzo1to4tp  12933  fzoend  12936  fzofzp1b  12943  elfzom1b  12944  peano2fzor  12952  fzoshftral  12962  zmodfzo  13070  zmodidfzo  13076  fzofi  13150  hashfzo  13593  wrdffz  13686  revcl  13970  revlen  13971  revccat  13975  revrev  13976  revco  14048  fzosump1  14957  telfsumo  15007  fsumparts  15011  geoser  15072  pwdif  15073  pwm1geoser  15074  geo2sum2  15080  dfphi2  15957  reumodprminv  15987  gsumwsubmcl  17833  gsumccat  17836  gsumwmhm  17841  efgsdmi  18606  efgs1b  18610  efgredlemf  18616  efgredlemd  18619  efgredlemc  18620  efgredlem  18622  efgredlemOLD  18623  cpmadugsumlemF  21178  advlogexp  24929  dchrisumlem1  25757  redwlklem  27149  wlkiswwlks2lem3  27347  wlkiswwlksupgr2  27353  clwlkclwwlklem2a  27494  wlk2v2e  27676  eucrct2eupthOLD  27766  eucrct2eupth  27767  submat1n  30669  eulerpartlemd  31226  fzssfzo  31412  signstfvn  31446  fzosumm1  38516  bccbc  40037  monoords  40939  elfzolem1  40964  stirlinglem12  41747  iccpartiltu  42900  iccpartigtl  42901  iccpartgt  42905  nnsum4primeseven  43273  nnsum4primesevenALTV  43274  nn0sumshdiglemA  43987  nn0sumshdiglemB  43988