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	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝜑 ) ↔ ( 𝑘 ∈ ℕ → ( 𝑚 ≤ 𝑘 → 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elnnuz	⊢ ( 𝑚 ∈ ℕ ↔ 𝑚 ∈ ( ℤ≥ ‘ 1 ) )
2		uztrn	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ 𝑚 ∈ ( ℤ≥ ‘ 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
3	1 2	sylan2b	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
4		elnnuz	⊢ ( 𝑘 ∈ ℕ ↔ 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
5	3 4	sylibr	⊢ ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ∧ 𝑚 ∈ ℕ ) → 𝑘 ∈ ℕ )
6	5	expcom	⊢ ( 𝑚 ∈ ℕ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑘 ∈ ℕ ) )
7		eluzle	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑚 ≤ 𝑘 )
8	7	a1i	⊢ ( 𝑚 ∈ ℕ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝑚 ≤ 𝑘 ) )
9	6 8	jcad	⊢ ( 𝑚 ∈ ℕ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → ( 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) ) )
10		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
11		nnz	⊢ ( 𝑚 ∈ ℕ → 𝑚 ∈ ℤ )
12		eluz2	⊢ ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ↔ ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ≤ 𝑘 ) )
13	12	biimpri	⊢ ( ( 𝑚 ∈ ℤ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) )
14	11 13	syl3an1	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℤ ∧ 𝑚 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) )
15	10 14	syl3an2	⊢ ( ( 𝑚 ∈ ℕ ∧ 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) )
16	15	3expib	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ) )
17	9 16	impbid	⊢ ( 𝑚 ∈ ℕ → ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) ) )
18	17	imbi1d	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝜑 ) ↔ ( ( 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) → 𝜑 ) ) )
19		impexp	⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑚 ≤ 𝑘 ) → 𝜑 ) ↔ ( 𝑘 ∈ ℕ → ( 𝑚 ≤ 𝑘 → 𝜑 ) ) )
20	18 19	bitrdi	⊢ ( 𝑚 ∈ ℕ → ( ( 𝑘 ∈ ( ℤ≥ ‘ 𝑚 ) → 𝜑 ) ↔ ( 𝑘 ∈ ℕ → ( 𝑚 ≤ 𝑘 → 𝜑 ) ) ) )