Theorem caucvg3lem 7110

Description: Lemma for caucvg3 7111.

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 3819	. . . 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 3806	. . . . . . 7 |- (x e. NN -> (F` x) e. CC)
6		reclt 6696	. . . . . . 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 1545	. . . . 5 |- (x e. NN -> (G` x) e. RR)
9	8	rgen 1695	. . . 4 |- A.x e. NN (G` x) e. RR
10	1, 2, 9	mpbir2an 729	. . 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 6872	. . 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 7109	. 2 |- E.v e. RR G ~~> v
14		ffnfv 3819	. . . . 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 6697	. . . . . . . 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 1545	. . . . . 6 |- (x e. NN -> (H` x) e. RR)
20	19	rgen 1695	. . . . 5 |- A.x e. NN (H` x) e. RR
21	14, 15, 20	mpbir2an 729	. . . 4 |- H:NN-->RR
22	4, 11, 15, 16	cauim 6873	. . . 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 7109	. . 3 |- E.t e. RR H ~~> t
24		axicn 5250	. . . . . . 7 |- i e. CC
25		1z 6114	. . . . . . . . 9 |- 1 e. ZZ
26		elnnuz 6380	. . . . . . . . . . 11 |- (x e. NN <-> x e. (ZZ>` 1))
27	19	recnd 5295	. . . . . . . . . . . 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 1695	. . . . . . . . 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 5889	. . . . . . . . . 10 |- NN e. V
34		fnex 3599	. . . . . . . . . 10 |- ((H Fn NN /\ NN e. V) -> H e. V)
35	15, 33, 34	mp2an 696	. . . . . . . . 9 |- H e. V
36		caucvg3lem.7	. . . . . . . . . 10 |- R Fn NN
37		fnex 3599	. . . . . . . . . 10 |- ((R Fn NN /\ NN e. V) -> R e. V)
38	36, 33, 37	mp2an 696	. . . . . . . . 9 |- R e. V
39		visset 1809	. . . . . . . . 9 |- t e. V
40	35, 38, 39	climmulc2 7073	. . . . . . . 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 695	. . . . . . 7 |- ((i e. CC /\ H ~~> t) -> R ~~> (i x. t))
42	24, 41	mpan 694	. . . . . 6 |- (H ~~> t -> R ~~> (i x. t))
43		oprex 3974	. . . . . . . 8 |- (i x. t) e. V
44		climcl 6924	. . . . . . . 8 |- (((i x. t) e. V /\ R ~~> (i x. t)) -> (i x. t) e. CC)
45	43, 44	mpan 694	. . . . . . 7 |- (R ~~> (i x. t) -> (i x. t) e. CC)
46		breq2 2618	. . . . . . . 8 |- (u = (i x. t) -> (R ~~> u <-> R ~~> (i x. t)))
47	46	rcla4ev 1873	. . . . . . 7 |- (((i x. t) e. CC /\ R ~~> (i x. t)) -> E.u e. CC R ~~> u)
48	45, 47	mpancom 704	. . . . . 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 1740	. . 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 5295	. . . . . . . . . . . . 13 |- (x e. NN -> (G` x) e. CC)
54		axmulcl 5253	. . . . . . . . . . . . . . . 16 |- ((i e. CC /\ (H` x) e. CC) -> (i x. (H` x)) e. CC)
55	24, 54	mpan 694	. . . . . . . . . . . . . . 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 1545	. . . . . . . . . . . . 13 |- (x e. NN -> (R` x) e. CC)
58		replimtOLD 6701	. . . . . . . . . . . . . . 15 |- ((F` x) e. CC -> (F` x) = ((Re` (F` x)) + ((Im` (F` x)) x. i)))
59	5, 58	syl 10	. . . . . . . . . . . . . 14 |- (x e. NN -> (F` x) = ((Re` (F` x)) + ((Im` (F` x)) x. i)))
60		axmulcom 5256	. . . . . . . . . . . . . . . . . 18 |- ((i e. CC /\ (H` x) e. CC) -> (i x. (H` x)) = ((H` x) x. i))
61	24, 60	mpan 694	. . . . . . . . . . . . . . . . 17 |- ((H` x) e. CC -> (i x. (H` x)) = ((H` x) x. i))
62	27, 61	syl 10	. . . . . . . . . . . . . . . 16 |- (x e. NN -> (i x. (H` x)) = ((H` x) x. i))
63	16	opreq1d 3966	. . . . . . . . . . . . . . . 16 |- (x e. NN -> ((H` x) x. i) = ((Im` (F` x)) x. i))
64	28, 62, 63	3eqtrd 1508	. . . . . . . . . . . . . . 15 |- (x e. NN -> (R` x) = ((Im` (F` x)) x. i))
65	3, 64	opreq12d 3969	. . . . . . . . . . . . . 14 |- (x e. NN -> ((G` x) + (R` x)) = ((Re` (F` x)) + ((Im` (F` x)) x. i)))
66	59, 65	eqtr4d 1507	. . . . . . . . . . . . 13 |- (x e. NN -> (F` x) = ((G` x) + (R` x)))
67	53, 57, 66	3jca 818	. . . . . . . . . . . 12 |- (x e. NN -> ((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))
68	26, 67	sylbir 201	. . . . . . . . . . 11 |- (x e. (ZZ>` 1) -> ((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x))))
69	68	rgen 1695	. . . . . . . . . 10 |- A.x e. (ZZ>` 1)((G` x) e. CC /\ (R` x) e. CC /\ (F` x) = ((G` x) + (R` x)))
70	25, 69	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))))
71		fnex 3599	. . . . . . . . . . 11 |- ((G Fn NN /\ NN e. V) -> G e. V)
72	2, 33, 71	mp2an 696	. . . . . . . . . 10 |- G e. V
73		fex 3643	. . . . . . . . . . 11 |- ((F:NN-->CC /\ NN e. V) -> F e. V)
74	4, 33, 73	mp2an 696	. . . . . . . . . 10 |- F e. V
75		visset 1809	. . . . . . . . . 10 |- v e. V
76		visset 1809	. . . . . . . . . 10 |- u e. V
77	72, 38, 74, 75, 76	climadd 7061	. . . . . . . . 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))
78	70, 77	mpan2 695	. . . . . . . 8 |- ((G ~~> v /\ R ~~> u) -> F ~~> (v + u))
79		oprex 3974	. . . . . . . . . 10 |- (v + u) e. V
80		climcl 6924	. . . . . . . . . 10 |- (((v + u) e. V /\ F ~~> (v + u)) -> (v + u) e. CC)
81	79, 80	mpan 694	. . . . . . . . 9 |- (F ~~> (v + u) -> (v + u) e. CC)
82		breq2 2618	. . . . . . . . . 10 |- (x = (v + u) -> (F ~~> x <-> F ~~> (v