Theorem fzoval 13042

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 7165	. . . 4 ⊢ (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
3	1, 2	oveqan12d 7177	. . 3 ⊢ ((𝑚 = 𝑀 ∧ 𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4		df-fzo 13037	. . 3 ⊢ ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5		ovex 7191	. . 3 ⊢ (𝑀...(𝑁 − 1)) ∈ V
6	3, 4, 5	ovmpoa 7307	. 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7		simpl 485	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
8	7	con3i 157	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9		fzof 13038	. . . . . . 7 ⊢ ..^:(ℤ × ℤ)⟶𝒫 ℤ
10	9	fdmi 6526	. . . . . 6 ⊢ dom ..^ = (ℤ × ℤ)
11	10	ndmov 7334	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
12	8, 11	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
13		simpl 485	. . . . . 6 ⊢ ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
14	13	con3i 157	. . . . 5 ⊢ (¬ 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
15		fzf 12899	. . . . . . 7 ⊢ ...:(ℤ × ℤ)⟶𝒫 ℤ
16	15	fdmi 6526	. . . . . 6 ⊢ dom ... = (ℤ × ℤ)
17	16	ndmov 7334	. . . . 5 ⊢ (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
18	14, 17	syl 17	. . . 4 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
19	12, 18	eqtr4d 2861	. . 3 ⊢ (¬ 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
20	19	adantr 483	. 2 ⊢ ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
21	6, 20	pm2.61ian 810	1 ⊢ (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∅c0 4293  𝒫 cpw 4541   × cxp 5555  (class class class)co 7158  1c1 10540   − cmin 10872  ℤcz 11984  ...cfz 12895  ..^cfzo 13036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-neg 10875  df-z 11985  df-uz 12247  df-fz 12896  df-fzo 13037

This theorem is referenced by:  elfzo  13043  fzon  13061  fzoss1  13067  fzoss2  13068  fz1fzo0m1  13088  fzval3  13109  fzo13pr  13124  fzo0to2pr  13125  fzo0to3tp  13126  fzo0to42pr  13127  fzo1to4tp  13128  fzoend  13131  fzofzp1b  13138  elfzom1b  13139  peano2fzor  13147  fzoshftral  13157  zmodfzo  13265  zmodidfzo  13271  fzofi  13345  hashfzo  13793  wrdffz  13887  revcl  14125  revlen  14126  revccat  14130  revrev  14131  revco  14198  fzosump1  15109  telfsumo  15159  fsumparts  15163  geoser  15224  pwdif  15225  pwm1geoser  15226  geo2sum2  15232  dfphi2  16113  reumodprminv  16143  gsumwsubmcl  18003  gsumsgrpccat  18006  gsumccatOLD  18007  gsumwmhm  18012  efgsdmi  18860  efgs1b  18864  efgredlemf  18869  efgredlemd  18872  efgredlemc  18873  efgredlem  18875  cpmadugsumlemF  21486  advlogexp  25240  dchrisumlem1  26067  redwlklem  27455  wlkiswwlks2lem3  27651  wlkiswwlksupgr2  27657  clwlkclwwlklem2a  27778  wlk2v2e  27938  eucrct2eupth  28026  cycpmco2  30777  submat1n  31072  eulerpartlemd  31626  fzssfzo  31811  signstfvn  31841  pthhashvtx  32376  fzosumm1  39133  bccbc  40684  monoords  41571  elfzolem1  41596  stirlinglem12  42377  iccpartiltu  43589  iccpartigtl  43590  iccpartgt  43594  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  nn0sumshdiglemA  44686  nn0sumshdiglemB  44687