Theorem nn0seqcvg

Description: A strictly-decreasing nonnegative integer sequence with initial term N reaches zero by the N th term. Inference version. (Contributed by Paul Chapman, 31-Mar-2011)

	Ref	Expression
Hypotheses	nn0seqcvg.1	|- F : NN0 --> NN0
	nn0seqcvg.2	|- N = ( F ` 0 )
	nn0seqcvg.3	|- ( k e. NN0 -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )
Assertion	nn0seqcvg	|- ( F ` N ) = 0

Proof

Step	Hyp	Ref	Expression
1		nn0seqcvg.1	|- F : NN0 --> NN0
2		nn0seqcvg.2	|- N = ( F ` 0 )
3		nn0seqcvg.3	|- ( k e. NN0 -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )
4		eqid	|- 1 = 1
5	1	a1i	|- ( 1 = 1 -> F : NN0 --> NN0 )
6	2	a1i	|- ( 1 = 1 -> N = ( F ` 0 ) )
7	3	adantl	|- ( ( 1 = 1 /\ k e. NN0 ) -> ( ( F ` ( k + 1 ) ) =/= 0 -> ( F ` ( k + 1 ) ) < ( F ` k ) ) )
8	5 6 7	nn0seqcvgd	|- ( 1 = 1 -> ( F ` N ) = 0 )
9	4 8	ax-mp	|- ( F ` N ) = 0