This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fz0add1fz1

Description: Translate membership in a 0-based half-open integer range into membership in a 1-based finite sequence of integers. (Contributed by Alexander van der Vekens, 23-Nov-2017)

Ref Expression
Assertion fz0add1fz1 
|- ( ( N e. NN0 /\ X e. ( 0 ..^ N ) ) -> ( X + 1 ) e. ( 1 ... N ) )

Proof

Step Hyp Ref Expression
1 1z 
 |-  1 e. ZZ
2 fzoaddel 
 |-  ( ( X e. ( 0 ..^ N ) /\ 1 e. ZZ ) -> ( X + 1 ) e. ( ( 0 + 1 ) ..^ ( N + 1 ) ) )
3 1 2 mpan2 
 |-  ( X e. ( 0 ..^ N ) -> ( X + 1 ) e. ( ( 0 + 1 ) ..^ ( N + 1 ) ) )
4 3 adantl 
 |-  ( ( N e. NN0 /\ X e. ( 0 ..^ N ) ) -> ( X + 1 ) e. ( ( 0 + 1 ) ..^ ( N + 1 ) ) )
5 0p1e1 
 |-  ( 0 + 1 ) = 1
6 5 oveq1i 
 |-  ( ( 0 + 1 ) ..^ ( N + 1 ) ) = ( 1 ..^ ( N + 1 ) )
7 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
8 fzval3 
 |-  ( N e. ZZ -> ( 1 ... N ) = ( 1 ..^ ( N + 1 ) ) )
9 8 eqcomd 
 |-  ( N e. ZZ -> ( 1 ..^ ( N + 1 ) ) = ( 1 ... N ) )
10 7 9 syl 
 |-  ( N e. NN0 -> ( 1 ..^ ( N + 1 ) ) = ( 1 ... N ) )
11 6 10 eqtrid 
 |-  ( N e. NN0 -> ( ( 0 + 1 ) ..^ ( N + 1 ) ) = ( 1 ... N ) )
12 11 eleq2d 
 |-  ( N e. NN0 -> ( ( X + 1 ) e. ( ( 0 + 1 ) ..^ ( N + 1 ) ) <-> ( X + 1 ) e. ( 1 ... N ) ) )
13 12 adantr 
 |-  ( ( N e. NN0 /\ X e. ( 0 ..^ N ) ) -> ( ( X + 1 ) e. ( ( 0 + 1 ) ..^ ( N + 1 ) ) <-> ( X + 1 ) e. ( 1 ... N ) ) )
14 4 13 mpbid 
 |-  ( ( N e. NN0 /\ X e. ( 0 ..^ N ) ) -> ( X + 1 ) e. ( 1 ... N ) )