Metamath Proof Explorer


Theorem recos4p

Description: Separate out the first four terms of the infinite series expansion of the cosine of a real number. (Contributed by Paul Chapman, 19-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypothesis efi4p.1
|- F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
Assertion recos4p
|- ( A e. RR -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 efi4p.1
 |-  F = ( n e. NN0 |-> ( ( ( _i x. A ) ^ n ) / ( ! ` n ) ) )
2 recosval
 |-  ( A e. RR -> ( cos ` A ) = ( Re ` ( exp ` ( _i x. A ) ) ) )
3 recn
 |-  ( A e. RR -> A e. CC )
4 1 efi4p
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
5 3 4 syl
 |-  ( A e. RR -> ( exp ` ( _i x. A ) ) = ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) )
6 5 fveq2d
 |-  ( A e. RR -> ( Re ` ( exp ` ( _i x. A ) ) ) = ( Re ` ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
7 1re
 |-  1 e. RR
8 resqcl
 |-  ( A e. RR -> ( A ^ 2 ) e. RR )
9 8 rehalfcld
 |-  ( A e. RR -> ( ( A ^ 2 ) / 2 ) e. RR )
10 resubcl
 |-  ( ( 1 e. RR /\ ( ( A ^ 2 ) / 2 ) e. RR ) -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. RR )
11 7 9 10 sylancr
 |-  ( A e. RR -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. RR )
12 11 recnd
 |-  ( A e. RR -> ( 1 - ( ( A ^ 2 ) / 2 ) ) e. CC )
13 ax-icn
 |-  _i e. CC
14 3nn0
 |-  3 e. NN0
15 reexpcl
 |-  ( ( A e. RR /\ 3 e. NN0 ) -> ( A ^ 3 ) e. RR )
16 14 15 mpan2
 |-  ( A e. RR -> ( A ^ 3 ) e. RR )
17 6re
 |-  6 e. RR
18 6pos
 |-  0 < 6
19 17 18 gt0ne0ii
 |-  6 =/= 0
20 redivcl
 |-  ( ( ( A ^ 3 ) e. RR /\ 6 e. RR /\ 6 =/= 0 ) -> ( ( A ^ 3 ) / 6 ) e. RR )
21 17 19 20 mp3an23
 |-  ( ( A ^ 3 ) e. RR -> ( ( A ^ 3 ) / 6 ) e. RR )
22 16 21 syl
 |-  ( A e. RR -> ( ( A ^ 3 ) / 6 ) e. RR )
23 resubcl
 |-  ( ( A e. RR /\ ( ( A ^ 3 ) / 6 ) e. RR ) -> ( A - ( ( A ^ 3 ) / 6 ) ) e. RR )
24 22 23 mpdan
 |-  ( A e. RR -> ( A - ( ( A ^ 3 ) / 6 ) ) e. RR )
25 24 recnd
 |-  ( A e. RR -> ( A - ( ( A ^ 3 ) / 6 ) ) e. CC )
26 mulcl
 |-  ( ( _i e. CC /\ ( A - ( ( A ^ 3 ) / 6 ) ) e. CC ) -> ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) e. CC )
27 13 25 26 sylancr
 |-  ( A e. RR -> ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) e. CC )
28 12 27 addcld
 |-  ( A e. RR -> ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) e. CC )
29 mulcl
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
30 13 3 29 sylancr
 |-  ( A e. RR -> ( _i x. A ) e. CC )
31 4nn0
 |-  4 e. NN0
32 1 eftlcl
 |-  ( ( ( _i x. A ) e. CC /\ 4 e. NN0 ) -> sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) e. CC )
33 30 31 32 sylancl
 |-  ( A e. RR -> sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) e. CC )
34 28 33 readdd
 |-  ( A e. RR -> ( Re ` ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) = ( ( Re ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
35 11 24 crred
 |-  ( A e. RR -> ( Re ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) = ( 1 - ( ( A ^ 2 ) / 2 ) ) )
36 35 oveq1d
 |-  ( A e. RR -> ( ( Re ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
37 6 34 36 3eqtrd
 |-  ( A e. RR -> ( Re ` ( exp ` ( _i x. A ) ) ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
38 2 37 eqtrd
 |-  ( A e. RR -> ( cos ` A ) = ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( Re ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )