Theorem fzoval 13621

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 7394	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7406	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13616	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7420	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7544	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13617	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6699	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7573	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13472	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6699	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7573	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2767	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 480	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 811	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∅c0 4296  𝒫 cpw 4563   × cxp 5636  (class class class)co 7387  1c1 11069   − cmin 11405  ℤcz 12529  ...cfz 13468  ..^cfzo 13615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-neg 11408  df-z 12530  df-uz 12794  df-fz 13469  df-fzo 13616

This theorem is referenced by:  elfzo  13622  fzon  13641  fzoss1  13647  fzoss2  13648  elfzolem1  13665  fz1fzo0m1  13671  fzval3  13695  fzo13pr  13710  fzo0to2pr  13711  fzo0to3tp  13713  fzo0to42pr  13714  fzo1to4tp  13715  fzoend  13718  fzofzp1b  13726  elfzom1b  13727  peano2fzor  13735  fzoshftral  13745  zmodfzo  13856  zmodidfzo  13862  fzofi  13939  hashfzo  14394  wrdffz  14500  revcl  14726  revlen  14727  revccat  14731  revrev  14732  revco  14800  fzosump1  15718  telfsumo  15768  fsumparts  15772  geoser  15833  pwdif  15834  pwm1geoser  15835  geo2sum2  15840  dfphi2  16744  reumodprminv  16775  gsumwsubmcl  18764  gsumsgrpccat  18767  gsumwmhm  18772  efgsdmi  19662  efgs1b  19666  efgredlemf  19671  efgredlemd  19674  efgredlemc  19675  efgredlem  19677  cpmadugsumlemF  22763  advlogexp  26564  dchrisumlem1  27400  redwlklem  29599  wlkiswwlks2lem3  29801  wlkiswwlksupgr2  29807  clwlkclwwlklem2a  29927  wlk2v2e  30086  eucrct2eupth  30174  cycpmco2  33090  submat1n  33795  eulerpartlemd  34357  fzssfzo  34530  signstfvn  34560  pthhashvtx  35115  remexz  42092  fzosumm1  42238  bccbc  44334  monoords  45295  stirlinglem12  46083  difltmodne  47343  iccpartiltu  47423  iccpartigtl  47424  iccpartgt  47428  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609