geolim3

Description: Geometric series convergence with arbitrary shift, radix, and multiplicative constant. (Contributed by Stefan O'Rear, 16-Nov-2014)

	Ref	Expression
Hypotheses	geolim3.a	$⊢ φ \to A \in ℤ$
	geolim3.b1	$⊢ φ \to B \in ℂ$
	geolim3.b2	$⊢ φ \to \|B\| < 1$
	geolim3.c	$⊢ φ \to C \in ℂ$
	geolim3.f	$⊢ F = (k \in ℤ_{\geq A} ⟼ C B^{k - A})$
Assertion	geolim3	$⊢ φ \to seq A (+ F) ⇝ (\frac{C}{1 - B})$

Proof

Step	Hyp	Ref	Expression
1		geolim3.a	$⊢ φ \to A \in ℤ$
2		geolim3.b1	$⊢ φ \to B \in ℂ$
3		geolim3.b2	$⊢ φ \to \|B\| < 1$
4		geolim3.c	$⊢ φ \to C \in ℂ$
5		geolim3.f	$⊢ F = (k \in ℤ_{\geq A} ⟼ C B^{k - A})$
6		seqeq3	$⊢ F = (k \in ℤ_{\geq A} ⟼ C B^{k - A}) \to seq A (+ F) = seq A (+ (k \in ℤ_{\geq A} ⟼ C B^{k - A}))$
7	5 6	ax-mp	$⊢ seq A (+ F) = seq A (+ (k \in ℤ_{\geq A} ⟼ C B^{k - A}))$
8		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
9		0zd	$⊢ φ \to 0 \in ℤ$
10		oveq2	$⊢ k = a \to B^{k} = B^{a}$
11		eqid	$⊢ (k \in ℕ_{0} ⟼ B^{k}) = (k \in ℕ_{0} ⟼ B^{k})$
12		ovex	$⊢ B^{a} \in V$
13	10 11 12	fvmpt	$⊢ a \in ℕ_{0} \to (k \in ℕ_{0} ⟼ B^{k}) (a) = B^{a}$
14	13	adantl	$⊢ (φ \land a \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ B^{k}) (a) = B^{a}$
15	2 3 14	geolim	$⊢ φ \to seq 0 (+ (k \in ℕ_{0} ⟼ B^{k})) ⇝ (\frac{1}{1 - B})$
16		expcl	$⊢ (B \in ℂ \land a \in ℕ_{0}) \to B^{a} \in ℂ$
17	2 16	sylan	$⊢ (φ \land a \in ℕ_{0}) \to B^{a} \in ℂ$
18	14 17	eqeltrd	$⊢ (φ \land a \in ℕ_{0}) \to (k \in ℕ_{0} ⟼ B^{k}) (a) \in ℂ$
19	1	zcnd	$⊢ φ \to A \in ℂ$
20		nn0cn	$⊢ a \in ℕ_{0} \to a \in ℂ$
21		fvex	$⊢ ℤ_{\geq A} \in V$
22	21	mptex	$⊢ (k \in ℤ_{\geq A} ⟼ C B^{k - A}) \in V$
23	22	shftval4	$⊢ (A \in ℂ \land a \in ℂ) \to ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A)) (a) = (k \in ℤ_{\geq A} ⟼ C B^{k - A}) (A + a)$
24	19 20 23	syl2an	$⊢ (φ \land a \in ℕ_{0}) \to ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A)) (a) = (k \in ℤ_{\geq A} ⟼ C B^{k - A}) (A + a)$
25		uzid	$⊢ A \in ℤ \to A \in ℤ_{\geq A}$
26	1 25	syl	$⊢ φ \to A \in ℤ_{\geq A}$
27		uzaddcl	$⊢ (A \in ℤ_{\geq A} \land a \in ℕ_{0}) \to A + a \in ℤ_{\geq A}$
28	26 27	sylan	$⊢ (φ \land a \in ℕ_{0}) \to A + a \in ℤ_{\geq A}$
29		oveq1	$⊢ k = A + a \to k - A = A + a - A$
30	29	oveq2d	$⊢ k = A + a \to B^{k - A} = B^{A + a - A}$
31	30	oveq2d	$⊢ k = A + a \to C B^{k - A} = C B^{A + a - A}$
32		eqid	$⊢ (k \in ℤ_{\geq A} ⟼ C B^{k - A}) = (k \in ℤ_{\geq A} ⟼ C B^{k - A})$
33		ovex	$⊢ C B^{A + a - A} \in V$
34	31 32 33	fvmpt	$⊢ A + a \in ℤ_{\geq A} \to (k \in ℤ_{\geq A} ⟼ C B^{k - A}) (A + a) = C B^{A + a - A}$
35	28 34	syl	$⊢ (φ \land a \in ℕ_{0}) \to (k \in ℤ_{\geq A} ⟼ C B^{k - A}) (A + a) = C B^{A + a - A}$
36		pncan2	$⊢ (A \in ℂ \land a \in ℂ) \to A + a - A = a$
37	19 20 36	syl2an	$⊢ (φ \land a \in ℕ_{0}) \to A + a - A = a$
38	37	oveq2d	$⊢ (φ \land a \in ℕ_{0}) \to B^{A + a - A} = B^{a}$
39	38 14	eqtr4d	$⊢ (φ \land a \in ℕ_{0}) \to B^{A + a - A} = (k \in ℕ_{0} ⟼ B^{k}) (a)$
40	39	oveq2d	$⊢ (φ \land a \in ℕ_{0}) \to C B^{A + a - A} = C (k \in ℕ_{0} ⟼ B^{k}) (a)$
41	24 35 40	3eqtrd	$⊢ (φ \land a \in ℕ_{0}) \to ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A)) (a) = C (k \in ℕ_{0} ⟼ B^{k}) (a)$
42	8 9 4 15 18 41	isermulc2	$⊢ φ \to seq 0 (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A))) ⇝ C (\frac{1}{1 - B})$
43	19	negidd	$⊢ φ \to A + (- A) = 0$
44	43	seqeq1d	$⊢ φ \to seq (A + (- A)) (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A))) = seq 0 (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A)))$
45		ax-1cn	$⊢ 1 \in ℂ$
46		subcl	$⊢ (1 \in ℂ \land B \in ℂ) \to 1 - B \in ℂ$
47	45 2 46	sylancr	$⊢ φ \to 1 - B \in ℂ$
48		abs1	$⊢ \|1\| = 1$
49	48	a1i	$⊢ φ \to \|1\| = 1$
50	2	abscld	$⊢ φ \to \|B\| \in ℝ$
51	50 3	gtned	$⊢ φ \to 1 \neq \|B\|$
52	49 51	eqnetrd	$⊢ φ \to \|1\| \neq \|B\|$
53		fveq2	$⊢ 1 = B \to \|1\| = \|B\|$
54	53	necon3i	$⊢ \|1\| \neq \|B\| \to 1 \neq B$
55	52 54	syl	$⊢ φ \to 1 \neq B$
56		subeq0	$⊢ (1 \in ℂ \land B \in ℂ) \to (1 - B = 0 \leftrightarrow 1 = B)$
57	45 2 56	sylancr	$⊢ φ \to (1 - B = 0 \leftrightarrow 1 = B)$
58	57	necon3bid	$⊢ φ \to (1 - B \neq 0 \leftrightarrow 1 \neq B)$
59	55 58	mpbird	$⊢ φ \to 1 - B \neq 0$
60	4 47 59	divrecd	$⊢ φ \to \frac{C}{1 - B} = C (\frac{1}{1 - B})$
61	42 44 60	3brtr4d	$⊢ φ \to seq (A + (- A)) (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A))) ⇝ (\frac{C}{1 - B})$
62	1	znegcld	$⊢ φ \to - A \in ℤ$
63	22	isershft	$⊢ (A \in ℤ \land - A \in ℤ) \to (seq A (+ (k \in ℤ_{\geq A} ⟼ C B^{k - A})) ⇝ (\frac{C}{1 - B}) \leftrightarrow seq (A + (- A)) (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A))) ⇝ (\frac{C}{1 - B}))$
64	1 62 63	syl2anc	$⊢ φ \to (seq A (+ (k \in ℤ_{\geq A} ⟼ C B^{k - A})) ⇝ (\frac{C}{1 - B}) \leftrightarrow seq (A + (- A)) (+ ((k \in ℤ_{\geq A} ⟼ C B^{k - A}) shift (- A))) ⇝ (\frac{C}{1 - B}))$
65	61 64	mpbird	$⊢ φ \to seq A (+ (k \in ℤ_{\geq A} ⟼ C B^{k - A})) ⇝ (\frac{C}{1 - B})$
66	7 65	eqbrtrid	$⊢ φ \to seq A (+ F) ⇝ (\frac{C}{1 - B})$

Metamath Proof Explorer

Theorem geolim3

Proof