Theorem rlimabs

Description: Limit of the absolute value of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	rlimabs.1	|- ( ( ph /\ k e. A ) -> B e. V )
	rlimabs.2	|- ( ph -> ( k e. A |-> B ) ~~>r C )
Assertion	rlimabs	|- ( ph -> ( k e. A |-> ( abs ` B ) ) ~~>r ( abs ` C ) )

Proof

Step	Hyp	Ref	Expression
1		rlimabs.1	|- ( ( ph /\ k e. A ) -> B e. V )
2		rlimabs.2	|- ( ph -> ( k e. A |-> B ) ~~>r C )
3	1 2	rlimmptrcl	|- ( ( ph /\ k e. A ) -> B e. CC )
4		rlimcl	|- ( ( k e. A |-> B ) ~~>r C -> C e. CC )
5	2 4	syl	|- ( ph -> C e. CC )
6		absf	|- abs : CC --> RR
7		ax-resscn	|- RR C_ CC
8		fss	|- ( ( abs : CC --> RR /\ RR C_ CC ) -> abs : CC --> CC )
9	6 7 8	mp2an	|- abs : CC --> CC
10	9	a1i	|- ( ph -> abs : CC --> CC )
11		abscn2	|- ( ( C e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( abs ` z ) - ( abs ` C ) ) ) < x ) )
12	5 11	sylan	|- ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - C ) ) < y -> ( abs ` ( ( abs ` z ) - ( abs ` C ) ) ) < x ) )
13	3 5 2 10 12	rlimcn1b	|- ( ph -> ( k e. A |-> ( abs ` B ) ) ~~>r ( abs ` C ) )