Theorem climmpt2

Description: Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014)

	Ref	Expression
Hypotheses	climmpt2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climmpt2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climmpt2.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	climmpt2.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
Assertion	climmpt2	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		climmpt2.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		climmpt2.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climmpt2.3	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
4		climmpt2.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
5		eqid	⊢ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) = ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) )
6	1 5	climmpt	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ 𝑉 ) → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐴 ) )
7	2 3 6	syl2anc	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐴 ) )
8	4	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
9		fveq2	⊢ ( 𝑘 = 𝑚 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑚 ) )
10	9	eleq1d	⊢ ( 𝑘 = 𝑚 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑚 ) ∈ ℂ ) )
11	10	cbvralvw	⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ∈ ℂ )
12		fveq2	⊢ ( 𝑚 = 𝑛 → ( 𝐹 ‘ 𝑚 ) = ( 𝐹 ‘ 𝑛 ) )
13	12	eleq1d	⊢ ( 𝑚 = 𝑛 → ( ( 𝐹 ‘ 𝑚 ) ∈ ℂ ↔ ( 𝐹 ‘ 𝑛 ) ∈ ℂ ) )
14	13	cbvralvw	⊢ ( ∀ 𝑚 ∈ 𝑍 ( 𝐹 ‘ 𝑚 ) ∈ ℂ ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
15	11 14	bitri	⊢ ( ∀ 𝑘 ∈ 𝑍 ( 𝐹 ‘ 𝑘 ) ∈ ℂ ↔ ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
16	8 15	sylib	⊢ ( 𝜑 → ∀ 𝑛 ∈ 𝑍 ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
17	16	r19.21bi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ℂ )
18	17	fmpttd	⊢ ( 𝜑 → ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) : 𝑍 ⟶ ℂ )
19	1 2 18	rlimclim	⊢ ( 𝜑 → ( ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝ 𝐴 ) )
20	7 19	bitr4d	⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑛 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑛 ) ) ⇝𝑟 𝐴 ) )