Theorem 2elfz3nn0

Description: If there are two elements in a finite set of sequential integers starting at 0, these two elements as well as the upper bound are nonnegative integers. (Contributed by Alexander van der Vekens, 7-Apr-2018)

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

Proof

Step	Hyp	Ref	Expression
1		elfznn0	|- ( A e. ( 0 ... N ) -> A e. NN0 )
2		elfz2nn0	|- ( B e. ( 0 ... N ) <-> ( B e. NN0 /\ N e. NN0 /\ B <_ N ) )
3		3anass	|- ( ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) <-> ( A e. NN0 /\ ( B e. NN0 /\ N e. NN0 ) ) )
4	3	simplbi2com	|- ( ( B e. NN0 /\ N e. NN0 ) -> ( A e. NN0 -> ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) ) )
5	4	3adant3	|- ( ( B e. NN0 /\ N e. NN0 /\ B <_ N ) -> ( A e. NN0 -> ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) ) )
6	2 5	sylbi	|- ( B e. ( 0 ... N ) -> ( A e. NN0 -> ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) ) )
7	1 6	mpan9	|- ( ( A e. ( 0 ... N ) /\ B e. ( 0 ... N ) ) -> ( A e. NN0 /\ B e. NN0 /\ N e. NN0 ) )