Metamath Proof Explorer

Theorem sinperlem

Description: Lemma for sinper and cosper . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Hypotheses sinperlem.1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) 𝑂 ( exp ‘ ( - i · 𝐴 ) ) ) / 𝐷 ) )
sinperlem.2 ⊢ ( ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ∈ ℂ → ( 𝐹 ‘ ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) 𝑂 ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) ) / 𝐷 ) )
Assertion sinperlem ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( 𝐹 ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sinperlem.1 ⊢ ( 𝐴 ∈ ℂ → ( 𝐹 ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) 𝑂 ( exp ‘ ( - i · 𝐴 ) ) ) / 𝐷 ) )
2 sinperlem.2 ⊢ ( ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ∈ ℂ → ( 𝐹 ‘ ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) 𝑂 ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) ) / 𝐷 ) )
3 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
4 2cn ⊢ 2 ∈ ℂ
5 picn ⊢ π ∈ ℂ
6 4 5 mulcli ⊢ ( 2 · π ) ∈ ℂ
7 mulcl ⊢ ( ( 𝐾 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → ( 𝐾 · ( 2 · π ) ) ∈ ℂ )
8 3 6 7 sylancl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( 2 · π ) ) ∈ ℂ )
9 ax-icn ⊢ i ∈ ℂ
10 adddi ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( i · 𝐴 ) + ( i · ( 𝐾 · ( 2 · π ) ) ) ) )
11 9 10 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( i · 𝐴 ) + ( i · ( 𝐾 · ( 2 · π ) ) ) ) )
12 8 11 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( i · 𝐴 ) + ( i · ( 𝐾 · ( 2 · π ) ) ) ) )
13 mul12 ⊢ ( ( i ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ ( 2 · π ) ∈ ℂ ) → ( i · ( 𝐾 · ( 2 · π ) ) ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
14 9 6 13 mp3an13 ⊢ ( 𝐾 ∈ ℂ → ( i · ( 𝐾 · ( 2 · π ) ) ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
15 3 14 syl ⊢ ( 𝐾 ∈ ℤ → ( i · ( 𝐾 · ( 2 · π ) ) ) = ( 𝐾 · ( i · ( 2 · π ) ) ) )
16 9 6 mulcli ⊢ ( i · ( 2 · π ) ) ∈ ℂ
17 mulcom ⊢ ( ( 𝐾 ∈ ℂ ∧ ( i · ( 2 · π ) ) ∈ ℂ ) → ( 𝐾 · ( i · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · 𝐾 ) )
18 3 16 17 sylancl ⊢ ( 𝐾 ∈ ℤ → ( 𝐾 · ( i · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · 𝐾 ) )
19 15 18 eqtrd ⊢ ( 𝐾 ∈ ℤ → ( i · ( 𝐾 · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · 𝐾 ) )
20 19 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( i · ( 𝐾 · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · 𝐾 ) )
21 20 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( i · 𝐴 ) + ( i · ( 𝐾 · ( 2 · π ) ) ) ) = ( ( i · 𝐴 ) + ( ( i · ( 2 · π ) ) · 𝐾 ) ) )
22 12 21 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( i · 𝐴 ) + ( ( i · ( 2 · π ) ) · 𝐾 ) ) )
23 22 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) )
24 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
25 9 24 mpan ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
26 efper ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( ( i · 𝐴 ) + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ ( i · 𝐴 ) ) )
27 25 26 sylan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( ( i · 𝐴 ) + ( ( i · ( 2 · π ) ) · 𝐾 ) ) ) = ( exp ‘ ( i · 𝐴 ) ) )
28 23 27 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) = ( exp ‘ ( i · 𝐴 ) ) )
29 negicn ⊢ - i ∈ ℂ
30 adddi ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( - i · 𝐴 ) + ( - i · ( 𝐾 · ( 2 · π ) ) ) ) )
31 29 30 mp3an1 ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( - i · 𝐴 ) + ( - i · ( 𝐾 · ( 2 · π ) ) ) ) )
32 8 31 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( - i · 𝐴 ) + ( - i · ( 𝐾 · ( 2 · π ) ) ) ) )
33 19 negeqd ⊢ ( 𝐾 ∈ ℤ → - ( i · ( 𝐾 · ( 2 · π ) ) ) = - ( ( i · ( 2 · π ) ) · 𝐾 ) )
34 mulneg1 ⊢ ( ( i ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( - i · ( 𝐾 · ( 2 · π ) ) ) = - ( i · ( 𝐾 · ( 2 · π ) ) ) )
35 9 8 34 sylancr ⊢ ( 𝐾 ∈ ℤ → ( - i · ( 𝐾 · ( 2 · π ) ) ) = - ( i · ( 𝐾 · ( 2 · π ) ) ) )
36 mulneg2 ⊢ ( ( ( i · ( 2 · π ) ) ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( i · ( 2 · π ) ) · - 𝐾 ) = - ( ( i · ( 2 · π ) ) · 𝐾 ) )
37 16 3 36 sylancr ⊢ ( 𝐾 ∈ ℤ → ( ( i · ( 2 · π ) ) · - 𝐾 ) = - ( ( i · ( 2 · π ) ) · 𝐾 ) )
38 33 35 37 3eqtr4d ⊢ ( 𝐾 ∈ ℤ → ( - i · ( 𝐾 · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · - 𝐾 ) )
39 38 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( - i · ( 𝐾 · ( 2 · π ) ) ) = ( ( i · ( 2 · π ) ) · - 𝐾 ) )
40 39 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( - i · 𝐴 ) + ( - i · ( 𝐾 · ( 2 · π ) ) ) ) = ( ( - i · 𝐴 ) + ( ( i · ( 2 · π ) ) · - 𝐾 ) ) )
41 32 40 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( - i · 𝐴 ) + ( ( i · ( 2 · π ) ) · - 𝐾 ) ) )
42 41 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) = ( exp ‘ ( ( - i · 𝐴 ) + ( ( i · ( 2 · π ) ) · - 𝐾 ) ) ) )
43 mulcl ⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
44 29 43 mpan ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
45 znegcl ⊢ ( 𝐾 ∈ ℤ → - 𝐾 ∈ ℤ )
46 efper ⊢ ( ( ( - i · 𝐴 ) ∈ ℂ ∧ - 𝐾 ∈ ℤ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( ( i · ( 2 · π ) ) · - 𝐾 ) ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
47 44 45 46 syl2an ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( ( - i · 𝐴 ) + ( ( i · ( 2 · π ) ) · - 𝐾 ) ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
48 42 47 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
49 28 48 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) 𝑂 ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) 𝑂 ( exp ‘ ( - i · 𝐴 ) ) ) )
50 49 oveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( ( ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) 𝑂 ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) ) / 𝐷 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) 𝑂 ( exp ‘ ( - i · 𝐴 ) ) ) / 𝐷 ) )
51 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐾 · ( 2 · π ) ) ∈ ℂ ) → ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ∈ ℂ )
52 8 51 sylan2 ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ∈ ℂ )
53 52 2 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( ( ( exp ‘ ( i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) 𝑂 ( exp ‘ ( - i · ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) ) ) / 𝐷 ) )
54 1 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( 𝐹 ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) 𝑂 ( exp ‘ ( - i · 𝐴 ) ) ) / 𝐷 ) )
55 50 53 54 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ ) → ( 𝐹 ‘ ( 𝐴 + ( 𝐾 · ( 2 · π ) ) ) ) = ( 𝐹 ‘ 𝐴 ) )