Proof of Theorem abssinper
Step | Hyp | Ref
| Expression |
1 | | zcn 9190 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℤ → 𝐾 ∈
ℂ) |
2 | | halfcl 9077 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℂ → (𝐾 / 2) ∈
ℂ) |
3 | | 2cn 8922 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℂ |
4 | | picn 13306 |
. . . . . . . . . . . . 13
⊢ π
∈ ℂ |
5 | | mulass 7878 |
. . . . . . . . . . . . 13
⊢ (((𝐾 / 2) ∈ ℂ ∧ 2
∈ ℂ ∧ π ∈ ℂ) → (((𝐾 / 2) · 2) · π) = ((𝐾 / 2) · (2 ·
π))) |
6 | 3, 4, 5 | mp3an23 1318 |
. . . . . . . . . . . 12
⊢ ((𝐾 / 2) ∈ ℂ →
(((𝐾 / 2) · 2)
· π) = ((𝐾 / 2)
· (2 · π))) |
7 | 2, 6 | syl 14 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℂ → (((𝐾 / 2) · 2) · π)
= ((𝐾 / 2) · (2
· π))) |
8 | | 2ap0 8944 |
. . . . . . . . . . . . 13
⊢ 2 #
0 |
9 | | divcanap1 8571 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 # 0) → ((𝐾 / 2) · 2) = 𝐾) |
10 | 3, 8, 9 | mp3an23 1318 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℂ → ((𝐾 / 2) · 2) = 𝐾) |
11 | 10 | oveq1d 5854 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℂ → (((𝐾 / 2) · 2) · π)
= (𝐾 ·
π)) |
12 | 7, 11 | eqtr3d 2199 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℂ → ((𝐾 / 2) · (2 ·
π)) = (𝐾 ·
π)) |
13 | 1, 12 | syl 14 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℤ → ((𝐾 / 2) · (2 ·
π)) = (𝐾 ·
π)) |
14 | 13 | adantl 275 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → ((𝐾 / 2) · (2 ·
π)) = (𝐾 ·
π)) |
15 | 14 | oveq2d 5855 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐴 + ((𝐾 / 2) · (2 · π))) = (𝐴 + (𝐾 · π))) |
16 | 15 | fveq2d 5487 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(sin‘(𝐴 + ((𝐾 / 2) · (2 ·
π)))) = (sin‘(𝐴 +
(𝐾 ·
π)))) |
17 | 16 | eqcomd 2170 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(sin‘(𝐴 + (𝐾 · π))) =
(sin‘(𝐴 + ((𝐾 / 2) · (2 ·
π))))) |
18 | 17 | adantr 274 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 / 2) ∈ ℤ) →
(sin‘(𝐴 + (𝐾 · π))) =
(sin‘(𝐴 + ((𝐾 / 2) · (2 ·
π))))) |
19 | | sinper 13328 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝐾 / 2) ∈ ℤ) →
(sin‘(𝐴 + ((𝐾 / 2) · (2 ·
π)))) = (sin‘𝐴)) |
20 | 19 | adantlr 469 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 / 2) ∈ ℤ) →
(sin‘(𝐴 + ((𝐾 / 2) · (2 ·
π)))) = (sin‘𝐴)) |
21 | 18, 20 | eqtrd 2197 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 / 2) ∈ ℤ) →
(sin‘(𝐴 + (𝐾 · π))) =
(sin‘𝐴)) |
22 | 21 | fveq2d 5487 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ (𝐾 / 2) ∈ ℤ) →
(abs‘(sin‘(𝐴 +
(𝐾 · π)))) =
(abs‘(sin‘𝐴))) |
23 | | peano2cn 8027 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℂ → (𝐾 + 1) ∈
ℂ) |
24 | | halfcl 9077 |
. . . . . . . . . . . 12
⊢ ((𝐾 + 1) ∈ ℂ →
((𝐾 + 1) / 2) ∈
ℂ) |
25 | 23, 24 | syl 14 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℂ → ((𝐾 + 1) / 2) ∈
ℂ) |
26 | 3, 4 | mulcli 7898 |
. . . . . . . . . . 11
⊢ (2
· π) ∈ ℂ |
27 | | mulcl 7874 |
. . . . . . . . . . 11
⊢ ((((𝐾 + 1) / 2) ∈ ℂ ∧
(2 · π) ∈ ℂ) → (((𝐾 + 1) / 2) · (2 · π))
∈ ℂ) |
28 | 25, 26, 27 | sylancl 410 |
. . . . . . . . . 10
⊢ (𝐾 ∈ ℂ → (((𝐾 + 1) / 2) · (2 ·
π)) ∈ ℂ) |
29 | | subadd23 8104 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ π
∈ ℂ ∧ (((𝐾 +
1) / 2) · (2 · π)) ∈ ℂ) → ((𝐴 − π) + (((𝐾 + 1) / 2) · (2 · π))) =
(𝐴 + ((((𝐾 + 1) / 2) · (2 · π))
− π))) |
30 | 4, 29 | mp3an2 1314 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ (((𝐾 + 1) / 2) · (2 ·
π)) ∈ ℂ) → ((𝐴 − π) + (((𝐾 + 1) / 2) · (2 · π))) =
(𝐴 + ((((𝐾 + 1) / 2) · (2 · π))
− π))) |
31 | 28, 30 | sylan2 284 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℂ) → ((𝐴 − π) + (((𝐾 + 1) / 2) · (2 ·
π))) = (𝐴 + ((((𝐾 + 1) / 2) · (2 ·
π)) − π))) |
32 | | divcanap1 8571 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐾 + 1) ∈ ℂ ∧ 2
∈ ℂ ∧ 2 # 0) → (((𝐾 + 1) / 2) · 2) = (𝐾 + 1)) |
33 | 3, 8, 32 | mp3an23 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 + 1) ∈ ℂ →
(((𝐾 + 1) / 2) · 2)
= (𝐾 + 1)) |
34 | 23, 33 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℂ → (((𝐾 + 1) / 2) · 2) = (𝐾 + 1)) |
35 | 34 | oveq1d 5854 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℂ → ((((𝐾 + 1) / 2) · 2) ·
π) = ((𝐾 + 1) ·
π)) |
36 | | ax-1cn 7840 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℂ |
37 | | adddir 7884 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ ∧ π ∈ ℂ) → ((𝐾 + 1) · π) = ((𝐾 · π) + (1 ·
π))) |
38 | 36, 4, 37 | mp3an23 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℂ → ((𝐾 + 1) · π) = ((𝐾 · π) + (1 ·
π))) |
39 | 35, 38 | eqtrd 2197 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 ∈ ℂ → ((((𝐾 + 1) / 2) · 2) ·
π) = ((𝐾 · π)
+ (1 · π))) |
40 | 4 | mulid2i 7896 |
. . . . . . . . . . . . . . . 16
⊢ (1
· π) = π |
41 | 40 | oveq2i 5850 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 · π) + (1 ·
π)) = ((𝐾 · π)
+ π) |
42 | 39, 41 | eqtr2di 2214 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℂ → ((𝐾 · π) + π) =
((((𝐾 + 1) / 2) · 2)
· π)) |
43 | | mulass 7878 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐾 + 1) / 2) ∈ ℂ ∧
2 ∈ ℂ ∧ π ∈ ℂ) → ((((𝐾 + 1) / 2) · 2) · π) =
(((𝐾 + 1) / 2) · (2
· π))) |
44 | 3, 4, 43 | mp3an23 1318 |
. . . . . . . . . . . . . . 15
⊢ (((𝐾 + 1) / 2) ∈ ℂ →
((((𝐾 + 1) / 2) · 2)
· π) = (((𝐾 + 1)
/ 2) · (2 · π))) |
45 | 25, 44 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ ℂ → ((((𝐾 + 1) / 2) · 2) ·
π) = (((𝐾 + 1) / 2)
· (2 · π))) |
46 | 42, 45 | eqtr2d 2198 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℂ → (((𝐾 + 1) / 2) · (2 ·
π)) = ((𝐾 · π)
+ π)) |
47 | 46 | oveq1d 5854 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℂ → ((((𝐾 + 1) / 2) · (2 ·
π)) − π) = (((𝐾
· π) + π) − π)) |
48 | | mulcl 7874 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ ℂ ∧ π
∈ ℂ) → (𝐾
· π) ∈ ℂ) |
49 | 4, 48 | mpan2 422 |
. . . . . . . . . . . . 13
⊢ (𝐾 ∈ ℂ → (𝐾 · π) ∈
ℂ) |
50 | | pncan 8098 |
. . . . . . . . . . . . 13
⊢ (((𝐾 · π) ∈ ℂ
∧ π ∈ ℂ) → (((𝐾 · π) + π) − π) =
(𝐾 ·
π)) |
51 | 49, 4, 50 | sylancl 410 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℂ → (((𝐾 · π) + π) −
π) = (𝐾 ·
π)) |
52 | 47, 51 | eqtrd 2197 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ ℂ → ((((𝐾 + 1) / 2) · (2 ·
π)) − π) = (𝐾
· π)) |
53 | 52 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℂ) →
((((𝐾 + 1) / 2) · (2
· π)) − π) = (𝐾 · π)) |
54 | 53 | oveq2d 5855 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝐴 + ((((𝐾 + 1) / 2) · (2 · π))
− π)) = (𝐴 +
(𝐾 ·
π))) |
55 | 31, 54 | eqtr2d 2198 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℂ) → (𝐴 + (𝐾 · π)) = ((𝐴 − π) + (((𝐾 + 1) / 2) · (2 ·
π)))) |
56 | 1, 55 | sylan2 284 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → (𝐴 + (𝐾 · π)) = ((𝐴 − π) + (((𝐾 + 1) / 2) · (2 ·
π)))) |
57 | 56 | fveq2d 5487 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(sin‘(𝐴 + (𝐾 · π))) =
(sin‘((𝐴 −
π) + (((𝐾 + 1) / 2)
· (2 · π))))) |
58 | 57 | adantr 274 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘(𝐴 +
(𝐾 · π))) =
(sin‘((𝐴 −
π) + (((𝐾 + 1) / 2)
· (2 · π))))) |
59 | | subcl 8091 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ π
∈ ℂ) → (𝐴
− π) ∈ ℂ) |
60 | 4, 59 | mpan2 422 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → (𝐴 − π) ∈
ℂ) |
61 | | sinper 13328 |
. . . . . . . 8
⊢ (((𝐴 − π) ∈ ℂ
∧ ((𝐾 + 1) / 2) ∈
ℤ) → (sin‘((𝐴 − π) + (((𝐾 + 1) / 2) · (2 · π)))) =
(sin‘(𝐴 −
π))) |
62 | 60, 61 | sylan 281 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘((𝐴
− π) + (((𝐾 + 1) /
2) · (2 · π)))) = (sin‘(𝐴 − π))) |
63 | 62 | adantlr 469 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘((𝐴
− π) + (((𝐾 + 1) /
2) · (2 · π)))) = (sin‘(𝐴 − π))) |
64 | | sinmpi 13334 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ →
(sin‘(𝐴 −
π)) = -(sin‘𝐴)) |
65 | 64 | ad2antrr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘(𝐴
− π)) = -(sin‘𝐴)) |
66 | 63, 65 | eqtrd 2197 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘((𝐴
− π) + (((𝐾 + 1) /
2) · (2 · π)))) = -(sin‘𝐴)) |
67 | 58, 66 | eqtrd 2197 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (sin‘(𝐴 +
(𝐾 · π))) =
-(sin‘𝐴)) |
68 | 67 | fveq2d 5487 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (abs‘(sin‘(𝐴 + (𝐾 · π)))) =
(abs‘-(sin‘𝐴))) |
69 | | sincl 11641 |
. . . . 5
⊢ (𝐴 ∈ ℂ →
(sin‘𝐴) ∈
ℂ) |
70 | 69 | absnegd 11125 |
. . . 4
⊢ (𝐴 ∈ ℂ →
(abs‘-(sin‘𝐴))
= (abs‘(sin‘𝐴))) |
71 | 70 | ad2antrr 480 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (abs‘-(sin‘𝐴)) = (abs‘(sin‘𝐴))) |
72 | 68, 71 | eqtrd 2197 |
. 2
⊢ (((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) ∧ ((𝐾 + 1) / 2) ∈ ℤ)
→ (abs‘(sin‘(𝐴 + (𝐾 · π)))) =
(abs‘(sin‘𝐴))) |
73 | | zeo 9290 |
. . 3
⊢ (𝐾 ∈ ℤ → ((𝐾 / 2) ∈ ℤ ∨
((𝐾 + 1) / 2) ∈
ℤ)) |
74 | 73 | adantl 275 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) → ((𝐾 / 2) ∈ ℤ ∨
((𝐾 + 1) / 2) ∈
ℤ)) |
75 | 22, 72, 74 | mpjaodan 788 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐾 ∈ ℤ) →
(abs‘(sin‘(𝐴 +
(𝐾 · π)))) =
(abs‘(sin‘𝐴))) |