Theorem fz0addge0

Description: The sum of two integers in 0-based finite sets of sequential integers is greater than or equal to zero. (Contributed by Alexander van der Vekens, 8-Jun-2018)

	Ref	Expression
Assertion	fz0addge0	|- ( ( A e. ( 0 ... M ) /\ B e. ( 0 ... N ) ) -> 0 <_ ( A + B ) )

Proof

Step	Hyp	Ref	Expression
1		elfznn0	|- ( A e. ( 0 ... M ) -> A e. NN0 )
2		elfznn0	|- ( B e. ( 0 ... N ) -> B e. NN0 )
3	1 2	anim12i	|- ( ( A e. ( 0 ... M ) /\ B e. ( 0 ... N ) ) -> ( A e. NN0 /\ B e. NN0 ) )
4		nn0re	|- ( A e. NN0 -> A e. RR )
5		nn0re	|- ( B e. NN0 -> B e. RR )
6	4 5	anim12i	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( A e. RR /\ B e. RR ) )
7		nn0ge0	|- ( A e. NN0 -> 0 <_ A )
8		nn0ge0	|- ( B e. NN0 -> 0 <_ B )
9	7 8	anim12i	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( 0 <_ A /\ 0 <_ B ) )
10	6 9	jca	|- ( ( A e. NN0 /\ B e. NN0 ) -> ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) )
11		addge0	|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A + B ) )
12	3 10 11	3syl	|- ( ( A e. ( 0 ... M ) /\ B e. ( 0 ... N ) ) -> 0 <_ ( A + B ) )