Theorem climsub 7066

Description: Limit of the difference of two converging sequences. Proposition 12-2.1(b) of [Gleason] p. 168.

Hypotheses

Ref	Expression
climsub.1	|- F e. V
climsub.2	|- G e. V
climsub.3	|- H e. V
climsub.4	|- A e. V
climsub.5	|- B e. V

Assertion

Ref	Expression
climsub	|- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))))) -> H ~~> (A - B))

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

Proof of Theorem climsub

Step	Hyp	Ref	Expression
1		climsub.1	. . . 4 |- F e. V
2		fvex 3717	. . . . 5 |- (ZZ>` M) e. V
3	2	opabex2 3596	. . . 4 |- {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} e. V
4		climsub.3	. . . 4 |- H e. V
5		climsub.4	. . . 4 |- A e. V
6		oprex 3968	. . . 4 |- (-u1 x. B) e. V
7	1, 3, 4, 5, 6	climadd 7053	. . 3 |- (((F ~~> A /\ {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B)) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) e. CC /\ (H` k) = ((F` k) + ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k))))) -> H ~~> (A + (-u1 x. B)))
8		simpll 412	. . . 4 |- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))))) -> F ~~> A)
9		ax1cn 5241	. . . . . . . 8 |- 1 e. CC
10	9	negcl 5341	. . . . . . 7 |- -u1 e. CC
11		climsub.2	. . . . . . . 8 |- G e. V
12		climsub.5	. . . . . . . 8 |- B e. V
13	11, 3, 12	climmulc2 7065	. . . . . . 7 |- (((-u1 e. CC /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k))))) -> {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B))
14	10, 13	mpanl1 704	. . . . . 6 |- ((G ~~> B /\ (M e. ZZ /\ A.k e. (ZZ>` M)((G` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k))))) -> {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B))
15		pm3.27 323	. . . . . . . . 9 |- ((k e. (ZZ>` M) /\ (G` k) e. CC) -> (G` k) e. CC)
16		fveq2 3709	. . . . . . . . . . . 12 |- (u = k -> (G` u) = (G` k))
17	16	opreq2d 3961	. . . . . . . . . . 11 |- (u = k -> (-u1 x. (G` u)) = (-u1 x. (G` k)))
18		eqid 1468	. . . . . . . . . . 11 |- {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} = {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}
19		oprex 3968	. . . . . . . . . . 11 |- (-u1 x. (G` k)) e. V
20	17, 18, 19	fvopab4 3765	. . . . . . . . . 10 |- (k e. (ZZ>` M) -> ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k)))
21	20	adantr 389	. . . . . . . . 9 |- ((k e. (ZZ>` M) /\ (G` k) e. CC) -> ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k)))
22	15, 21	jca 288	. . . . . . . 8 |- ((k e. (ZZ>` M) /\ (G` k) e. CC) -> ((G` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k))))
23	22	3ad2antr2 811	. . . . . . 7 |- ((k e. (ZZ>` M) /\ ((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k)))) -> ((G` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k))))
24	23	r19.20ia 1697	. . . . . 6 |- (A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))) -> A.k e. (ZZ>` M)((G` k) e. CC /\ ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) = (-u1 x. (G` k))))
25	14, 24	sylanr2 463	. . . . 5 |- ((G ~~> B /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))))) -> {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B))
26	25	adantll 392	. . . 4 |- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))))) -> {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B))
27	8, 26	jca 288	. . 3 |- (((F ~~> A /\ G ~~> B) /\ (M e. ZZ /\ A.k e. (ZZ>` M)((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))))) -> (F ~~> A /\ {<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))} ~~> (-u1 x. B)))
28		3simp1 786	. . . . . . . 8 |- (((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k))) -> (F` k) e. CC)
29	28	adantl 388	. . . . . . 7 |- ((k e. (ZZ>` M) /\ ((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k)))) -> (F` k) e. CC)
30		axmulcl 5245	. . . . . . . . . . 11 |- ((-u1 e. CC /\ (G` k) e. CC) -> (-u1 x. (G` k)) e. CC)
31	10, 30	mpan 693	. . . . . . . . . 10 |- ((G` k) e. CC -> (-u1 x. (G` k)) e. CC)
32	31	adantl 388	. . . . . . . . 9 |- ((k e. (ZZ>` M) /\ (G` k) e. CC) -> (-u1 x. (G` k)) e. CC)
33	21, 32	eqeltrd 1540	. . . . . . . 8 |- ((k e. (ZZ>` M) /\ (G` k) e. CC) -> ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) e. CC)
34	33	3ad2antr2 811	. . . . . . 7 |- ((k e. (ZZ>` M) /\ ((F` k) e. CC /\ (G` k) e. CC /\ (H` k) = ((F` k) - (G` k)))) -> ({<.u, v>. | (u e. (ZZ>` M) /\ v = (-u1 x. (G` u)))}` k) e. CC)
35		id 59	. . . . . . . . . . 11 |- ((H` k) = ((F` k) - (G` k)) -> (H` k) = ((F` k) - (G` k)))
36		mulm1t 5443	. . . . . . . . . . . . . 14 |- ((G` k) e. CC -> (-u1 x. (G` k)) = -u(G` k))
37	36	opreq2d 3961	. . . . . . . . . . . . 13 |- ((G` k) e. CC -> ((F` k) + (-u1 x. (G` k))) = ((F` k) + -u(G` k)))
38	37	adantl 388	. . . . . . . . . . . 12 |- (((F` k) e. CC /\ (G` k) e. CC) -> ((F` k) + (-u1 x. (G` k))) = ((F` k) + -u(G` k)))
39		negsubt 5354	. . . . . . . . . . . 12 |- (((F` k) e. CC /\ (G` k) e. CC) -> ((F` k) + -u(G` k)) = ((F` k) - (G` k)))
40	38, 39	eqtr2d 1500	. . . . . . . . . . 11