Theorem climuzcnv

Description: Utility lemma to convert between m <_ k and k e. ( ZZ>=m ) in limit theorems. (Contributed by Paul Chapman, 10-Nov-2012)

	Ref	Expression
Assertion	climuzcnv	|- ( m e. NN -> ( ( k e. ( ZZ>= ` m ) -> ph ) <-> ( k e. NN -> ( m <_ k -> ph ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	|- ( m e. NN <-> m e. ( ZZ>= ` 1 ) )
2		uztrn	|- ( ( k e. ( ZZ>= ` m ) /\ m e. ( ZZ>= ` 1 ) ) -> k e. ( ZZ>= ` 1 ) )
3	1 2	sylan2b	|- ( ( k e. ( ZZ>= ` m ) /\ m e. NN ) -> k e. ( ZZ>= ` 1 ) )
4		elnnuz	|- ( k e. NN <-> k e. ( ZZ>= ` 1 ) )
5	3 4	sylibr	|- ( ( k e. ( ZZ>= ` m ) /\ m e. NN ) -> k e. NN )
6	5	expcom	|- ( m e. NN -> ( k e. ( ZZ>= ` m ) -> k e. NN ) )
7		eluzle	|- ( k e. ( ZZ>= ` m ) -> m <_ k )
8	7	a1i	|- ( m e. NN -> ( k e. ( ZZ>= ` m ) -> m <_ k ) )
9	6 8	jcad	|- ( m e. NN -> ( k e. ( ZZ>= ` m ) -> ( k e. NN /\ m <_ k ) ) )
10		nnz	|- ( k e. NN -> k e. ZZ )
11		nnz	|- ( m e. NN -> m e. ZZ )
12		eluz2	|- ( k e. ( ZZ>= ` m ) <-> ( m e. ZZ /\ k e. ZZ /\ m <_ k ) )
13	12	biimpri	|- ( ( m e. ZZ /\ k e. ZZ /\ m <_ k ) -> k e. ( ZZ>= ` m ) )
14	11 13	syl3an1	|- ( ( m e. NN /\ k e. ZZ /\ m <_ k ) -> k e. ( ZZ>= ` m ) )
15	10 14	syl3an2	|- ( ( m e. NN /\ k e. NN /\ m <_ k ) -> k e. ( ZZ>= ` m ) )
16	15	3expib	|- ( m e. NN -> ( ( k e. NN /\ m <_ k ) -> k e. ( ZZ>= ` m ) ) )
17	9 16	impbid	|- ( m e. NN -> ( k e. ( ZZ>= ` m ) <-> ( k e. NN /\ m <_ k ) ) )
18	17	imbi1d	|- ( m e. NN -> ( ( k e. ( ZZ>= ` m ) -> ph ) <-> ( ( k e. NN /\ m <_ k ) -> ph ) ) )
19		impexp	|- ( ( ( k e. NN /\ m <_ k ) -> ph ) <-> ( k e. NN -> ( m <_ k -> ph ) ) )
20	18 19	bitrdi	|- ( m e. NN -> ( ( k e. ( ZZ>= ` m ) -> ph ) <-> ( k e. NN -> ( m <_ k -> ph ) ) ) )