| Step | Hyp | Ref
| Expression |
| 1 | | 2z 12649 |
. . . . 5
⊢ 2 ∈
ℤ |
| 2 | | divides 16292 |
. . . . 5
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 ∥ 𝐾 ↔ ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾)) |
| 3 | 1, 2 | mpan 690 |
. . . 4
⊢ (𝐾 ∈ ℤ → (2
∥ 𝐾 ↔
∃𝑛 ∈ ℤ
(𝑛 · 2) = 𝐾)) |
| 4 | 3 | biimpa 476 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → ∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾) |
| 5 | | zcn 12618 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
| 6 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → 2 ∈
ℂ) |
| 7 | | picn 26501 |
. . . . . . . . . . . . . . 15
⊢ π
∈ ℂ |
| 8 | 7 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → π
∈ ℂ) |
| 9 | 5, 6, 8 | mulassd 11284 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → ((𝑛 · 2) · π) =
(𝑛 · (2 ·
π))) |
| 10 | 9 | eqcomd 2743 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (𝑛 · (2 · π)) =
((𝑛 · 2) ·
π)) |
| 11 | 10 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (𝑛 · (2 · π)) = ((𝑛 · 2) ·
π)) |
| 12 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ ((𝑛 · 2) = 𝐾 → ((𝑛 · 2) · π) = (𝐾 ·
π)) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → ((𝑛 · 2) · π) = (𝐾 ·
π)) |
| 14 | 11, 13 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (𝐾 · π) = (𝑛 · (2 ·
π))) |
| 15 | 14 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · π)) = (cos‘(𝑛 · (2 ·
π)))) |
| 16 | | cos2kpi 26526 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ →
(cos‘(𝑛 · (2
· π))) = 1) |
| 17 | 16 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝑛 · (2 · π))) =
1) |
| 18 | 15, 17 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · π)) = 1) |
| 19 | 18 | 3adant1 1131 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · π)) = 1) |
| 20 | | iftrue 4531 |
. . . . . . . . 9
⊢ (2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
1) |
| 21 | 20 | eqcomd 2743 |
. . . . . . . 8
⊢ (2
∥ 𝐾 → 1 = if(2
∥ 𝐾, 1,
-1)) |
| 22 | 21 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → 1 = if(2 ∥ 𝐾, 1, -1)) |
| 23 | 19, 22 | eqtrd 2777 |
. . . . . 6
⊢ ((2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ (𝑛 · 2) = 𝐾) → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1)) |
| 24 | 23 | 3exp 1120 |
. . . . 5
⊢ (2
∥ 𝐾 → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1)))) |
| 25 | 24 | adantl 481 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (𝑛 ∈ ℤ → ((𝑛 · 2) = 𝐾 → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1)))) |
| 26 | 25 | rexlimdv 3153 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (∃𝑛 ∈ ℤ (𝑛 · 2) = 𝐾 → (cos‘(𝐾 · π)) = if(2 ∥ 𝐾, 1, -1))) |
| 27 | 4, 26 | mpd 15 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ 2 ∥
𝐾) → (cos‘(𝐾 · π)) = if(2 ∥
𝐾, 1, -1)) |
| 28 | | odd2np1 16378 |
. . . 4
⊢ (𝐾 ∈ ℤ → (¬ 2
∥ 𝐾 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾)) |
| 29 | 28 | biimpa 476 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝐾) |
| 30 | 6, 5 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
| 31 | | 1cnd 11256 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → 1 ∈
ℂ) |
| 32 | 30, 31, 8 | adddird 11286 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) ·
π) = (((2 · 𝑛)
· π) + (1 · π))) |
| 33 | 6, 5 | mulcomd 11282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) = (𝑛 · 2)) |
| 34 | 33 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) · π)
= ((𝑛 · 2) ·
π)) |
| 35 | 34, 9 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → ((2
· 𝑛) · π)
= (𝑛 · (2 ·
π))) |
| 36 | 7 | mullidi 11266 |
. . . . . . . . . . . . . . 15
⊢ (1
· π) = π |
| 37 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (1
· π) = π) |
| 38 | 35, 37 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → (((2
· 𝑛) · π)
+ (1 · π)) = ((𝑛
· (2 · π)) + π)) |
| 39 | | 2cn 12341 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
| 40 | 39, 7 | mulcli 11268 |
. . . . . . . . . . . . . . . 16
⊢ (2
· π) ∈ ℂ |
| 41 | 40 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℤ → (2
· π) ∈ ℂ) |
| 42 | 5, 41 | mulcld 11281 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℤ → (𝑛 · (2 · π))
∈ ℂ) |
| 43 | 42, 8 | addcomd 11463 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℤ → ((𝑛 · (2 · π)) +
π) = (π + (𝑛 ·
(2 · π)))) |
| 44 | 32, 38, 43 | 3eqtrrd 2782 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℤ → (π +
(𝑛 · (2 ·
π))) = (((2 · 𝑛)
+ 1) · π)) |
| 45 | 44 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (π + (𝑛 · (2 · π))) =
(((2 · 𝑛) + 1)
· π)) |
| 46 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑛) + 1) = 𝐾 → (((2 · 𝑛) + 1) · π) = (𝐾 ·
π)) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (((2 · 𝑛) + 1) · π) = (𝐾 ·
π)) |
| 48 | 45, 47 | eqtr2d 2778 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (𝐾 · π) = (π + (𝑛 · (2 ·
π)))) |
| 49 | 48 | fveq2d 6910 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · π)) =
(cos‘(π + (𝑛
· (2 · π))))) |
| 50 | | cosper 26524 |
. . . . . . . . . . 11
⊢ ((π
∈ ℂ ∧ 𝑛
∈ ℤ) → (cos‘(π + (𝑛 · (2 · π)))) =
(cos‘π)) |
| 51 | 7, 50 | mpan 690 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ →
(cos‘(π + (𝑛
· (2 · π)))) = (cos‘π)) |
| 52 | 51 | adantr 480 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(π +
(𝑛 · (2 ·
π)))) = (cos‘π)) |
| 53 | | cospi 26514 |
. . . . . . . . . 10
⊢
(cos‘π) = -1 |
| 54 | 53 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘π) =
-1) |
| 55 | 49, 52, 54 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · π)) =
-1) |
| 56 | 55 | 3adant1 1131 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · π)) =
-1) |
| 57 | | iffalse 4534 |
. . . . . . . . 9
⊢ (¬ 2
∥ 𝐾 → if(2
∥ 𝐾, 1, -1) =
-1) |
| 58 | 57 | eqcomd 2743 |
. . . . . . . 8
⊢ (¬ 2
∥ 𝐾 → -1 = if(2
∥ 𝐾, 1,
-1)) |
| 59 | 58 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → -1 = if(2 ∥ 𝐾, 1, -1)) |
| 60 | 56, 59 | eqtrd 2777 |
. . . . . 6
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑛 ∈ ℤ ∧ ((2
· 𝑛) + 1) = 𝐾) → (cos‘(𝐾 · π)) = if(2 ∥
𝐾, 1, -1)) |
| 61 | 60 | 3exp 1120 |
. . . . 5
⊢ (¬ 2
∥ 𝐾 → (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) = 𝐾 → (cos‘(𝐾 · π)) = if(2 ∥
𝐾, 1,
-1)))) |
| 62 | 61 | adantl 481 |
. . . 4
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) → (𝑛 ∈ ℤ → (((2
· 𝑛) + 1) = 𝐾 → (cos‘(𝐾 · π)) = if(2 ∥
𝐾, 1,
-1)))) |
| 63 | 62 | rexlimdv 3153 |
. . 3
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝐾 → (cos‘(𝐾 · π)) = if(2 ∥
𝐾, 1,
-1))) |
| 64 | 29, 63 | mpd 15 |
. 2
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) →
(cos‘(𝐾 ·
π)) = if(2 ∥ 𝐾, 1,
-1)) |
| 65 | 27, 64 | pm2.61dan 813 |
1
⊢ (𝐾 ∈ ℤ →
(cos‘(𝐾 ·
π)) = if(2 ∥ 𝐾, 1,
-1)) |