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

Theorem fzoval 11550
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  |-  ( N  e.  ZZ  ->  ( M..^ N )  =  ( M ... ( N  -  1 ) ) )

Proof of Theorem fzoval
Dummy variables  m  n are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 id 22 . . . 4  |-  ( m  =  M  ->  m  =  M )
2 oveq1 6097 . . . 4  |-  ( n  =  N  ->  (
n  -  1 )  =  ( N  - 
1 ) )
31, 2oveqan12d 6109 . . 3  |-  ( ( m  =  M  /\  n  =  N )  ->  ( m ... (
n  -  1 ) )  =  ( M ... ( N  - 
1 ) ) )
4 df-fzo 11545 . . 3  |- ..^  =  ( m  e.  ZZ ,  n  e.  ZZ  |->  ( m ... ( n  - 
1 ) ) )
5 ovex 6115 . . 3  |-  ( M ... ( N  - 
1 ) )  e. 
_V
63, 4, 5ovmpt2a 6220 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M..^ N )  =  ( M ... ( N  -  1
) ) )
7 simpl 454 . . . . . 6  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  M  e.  ZZ )
87con3i 135 . . . . 5  |-  ( -.  M  e.  ZZ  ->  -.  ( M  e.  ZZ  /\  N  e.  ZZ ) )
9 fzof 11546 . . . . . . 7  |- ..^ : ( ZZ  X.  ZZ ) --> ~P ZZ
109fdmi 5561 . . . . . 6  |-  dom ..^  =  ( ZZ  X.  ZZ )
1110ndmov 6246 . . . . 5  |-  ( -.  ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M..^ N
)  =  (/) )
128, 11syl 16 . . . 4  |-  ( -.  M  e.  ZZ  ->  ( M..^ N )  =  (/) )
13 simpl 454 . . . . . 6  |-  ( ( M  e.  ZZ  /\  ( N  -  1
)  e.  ZZ )  ->  M  e.  ZZ )
1413con3i 135 . . . . 5  |-  ( -.  M  e.  ZZ  ->  -.  ( M  e.  ZZ  /\  ( N  -  1 )  e.  ZZ ) )
15 fzf 11437 . . . . . . 7  |-  ... :
( ZZ  X.  ZZ )
--> ~P ZZ
1615fdmi 5561 . . . . . 6  |-  dom  ...  =  ( ZZ  X.  ZZ )
1716ndmov 6246 . . . . 5  |-  ( -.  ( M  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  ->  ( M ... ( N  -  1
) )  =  (/) )
1814, 17syl 16 . . . 4  |-  ( -.  M  e.  ZZ  ->  ( M ... ( N  -  1 ) )  =  (/) )
1912, 18eqtr4d 2476 . . 3  |-  ( -.  M  e.  ZZ  ->  ( M..^ N )  =  ( M ... ( N  -  1 ) ) )
2019adantr 462 . 2  |-  ( ( -.  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M..^ N
)  =  ( M ... ( N  - 
1 ) ) )
216, 20pm2.61ian 783 1  |-  ( N  e.  ZZ  ->  ( M..^ N )  =  ( M ... ( N  -  1 ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1364    e. wcel 1761   (/)c0 3634   ~Pcpw 3857    X. cxp 4834  (class class class)co 6090   1c1 9279    - cmin 9591   ZZcz 10642   ...cfz 11433  ..^cfzo 11544
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-1st 6576  df-2nd 6577  df-neg 9594  df-z 10643  df-uz 10858  df-fz 11434  df-fzo 11545
This theorem is referenced by:  elfzo  11551  fzon  11567  fzoss1  11572  fzoss2  11573  fzval3  11601  fzo0to2pr  11610  fzo0to3tp  11611  fzo0to42pr  11612  fzoend  11614  fzofzp1b  11621  elfzom1b  11622  peano2fzor  11628  fzoshftral  11632  zmodfzo  11726  zmodidfzo  11733  fzofi  11792  hashfzo  12186  revcl  12397  revlen  12398  revccat  12402  revrev  12403  revco  12458  fzosump1  13217  fsumtscopo  13261  fsumparts  13265  geoser  13325  geo2sum2  13330  dfphi2  13845  reumodprminv  13868  gsumwsubmcl  15509  gsumccat  15512  gsumwmhm  15516  efgsdmi  16222  efgs1b  16226  efgredlemf  16231  efgredlemd  16234  efgredlemc  16235  efgredlem  16237  advlogexp  22043  dchrisumlem1  22681  wlkntrllem2  23378  redwlk  23424  constr3pthlem1  23460  constr3pthlem3  23462  eulerpartlemd  26663  fzssfzo  26848  signstfvn  26884  stirlinglem12  29789  wlkiswwlk2lem3  30236  clwlkisclwwlklem2a  30356
  Copyright terms: Public domain W3C validator