Theorem caucvg3lem 7166

Description: Lemma for caucvg3 7167.

Hypotheses

Ref	Expression
caucvg3lem.1	|- F:NN-->CC
caucvg3lem.2	|- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
caucvg3lem.3	|- G Fn NN
caucvg3lem.4	|- (x e. NN -> (G` x) = (Re` (F` x)))
caucvg3lem.5	|- H Fn NN
caucvg3lem.6	|- (x e. NN -> (H` x) = (Im` (F` x)))
caucvg3lem.7	|- R Fn NN
caucvg3lem.8	|- (x e. NN -> (R` x) = (i x. (H` x)))

Assertion

Ref	Expression
caucvg3lem	|- E.x e. CC F ~~> x

Distinct variable groups:   x,F   x,y,z,w,G   x,H,y,z,w   x,R

Proof of Theorem caucvg3lem

Step	Hyp	Ref	Expression
1		ffnfv 3828	. . . 4 |- (G:NN-->RR <-> (G Fn NN /\ A.x e. NN (G` x) e. RR))
2		caucvg3lem.3	. . . 4 |- G Fn NN
3		caucvg3lem.4	. . . . . 6 |- (x e. NN -> (G` x) = (Re` (F` x)))
4		caucvg3lem.1	. . . . . . . 8 |- F:NN-->CC
5	4	ffvelrni 3815	. . . . . . 7 |- (x e. NN -> (F` x) e. CC)
6		reclt 6757	. . . . . . 7 |- ((F` x) e. CC -> (Re` (F` x)) e. RR)
7	5, 6	syl 10	. . . . . 6 |- (x e. NN -> (Re` (F` x)) e. RR)
8	3, 7	eqeltrd 1548	. . . . 5 |- (x e. NN -> (G` x) e. RR)
9	8	rgen 1698	. . . 4 |- A.x e. NN (G` x) e. RR
10	1, 2, 9	mpbir2an 730	. . 3 |- G:NN-->RR
11		caucvg3lem.2	. . . 4 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((F` y) - (F` w))) < z))
12	4, 11, 2, 3	caure 6927	. . 3 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((G` y) - (G` w))) < z))
13	10, 12	caucvg2 7165	. 2 |- E.v e. RR G ~~> v
14		ffnfv 3828	. . . . 5 |- (H:NN-->RR <-> (H Fn NN /\ A.x e. NN (H` x) e. RR))
15		caucvg3lem.5	. . . . 5 |- H Fn NN
16		caucvg3lem.6	. . . . . . 7 |- (x e. NN -> (H` x) = (Im` (F` x)))
17		imclt 6758	. . . . . . . 8 |- ((F` x) e. CC -> (Im` (F` x)) e. RR)
18	5, 17	syl 10	. . . . . . 7 |- (x e. NN -> (Im` (F` x)) e. RR)
19	16, 18	eqeltrd 1548	. . . . . 6 |- (x e. NN -> (H` x) e. RR)
20	19	rgen 1698	. . . . 5 |- A.x e. NN (H` x) e. RR
21	14, 15, 20	mpbir2an 730	. . . 4 |- H:NN-->RR
22	4, 11, 15, 16	cauim 6928	. . . 4 |- A.z e. RR (0 < z -> E.w e. NN A.y e. NN (w < y -> (abs` ((H` y) - (H` w))) < z))
23	21, 22	caucvg2 7165	. . 3 |- E.t e. RR H ~~> t
24		axicn 5270	. . . . . . 7 |- i e. CC
25		1z 6159	. . . . . . . . 9 |- 1 e. ZZ
26		elnnuz 6440	. . . . . . . . . . 11 |- (x e. NN <-> x e. (ZZ>` 1))
27	19	recnd 5315	. . . . . . . . . . . 12 |- (x e. NN -> (H` x) e. CC)
28		caucvg3lem.8	. . . . . . . . . . . 12 |- (x e. NN -> (R` x) = (i x. (H` x)))
29	27, 28	jca 288	. . . . . . . . . . 11 |- (x e. NN -> ((H` x) e. CC /\ (R` x) = (i x. (H` x))))
30	26, 29	sylbir 201	. . . . . . . . . 10 |- (x e. (ZZ>` 1) -> ((H` x) e. CC /\ (R` x) = (i x. (H` x))))
31	30	rgen 1698	. . . . . . . . 9 |- A.x e. (ZZ>` 1)((H` x) e. CC /\ (R` x) = (i x. (H` x)))
32	25, 31	pm3.2i 285	. . . . . . . 8 |- (1 e. ZZ /\ A.x e. (ZZ>` 1)((H` x) e. CC /\ (R` x) = (i x. (H` x))))
33		nnex 5933	. . . . . . . . . 10 |- NN e. V
34		fnex 3607	. . . . . . . . . 10 |- ((H Fn NN /\ NN e. V) -> H e. V)
35	15, 33, 34	mp2an 697	. . . . . . . . 9 |- H e. V
36		caucvg3lem.7	. . . . . . . . . 10 |- R Fn NN
37		fnex 3607	. . . . . . . . . 10 |- ((R Fn NN /\ NN e. V) -> R e. V)
38	36, 33, 37	mp2an 697	. . . . . . . . 9 |- R e. V
39		visset 1813	. . . . . . . . 9 |- t e. V
40	35, 38, 39	climmulc2 7129	. . . . . . . 8 |- (((i e. CC /\ H ~~> t) /\ (1 e. ZZ /\ A.x e. (ZZ>` 1)((H` x) e. CC /\ (R` x) = (i x. (H` x))))) -> R ~~> (i x. t))
41	32, 40	mpan2 696	. . . . . . 7 |- ((i e. CC /\ H ~~> t) -> R ~~> (i x. t))
42	24, 41	mpan 695	. . . . . 6 |- (H ~~> t -> R ~~> (i x. t))
43		oprex 3983	. . . . . . . 8 |- (i x. t) e. V
44		climcl 6978	. . . . . . . 8 |- (((i x. t) e. V /\ R ~~> (i x. t)) -> (i x. t) e. CC)
45	43, 44	mpan 695	. . . . . . 7 |- (R ~~> (i x. t) -> (i x. t) e. CC)
46		breq2 2623	. . . . . . . 8 |- (u = (i x. t) -> (R ~~> u <-> R ~~> (i x. t)))
47	46	rcla4ev 1877	. . . . . . 7 |- (((i x. t) e. CC /\ R ~~> (i x. t)) -> E.u e. CC R ~~> u)
48	45, 47	mpancom 705	. . . . . 6 |- (R ~~> (i x. t) -> E.u e. CC R ~~> u)
49	42, 48	syl 10	. . . . 5 |- (H ~~> t -> E.u e. CC R ~~> u)
50	49	a1i 8	. . . 4 |- (t e. RR -> (H ~~> t -> E.u e. CC R ~~> u))
51	50	r19.23aiv 1743	. . 3 |- (E.t e. RR H ~~> t -> E.u e. CC R ~~> u)
52	23, 51	ax-mp 7	. 2 |- E.u e. CC R ~~> u
53	8	recnd 5315	. . . . . . . . . . . . 13 |- (x e. NN -> (G` x) e. CC)
54		axmulcl 5273	. . . . . . . . . . . . . . . 16 |- ((i e. CC /\ (H` x) e. CC) -> (i x. (H` x)) e. CC)
55	24, 54	mpan 695	. . . . . . . . . . . . . . 15 |- ((H` x) e. CC -> (i x. (H` x)) e. CC)
56	27, 55	syl 10	. . . . . . . . . . . . . 14 |- (x e. NN -> (i x. (H` x)) e. CC)
57	28, 56	eqeltrd 1548	. . . . . . . . . . . . 13 |- (x e. NN -> (R` x) e. CC)
58		replimt 6761	. . . . . . . . . . . . . . 15 |- ((F` x) e. CC -> (F` x) = ((Re` (F` x)) + (i x. (Im` (F` x)))))
59	5, 58	syl 10	. . . . . . . . . . . . . 14 |- (x e. NN -> (F` x) = ((Re` (F` x)) + (i x. (Im` (F` x)))))
60	16	opreq2d 3976	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (i x. (H` x)) = (i x. (Im` (F` x))))
61	28, 60	eqtrd 1507	. . . . . . . . . . . . . . 15 |- (x e. NN -> (R` x) = (i x. (Im` (F` x))))
62	3, 61	opreq12d 3978	. . . . . . . . . . . . . 14 |- (x e. NN -> ((G` x) + (R` x)) = ((Re` (F` x)) + (i x. (Im` (F` x)))))
63	59, 62	eqtr4d 1510	. . . . . . . . . . . . 13 |- (x e. NN -> (F` x) = ((G` x) + (R` x)))
64	53, 57, 63	3jca 819	. . . . . . . . . . . 12 |- (x e. NN -> ((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))
65	26, 64	sylbir 201	. . . . . . . . . . 11 |- (x e. (ZZ>` 1) -> ((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))
66	65	rgen 1698	. . . . . . . . . 10 |- A.x e. (ZZ>` 1)((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x)))
67	25, 66	pm3.2i 285	. . . . . . . . 9 |- (1 e. ZZ /\ A.x e. (ZZ>` 1)((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))
68		fnex 3607	. . . . . . . . . . 11 |- ((G Fn NN /\ NN e. V) -> G e. V)
69	2, 33, 68	mp2an 697	. . . . . . . . . 10 |- G e. V
70		fex 3652	. . . . . . . . . . 11 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
71	4, 33, 70	mp2an 697	. . . . . . . . . 10 |- F e. V
72		visset 1813	. . . . . . . . . 10 |- v e. V
73		visset 1813	. . . . . . . . . 10 |- u e. V
74	69, 38, 71, 72, 73	climadd 7117	. . . . . . . . 9 |- (((G ~~> v /\ R ~~> u) /\ (1 e. ZZ /\ A.x e. (ZZ>` 1)((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))) -> F ~~> (v + u))
75	67, 74	mpan2 696	. . . . . . . 8 |- ((G ~~> v /\ R ~~> u) -> F ~~> (v + u))
76		oprex 3983	. . . . . . . . . 10 |- (v + u) e. V
77		climcl 6978	. . . . . . . . . 10 |- (((v + u) e. V /\ F ~~> (v + u)) -> (v + u) e. CC)
78	76, 77	mpan 695	. . . . . . . . 9 |- (F ~~> (v + u) -> (v + u) e. CC)
79		breq2 2623	. . . . . . . . . 10 |- (x = (v + u) -> (F ~~> x <-> F ~~> (v + u)))
80	79	rcla4ev 1877	. . . . . . . . 9 |- (((v + u) e. CC /\ F ~~> (v + u)) -> E.x e. CC F ~~> x)
81	78, 80	mpancom 705	. . . . . . . 8 |- (F ~~> (v + u) -> E.x e. CC F ~~> x)
82	75, 81	syl 10	. . . . . . 7 |- ((G ~~> v /\ R ~~> u) -> E.x e. CC F ~~> x)
83	82	ex 373	. . . . . 6 |- (G ~~> v -> (R ~~> u -> E.x