Metamath Proof Explorer

Theorem elfz0add

Description: An element of a finite set of sequential nonnegative integers is an element of an extended finite set of sequential nonnegative integers. (Contributed by Alexander van der Vekens, 28-Mar-2018) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Assertion elfz0add 
|- ( ( A e. NN0 /\ B e. NN0 ) -> ( N e. ( 0 ... A ) -> N e. ( 0 ... ( A + B ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
2 uzid 
 |-  ( A e. ZZ -> A e. ( ZZ>= ` A ) )
3 1 2 syl 
 |-  ( A e. NN0 -> A e. ( ZZ>= ` A ) )
4 uzaddcl 
 |-  ( ( A e. ( ZZ>= ` A ) /\ B e. NN0 ) -> ( A + B ) e. ( ZZ>= ` A ) )
5 3 4 sylan 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( A + B ) e. ( ZZ>= ` A ) )
6 fzss2 
 |-  ( ( A + B ) e. ( ZZ>= ` A ) -> ( 0 ... A ) C_ ( 0 ... ( A + B ) ) )
7 5 6 syl 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( 0 ... A ) C_ ( 0 ... ( A + B ) ) )
8 7 sseld 
 |-  ( ( A e. NN0 /\ B e. NN0 ) -> ( N e. ( 0 ... A ) -> N e. ( 0 ... ( A + B ) ) ) )