MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fzoval Structured version   Visualization version   GIF version

Theorem fzoval 12678
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.
StepHypRef Expression
1 id 22 . . . 4 (𝑚 = 𝑀𝑚 = 𝑀)
2 oveq1 6848 . . . 4 (𝑛 = 𝑁 → (𝑛 − 1) = (𝑁 − 1))
31, 2oveqan12d 6860 . . 3 ((𝑚 = 𝑀𝑛 = 𝑁) → (𝑚...(𝑛 − 1)) = (𝑀...(𝑁 − 1)))
4 df-fzo 12673 . . 3 ..^ = (𝑚 ∈ ℤ, 𝑛 ∈ ℤ ↦ (𝑚...(𝑛 − 1)))
5 ovex 6873 . . 3 (𝑀...(𝑁 − 1)) ∈ V
63, 4, 5ovmpt2a 6988 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
7 simpl 474 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
87con3i 151 . . . . 5 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ))
9 fzof 12674 . . . . . . 7 ..^:(ℤ × ℤ)⟶𝒫 ℤ
109fdmi 6232 . . . . . 6 dom ..^ = (ℤ × ℤ)
1110ndmov 7015 . . . . 5 (¬ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = ∅)
128, 11syl 17 . . . 4 𝑀 ∈ ℤ → (𝑀..^𝑁) = ∅)
13 simpl 474 . . . . . 6 ((𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → 𝑀 ∈ ℤ)
1413con3i 151 . . . . 5 𝑀 ∈ ℤ → ¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ))
15 fzf 12536 . . . . . . 7 ...:(ℤ × ℤ)⟶𝒫 ℤ
1615fdmi 6232 . . . . . 6 dom ... = (ℤ × ℤ)
1716ndmov 7015 . . . . 5 (¬ (𝑀 ∈ ℤ ∧ (𝑁 − 1) ∈ ℤ) → (𝑀...(𝑁 − 1)) = ∅)
1814, 17syl 17 . . . 4 𝑀 ∈ ℤ → (𝑀...(𝑁 − 1)) = ∅)
1912, 18eqtr4d 2801 . . 3 𝑀 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
2019adantr 472 . 2 ((¬ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
216, 20pm2.61ian 846 1 (𝑁 ∈ ℤ → (𝑀..^𝑁) = (𝑀...(𝑁 − 1)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384   = wceq 1652  wcel 2155  c0 4078  𝒫 cpw 4314   × cxp 5274  (class class class)co 6841  1c1 10189  cmin 10519  cz 11623  ...cfz 12532  ..^cfzo 12672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-op 4340  df-uni 4594  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-id 5184  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-fv 6075  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-1st 7365  df-2nd 7366  df-neg 10522  df-z 11624  df-uz 11886  df-fz 12533  df-fzo 12673
This theorem is referenced by:  elfzo  12679  fzon  12696  fzoss1  12702  fzoss2  12703  fz1fzo0m1  12723  fzval3  12744  fzo13pr  12759  fzo0to2pr  12760  fzo0to3tp  12761  fzo0to42pr  12762  fzo1to4tp  12763  fzoend  12766  fzofzp1b  12773  elfzom1b  12774  peano2fzor  12782  fzoshftral  12792  zmodfzo  12900  zmodidfzo  12906  fzofi  12980  hashfzo  13416  wrdffz  13506  revcl  13784  revlen  13785  revccat  13789  revrev  13790  revco  13864  fzosump1  14767  telfsumo  14819  fsumparts  14823  geoser  14884  geo2sum2  14890  dfphi2  15759  reumodprminv  15789  gsumwsubmcl  17642  gsumccat  17645  gsumwmhm  17650  efgsdmi  18410  efgs1b  18414  efgredlemf  18419  efgredlemd  18422  efgredlemc  18423  efgredlem  18425  cpmadugsumlemF  20959  advlogexp  24691  dchrisumlem1  25468  redwlklem  26858  wlkiswwlks2lem3  27060  wlkiswwlksupgr2  27066  clwlkclwwlklem2a  27203  wlk2v2e  27392  eucrct2eupth  27480  submat1n  30252  eulerpartlemd  30809  fzssfzo  30995  signstfvn  31028  bccbc  39150  monoords  40082  elfzolem1  40107  stirlinglem12  40871  iccpartiltu  42024  iccpartigtl  42025  iccpartgt  42029  pwdif  42109  pwm1geoserALT  42110  nnsum4primeseven  42296  nnsum4primesevenALTV  42297  nn0sumshdiglemA  43014  nn0sumshdiglemB  43015
  Copyright terms: Public domain W3C validator