Metamath Proof Explorer

Theorem resin4p

Description: Separate out the first four terms of the infinite series expansion of the sine 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 resin4p 
|- ( A e. RR -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` 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 resinval 
 |-  ( A e. RR -> ( sin ` A ) = ( Im ` ( 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 -> ( Im ` ( exp ` ( _i x. A ) ) ) = ( Im ` ( ( ( 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 imaddd 
 |-  ( A e. RR -> ( Im ` ( ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) + sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) = ( ( Im ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
35 11 24 crimd 
 |-  ( A e. RR -> ( Im ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) = ( A - ( ( A ^ 3 ) / 6 ) ) )
36 35 oveq1d 
 |-  ( A e. RR -> ( ( Im ` ( ( 1 - ( ( A ^ 2 ) / 2 ) ) + ( _i x. ( A - ( ( A ^ 3 ) / 6 ) ) ) ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
37 6 34 36 3eqtrd 
 |-  ( A e. RR -> ( Im ` ( exp ` ( _i x. A ) ) ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )
38 2 37 eqtrd 
 |-  ( A e. RR -> ( sin ` A ) = ( ( A - ( ( A ^ 3 ) / 6 ) ) + ( Im ` sum_ k e. ( ZZ>= ` 4 ) ( F ` k ) ) ) )