Metamath Proof Explorer


Theorem climcj

Description: Limit of the complex conjugate 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 = M
climcn1lem.2 φ F A
climcn1lem.4 φ G W
climcn1lem.5 φ M
climcn1lem.6 φ k Z F k
climcj.7 φ k Z G k = F k
Assertion climcj φ G A

Proof

Step Hyp Ref Expression
1 climcn1lem.1 Z = M
2 climcn1lem.2 φ F A
3 climcn1lem.4 φ G W
4 climcn1lem.5 φ M
5 climcn1lem.6 φ k Z F k
6 climcj.7 φ k Z G k = F k
7 cjf * :
8 cjcn2 A x + y + z z A < y z A < x
9 1 2 3 4 5 7 8 6 climcn1lem φ G A