Description: Limit of the real part of a sequence. Proposition 12-2.4(c) of Gleason p. 172. (Contributed by NM, 7-Jun-2006) (Revised by Mario Carneiro, 9-Feb-2014)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | climcn1lem.1 | |- Z = ( ZZ>= ` M ) |
|
| climcn1lem.2 | |- ( ph -> F ~~> A ) |
||
| climcn1lem.4 | |- ( ph -> G e. W ) |
||
| climcn1lem.5 | |- ( ph -> M e. ZZ ) |
||
| climcn1lem.6 | |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
||
| climre.7 | |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Re ` ( F ` k ) ) ) |
||
| Assertion | climre | |- ( ph -> G ~~> ( Re ` A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | climcn1lem.1 | |- Z = ( ZZ>= ` M ) |
|
| 2 | climcn1lem.2 | |- ( ph -> F ~~> A ) |
|
| 3 | climcn1lem.4 | |- ( ph -> G e. W ) |
|
| 4 | climcn1lem.5 | |- ( ph -> M e. ZZ ) |
|
| 5 | climcn1lem.6 | |- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
|
| 6 | climre.7 | |- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( Re ` ( F ` k ) ) ) |
|
| 7 | ref | |- Re : CC --> RR |
|
| 8 | ax-resscn | |- RR C_ CC |
|
| 9 | fss | |- ( ( Re : CC --> RR /\ RR C_ CC ) -> Re : CC --> CC ) |
|
| 10 | 7 8 9 | mp2an | |- Re : CC --> CC |
| 11 | recn2 | |- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) < x ) ) |
|
| 12 | 1 2 3 4 5 10 11 6 | climcn1lem | |- ( ph -> G ~~> ( Re ` A ) ) |