Theorem efiatan2 22334

Description: Value of the exponential of an artcangent. (Contributed by Mario Carneiro, 3-Apr-2015.)

Assertion

Ref	Expression
efiatan2	|- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )

Proof of Theorem efiatan2

Step	Hyp	Ref	Expression
1		ax-icn 9362	. . . . 5 |- _i e. CC
2		atancl 22298	. . . . 5 |- ( A e. dom arctan -> (arctan ` A ) e. CC )
3		mulcl 9387	. . . . 5 |- ( ( _i e. CC /\ (arctan ` A ) e. CC ) -> ( _i x. (arctan ` A ) ) e. CC )
4	1, 2, 3	sylancr 663	. . . 4 |- ( A e. dom arctan -> ( _i x. (arctan ` A ) ) e. CC )
5		efcl 13389	. . . 4 |- ( ( _i x. (arctan ` A ) ) e. CC -> ( exp ` ( _i x. (arctan ` A ) ) ) e. CC )
6	4, 5	syl 16	. . 3 |- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) e. CC )
7		ax-1cn 9361	. . . . 5 |- 1 e. CC
8		atandm2 22294	. . . . . . 7 |- ( A e. dom arctan <-> ( A e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 /\ ( 1 + ( _i x. A ) ) =/= 0 ) )
9	8	simp1bi 1003	. . . . . 6 |- ( A e. dom arctan -> A e. CC )
10	9	sqcld 12027	. . . . 5 |- ( A e. dom arctan -> ( A ^ 2 ) e. CC )
11		addcl 9385	. . . . 5 |- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 + ( A ^ 2 ) ) e. CC )
12	7, 10, 11	sylancr 663	. . . 4 |- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) e. CC )
13	12	sqrcld 12944	. . 3 |- ( A e. dom arctan -> ( sqr ` ( 1 + ( A ^ 2 ) ) ) e. CC )
14	12	sqsqrd 12946	. . . . 5 |- ( A e. dom arctan -> ( ( sqr ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) = ( 1 + ( A ^ 2 ) ) )
15		atandm4 22296	. . . . . 6 |- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
16	15	simprbi 464	. . . . 5 |- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) =/= 0 )
17	14, 16	eqnetrd 2654	. . . 4 |- ( A e. dom arctan -> ( ( sqr ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 )
18		sqne0 11953	. . . . 5 |- ( ( sqr ` ( 1 + ( A ^ 2 ) ) ) e. CC -> ( ( ( sqr ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqr ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
19	13, 18	syl 16	. . . 4 |- ( A e. dom arctan -> ( ( ( sqr ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqr ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
20	17, 19	mpbid 210	. . 3 |- ( A e. dom arctan -> ( sqr ` ( 1 + ( A ^ 2 ) ) ) =/= 0 )
21	6, 13, 20	divcan4d 10134	. 2 |- ( A e. dom arctan -> ( ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) = ( exp ` ( _i x. (arctan ` A ) ) ) )
22		halfcn 10562	. . . . . . 7 |- ( 1 / 2 ) e. CC
23	12, 16	logcld 22044	. . . . . . 7 |- ( A e. dom arctan -> ( log ` ( 1 + ( A ^ 2 ) ) ) e. CC )
24		mulcl 9387	. . . . . . 7 |- ( ( ( 1 / 2 ) e. CC /\ ( log ` ( 1 + ( A ^ 2 ) ) ) e. CC ) -> ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) e. CC )
25	22, 23, 24	sylancr 663	. . . . . 6 |- ( A e. dom arctan -> ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) e. CC )
26		efadd 13400	. . . . . 6 |- ( ( ( _i x. (arctan ` A ) ) e. CC /\ ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) e. CC ) -> ( exp ` ( ( _i x. (arctan ` A ) ) + ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) = ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) )
27	4, 25, 26	syl2anc 661	. . . . 5 |- ( A e. dom arctan -> ( exp ` ( ( _i x. (arctan ` A ) ) + ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) = ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) )
28		2cn 10413	. . . . . . . . . . . 12 |- 2 e. CC
29	28	a1i 11	. . . . . . . . . . 11 |- ( A e. dom arctan -> 2 e. CC )
30		mulcl 9387	. . . . . . . . . . . . . 14 |- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
31	1, 9, 30	sylancr 663	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( _i x. A ) e. CC )
32		addcl 9385	. . . . . . . . . . . . 13 |- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
33	7, 31, 32	sylancr 663	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
34	8	simp3bi 1005	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) =/= 0 )
35	33, 34	logcld 22044	. . . . . . . . . . 11 |- ( A e. dom arctan -> ( log ` ( 1 + ( _i x. A ) ) ) e. CC )
36	29, 35, 4	subdid 9821	. . . . . . . . . 10 |- ( A e. dom arctan -> ( 2 x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) ) = ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( 2 x. ( _i x. (arctan ` A ) ) ) ) )
37		atanval 22301	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> (arctan ` A ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) )
38	37	oveq2d 6128	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( ( 2 x. _i ) x. (arctan ` A ) ) = ( ( 2 x. _i ) x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
39	1	a1i 11	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> _i e. CC )
40	29, 39, 2	mulassd 9430	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( ( 2 x. _i ) x. (arctan ` A ) ) = ( 2 x. ( _i x. (arctan ` A ) ) ) )
41		halfcl 10571	. . . . . . . . . . . . . . . . . 18 |- ( _i e. CC -> ( _i / 2 ) e. CC )
42	1, 41	ax-mp 5	. . . . . . . . . . . . . . . . 17 |- ( _i / 2 ) e. CC
43	28, 1, 42	mulassi 9416	. . . . . . . . . . . . . . . 16 |- ( ( 2 x. _i ) x. ( _i / 2 ) ) = ( 2 x. ( _i x. ( _i / 2 ) ) )
44	28, 1, 42	mul12i 9585	. . . . . . . . . . . . . . . 16 |- ( 2 x. ( _i x. ( _i / 2 ) ) ) = ( _i x. ( 2 x. ( _i / 2 ) ) )
45		2ne0 10435	. . . . . . . . . . . . . . . . . . 19 |- 2 =/= 0
46	1, 28, 45	divcan2i 10095	. . . . . . . . . . . . . . . . . 18 |- ( 2 x. ( _i / 2 ) ) = _i
47	46	oveq2i 6123	. . . . . . . . . . . . . . . . 17 |- ( _i x. ( 2 x. ( _i / 2 ) ) ) = ( _i x. _i )
48		ixi 9986	. . . . . . . . . . . . . . . . 17 |- ( _i x. _i ) = -u 1
49	47, 48	eqtri 2463	. . . . . . . . . . . . . . . 16 |- ( _i x. ( 2 x. ( _i / 2 ) ) ) = -u 1
50	43, 44, 49	3eqtri 2467	. . . . . . . . . . . . . . 15 |- ( ( 2 x. _i ) x. ( _i / 2 ) ) = -u 1
51	50	oveq1i 6122	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. _i ) x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( -u 1 x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
52		subcl 9630	. . . . . . . . . . . . . . . . . 18 |- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
53	7, 31, 52	sylancr 663	. . . . . . . . . . . . . . . . 17 |- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
54	8	simp2bi 1004	. . . . . . . . . . . . . . . . 17 |- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) =/= 0 )
55	53, 54	logcld 22044	. . . . . . . . . . . . . . . 16 |- ( A e. dom arctan -> ( log ` ( 1 - ( _i x. A ) ) ) e. CC )
56	55, 35	subcld 9740	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
57	56	mulm1d 9817	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( -u 1 x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
58	51, 57	syl5eq 2487	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( ( ( 2 x. _i ) x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
59		2mulicn 10569	. . . . . . . . . . . . . . 15 |- ( 2 x. _i ) e. CC
60	59	a1i 11	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( 2 x. _i ) e. CC )
61	42	a1i 11	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( _i / 2 ) e. CC )
62	60, 61, 56	mulassd 9430	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( ( ( 2 x. _i ) x. ( _i / 2 ) ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) = ( ( 2 x. _i ) x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) )
63	55, 35	negsubdi2d 9756	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> -u ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
64	58, 62, 63	3eqtr3d 2483	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( ( 2 x. _i ) x. ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. A ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
65	38, 40, 64	3eqtr3d 2483	. . . . . . . . . . 11 |- ( A e. dom arctan -> ( 2 x. ( _i x. (arctan ` A ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) )
66	65	oveq2d 6128	. . . . . . . . . 10 |- ( A e. dom arctan -> ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( 2 x. ( _i x. (arctan ` A ) ) ) ) = ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
67		mulcl 9387	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ ( log ` ( 1 + ( _i x. A ) ) ) e. CC ) -> ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
68	28, 35, 67	sylancr 663	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) e. CC )
69	68, 35, 55	subsubd 9768	. . . . . . . . . . 11 |- ( A e. dom arctan -> ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) )
70	35	2timesd 10588	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) )
71	70	oveq1d 6127	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) )
72	35, 35	pncand 9741	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
73	71, 72	eqtrd 2475	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
74	73	oveq1d 6127	. . . . . . . . . . 11 |- ( A e. dom arctan -> ( ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( log ` ( 1 + ( _i x. A ) ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) )
75		atanlogadd 22331	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log )
76		logef 22052	. . . . . . . . . . . . 13 |- ( ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) e. ran log -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) )
77	75, 76	syl 16	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) )
78		efadd 13400	. . . . . . . . . . . . . . 15 |- ( ( ( log ` ( 1 + ( _i x. A ) ) ) e. CC /\ ( log ` ( 1 - ( _i x. A ) ) ) e. CC ) -> ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) x. ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
79	35, 55, 78	syl2anc 661	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) x. ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) )
80		eflog 22050	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 + ( _i x. A ) ) e. CC /\ ( 1 + ( _i x. A ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( 1 + ( _i x. A ) ) )
81	33, 34, 80	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) = ( 1 + ( _i x. A ) ) )
82		eflog 22050	. . . . . . . . . . . . . . . 16 |- ( ( ( 1 - ( _i x. A ) ) e. CC /\ ( 1 - ( _i x. A ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( 1 - ( _i x. A ) ) )
83	53, 54, 82	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) = ( 1 - ( _i x. A ) ) )
84	81, 83	oveq12d 6130	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) x. ( exp ` ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) )
85		sq1 11981	. . . . . . . . . . . . . . . . 17 |- ( 1 ^ 2 ) = 1
86	85	a1i 11	. . . . . . . . . . . . . . . 16 |- ( A e. dom arctan -> ( 1 ^ 2 ) = 1 )
87		sqmul 11950	. . . . . . . . . . . . . . . . . 18 |- ( ( _i e. CC /\ A e. CC ) -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) )
88	1, 9, 87	sylancr 663	. . . . . . . . . . . . . . . . 17 |- ( A e. dom arctan -> ( ( _i x. A ) ^ 2 ) = ( ( _i ^ 2 ) x. ( A ^ 2 ) ) )
89		i2 11987	. . . . . . . . . . . . . . . . . . 19 |- ( _i ^ 2 ) = -u 1
90	89	oveq1i 6122	. . . . . . . . . . . . . . . . . 18 |- ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = ( -u 1 x. ( A ^ 2 ) )
91	10	mulm1d 9817	. . . . . . . . . . . . . . . . . 18 |- ( A e. dom arctan -> ( -u 1 x. ( A ^ 2 ) ) = -u ( A ^ 2 ) )
92	90, 91	syl5eq 2487	. . . . . . . . . . . . . . . . 17 |- ( A e. dom arctan -> ( ( _i ^ 2 ) x. ( A ^ 2 ) ) = -u ( A ^ 2 ) )
93	88, 92	eqtrd 2475	. . . . . . . . . . . . . . . 16 |- ( A e. dom arctan -> ( ( _i x. A ) ^ 2 ) = -u ( A ^ 2 ) )
94	86, 93	oveq12d 6130	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( 1 - -u ( A ^ 2 ) ) )
95		subsq 11994	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) )
96	7, 31, 95	sylancr 663	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( ( 1 ^ 2 ) - ( ( _i x. A ) ^ 2 ) ) = ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) )
97		subneg 9679	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 - -u ( A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) )
98	7, 10, 97	sylancr 663	. . . . . . . . . . . . . . 15 |- ( A e. dom arctan -> ( 1 - -u ( A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) )
99	94, 96, 98	3eqtr3d 2483	. . . . . . . . . . . . . 14 |- ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) x. ( 1 - ( _i x. A ) ) ) = ( 1 + ( A ^ 2 ) ) )
100	79, 84, 99	3eqtrd 2479	. . . . . . . . . . . . 13 |- ( A e. dom arctan -> ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( 1 + ( A ^ 2 ) ) )
101	100	fveq2d 5716	. . . . . . . . . . . 12 |- ( A e. dom arctan -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) ) ) = ( log ` ( 1 + ( A ^ 2 ) ) ) )
102	77, 101	eqtr3d 2477	. . . . . . . . . . 11 |- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) + ( log ` ( 1 - ( _i x. A ) ) ) ) = ( log ` ( 1 + ( A ^ 2 ) ) ) )
103	69, 74, 102	3eqtrd 2479	. . . . . . . . . 10 |- ( A e. dom arctan -> ( ( 2 x. ( log ` ( 1 + ( _i x. A ) ) ) ) - ( ( log ` ( 1 + ( _i x. A ) ) ) - ( log ` ( 1 - ( _i x. A ) ) ) ) ) = ( log ` ( 1 + ( A ^ 2 ) ) ) )
104	36, 66, 103	3eqtrd 2479	. . . . . . . . 9 |- ( A e. dom arctan -> ( 2 x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) ) = ( log ` ( 1 + ( A ^ 2 ) ) ) )
105	104	oveq1d 6127	. . . . . . . 8 |- ( A e. dom arctan -> ( ( 2 x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) ) / 2 ) = ( ( log ` ( 1 + ( A ^ 2 ) ) ) / 2 ) )
106	35, 4	subcld 9740	. . . . . . . . 9 |- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) e. CC )
107	45	a1i 11	. . . . . . . . 9 |- ( A e. dom arctan -> 2 =/= 0 )
108	106, 29, 107	divcan3d 10133	. . . . . . . 8 |- ( A e. dom arctan -> ( ( 2 x. ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) ) / 2 ) = ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) )
109	23, 29, 107	divrec2d 10132	. . . . . . . 8 |- ( A e. dom arctan -> ( ( log ` ( 1 + ( A ^ 2 ) ) ) / 2 ) = ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) )
110	105, 108, 109	3eqtr3d 2483	. . . . . . 7 |- ( A e. dom arctan -> ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) = ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) )
111	35, 4, 25	subaddd 9758	. . . . . . 7 |- ( A e. dom arctan -> ( ( ( log ` ( 1 + ( _i x. A ) ) ) - ( _i x. (arctan ` A ) ) ) = ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) <-> ( ( _i x. (arctan ` A ) ) + ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) ) )
112	110, 111	mpbid 210	. . . . . 6 |- ( A e. dom arctan -> ( ( _i x. (arctan ` A ) ) + ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) = ( log ` ( 1 + ( _i x. A ) ) ) )
113	112	fveq2d 5716	. . . . 5 |- ( A e. dom arctan -> ( exp ` ( ( _i x. (arctan ` A ) ) + ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) = ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
114	27, 113	eqtr3d 2477	. . . 4 |- ( A e. dom arctan -> ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) = ( exp ` ( log ` ( 1 + ( _i x. A ) ) ) ) )
115	22	a1i 11	. . . . . . 7 |- ( A e. dom arctan -> ( 1 / 2 ) e. CC )
116	12, 16, 115	cxpefd 22179	. . . . . 6 |- ( A e. dom arctan -> ( ( 1 + ( A ^ 2 ) ) ^c ( 1 / 2 ) ) = ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) )
117		cxpsqr 22170	. . . . . . 7 |- ( ( 1 + ( A ^ 2 ) ) e. CC -> ( ( 1 + ( A ^ 2 ) ) ^c ( 1 / 2 ) ) = ( sqr ` ( 1 + ( A ^ 2 ) ) ) )
118	12, 117	syl 16	. . . . . 6 |- ( A e. dom arctan -> ( ( 1 + ( A ^ 2 ) ) ^c ( 1 / 2 ) ) = ( sqr ` ( 1 + ( A ^ 2 ) ) ) )
119	116, 118	eqtr3d 2477	. . . . 5 |- ( A e. dom arctan -> ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) = ( sqr ` ( 1 + ( A ^ 2 ) ) ) )
120	119	oveq2d 6128	. . . 4 |- ( A e. dom arctan -> ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( exp ` ( ( 1 / 2 ) x. ( log ` ( 1 + ( A ^ 2 ) ) ) ) ) ) = ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )
121	114, 120, 81	3eqtr3d 2483	. . 3 |- ( A e. dom arctan -> ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) = ( 1 + ( _i x. A ) ) )
122	121	oveq1d 6127	. 2 |- ( A e. dom arctan -> ( ( ( exp ` ( _i x. (arctan ` A ) ) ) x. ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )
123	21, 122	eqtr3d 2477	1 |- ( A e. dom arctan -> ( exp ` ( _i x. (arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqr ` ( 1 + ( A ^ 2 ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   e. wcel 1756   =/= wne 2620   dom cdm 4861   ran crn 4862   ` cfv 5439  (class class class)co 6112   CCcc 9301   0cc0 9303   1c1 9304   _ici 9305   + caddc 9306   x. cmul 9308   - cmin 9616   -ucneg 9617   / cdiv 10014   2c2 10392   ^cexp 11886   sqrcsqr 12743   expce 13368   logclog 22028   ^c ccxp 22029  arctancatan 22281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-inf2 7868  ax-cnex 9359  ax-resscn 9360  ax-1cn 9361  ax-icn 9362  ax-addcl 9363  ax-addrcl 9364  ax-mulcl 9365  ax-mulrcl 9366  ax-mulcom 9367  ax-addass 9368  ax-mulass 9369  ax-distr 9370  ax-i2m1 9371  ax-1ne0 9372  ax-1rid 9373  ax-rnegex 9374  ax-rrecex 9375  ax-cnre 9376  ax-pre-lttri 9377  ax-pre-lttrn 9378  ax-pre-ltadd 9379  ax-pre-mulgt0 9380  ax-pre-sup 9381  ax-addf 9382  ax-mulf 9383

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-fal 1375  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-nel 2623  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-iin 4195  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-of 6341  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-2o 6942  df-oadd 6945  df-er 7122  df-map 7237  df-pm 7238  df-ixp 7285  df-en 7332  df-dom 7333  df-sdom 7334  df-fin 7335  df-fsupp 7642  df-fi 7682  df-sup 7712  df-oi 7745  df-card 8130  df-cda 8358  df-pnf 9441  df-mnf 9442  df-xr 9443  df-ltxr 9444  df-le 9445  df-sub 9618  df-neg 9619  df-div 10015  df-nn 10344  df-2 10401  df-3 10402  df-4 10403  df-5 10404  df-6 10405  df-7 10406  df-8 10407  df-9 10408  df-10 10409  df-n0 10601  df-z 10668  df-dec 10777  df-uz 10883  df-q 10975  df-rp 11013  df-xneg 11110  df-xadd 11111  df-xmul 11112  df-ioo 11325  df-ioc 11326  df-ico 11327  df-icc 11328  df-fz 11459  df-fzo 11570  df-fl 11663  df-mod 11730  df-seq 11828  df-exp 11887  df-fac 12073  df-bc 12100  df-hash 12125  df-shft 12577  df-cj 12609  df-re 12610  df-im 12611  df-sqr 12745  df-abs 12746  df-limsup 12970  df-clim 12987  df-rlim 12988  df-sum 13185  df-ef 13374  df-sin 13376  df-cos 13377  df-pi 13379  df-struct 14197  df-ndx 14198  df-slot 14199  df-base 14200  df-sets 14201  df-ress 14202  df-plusg 14272  df-mulr 14273  df-starv 14274  df-sca 14275  df-vsca 14276  df-ip 14277  df-tset 14278  df-ple 14279  df-ds 14281  df-unif 14282  df-hom 14283  df-cco 14284  df-rest 14382  df-topn 14383  df-0g 14401  df-gsum 14402  df-topgen 14403  df-pt 14404  df-prds 14407  df-xrs 14461  df-qtop 14466  df-imas 14467  df-xps 14469  df-mre 14545  df-mrc 14546  df-acs 14548  df-mnd 15436  df-submnd 15486  df-mulg 15569  df-cntz 15856  df-cmn 16300  df-psmet 17831  df-xmet 17832  df-met 17833  df-bl 17834  df-mopn 17835  df-fbas 17836  df-fg 17837  df-cnfld 17841  df-top 18525  df-bases 18527  df-topon 18528  df-topsp 18529  df-cld 18645  df-ntr 18646  df-cls 18647  df-nei 18724  df-lp 18762  df-perf 18763  df-cn 18853  df-cnp 18854  df-haus 18941  df-tx 19157  df-hmeo 19350  df-fil 19441  df-fm 19533  df-flim 19534  df-flf 19535  df-xms 19917  df-ms 19918  df-tms 19919  df-cncf 20476  df-limc 21363  df-dv 21364  df-log 22030  df-cxp 22031  df-atan 22284

This theorem is referenced by:  cosatan  22338