Theorem divcnvshft

Description: Limit of a ratio function. (Contributed by Scott Fenton, 16-Dec-2017)

	Ref	Expression
Hypotheses	divcnvshft.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	divcnvshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	divcnvshft.3	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	divcnvshft.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
	divcnvshft.5	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	divcnvshft.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
Assertion	divcnvshft	⊢ ( 𝜑 → 𝐹 ⇝ 0 )

Proof

Step	Hyp	Ref	Expression
1		divcnvshft.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		divcnvshft.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		divcnvshft.3	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		divcnvshft.4	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
5		divcnvshft.5	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
6		divcnvshft.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
7		divcnv	⊢ ( 𝐴 ∈ ℂ → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
8	3 7	syl	⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
9		nnssz	⊢ ℕ ⊆ ℤ
10		resmpt	⊢ ( ℕ ⊆ ℤ → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) )
11	9 10	ax-mp	⊢ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) )
12		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
13	12	reseq2i	⊢ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ℕ ) = ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) )
14	11 13	eqtr3i	⊢ ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) = ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) )
15	14	breq1i	⊢ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 )
16		1z	⊢ 1 ∈ ℤ
17		zex	⊢ ℤ ∈ V
18	17	mptex	⊢ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V
19		climres	⊢ ( ( 1 ∈ ℤ ∧ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V ) → ( ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ) )
20	16 18 19	mp2an	⊢ ( ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ↾ ( ℤ≥ ‘ 1 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
21	15 20	bitri	⊢ ( ( 𝑚 ∈ ℕ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
22	8 21	sylib	⊢ ( 𝜑 → ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 )
23	18	a1i	⊢ ( 𝜑 → ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ∈ V )
24		uzssz	⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
25	1 24	eqsstri	⊢ 𝑍 ⊆ ℤ
26	25	sseli	⊢ ( 𝑘 ∈ 𝑍 → 𝑘 ∈ ℤ )
27	26	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝑘 ∈ ℤ )
28	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℤ )
29	27 28	zaddcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝑘 + 𝐵 ) ∈ ℤ )
30		oveq2	⊢ ( 𝑚 = ( 𝑘 + 𝐵 ) → ( 𝐴 / 𝑚 ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
31		eqid	⊢ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) = ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) )
32		ovex	⊢ ( 𝐴 / ( 𝑘 + 𝐵 ) ) ∈ V
33	30 31 32	fvmpt	⊢ ( ( 𝑘 + 𝐵 ) ∈ ℤ → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
34	29 33	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐴 / ( 𝑘 + 𝐵 ) ) )
35	34 6	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ‘ ( 𝑘 + 𝐵 ) ) = ( 𝐹 ‘ 𝑘 ) )
36	1 2 4 5 23 35	climshft2	⊢ ( 𝜑 → ( 𝐹 ⇝ 0 ↔ ( 𝑚 ∈ ℤ ↦ ( 𝐴 / 𝑚 ) ) ⇝ 0 ) )
37	22 36	mpbird	⊢ ( 𝜑 → 𝐹 ⇝ 0 )