This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ) )