Theorem fzoval 13609

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 7369	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7381	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13604	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7395	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7517	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8		fzof 13605	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
9	8	fdmi 6675	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
10	9	ndmov 7546	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
11	7, 10	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
12		simpl 482	. . . . 5 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
13		fzf 13460	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
14	13	fdmi 6675	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
15	14	ndmov 7546	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
16	12, 15	nsyl5 159	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
17	11, 16	eqtr4d 2775	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
18	17	adantr 480	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
19	6, 18	pm2.61ian 812	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∅c0 4274  𝒫 cpw 4542   × cxp 5624  (class class class)co 7362  1c1 11034   − cmin 11372  ℤcz 12519  ...cfz 13456  ..^cfzo 13603

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5372  ax-un 7684  ax-cnex 11089  ax-resscn 11090

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-1st 7937  df-2nd 7938  df-neg 11375  df-z 12520  df-uz 12784  df-fz 13457  df-fzo 13604

This theorem is referenced by:  elfzo  13610  fzon  13630  fzoss1  13636  fzoss2  13637  elfzolem1  13654  fz1fzo0m1  13660  fzval3  13684  fzo13pr  13699  fzo0to2pr  13700  fzo0to3tp  13702  fzo0to42pr  13703  fzo1to4tp  13704  fzoend  13707  fzofzp1b  13715  elfzom1b  13716  peano2fzor  13725  fzoshftral  13737  zmodfzo  13848  zmodidfzo  13854  fzofi  13931  hashfzo  14386  wrdffz  14492  revcl  14718  revlen  14719  revccat  14723  revrev  14724  revco  14791  fzosump1  15709  telfsumo  15760  fsumparts  15764  geoser  15827  pwdif  15828  pwm1geoser  15829  geo2sum2  15834  dfphi2  16739  reumodprminv  16770  gsumwsubmcl  18800  gsumsgrpccat  18803  gsumwmhm  18808  efgsdmi  19702  efgs1b  19706  efgredlemf  19711  efgredlemd  19714  efgredlemc  19715  efgredlem  19717  cpmadugsumlemF  22855  advlogexp  26636  dchrisumlem1  27470  redwlklem  29757  wlkiswwlks2lem3  29958  wlkiswwlksupgr2  29964  clwlkclwwlklem2a  30087  wlk2v2e  30246  eucrct2eupth  30334  gsummulsubdishift1  33148  cycpmco2  33213  submat1n  33969  eulerpartlemd  34530  fzssfzo  34703  signstfvn  34733  pthhashvtx  35330  remexz  42563  fzosumm1  42709  bccbc  44796  monoords  45754  stirlinglem12  46537  difltmodne  47814  muldvdsfacm1  47853  iccpartiltu  47900  iccpartigtl  47901  iccpartgt  47905  nprmmul1  48005  nnsum4primeseven  48294  nnsum4primesevenALTV  48295  nn0sumshdiglemA  49113  nn0sumshdiglemB  49114