Theorem climmulc2 7129

Description: Limit of a sequence multiplied by a constant C. Corollary 12-2.2 of [Gleason] p. 171.

Hypotheses

Ref	Expression
climmulc2.1	|- F e. V
climmulc2.2	|- G e. V
climmulc2.3	|- A e. V

Assertion

Ref	Expression
climmulc2	|- (((C e. CC /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (C x. (F` k))))) -> G ~~> (C x. A))

Distinct variable groups:   C,k   k,F   k,G   k,M

Proof of Theorem climmulc2

Step	Hyp	Ref	Expression
1		opreq1 3968	. . . . . . . . 9 |- (x = C -> (x x. (F` k)) = (C x. (F` k)))
2	1	eqeq2d 1486	. . . . . . . 8 |- (x = C -> ((G` k) = (x x. (F` k)) <-> (G` k) = (C x. (F` k))))
3	2	anbi2d 616	. . . . . . 7 |- (x = C -> (((F` k) e. CC /\ (G` k) = (x x. (F` k))) <-> ((F` k) e. CC /\ (G` k) = (C x. (F` k)))))
4	3	ralbidv 1663	. . . . . 6 |- (x = C -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) <-> A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (C x. (F` k)))))
5		opreq1 3968	. . . . . . 7 |- (x = C -> (x x. A) = (C x. A))
6	5	breq2d 2630	. . . . . 6 |- (x = C -> (G ~~> (x x. A) <-> G ~~> (C x. A)))
7	4, 6	imbi12d 626	. . . . 5 |- (x = C -> ((A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> G ~~> (x x. A)) <-> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (C x. (F` k))) -> G ~~> (C x. A))))
8	7	imbi2d 612	. . . 4 |- (x = C -> ((M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> G ~~> (x x. A))) <-> (M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (C x. (F` k))) -> G ~~> (C x. A)))))
9	8	imbi2d 612	. . 3 |- (x = C -> ((F ~~> A -> (M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> G ~~> (x x. A)))) <-> (F ~~> A -> (M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (C x. (F` k))) -> G ~~> (C x. A))))))
10		zex 6144	. . . . . . 7 |- ZZ e. V
11		snex 2750	. . . . . . 7 |- {x} e. V
12	10, 11	xpex 3260	. . . . . 6 |- (ZZ X. {x}) e. V
13		climmulc2.1	. . . . . 6 |- F e. V
14		climmulc2.2	. . . . . 6 |- G e. V
15		visset 1813	. . . . . 6 |- x e. V
16		climmulc2.3	. . . . . 6 |- A e. V
17	12, 13, 14, 15, 16	climmul 7128	. . . . 5 |- ((((ZZ X. {x}) ~~> x /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)(((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k))))) -> G ~~> (x x. A))
18		climconst2 7095	. . . . . . 7 |- (x e. CC -> (ZZ X. {x}) ~~> x)
19	18	anim1i 334	. . . . . 6 |- ((x e. CC /\ F ~~> A) -> ((ZZ X. {x}) ~~> x /\ F ~~> A))
20	19	adantr 389	. . . . 5 |- (((x e. CC /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))))) -> ((ZZ X. {x}) ~~> x /\ F ~~> A))
21		fvconst2g 3844	. . . . . . . . . . . . 13 |- ((x e. CC /\ k e. ZZ) -> ((ZZ X. {x})` k) = x)
22		eluzelz 6423	. . . . . . . . . . . . 13 |- (k e. (ZZ>` M) -> k e. ZZ)
23	21, 22	sylan2 451	. . . . . . . . . . . 12 |- ((x e. CC /\ k e. (ZZ>` M)) -> ((ZZ X. {x})` k) = x)
24		pm3.26 319	. . . . . . . . . . . 12 |- ((x e. CC /\ k e. (ZZ>` M)) -> x e. CC)
25	23, 24	eqeltrd 1548	. . . . . . . . . . 11 |- ((x e. CC /\ k e. (ZZ>` M)) -> ((ZZ X. {x})` k) e. CC)
26	25	a1d 12	. . . . . . . . . 10 |- ((x e. CC /\ k e. (ZZ>` M)) -> (((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> ((ZZ X. {x})` k) e. CC))
27		pm3.26 319	. . . . . . . . . . 11 |- (((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> (F` k) e. CC)
28	27	a1i 8	. . . . . . . . . 10 |- ((x e. CC /\ k e. (ZZ>` M)) -> (((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> (F` k) e. CC))
29	23	opreq1d 3975	. . . . . . . . . . . . 13 |- ((x e. CC /\ k e. (ZZ>` M)) -> (((ZZ X. {x})` k) x. (F` k)) = (x x. (F` k)))
30	29	eqeq2d 1486	. . . . . . . . . . . 12 |- ((x e. CC /\ k e. (ZZ>` M)) -> ((G` k) = (((ZZ X. {x})` k) x. (F` k)) <-> (G` k) = (x x. (F` k))))
31	30	biimprd 154	. . . . . . . . . . 11 |- ((x e. CC /\ k e. (ZZ>` M)) -> ((G` k) = (x x. (F` k)) -> (G` k) = (((ZZ X. {x})` k) x. (F` k))))
32	31	adantld 390	. . . . . . . . . 10 |- ((x e. CC /\ k e. (ZZ>` M)) -> (((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> (G` k) = (((ZZ X. {x})` k) x. (F` k))))
33	26, 28, 32	3jcad 820	. . . . . . . . 9 |- ((x e. CC /\ k e. (ZZ>` M)) -> (((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> (((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k)))))
34	33	r19.20dva 1709	. . . . . . . 8 |- (x e. CC -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> A.k e. (ZZ>` M)(((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k)))))
35	34	anim2d 561	. . . . . . 7 |- (x e. CC -> ((M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k)))) -> (M e. ZZ /\ A.k e. (ZZ>` M)(((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k))))))
36	35	imp 350	. . . . . 6 |- ((x e. CC /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))))) -> (M e. ZZ /\ A.k e. (ZZ>` M)(((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k)))))
37	36	adantlr 393	. . . . 5 |- (((x e. CC /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))))) -> (M e. ZZ /\ A.k e. (ZZ>` M)(((ZZ X. {x})` k) e. CC /\ (F` k) e. CC /\ (G` k) = (((ZZ X. {x})` k) x. (F` k)))))
38	17, 20, 37	sylanc 471	. . . 4 |- (((x e. CC /\ F ~~> A) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))))) -> G ~~> (x x. A))
39	38	exp43 384	. . 3 |- (x e. CC -> (F ~~> A -> (M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) = (x x. (F` k))) -> G ~~> (x x. A)))))
40	9, 39	vtoclga 1852	. 2 |- (C e. CC -> (F ~~> A -> (M e. ZZ -> (A.k e. (ZZ>` M)((F` k) e. CC