Theorem sqcn 8335

Description: The square function on complex numbers is continuous.

Hypotheses

Ref	Expression
sqcn.2	|- D = (IndMet` <.<. + , x. >., abs>.)
sqcn.j	|- J = (Open` D)
sqcn.1	|- F = {<.x, y>. | (x e. CC /\ y = (x^2))}

Assertion

Ref	Expression
sqcn	|- F e. (J Cn J)

Distinct variable group:   x,y

Proof of Theorem sqcn

Step	Hyp	Ref	Expression
1		sqcn.2	. . . . 5 |- D = (IndMet` <.<. + , x. >., abs>.)
2		eqid 1475	. . . . . 6 |- <.<. + , x. >., abs>. = <.<. + , x. >., abs>.
3		eqid 1475	. . . . . 6 |- (abs o. - ) = (abs o. - )
4	2, 3	cnims 8334	. . . . 5 |- (abs o. - ) = (IndMet` <.<. + , x. >., abs>.)
5	1, 4	eqtr4 1498	. . . 4 |- D = (abs o. - )
6	5	cnmet 7904	. . 3 |- D e. Met
7		sqcn.1	. . . 4 |- F = {<.x, y>. | (x e. CC /\ y = (x^2))}
8		sqclt 6611	. . . 4 |- (x e. CC -> (x^2) e. CC)
9	7, 8	fopab 3827	. . 3 |- F:CC-->CC
10	5	cnmetba 7903	. . . 4 |- CC = dom dom D
11		sqcn.j	. . . 4 |- J = (Open` D)
12		eqid 1475	. . . 4 |- {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} = {<.w, v>. | (w e. NN /\ v = (F` (f` w)))}
13	10, 10, 11, 11, 12	metcn4 7971	. . 3 |- ((D e. Met /\ D e. Met /\ F:CC-->CC) -> (F e. (J Cn J) <-> A.f(f:NN-->CC -> A.z e. CC (f(~~>m` D)z -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} (~~>m` D)(F` z)))))
14	6, 6, 9, 13	mp3an 916	. 2 |- (F e. (J Cn J) <-> A.f(f:NN-->CC -> A.z e. CC (f(~~>m` D)z -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} (~~>m` D)(F` z))))
15		visset 1813	. . . . . . . . . 10 |- f e. V
16		nnex 5933	. . . . . . . . . . 11 |- NN e. V
17	16	opabex2 3610	. . . . . . . . . 10 |- {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} e. V
18		visset 1813	. . . . . . . . . 10 |- z e. V
19	15, 15, 17, 18, 18	climmul 7128	. . . . . . . . 9 |- (((f ~~> z /\ f ~~> z) /\ (1 e. ZZ /\ A.u e. (ZZ>` 1)((f` u) e. CC /\ (f` u) e. CC /\ ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u))))) -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (z x. z))
20		id 59	. . . . . . . . . 10 |- (f ~~> z -> f ~~> z)
21	20	ancli 296	. . . . . . . . 9 |- (f ~~> z -> (f ~~> z /\ f ~~> z))
22		ffvelrn 3814	. . . . . . . . . . . . 13 |- ((f:NN-->CC /\ u e. NN) -> (f` u) e. CC)
23		fveq2 3724	. . . . . . . . . . . . . . . . 17 |- (w = u -> (f` w) = (f` u))
24	23	fveq2d 3728	. . . . . . . . . . . . . . . 16 |- (w = u -> (F` (f` w)) = (F` (f` u)))
25		fvex 3732	. . . . . . . . . . . . . . . 16 |- (F` (f` u)) e. V
26	24, 12, 25	fvopab4 3780	. . . . . . . . . . . . . . 15 |- (u e. NN -> ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = (F` (f` u)))
27	26	adantl 388	. . . . . . . . . . . . . 14 |- ((f:NN-->CC /\ u e. NN) -> ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = (F` (f` u)))
28		opreq1 3968	. . . . . . . . . . . . . . . . 17 |- (x = (f` u) -> (x^2) = ((f` u)^2))
29		oprex 3983	. . . . . . . . . . . . . . . . 17 |- ((f` u)^2) e. V
30	28, 7, 29	fvopab4 3780	. . . . . . . . . . . . . . . 16 |- ((f` u) e. CC -> (F` (f` u)) = ((f` u)^2))
31		sqvalt 6609	. . . . . . . . . . . . . . . 16 |- ((f` u) e. CC -> ((f` u)^2) = ((f` u) x. (f` u)))
32	30, 31	eqtrd 1507	. . . . . . . . . . . . . . 15 |- ((f` u) e. CC -> (F` (f` u)) = ((f` u) x. (f` u)))
33	22, 32	syl 10	. . . . . . . . . . . . . 14 |- ((f:NN-->CC /\ u e. NN) -> (F` (f` u)) = ((f` u) x. (f` u)))
34	27, 33	eqtrd 1507	. . . . . . . . . . . . 13 |- ((f:NN-->CC /\ u e. NN) -> ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u)))
35	22, 22, 34	3jca 819	. . . . . . . . . . . 12 |- ((f:NN-->CC /\ u e. NN) -> ((f` u) e. CC /\ (f` u) e. CC /\ ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u))))
36		elnnuz 6440	. . . . . . . . . . . 12 |- (u e. NN <-> u e. (ZZ>` 1))
37	35, 36	sylan2br 453	. . . . . . . . . . 11 |- ((f:NN-->CC /\ u e. (ZZ>` 1)) -> ((f` u) e. CC /\ (f` u) e. CC /\ ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u))))
38	37	r19.21aiva 1714	. . . . . . . . . 10 |- (f:NN-->CC -> A.u e. (ZZ>` 1)((f` u) e. CC /\ (f` u) e. CC /\ ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u))))
39		1z 6159	. . . . . . . . . 10 |- 1 e. ZZ
40	38, 39	jctil 292	. . . . . . . . 9 |- (f:NN-->CC -> (1 e. ZZ /\ A.u e. (ZZ>` 1)((f` u) e. CC /\ (f` u) e. CC /\ ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))}` u) = ((f` u) x. (f` u)))))
41	19, 21, 40	syl2an 454	. . . . . . . 8 |- ((f ~~> z /\ f:NN-->CC) -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (z x. z))
42	41	adantrl 394	. . . . . . 7 |- ((f ~~> z /\ (z e. CC /\ f:NN-->CC)) -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (z x. z))
43		opreq1 3968	. . . . . . . . . 10 |- (x = z -> (x^2) = (z^2))
44		oprex 3983	. . . . . . . . . 10 |- (z^2) e. V
45	43, 7, 44	fvopab4 3780	. . . . . . . . 9 |- (z e. CC -> (F` z) = (z^2))
46		sqvalt 6609	. . . . . . . . 9 |- (z e. CC -> (z^2) = (z x. z))
47	45, 46	eqtrd 1507	. . . . . . . 8 |- (z e. CC -> (F` z) = (z x. z))
48	47	ad2antrl 406	. . . . . . 7 |- ((f ~~> z /\ (z e. CC /\ f:NN-->CC)) -> (F` z) = (z x. z))
49	42, 48	breqtrrd 2641	. . . . . 6 |- ((f ~~> z /\ (z e. CC /\ f:NN-->CC)) -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (F` z))
50	49	expcom 374	. . . . 5 |- ((z e. CC /\ f:NN-->CC) -> (f ~~> z -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (F` z)))
51	5	lmclimnn 7964	. . . . 5 |- ((z e. CC /\ f:NN-->CC) -> (f(~~>m` D)z <-> f ~~> z))
52		ffvelrn 3814	. . . . . . . . . 10 |- ((f:NN-->CC /\ w e. NN) -> (f` w) e. CC)
53	9	ffvelrni 3815	. . . . . . . . . 10 |- ((f` w) e. CC -> (F` (f` w)) e. CC)
54	52, 53	syl 10	. . . . . . . . 9 |- ((f:NN-->CC /\ w e. NN) -> (F` (f` w)) e. CC)
55	54	r19.21aiva 1714	. . . . . . . 8 |- (f:NN-->CC -> A.w e. NN (F` (f` w)) e. CC)
56	12	fopab2 3823	. . . . . . . 8 |- (A.w e. NN (F` (f` w)) e. CC <-> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))}:NN-->CC)
57	55, 56	sylib 198	. . . . . . 7 |- (f:NN-->CC -> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))}:NN-->CC)
58		fvex 3732	. . . . . . . 8 |- (F` z) e. V
59	5	lmclimnn 7964	. . . . . . . 8 |- (((F` z) e. V /\ {<.w, v>. | (w e. NN /\ v = (F` (f` w)))}:NN-->CC) -> ({<.w, v>. | (w e. NN /\ v = (F` (f` w)))} (~~>m` D)(F` z) <-> {<.w, v>. | (w e. NN /\ v = (F` (f` w)))} ~~> (F` z)))
60	58, 59	mpan 695	. . . . . . 7 |- ({<.w, v>. | (w e. NN /\ v = (F