Step | Hyp | Ref
| Expression |
1 | | oveq2 7413 |
. . . . 5
β’ (π₯ = 0 β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = (((cosβπ΄) + (i Β· (sinβπ΄)))β0)) |
2 | | oveq1 7412 |
. . . . . . 7
β’ (π₯ = 0 β (π₯ Β· π΄) = (0 Β· π΄)) |
3 | 2 | fveq2d 6892 |
. . . . . 6
β’ (π₯ = 0 β (cosβ(π₯ Β· π΄)) = (cosβ(0 Β· π΄))) |
4 | 2 | fveq2d 6892 |
. . . . . . 7
β’ (π₯ = 0 β (sinβ(π₯ Β· π΄)) = (sinβ(0 Β· π΄))) |
5 | 4 | oveq2d 7421 |
. . . . . 6
β’ (π₯ = 0 β (i Β·
(sinβ(π₯ Β·
π΄))) = (i Β·
(sinβ(0 Β· π΄)))) |
6 | 3, 5 | oveq12d 7423 |
. . . . 5
β’ (π₯ = 0 β ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) = ((cosβ(0 Β· π΄)) + (i Β· (sinβ(0
Β· π΄))))) |
7 | 1, 6 | eqeq12d 2748 |
. . . 4
β’ (π₯ = 0 β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) β (((cosβπ΄) + (i Β· (sinβπ΄)))β0) = ((cosβ(0 Β· π΄)) + (i Β· (sinβ(0
Β· π΄)))))) |
8 | 7 | imbi2d 340 |
. . 3
β’ (π₯ = 0 β ((π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄))))) β (π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))β0) = ((cosβ(0
Β· π΄)) + (i Β·
(sinβ(0 Β· π΄))))))) |
9 | | oveq2 7413 |
. . . . 5
β’ (π₯ = π β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = (((cosβπ΄) + (i Β· (sinβπ΄)))βπ)) |
10 | | oveq1 7412 |
. . . . . . 7
β’ (π₯ = π β (π₯ Β· π΄) = (π Β· π΄)) |
11 | 10 | fveq2d 6892 |
. . . . . 6
β’ (π₯ = π β (cosβ(π₯ Β· π΄)) = (cosβ(π Β· π΄))) |
12 | 10 | fveq2d 6892 |
. . . . . . 7
β’ (π₯ = π β (sinβ(π₯ Β· π΄)) = (sinβ(π Β· π΄))) |
13 | 12 | oveq2d 7421 |
. . . . . 6
β’ (π₯ = π β (i Β· (sinβ(π₯ Β· π΄))) = (i Β· (sinβ(π Β· π΄)))) |
14 | 11, 13 | oveq12d 7423 |
. . . . 5
β’ (π₯ = π β ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) |
15 | 9, 14 | eqeq12d 2748 |
. . . 4
β’ (π₯ = π β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))))) |
16 | 15 | imbi2d 340 |
. . 3
β’ (π₯ = π β ((π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄))))) β (π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))))) |
17 | | oveq2 7413 |
. . . . 5
β’ (π₯ = (π + 1) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1))) |
18 | | oveq1 7412 |
. . . . . . 7
β’ (π₯ = (π + 1) β (π₯ Β· π΄) = ((π + 1) Β· π΄)) |
19 | 18 | fveq2d 6892 |
. . . . . 6
β’ (π₯ = (π + 1) β (cosβ(π₯ Β· π΄)) = (cosβ((π + 1) Β· π΄))) |
20 | 18 | fveq2d 6892 |
. . . . . . 7
β’ (π₯ = (π + 1) β (sinβ(π₯ Β· π΄)) = (sinβ((π + 1) Β· π΄))) |
21 | 20 | oveq2d 7421 |
. . . . . 6
β’ (π₯ = (π + 1) β (i Β· (sinβ(π₯ Β· π΄))) = (i Β· (sinβ((π + 1) Β· π΄)))) |
22 | 19, 21 | oveq12d 7423 |
. . . . 5
β’ (π₯ = (π + 1) β ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))) |
23 | 17, 22 | eqeq12d 2748 |
. . . 4
β’ (π₯ = (π + 1) β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄)))))) |
24 | 23 | imbi2d 340 |
. . 3
β’ (π₯ = (π + 1) β ((π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄))))) β (π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))))) |
25 | | oveq2 7413 |
. . . . 5
β’ (π₯ = π β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = (((cosβπ΄) + (i Β· (sinβπ΄)))βπ)) |
26 | | oveq1 7412 |
. . . . . . 7
β’ (π₯ = π β (π₯ Β· π΄) = (π Β· π΄)) |
27 | 26 | fveq2d 6892 |
. . . . . 6
β’ (π₯ = π β (cosβ(π₯ Β· π΄)) = (cosβ(π Β· π΄))) |
28 | 26 | fveq2d 6892 |
. . . . . . 7
β’ (π₯ = π β (sinβ(π₯ Β· π΄)) = (sinβ(π Β· π΄))) |
29 | 28 | oveq2d 7421 |
. . . . . 6
β’ (π₯ = π β (i Β· (sinβ(π₯ Β· π΄))) = (i Β· (sinβ(π Β· π΄)))) |
30 | 27, 29 | oveq12d 7423 |
. . . . 5
β’ (π₯ = π β ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) |
31 | 25, 30 | eqeq12d 2748 |
. . . 4
β’ (π₯ = π β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄)))) β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))))) |
32 | 31 | imbi2d 340 |
. . 3
β’ (π₯ = π β ((π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ₯) = ((cosβ(π₯ Β· π΄)) + (i Β· (sinβ(π₯ Β· π΄))))) β (π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))))) |
33 | | coscl 16066 |
. . . . . 6
β’ (π΄ β β β
(cosβπ΄) β
β) |
34 | | ax-icn 11165 |
. . . . . . 7
β’ i β
β |
35 | | sincl 16065 |
. . . . . . 7
β’ (π΄ β β β
(sinβπ΄) β
β) |
36 | | mulcl 11190 |
. . . . . . 7
β’ ((i
β β β§ (sinβπ΄) β β) β (i Β·
(sinβπ΄)) β
β) |
37 | 34, 35, 36 | sylancr 587 |
. . . . . 6
β’ (π΄ β β β (i
Β· (sinβπ΄))
β β) |
38 | | addcl 11188 |
. . . . . 6
β’
(((cosβπ΄)
β β β§ (i Β· (sinβπ΄)) β β) β ((cosβπ΄) + (i Β· (sinβπ΄))) β
β) |
39 | 33, 37, 38 | syl2anc 584 |
. . . . 5
β’ (π΄ β β β
((cosβπ΄) + (i
Β· (sinβπ΄)))
β β) |
40 | | exp0 14027 |
. . . . 5
β’
(((cosβπ΄) + (i
Β· (sinβπ΄)))
β β β (((cosβπ΄) + (i Β· (sinβπ΄)))β0) = 1) |
41 | 39, 40 | syl 17 |
. . . 4
β’ (π΄ β β β
(((cosβπ΄) + (i
Β· (sinβπ΄)))β0) = 1) |
42 | | mul02 11388 |
. . . . . . . 8
β’ (π΄ β β β (0
Β· π΄) =
0) |
43 | 42 | fveq2d 6892 |
. . . . . . 7
β’ (π΄ β β β
(cosβ(0 Β· π΄))
= (cosβ0)) |
44 | | cos0 16089 |
. . . . . . 7
β’
(cosβ0) = 1 |
45 | 43, 44 | eqtrdi 2788 |
. . . . . 6
β’ (π΄ β β β
(cosβ(0 Β· π΄))
= 1) |
46 | 42 | fveq2d 6892 |
. . . . . . . . 9
β’ (π΄ β β β
(sinβ(0 Β· π΄))
= (sinβ0)) |
47 | | sin0 16088 |
. . . . . . . . 9
β’
(sinβ0) = 0 |
48 | 46, 47 | eqtrdi 2788 |
. . . . . . . 8
β’ (π΄ β β β
(sinβ(0 Β· π΄))
= 0) |
49 | 48 | oveq2d 7421 |
. . . . . . 7
β’ (π΄ β β β (i
Β· (sinβ(0 Β· π΄))) = (i Β· 0)) |
50 | 34 | mul01i 11400 |
. . . . . . 7
β’ (i
Β· 0) = 0 |
51 | 49, 50 | eqtrdi 2788 |
. . . . . 6
β’ (π΄ β β β (i
Β· (sinβ(0 Β· π΄))) = 0) |
52 | 45, 51 | oveq12d 7423 |
. . . . 5
β’ (π΄ β β β
((cosβ(0 Β· π΄))
+ (i Β· (sinβ(0 Β· π΄)))) = (1 + 0)) |
53 | | ax-1cn 11164 |
. . . . . 6
β’ 1 β
β |
54 | 53 | addridi 11397 |
. . . . 5
β’ (1 + 0) =
1 |
55 | 52, 54 | eqtrdi 2788 |
. . . 4
β’ (π΄ β β β
((cosβ(0 Β· π΄))
+ (i Β· (sinβ(0 Β· π΄)))) = 1) |
56 | 41, 55 | eqtr4d 2775 |
. . 3
β’ (π΄ β β β
(((cosβπ΄) + (i
Β· (sinβπ΄)))β0) = ((cosβ(0 Β· π΄)) + (i Β· (sinβ(0
Β· π΄))))) |
57 | | expp1 14030 |
. . . . . . . . 9
β’
((((cosβπ΄) +
(i Β· (sinβπ΄)))
β β β§ π
β β0) β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
58 | 39, 57 | sylan 580 |
. . . . . . . 8
β’ ((π΄ β β β§ π β β0)
β (((cosβπ΄) + (i
Β· (sinβπ΄)))β(π + 1)) = ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
59 | 58 | ancoms 459 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β)
β (((cosβπ΄) + (i
Β· (sinβπ΄)))β(π + 1)) = ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
60 | 59 | adantr 481 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β)
β§ (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
61 | | oveq1 7412 |
. . . . . . 7
β’
((((cosβπ΄) +
(i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄)))) = (((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
62 | 61 | adantl 482 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β)
β§ (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) β ((((cosβπ΄) + (i Β· (sinβπ΄)))βπ) Β· ((cosβπ΄) + (i Β· (sinβπ΄)))) = (((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) Β· ((cosβπ΄) + (i Β· (sinβπ΄))))) |
63 | | nn0cn 12478 |
. . . . . . . . . . . . 13
β’ (π β β0
β π β
β) |
64 | | mulcl 11190 |
. . . . . . . . . . . . 13
β’ ((π β β β§ π΄ β β) β (π Β· π΄) β β) |
65 | 63, 64 | sylan 580 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β (π Β· π΄) β
β) |
66 | | sinadd 16103 |
. . . . . . . . . . . 12
β’ (((π Β· π΄) β β β§ π΄ β β) β (sinβ((π Β· π΄) + π΄)) = (((sinβ(π Β· π΄)) Β· (cosβπ΄)) + ((cosβ(π Β· π΄)) Β· (sinβπ΄)))) |
67 | 65, 66 | sylancom 588 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (sinβ((π
Β· π΄) + π΄)) = (((sinβ(π Β· π΄)) Β· (cosβπ΄)) + ((cosβ(π Β· π΄)) Β· (sinβπ΄)))) |
68 | 33 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (cosβπ΄) β
β) |
69 | | sincl 16065 |
. . . . . . . . . . . . . 14
β’ ((π Β· π΄) β β β (sinβ(π Β· π΄)) β β) |
70 | 65, 69 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (sinβ(π
Β· π΄)) β
β) |
71 | | mulcom 11192 |
. . . . . . . . . . . . 13
β’
(((cosβπ΄)
β β β§ (sinβ(π Β· π΄)) β β) β ((cosβπ΄) Β· (sinβ(π Β· π΄))) = ((sinβ(π Β· π΄)) Β· (cosβπ΄))) |
72 | 68, 70, 71 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((cosβπ΄)
Β· (sinβ(π
Β· π΄))) =
((sinβ(π Β·
π΄)) Β·
(cosβπ΄))) |
73 | 72 | oveq1d 7420 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβπ΄)
Β· (sinβ(π
Β· π΄))) +
((cosβ(π Β·
π΄)) Β·
(sinβπ΄))) =
(((sinβ(π Β·
π΄)) Β·
(cosβπ΄)) +
((cosβ(π Β·
π΄)) Β·
(sinβπ΄)))) |
74 | | mulcl 11190 |
. . . . . . . . . . . . 13
β’
(((cosβπ΄)
β β β§ (sinβ(π Β· π΄)) β β) β ((cosβπ΄) Β· (sinβ(π Β· π΄))) β β) |
75 | 68, 70, 74 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((cosβπ΄)
Β· (sinβ(π
Β· π΄))) β
β) |
76 | | coscl 16066 |
. . . . . . . . . . . . . 14
β’ ((π Β· π΄) β β β (cosβ(π Β· π΄)) β β) |
77 | 65, 76 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (cosβ(π
Β· π΄)) β
β) |
78 | 35 | adantl 482 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (sinβπ΄) β
β) |
79 | | mulcl 11190 |
. . . . . . . . . . . . 13
β’
(((cosβ(π
Β· π΄)) β β
β§ (sinβπ΄) β
β) β ((cosβ(π Β· π΄)) Β· (sinβπ΄)) β β) |
80 | 77, 78, 79 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) β
β) |
81 | | addcom 11396 |
. . . . . . . . . . . 12
β’
((((cosβπ΄)
Β· (sinβ(π
Β· π΄))) β
β β§ ((cosβ(π Β· π΄)) Β· (sinβπ΄)) β β) β (((cosβπ΄) Β· (sinβ(π Β· π΄))) + ((cosβ(π Β· π΄)) Β· (sinβπ΄))) = (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄))))) |
82 | 75, 80, 81 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβπ΄)
Β· (sinβ(π
Β· π΄))) +
((cosβ(π Β·
π΄)) Β·
(sinβπ΄))) =
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))) |
83 | 67, 73, 82 | 3eqtr2d 2778 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β (sinβ((π
Β· π΄) + π΄)) = (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄))))) |
84 | 83 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β)
β (i Β· (sinβ((π Β· π΄) + π΄))) = (i Β· (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄)))))) |
85 | 84 | oveq2d 7421 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β)
β ((cosβ((π
Β· π΄) + π΄)) + (i Β·
(sinβ((π Β·
π΄) + π΄)))) = ((cosβ((π Β· π΄) + π΄)) + (i Β· (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄))))))) |
86 | | adddir 11201 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β β§ π΄ β
β) β ((π + 1)
Β· π΄) = ((π Β· π΄) + (1 Β· π΄))) |
87 | | mullid 11209 |
. . . . . . . . . . . . . . 15
β’ (π΄ β β β (1
Β· π΄) = π΄) |
88 | 87 | oveq2d 7421 |
. . . . . . . . . . . . . 14
β’ (π΄ β β β ((π Β· π΄) + (1 Β· π΄)) = ((π Β· π΄) + π΄)) |
89 | 88 | 3ad2ant3 1135 |
. . . . . . . . . . . . 13
β’ ((π β β β§ 1 β
β β§ π΄ β
β) β ((π
Β· π΄) + (1 Β·
π΄)) = ((π Β· π΄) + π΄)) |
90 | 86, 89 | eqtrd 2772 |
. . . . . . . . . . . 12
β’ ((π β β β§ 1 β
β β§ π΄ β
β) β ((π + 1)
Β· π΄) = ((π Β· π΄) + π΄)) |
91 | 63, 90 | syl3an1 1163 |
. . . . . . . . . . 11
β’ ((π β β0
β§ 1 β β β§ π΄ β β) β ((π + 1) Β· π΄) = ((π Β· π΄) + π΄)) |
92 | 53, 91 | mp3an2 1449 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β ((π + 1) Β·
π΄) = ((π Β· π΄) + π΄)) |
93 | 92 | fveq2d 6892 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β)
β (cosβ((π + 1)
Β· π΄)) =
(cosβ((π Β·
π΄) + π΄))) |
94 | 92 | fveq2d 6892 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β (sinβ((π + 1)
Β· π΄)) =
(sinβ((π Β·
π΄) + π΄))) |
95 | 94 | oveq2d 7421 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β)
β (i Β· (sinβ((π + 1) Β· π΄))) = (i Β· (sinβ((π Β· π΄) + π΄)))) |
96 | 93, 95 | oveq12d 7423 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β)
β ((cosβ((π + 1)
Β· π΄)) + (i Β·
(sinβ((π + 1)
Β· π΄)))) =
((cosβ((π Β·
π΄) + π΄)) + (i Β· (sinβ((π Β· π΄) + π΄))))) |
97 | | mulcl 11190 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ (sinβ(π Β· π΄)) β β) β (i Β·
(sinβ(π Β·
π΄))) β
β) |
98 | 34, 97 | mpan 688 |
. . . . . . . . . . . . 13
β’
((sinβ(π
Β· π΄)) β β
β (i Β· (sinβ(π Β· π΄))) β β) |
99 | 65, 69, 98 | 3syl 18 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β (i Β· (sinβ(π Β· π΄))) β β) |
100 | 33, 37 | jca 512 |
. . . . . . . . . . . . 13
β’ (π΄ β β β
((cosβπ΄) β
β β§ (i Β· (sinβπ΄)) β β)) |
101 | 100 | adantl 482 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((cosβπ΄)
β β β§ (i Β· (sinβπ΄)) β β)) |
102 | | muladd 11642 |
. . . . . . . . . . . 12
β’
((((cosβ(π
Β· π΄)) β β
β§ (i Β· (sinβ(π Β· π΄))) β β) β§ ((cosβπ΄) β β β§ (i
Β· (sinβπ΄))
β β)) β (((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) Β· ((cosβπ΄) + (i Β· (sinβπ΄)))) = ((((cosβ(π Β· π΄)) Β· (cosβπ΄)) + ((i Β· (sinβπ΄)) Β· (i Β·
(sinβ(π Β·
π΄))))) +
(((cosβ(π Β·
π΄)) Β· (i Β·
(sinβπ΄))) +
((cosβπ΄) Β· (i
Β· (sinβ(π
Β· π΄))))))) |
103 | 77, 99, 101, 102 | syl21anc 836 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) + (i Β·
(sinβ(π Β·
π΄)))) Β·
((cosβπ΄) + (i
Β· (sinβπ΄)))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) + ((i
Β· (sinβπ΄))
Β· (i Β· (sinβ(π Β· π΄))))) + (((cosβ(π Β· π΄)) Β· (i Β· (sinβπ΄))) + ((cosβπ΄) Β· (i Β·
(sinβ(π Β·
π΄))))))) |
104 | 78, 34 | jctil 520 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄ β β)
β (i β β β§ (sinβπ΄) β β)) |
105 | 70, 34 | jctil 520 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄ β β)
β (i β β β§ (sinβ(π Β· π΄)) β β)) |
106 | | mul4 11378 |
. . . . . . . . . . . . . . 15
β’ (((i
β β β§ (sinβπ΄) β β) β§ (i β β
β§ (sinβ(π
Β· π΄)) β
β)) β ((i Β· (sinβπ΄)) Β· (i Β· (sinβ(π Β· π΄)))) = ((i Β· i) Β·
((sinβπ΄) Β·
(sinβ(π Β·
π΄))))) |
107 | | ixi 11839 |
. . . . . . . . . . . . . . . 16
β’ (i
Β· i) = -1 |
108 | 107 | oveq1i 7415 |
. . . . . . . . . . . . . . 15
β’ ((i
Β· i) Β· ((sinβπ΄) Β· (sinβ(π Β· π΄)))) = (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄)))) |
109 | 106, 108 | eqtrdi 2788 |
. . . . . . . . . . . . . 14
β’ (((i
β β β§ (sinβπ΄) β β) β§ (i β β
β§ (sinβ(π
Β· π΄)) β
β)) β ((i Β· (sinβπ΄)) Β· (i Β· (sinβ(π Β· π΄)))) = (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄))))) |
110 | 104, 105,
109 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β ((i Β· (sinβπ΄)) Β· (i Β· (sinβ(π Β· π΄)))) = (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄))))) |
111 | 110 | oveq2d 7421 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) + ((i
Β· (sinβπ΄))
Β· (i Β· (sinβ(π Β· π΄))))) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) + (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄)))))) |
112 | 111 | oveq1d 7420 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β ((((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) + ((i
Β· (sinβπ΄))
Β· (i Β· (sinβ(π Β· π΄))))) + (((cosβ(π Β· π΄)) Β· (i Β· (sinβπ΄))) + ((cosβπ΄) Β· (i Β·
(sinβ(π Β·
π΄)))))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) +
(((cosβ(π Β·
π΄)) Β· (i Β·
(sinβπ΄))) +
((cosβπ΄) Β· (i
Β· (sinβ(π
Β· π΄))))))) |
113 | | mul12 11375 |
. . . . . . . . . . . . . . . 16
β’
(((cosβ(π
Β· π΄)) β β
β§ i β β β§ (sinβπ΄) β β) β ((cosβ(π Β· π΄)) Β· (i Β· (sinβπ΄))) = (i Β·
((cosβ(π Β·
π΄)) Β·
(sinβπ΄)))) |
114 | 34, 113 | mp3an2 1449 |
. . . . . . . . . . . . . . 15
β’
(((cosβ(π
Β· π΄)) β β
β§ (sinβπ΄) β
β) β ((cosβ(π Β· π΄)) Β· (i Β· (sinβπ΄))) = (i Β·
((cosβ(π Β·
π΄)) Β·
(sinβπ΄)))) |
115 | 77, 78, 114 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄ β β)
β ((cosβ(π
Β· π΄)) Β· (i
Β· (sinβπ΄))) =
(i Β· ((cosβ(π
Β· π΄)) Β·
(sinβπ΄)))) |
116 | | mul12 11375 |
. . . . . . . . . . . . . . . 16
β’
(((cosβπ΄)
β β β§ i β β β§ (sinβ(π Β· π΄)) β β) β ((cosβπ΄) Β· (i Β·
(sinβ(π Β·
π΄)))) = (i Β·
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))) |
117 | 34, 116 | mp3an2 1449 |
. . . . . . . . . . . . . . 15
β’
(((cosβπ΄)
β β β§ (sinβ(π Β· π΄)) β β) β ((cosβπ΄) Β· (i Β·
(sinβ(π Β·
π΄)))) = (i Β·
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))) |
118 | 68, 70, 117 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ ((π β β0
β§ π΄ β β)
β ((cosβπ΄)
Β· (i Β· (sinβ(π Β· π΄)))) = (i Β· ((cosβπ΄) Β· (sinβ(π Β· π΄))))) |
119 | 115, 118 | oveq12d 7423 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β· (i
Β· (sinβπ΄))) +
((cosβπ΄) Β· (i
Β· (sinβ(π
Β· π΄))))) = ((i
Β· ((cosβ(π
Β· π΄)) Β·
(sinβπ΄))) + (i
Β· ((cosβπ΄)
Β· (sinβ(π
Β· π΄)))))) |
120 | | adddi 11195 |
. . . . . . . . . . . . . . 15
β’ ((i
β β β§ ((cosβ(π Β· π΄)) Β· (sinβπ΄)) β β β§ ((cosβπ΄) Β· (sinβ(π Β· π΄))) β β) β (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))) = ((i Β·
((cosβ(π Β·
π΄)) Β·
(sinβπ΄))) + (i
Β· ((cosβπ΄)
Β· (sinβ(π
Β· π΄)))))) |
121 | 34, 120 | mp3an1 1448 |
. . . . . . . . . . . . . 14
β’
((((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) β
β β§ ((cosβπ΄) Β· (sinβ(π Β· π΄))) β β) β (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))) = ((i Β·
((cosβ(π Β·
π΄)) Β·
(sinβπ΄))) + (i
Β· ((cosβπ΄)
Β· (sinβ(π
Β· π΄)))))) |
122 | 80, 75, 121 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β (i Β· (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄))))) = ((i Β· ((cosβ(π Β· π΄)) Β· (sinβπ΄))) + (i Β· ((cosβπ΄) Β· (sinβ(π Β· π΄)))))) |
123 | 119, 122 | eqtr4d 2775 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β· (i
Β· (sinβπ΄))) +
((cosβπ΄) Β· (i
Β· (sinβ(π
Β· π΄))))) = (i
Β· (((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄)))))) |
124 | 123 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β ((((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) +
(((cosβ(π Β·
π΄)) Β· (i Β·
(sinβπ΄))) +
((cosβπ΄) Β· (i
Β· (sinβ(π
Β· π΄)))))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) + (i
Β· (((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
125 | 103, 112,
124 | 3eqtrd 2776 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) + (i Β·
(sinβ(π Β·
π΄)))) Β·
((cosβπ΄) + (i
Β· (sinβπ΄)))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) + (i
Β· (((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
126 | | mulcl 11190 |
. . . . . . . . . . . . . 14
β’
(((sinβπ΄)
β β β§ (sinβ(π Β· π΄)) β β) β ((sinβπ΄) Β· (sinβ(π Β· π΄))) β β) |
127 | 78, 70, 126 | syl2anc 584 |
. . . . . . . . . . . . 13
β’ ((π β β0
β§ π΄ β β)
β ((sinβπ΄)
Β· (sinβ(π
Β· π΄))) β
β) |
128 | | mulm1 11651 |
. . . . . . . . . . . . 13
β’
(((sinβπ΄)
Β· (sinβ(π
Β· π΄))) β
β β (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄)))) = -((sinβπ΄) Β· (sinβ(π Β· π΄)))) |
129 | 127, 128 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β (-1 Β· ((sinβπ΄) Β· (sinβ(π Β· π΄)))) = -((sinβπ΄) Β· (sinβ(π Β· π΄)))) |
130 | 129 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) =
(((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) +
-((sinβπ΄) Β·
(sinβ(π Β·
π΄))))) |
131 | 130 | oveq1d 7420 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β ((((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) + (-1
Β· ((sinβπ΄)
Β· (sinβ(π
Β· π΄))))) + (i
Β· (((cosβ(π
Β· π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄)))))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) +
-((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
132 | | mulcl 11190 |
. . . . . . . . . . . . 13
β’
(((cosβ(π
Β· π΄)) β β
β§ (cosβπ΄) β
β) β ((cosβ(π Β· π΄)) Β· (cosβπ΄)) β β) |
133 | 77, 68, 132 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) β
β) |
134 | | negsub 11504 |
. . . . . . . . . . . 12
β’
((((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) β
β β§ ((sinβπ΄) Β· (sinβ(π Β· π΄))) β β) β
(((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) +
-((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβ(π Β· π΄))))) |
135 | 133, 127,
134 | syl2anc 584 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) +
-((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβ(π Β· π΄))))) |
136 | 135 | oveq1d 7420 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β ((((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) +
-((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄)))))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) β
((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
137 | 125, 131,
136 | 3eqtrd 2776 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) + (i Β·
(sinβ(π Β·
π΄)))) Β·
((cosβπ΄) + (i
Β· (sinβπ΄)))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) β
((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
138 | | cosadd 16104 |
. . . . . . . . . . . 12
β’ (((π Β· π΄) β β β§ π΄ β β) β (cosβ((π Β· π΄) + π΄)) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) β ((sinβ(π Β· π΄)) Β· (sinβπ΄)))) |
139 | 65, 138 | sylancom 588 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (cosβ((π
Β· π΄) + π΄)) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) β ((sinβ(π Β· π΄)) Β· (sinβπ΄)))) |
140 | | mulcom 11192 |
. . . . . . . . . . . . 13
β’
(((sinβ(π
Β· π΄)) β β
β§ (sinβπ΄) β
β) β ((sinβ(π Β· π΄)) Β· (sinβπ΄)) = ((sinβπ΄) Β· (sinβ(π Β· π΄)))) |
141 | 70, 78, 140 | syl2anc 584 |
. . . . . . . . . . . 12
β’ ((π β β0
β§ π΄ β β)
β ((sinβ(π
Β· π΄)) Β·
(sinβπ΄)) =
((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) |
142 | 141 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) Β·
(cosβπ΄)) β
((sinβ(π Β·
π΄)) Β·
(sinβπ΄))) =
(((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) β
((sinβπ΄) Β·
(sinβ(π Β·
π΄))))) |
143 | 139, 142 | eqtrd 2772 |
. . . . . . . . . 10
β’ ((π β β0
β§ π΄ β β)
β (cosβ((π
Β· π΄) + π΄)) = (((cosβ(π Β· π΄)) Β· (cosβπ΄)) β ((sinβπ΄) Β· (sinβ(π Β· π΄))))) |
144 | 143 | oveq1d 7420 |
. . . . . . . . 9
β’ ((π β β0
β§ π΄ β β)
β ((cosβ((π
Β· π΄) + π΄)) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄)))))) =
((((cosβ(π Β·
π΄)) Β·
(cosβπ΄)) β
((sinβπ΄) Β·
(sinβ(π Β·
π΄)))) + (i Β·
(((cosβ(π Β·
π΄)) Β·
(sinβπ΄)) +
((cosβπ΄) Β·
(sinβ(π Β·
π΄))))))) |
145 | 137, 144 | eqtr4d 2775 |
. . . . . . . 8
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) + (i Β·
(sinβ(π Β·
π΄)))) Β·
((cosβπ΄) + (i
Β· (sinβπ΄)))) =
((cosβ((π Β·
π΄) + π΄)) + (i Β· (((cosβ(π Β· π΄)) Β· (sinβπ΄)) + ((cosβπ΄) Β· (sinβ(π Β· π΄))))))) |
146 | 85, 96, 145 | 3eqtr4rd 2783 |
. . . . . . 7
β’ ((π β β0
β§ π΄ β β)
β (((cosβ(π
Β· π΄)) + (i Β·
(sinβ(π Β·
π΄)))) Β·
((cosβπ΄) + (i
Β· (sinβπ΄)))) =
((cosβ((π + 1)
Β· π΄)) + (i Β·
(sinβ((π + 1)
Β· π΄))))) |
147 | 146 | adantr 481 |
. . . . . 6
β’ (((π β β0
β§ π΄ β β)
β§ (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) β (((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) Β· ((cosβπ΄) + (i Β· (sinβπ΄)))) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))) |
148 | 60, 62, 147 | 3eqtrd 2776 |
. . . . 5
β’ (((π β β0
β§ π΄ β β)
β§ (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))) |
149 | 148 | exp31 420 |
. . . 4
β’ (π β β0
β (π΄ β β
β ((((cosβπ΄) +
(i Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))) β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))))) |
150 | 149 | a2d 29 |
. . 3
β’ (π β β0
β ((π΄ β β
β (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) β (π΄ β β β (((cosβπ΄) + (i Β· (sinβπ΄)))β(π + 1)) = ((cosβ((π + 1) Β· π΄)) + (i Β· (sinβ((π + 1) Β· π΄))))))) |
151 | 8, 16, 24, 32, 56, 150 | nn0ind 12653 |
. 2
β’ (π β β0
β (π΄ β β
β (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄)))))) |
152 | 151 | impcom 408 |
1
β’ ((π΄ β β β§ π β β0)
β (((cosβπ΄) + (i
Β· (sinβπ΄)))βπ) = ((cosβ(π Β· π΄)) + (i Β· (sinβ(π Β· π΄))))) |