divcnvlin

Description: Limit of the ratio of two linear functions. (Contributed by Scott Fenton, 17-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		divcnvlin.1	$⊢ Z = ℤ_{\geq M}$
2		divcnvlin.2	$⊢ φ \to M \in ℤ$
3		divcnvlin.3	$⊢ φ \to A \in ℂ$
4		divcnvlin.4	$⊢ φ \to B \in ℤ$
5		divcnvlin.5	$⊢ φ \to F \in V$
6		divcnvlin.6	$⊢ (φ \land k \in Z) \to F (k) = \frac{k + A}{k + B}$
7		nncn	$⊢ m \in ℕ \to m \in ℂ$
8	7	adantl	$⊢ (φ \land m \in ℕ) \to m \in ℂ$
9	4	zcnd	$⊢ φ \to B \in ℂ$
10	3 9	subcld	$⊢ φ \to A - B \in ℂ$
11	10	adantr	$⊢ (φ \land m \in ℕ) \to A - B \in ℂ$
12		nnne0	$⊢ m \in ℕ \to m \neq 0$
13	12	adantl	$⊢ (φ \land m \in ℕ) \to m \neq 0$
14	8 11 8 13	divdird	$⊢ (φ \land m \in ℕ) \to \frac{m + A - B}{m} = (\frac{m}{m}) + (\frac{A - B}{m})$
15	8 13	dividd	$⊢ (φ \land m \in ℕ) \to \frac{m}{m} = 1$
16	15	oveq1d	$⊢ (φ \land m \in ℕ) \to (\frac{m}{m}) + (\frac{A - B}{m}) = 1 + (\frac{A - B}{m})$
17	14 16	eqtrd	$⊢ (φ \land m \in ℕ) \to \frac{m + A - B}{m} = 1 + (\frac{A - B}{m})$
18	17	mpteq2dva	$⊢ φ \to (m \in ℕ ⟼ \frac{m + A - B}{m}) = (m \in ℕ ⟼ 1 + (\frac{A - B}{m}))$
19		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
20		1zzd	$⊢ φ \to 1 \in ℤ$
21		divcnv	$⊢ A - B \in ℂ \to (m \in ℕ ⟼ \frac{A - B}{m}) ⇝ 0$
22	10 21	syl	$⊢ φ \to (m \in ℕ ⟼ \frac{A - B}{m}) ⇝ 0$
23		1cnd	$⊢ φ \to 1 \in ℂ$
24		nnex	$⊢ ℕ \in V$
25	24	mptex	$⊢ (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) \in V$
26	25	a1i	$⊢ φ \to (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) \in V$
27	11 8 13	divcld	$⊢ (φ \land m \in ℕ) \to \frac{A - B}{m} \in ℂ$
28	27	fmpttd	$⊢ φ \to (m \in ℕ ⟼ \frac{A - B}{m}) : ℕ ⟶ ℂ$
29	28	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to (m \in ℕ ⟼ \frac{A - B}{m}) (k) \in ℂ$
30		oveq2	$⊢ m = k \to \frac{A - B}{m} = \frac{A - B}{k}$
31	30	oveq2d	$⊢ m = k \to 1 + (\frac{A - B}{m}) = 1 + (\frac{A - B}{k})$
32		eqid	$⊢ (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) = (m \in ℕ ⟼ 1 + (\frac{A - B}{m}))$
33		ovex	$⊢ 1 + (\frac{A - B}{k}) \in V$
34	31 32 33	fvmpt	$⊢ k \in ℕ \to (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) (k) = 1 + (\frac{A - B}{k})$
35		eqid	$⊢ (m \in ℕ ⟼ \frac{A - B}{m}) = (m \in ℕ ⟼ \frac{A - B}{m})$
36		ovex	$⊢ \frac{A - B}{k} \in V$
37	30 35 36	fvmpt	$⊢ k \in ℕ \to (m \in ℕ ⟼ \frac{A - B}{m}) (k) = \frac{A - B}{k}$
38	37	oveq2d	$⊢ k \in ℕ \to 1 + (m \in ℕ ⟼ \frac{A - B}{m}) (k) = 1 + (\frac{A - B}{k})$
39	34 38	eqtr4d	$⊢ k \in ℕ \to (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) (k) = 1 + (m \in ℕ ⟼ \frac{A - B}{m}) (k)$
40	39	adantl	$⊢ (φ \land k \in ℕ) \to (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) (k) = 1 + (m \in ℕ ⟼ \frac{A - B}{m}) (k)$
41	19 20 22 23 26 29 40	climaddc2	$⊢ φ \to (m \in ℕ ⟼ 1 + (\frac{A - B}{m})) ⇝ (1 + 0)$
42	18 41	eqbrtrd	$⊢ φ \to (m \in ℕ ⟼ \frac{m + A - B}{m}) ⇝ (1 + 0)$
43		nnssz	$⊢ ℕ \subseteq ℤ$
44		resmpt	$⊢ ℕ \subseteq ℤ \to {(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℕ} = (m \in ℕ ⟼ \frac{m + A - B}{m})$
45	43 44	ax-mp	$⊢ {(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℕ} = (m \in ℕ ⟼ \frac{m + A - B}{m})$
46	19	reseq2i	$⊢ {(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℕ} = {(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℤ_{\geq 1}}$
47	45 46	eqtr3i	$⊢ (m \in ℕ ⟼ \frac{m + A - B}{m}) = {(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℤ_{\geq 1}}$
48		1p0e1	$⊢ 1 + 0 = 1$
49	47 48	breq12i	$⊢ (m \in ℕ ⟼ \frac{m + A - B}{m}) ⇝ (1 + 0) \leftrightarrow ({(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 1$
50		1z	$⊢ 1 \in ℤ$
51		zex	$⊢ ℤ \in V$
52	51	mptex	$⊢ (m \in ℤ ⟼ \frac{m + A - B}{m}) \in V$
53		climres	$⊢ (1 \in ℤ \land (m \in ℤ ⟼ \frac{m + A - B}{m}) \in V) \to (({(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 1 \leftrightarrow (m \in ℤ ⟼ \frac{m + A - B}{m}) ⇝ 1)$
54	50 52 53	mp2an	$⊢ ({(m \in ℤ ⟼ \frac{m + A - B}{m}) ↾}_{ℤ_{\geq 1}}) ⇝ 1 \leftrightarrow (m \in ℤ ⟼ \frac{m + A - B}{m}) ⇝ 1$
55	49 54	bitri	$⊢ (m \in ℕ ⟼ \frac{m + A - B}{m}) ⇝ (1 + 0) \leftrightarrow (m \in ℤ ⟼ \frac{m + A - B}{m}) ⇝ 1$
56	42 55	sylib	$⊢ φ \to (m \in ℤ ⟼ \frac{m + A - B}{m}) ⇝ 1$
57	52	a1i	$⊢ φ \to (m \in ℤ ⟼ \frac{m + A - B}{m}) \in V$
58		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
59	58 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
60	59	zcnd	$⊢ k \in Z \to k \in ℂ$
61	60	adantl	$⊢ (φ \land k \in Z) \to k \in ℂ$
62	4	adantr	$⊢ (φ \land k \in Z) \to B \in ℤ$
63	62	zcnd	$⊢ (φ \land k \in Z) \to B \in ℂ$
64	3	adantr	$⊢ (φ \land k \in Z) \to A \in ℂ$
65	61 63 64	ppncand	$⊢ (φ \land k \in Z) \to k + B + (A - B) = k + A$
66	65	oveq1d	$⊢ (φ \land k \in Z) \to \frac{k + B + (A - B)}{k + B} = \frac{k + A}{k + B}$
67	59	adantl	$⊢ (φ \land k \in Z) \to k \in ℤ$
68	67 62	zaddcld	$⊢ (φ \land k \in Z) \to k + B \in ℤ$
69		oveq1	$⊢ m = k + B \to m + A - B = k + B + (A - B)$
70		id	$⊢ m = k + B \to m = k + B$
71	69 70	oveq12d	$⊢ m = k + B \to \frac{m + A - B}{m} = \frac{k + B + (A - B)}{k + B}$
72		eqid	$⊢ (m \in ℤ ⟼ \frac{m + A - B}{m}) = (m \in ℤ ⟼ \frac{m + A - B}{m})$
73		ovex	$⊢ \frac{k + B + (A - B)}{k + B} \in V$
74	71 72 73	fvmpt	$⊢ k + B \in ℤ \to (m \in ℤ ⟼ \frac{m + A - B}{m}) (k + B) = \frac{k + B + (A - B)}{k + B}$
75	68 74	syl	$⊢ (φ \land k \in Z) \to (m \in ℤ ⟼ \frac{m + A - B}{m}) (k + B) = \frac{k + B + (A - B)}{k + B}$
76	66 75 6	3eqtr4d	$⊢ (φ \land k \in Z) \to (m \in ℤ ⟼ \frac{m + A - B}{m}) (k + B) = F (k)$
77	1 2 4 5 57 76	climshft2	$⊢ φ \to (F ⇝ 1 \leftrightarrow (m \in ℤ ⟼ \frac{m + A - B}{m}) ⇝ 1)$
78	56 77	mpbird	$⊢ φ \to F ⇝ 1$

Metamath Proof Explorer

Theorem divcnvlin

Proof