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 A0B0N0AN0A+B

Proof

Step Hyp Ref Expression
1 nn0z A0A
2 uzid AAA
3 1 2 syl A0AA
4 uzaddcl AAB0A+BA
5 3 4 sylan A0B0A+BA
6 fzss2 A+BA0A0A+B
7 5 6 syl A0B00A0A+B
8 7 sseld A0B0N0AN0A+B