Metamath Proof Explorer

Theorem fzoval

Description: Value of the half-open integer set in terms of the closed integer set. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzoval 
|- ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( m = M -> m = M )
2 oveq1 
 |-  ( n = N -> ( n - 1 ) = ( N - 1 ) )
3 1 2 oveqan12d 
 |-  ( ( m = M /\ n = N ) -> ( m ... ( n - 1 ) ) = ( M ... ( N - 1 ) ) )
4 df-fzo 
 |-  ..^ = ( m e. ZZ , n e. ZZ |-> ( m ... ( n - 1 ) ) )
5 ovex 
 |-  ( M ... ( N - 1 ) ) e. _V
6 3 4 5 ovmpoa 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
7 simpl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M e. ZZ )
8 fzof 
 |-  ..^ : ( ZZ X. ZZ ) --> ~P ZZ
9 8 fdmi 
 |-  dom ..^ = ( ZZ X. ZZ )
10 9 ndmov 
 |-  ( -. ( M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = (/) )
11 7 10 nsyl5 
 |-  ( -. M e. ZZ -> ( M ..^ N ) = (/) )
12 simpl 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> M e. ZZ )
13 fzf 
 |-  ... : ( ZZ X. ZZ ) --> ~P ZZ
14 13 fdmi 
 |-  dom ... = ( ZZ X. ZZ )
15 14 ndmov 
 |-  ( -. ( M e. ZZ /\ ( N - 1 ) e. ZZ ) -> ( M ... ( N - 1 ) ) = (/) )
16 12 15 nsyl5 
 |-  ( -. M e. ZZ -> ( M ... ( N - 1 ) ) = (/) )
17 11 16 eqtr4d 
 |-  ( -. M e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
18 17 adantr 
 |-  ( ( -. M e. ZZ /\ N e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
19 6 18 pm2.61ian 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )