divcnvshft

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

	Ref	Expression
Hypotheses	divcnvshft.1	$⊢ Z = ℤ_{\geq M}$
	divcnvshft.2	$⊢ φ \to M \in ℤ$
	divcnvshft.3	$⊢ φ \to A \in ℂ$
	divcnvshft.4	$⊢ φ \to B \in ℤ$
	divcnvshft.5	$⊢ φ \to F \in V$
	divcnvshft.6	$⊢ (φ \land k \in Z) \to F (k) = \frac{A}{k + B}$
Assertion	divcnvshft	$⊢ φ \to F ⇝ 0$

Proof

Step	Hyp	Ref	Expression
1		divcnvshft.1	$⊢ Z = ℤ_{\geq M}$
2		divcnvshft.2	$⊢ φ \to M \in ℤ$
3		divcnvshft.3	$⊢ φ \to A \in ℂ$
4		divcnvshft.4	$⊢ φ \to B \in ℤ$
5		divcnvshft.5	$⊢ φ \to F \in V$
6		divcnvshft.6	$⊢ (φ \land k \in Z) \to F (k) = \frac{A}{k + B}$
7		divcnv	$⊢ A \in ℂ \to (m \in ℕ ⟼ \frac{A}{m}) ⇝ 0$
8	3 7	syl	$⊢ φ \to (m \in ℕ ⟼ \frac{A}{m}) ⇝ 0$
9		nnssz	$⊢ ℕ \subseteq ℤ$
10		resmpt	$⊢ ℕ \subseteq ℤ \to {(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℕ} = (m \in ℕ ⟼ \frac{A}{m})$
11	9 10	ax-mp	$⊢ {(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℕ} = (m \in ℕ ⟼ \frac{A}{m})$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	12	reseq2i	$⊢ {(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℕ} = {(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℤ_{\geq 1}}$
14	11 13	eqtr3i	$⊢ (m \in ℕ ⟼ \frac{A}{m}) = {(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℤ_{\geq 1}}$
15	14	breq1i	$⊢ (m \in ℕ ⟼ \frac{A}{m}) ⇝ 0 \leftrightarrow ({(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 0$
16		1z	$⊢ 1 \in ℤ$
17		zex	$⊢ ℤ \in V$
18	17	mptex	$⊢ (m \in ℤ ⟼ \frac{A}{m}) \in V$
19		climres	$⊢ (1 \in ℤ \land (m \in ℤ ⟼ \frac{A}{m}) \in V) \to (({(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 0 \leftrightarrow (m \in ℤ ⟼ \frac{A}{m}) ⇝ 0)$
20	16 18 19	mp2an	$⊢ ({(m \in ℤ ⟼ \frac{A}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 0 \leftrightarrow (m \in ℤ ⟼ \frac{A}{m}) ⇝ 0$
21	15 20	bitri	$⊢ (m \in ℕ ⟼ \frac{A}{m}) ⇝ 0 \leftrightarrow (m \in ℤ ⟼ \frac{A}{m}) ⇝ 0$
22	8 21	sylib	$⊢ φ \to (m \in ℤ ⟼ \frac{A}{m}) ⇝ 0$
23	18	a1i	$⊢ φ \to (m \in ℤ ⟼ \frac{A}{m}) \in V$
24		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
25	1 24	eqsstri	$⊢ Z \subseteq ℤ$
26	25	sseli	$⊢ k \in Z \to k \in ℤ$
27	26	adantl	$⊢ (φ \land k \in Z) \to k \in ℤ$
28	4	adantr	$⊢ (φ \land k \in Z) \to B \in ℤ$
29	27 28	zaddcld	$⊢ (φ \land k \in Z) \to k + B \in ℤ$
30		oveq2	$⊢ m = k + B \to \frac{A}{m} = \frac{A}{k + B}$
31		eqid	$⊢ (m \in ℤ ⟼ \frac{A}{m}) = (m \in ℤ ⟼ \frac{A}{m})$
32		ovex	$⊢ \frac{A}{k + B} \in V$
33	30 31 32	fvmpt	$⊢ k + B \in ℤ \to (m \in ℤ ⟼ \frac{A}{m}) (k + B) = \frac{A}{k + B}$
34	29 33	syl	$⊢ (φ \land k \in Z) \to (m \in ℤ ⟼ \frac{A}{m}) (k + B) = \frac{A}{k + B}$
35	34 6	eqtr4d	$⊢ (φ \land k \in Z) \to (m \in ℤ ⟼ \frac{A}{m}) (k + B) = F (k)$
36	1 2 4 5 23 35	climshft2	$⊢ φ \to (F ⇝ 0 \leftrightarrow (m \in ℤ ⟼ \frac{A}{m}) ⇝ 0)$
37	22 36	mpbird	$⊢ φ \to F ⇝ 0$

Metamath Proof Explorer

Theorem divcnvshft

Proof