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 ( 𝐴 ∈ dom arctan → ( cos ‘ ( arctan ‘ 𝐴 ) ) = ( 1 / ( √ ‘ ( 1 + ( 𝐴 ↑ 2 ) ) ) ) )

Proof

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