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 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
Assertion recos4p ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 efi4p.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ0 ↦ ( ( ( i · 𝐴 ) ↑ 𝑛 ) / ( ! ‘ 𝑛 ) ) )
2 recosval ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) )
3 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 1 efi4p ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )
5 3 4 syl ⊢ ( 𝐴 ∈ ℝ → ( exp ‘ ( i · 𝐴 ) ) = ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) )
6 5 fveq2d ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ℜ ‘ ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )
7 1re ⊢ 1 ∈ ℝ
8 resqcl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 2 ) ∈ ℝ )
9 8 rehalfcld ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℝ )
10 resubcl ⊢ ( ( 1 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) / 2 ) ∈ ℝ ) → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℝ )
11 7 9 10 sylancr ⊢ ( 𝐴 ∈ ℝ → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℝ )
12 11 recnd ⊢ ( 𝐴 ∈ ℝ → ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) ∈ ℂ )
13 ax-icn ⊢ i ∈ ℂ
14 3nn0 ⊢ 3 ∈ ℕ0
15 reexpcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 3 ∈ ℕ0 ) → ( 𝐴 ↑ 3 ) ∈ ℝ )
16 14 15 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ↑ 3 ) ∈ ℝ )
17 6re ⊢ 6 ∈ ℝ
18 6pos ⊢ 0 < 6
19 17 18 gt0ne0ii ⊢ 6 ≠ 0
20 redivcl ⊢ ( ( ( 𝐴 ↑ 3 ) ∈ ℝ ∧ 6 ∈ ℝ ∧ 6 ≠ 0 ) → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ )
21 17 19 20 mp3an23 ⊢ ( ( 𝐴 ↑ 3 ) ∈ ℝ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ )
22 16 21 syl ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ )
23 resubcl ⊢ ( ( 𝐴 ∈ ℝ ∧ ( ( 𝐴 ↑ 3 ) / 6 ) ∈ ℝ ) → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℝ )
24 22 23 mpdan ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℝ )
25 24 recnd ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℂ )
26 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ∈ ℂ ) → ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ∈ ℂ )
27 13 25 26 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ∈ ℂ )
28 12 27 addcld ⊢ ( 𝐴 ∈ ℝ → ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) ∈ ℂ )
29 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
30 13 3 29 sylancr ⊢ ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∈ ℂ )
31 4nn0 ⊢ 4 ∈ ℕ0
32 1 eftlcl ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 4 ∈ ℕ0 ) → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
33 30 31 32 sylancl ⊢ ( 𝐴 ∈ ℝ → Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
34 28 33 readdd ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) + Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( ( ℜ ‘ ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )
35 11 24 crred ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) ) = ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) )
36 35 oveq1d ⊢ ( 𝐴 ∈ ℝ → ( ( ℜ ‘ ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( i · ( 𝐴 − ( ( 𝐴 ↑ 3 ) / 6 ) ) ) ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )
37 6 34 36 3eqtrd ⊢ ( 𝐴 ∈ ℝ → ( ℜ ‘ ( exp ‘ ( i · 𝐴 ) ) ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )
38 2 37 eqtrd ⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) = ( ( 1 − ( ( 𝐴 ↑ 2 ) / 2 ) ) + ( ℜ ‘ Σ 𝑘 ∈ ( ℤ≥ ‘ 4 ) ( 𝐹 ‘ 𝑘 ) ) ) )