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:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
	nn0seqcvg.2	$$⊢N=F\left(0\right)$$
	nn0seqcvg.3	$$⊢k\in {\mathbb{N}}_0\to \left(F\left(k+1\right)\ne 0\to F\left(k+1\right)<F\left(k\right)\right)$$
Assertion	nn0seqcvg	$$⊢F\left(N\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		nn0seqcvg.1	$$⊢F:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
2		nn0seqcvg.2	$$⊢N=F\left(0\right)$$
3		nn0seqcvg.3	$$⊢k\in {\mathbb{N}}_0\to \left(F\left(k+1\right)\ne 0\to F\left(k+1\right)<F\left(k\right)\right)$$
4		eqid	$$⊢1=1$$
5	1	a1i	$$⊢1=1\to F:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
6	2	a1i	$$⊢1=1\to N=F\left(0\right)$$
7	3	adantl	$$⊢\left(1=1\wedge k\in {\mathbb{N}}_0\right)\to \left(F\left(k+1\right)\ne 0\to F\left(k+1\right)<F\left(k\right)\right)$$
8	5 6 7	nn0seqcvgd	$$⊢1=1\to F\left(N\right)=0$$
9	4 8	ax-mp	$$⊢F\left(N\right)=0$$