Theorem cosatan

Description: The cosine of an arctangent. (Contributed by Mario Carneiro, 3-Apr-2015)

	Ref	Expression
Assertion	cosatan	|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		atancl	|- ( A e. dom arctan -> ( arctan ` A ) e. CC )
2		cosval	|- ( ( arctan ` A ) e. CC -> ( cos ` ( arctan ` A ) ) = ( ( ( exp ` ( _i x. ( arctan ` A ) ) ) + ( exp ` ( -u _i x. ( arctan ` A ) ) ) ) / 2 ) )
3	1 2	syl	|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) = ( ( ( exp ` ( _i x. ( arctan ` A ) ) ) + ( exp ` ( -u _i x. ( arctan ` A ) ) ) ) / 2 ) )
4		efiatan2	|- ( A e. dom arctan -> ( exp ` ( _i x. ( arctan ` A ) ) ) = ( ( 1 + ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
5		ax-icn	|- _i e. CC
6		mulneg12	|- ( ( _i e. CC /\ ( arctan ` A ) e. CC ) -> ( -u _i x. ( arctan ` A ) ) = ( _i x. -u ( arctan ` A ) ) )
7	5 1 6	sylancr	|- ( A e. dom arctan -> ( -u _i x. ( arctan ` A ) ) = ( _i x. -u ( arctan ` A ) ) )
8		atanneg	|- ( A e. dom arctan -> ( arctan ` -u A ) = -u ( arctan ` A ) )
9	8	oveq2d	|- ( A e. dom arctan -> ( _i x. ( arctan ` -u A ) ) = ( _i x. -u ( arctan ` A ) ) )
10	7 9	eqtr4d	|- ( A e. dom arctan -> ( -u _i x. ( arctan ` A ) ) = ( _i x. ( arctan ` -u A ) ) )
11	10	fveq2d	|- ( A e. dom arctan -> ( exp ` ( -u _i x. ( arctan ` A ) ) ) = ( exp ` ( _i x. ( arctan ` -u A ) ) ) )
12		atandmneg	|- ( A e. dom arctan -> -u A e. dom arctan )
13		efiatan2	|- ( -u A e. dom arctan -> ( exp ` ( _i x. ( arctan ` -u A ) ) ) = ( ( 1 + ( _i x. -u A ) ) / ( sqrt ` ( 1 + ( -u A ^ 2 ) ) ) ) )
14	12 13	syl	|- ( A e. dom arctan -> ( exp ` ( _i x. ( arctan ` -u A ) ) ) = ( ( 1 + ( _i x. -u A ) ) / ( sqrt ` ( 1 + ( -u A ^ 2 ) ) ) ) )
15		atandm4	|- ( A e. dom arctan <-> ( A e. CC /\ ( 1 + ( A ^ 2 ) ) =/= 0 ) )
16	15	simplbi	|- ( A e. dom arctan -> A e. CC )
17		mulneg2	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
18	5 16 17	sylancr	|- ( A e. dom arctan -> ( _i x. -u A ) = -u ( _i x. A ) )
19	18	oveq2d	|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 + -u ( _i x. A ) ) )
20		ax-1cn	|- 1 e. CC
21		mulcl	|- ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
22	5 16 21	sylancr	|- ( A e. dom arctan -> ( _i x. A ) e. CC )
23		negsub	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
24	20 22 23	sylancr	|- ( A e. dom arctan -> ( 1 + -u ( _i x. A ) ) = ( 1 - ( _i x. A ) ) )
25	19 24	eqtrd	|- ( A e. dom arctan -> ( 1 + ( _i x. -u A ) ) = ( 1 - ( _i x. A ) ) )
26		sqneg	|- ( A e. CC -> ( -u A ^ 2 ) = ( A ^ 2 ) )
27	16 26	syl	|- ( A e. dom arctan -> ( -u A ^ 2 ) = ( A ^ 2 ) )
28	27	oveq2d	|- ( A e. dom arctan -> ( 1 + ( -u A ^ 2 ) ) = ( 1 + ( A ^ 2 ) ) )
29	28	fveq2d	|- ( A e. dom arctan -> ( sqrt ` ( 1 + ( -u A ^ 2 ) ) ) = ( sqrt ` ( 1 + ( A ^ 2 ) ) ) )
30	25 29	oveq12d	|- ( A e. dom arctan -> ( ( 1 + ( _i x. -u A ) ) / ( sqrt ` ( 1 + ( -u A ^ 2 ) ) ) ) = ( ( 1 - ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
31	11 14 30	3eqtrd	|- ( A e. dom arctan -> ( exp ` ( -u _i x. ( arctan ` A ) ) ) = ( ( 1 - ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
32	4 31	oveq12d	|- ( A e. dom arctan -> ( ( exp ` ( _i x. ( arctan ` A ) ) ) + ( exp ` ( -u _i x. ( arctan ` A ) ) ) ) = ( ( ( 1 + ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) + ( ( 1 - ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) ) )
33		addcl	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 + ( _i x. A ) ) e. CC )
34	20 22 33	sylancr	|- ( A e. dom arctan -> ( 1 + ( _i x. A ) ) e. CC )
35		subcl	|- ( ( 1 e. CC /\ ( _i x. A ) e. CC ) -> ( 1 - ( _i x. A ) ) e. CC )
36	20 22 35	sylancr	|- ( A e. dom arctan -> ( 1 - ( _i x. A ) ) e. CC )
37	16	sqcld	|- ( A e. dom arctan -> ( A ^ 2 ) e. CC )
38		addcl	|- ( ( 1 e. CC /\ ( A ^ 2 ) e. CC ) -> ( 1 + ( A ^ 2 ) ) e. CC )
39	20 37 38	sylancr	|- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) e. CC )
40	39	sqrtcld	|- ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC )
41	39	sqsqrtd	|- ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) = ( 1 + ( A ^ 2 ) ) )
42	15	simprbi	|- ( A e. dom arctan -> ( 1 + ( A ^ 2 ) ) =/= 0 )
43	41 42	eqnetrd	|- ( A e. dom arctan -> ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 )
44		sqne0	|- ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) e. CC -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
45	40 44	syl	|- ( A e. dom arctan -> ( ( ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ^ 2 ) =/= 0 <-> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 ) )
46	43 45	mpbid	|- ( A e. dom arctan -> ( sqrt ` ( 1 + ( A ^ 2 ) ) ) =/= 0 )
47	34 36 40 46	divdird	|- ( A e. dom arctan -> ( ( ( 1 + ( _i x. A ) ) + ( 1 - ( _i x. A ) ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) = ( ( ( 1 + ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) + ( ( 1 - ( _i x. A ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) ) )
48	20	a1i	|- ( A e. dom arctan -> 1 e. CC )
49	48 22 48	ppncand	|- ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) + ( 1 - ( _i x. A ) ) ) = ( 1 + 1 ) )
50		df-2	|- 2 = ( 1 + 1 )
51	49 50	eqtr4di	|- ( A e. dom arctan -> ( ( 1 + ( _i x. A ) ) + ( 1 - ( _i x. A ) ) ) = 2 )
52	51	oveq1d	|- ( A e. dom arctan -> ( ( ( 1 + ( _i x. A ) ) + ( 1 - ( _i x. A ) ) ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) = ( 2 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
53	32 47 52	3eqtr2d	|- ( A e. dom arctan -> ( ( exp ` ( _i x. ( arctan ` A ) ) ) + ( exp ` ( -u _i x. ( arctan ` A ) ) ) ) = ( 2 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
54	53	oveq1d	|- ( A e. dom arctan -> ( ( ( exp ` ( _i x. ( arctan ` A ) ) ) + ( exp ` ( -u _i x. ( arctan ` A ) ) ) ) / 2 ) = ( ( 2 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) / 2 ) )
55		2cnd	|- ( A e. dom arctan -> 2 e. CC )
56		2ne0	|- 2 =/= 0
57	56	a1i	|- ( A e. dom arctan -> 2 =/= 0 )
58	55 40 55 46 57	divdiv32d	|- ( A e. dom arctan -> ( ( 2 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) / 2 ) = ( ( 2 / 2 ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
59		2div2e1	|- ( 2 / 2 ) = 1
60	59	oveq1i	|- ( ( 2 / 2 ) / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) )
61	58 60	eqtrdi	|- ( A e. dom arctan -> ( ( 2 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) / 2 ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )
62	3 54 61	3eqtrd	|- ( A e. dom arctan -> ( cos ` ( arctan ` A ) ) = ( 1 / ( sqrt ` ( 1 + ( A ^ 2 ) ) ) ) )