Step | Hyp | Ref
| Expression |
1 | | pire 14177 |
. . . . . . . 8
⊢ π
∈ ℝ |
2 | | 2re 8988 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
3 | 2, 1 | remulcli 7970 |
. . . . . . . . 9
⊢ (2
· π) ∈ ℝ |
4 | 3 | rexri 8014 |
. . . . . . . 8
⊢ (2
· π) ∈ ℝ* |
5 | | elico2 9936 |
. . . . . . . 8
⊢ ((π
∈ ℝ ∧ (2 · π) ∈ ℝ*) →
(𝐴 ∈ (π[,)(2
· π)) ↔ (𝐴
∈ ℝ ∧ π ≤ 𝐴 ∧ 𝐴 < (2 · π)))) |
6 | 1, 4, 5 | mp2an 426 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) ↔ (𝐴 ∈
ℝ ∧ π ≤ 𝐴
∧ 𝐴 < (2 ·
π))) |
7 | 6 | simp1bi 1012 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 ∈
ℝ) |
8 | 7 | recnd 7985 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 ∈
ℂ) |
9 | | 2cn 8989 |
. . . . . . 7
⊢ 2 ∈
ℂ |
10 | | picn 14178 |
. . . . . . 7
⊢ π
∈ ℂ |
11 | 9, 10 | mulcli 7961 |
. . . . . 6
⊢ (2
· π) ∈ ℂ |
12 | 11 | a1i 9 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (2 · π) ∈ ℂ) |
13 | 8, 12 | subcld 8267 |
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 − (2
· π)) ∈ ℂ) |
14 | | cosneg 11734 |
. . . 4
⊢ ((𝐴 − (2 · π))
∈ ℂ → (cos‘-(𝐴 − (2 · π))) =
(cos‘(𝐴 − (2
· π)))) |
15 | 13, 14 | syl 14 |
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) =
(cos‘(𝐴 − (2
· π)))) |
16 | 12 | mulm1d 8366 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (-1 · (2 · π)) = -(2 ·
π)) |
17 | 16 | oveq2d 5890 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + (-1
· (2 · π))) = (𝐴 + -(2 · π))) |
18 | 8, 12 | negsubd 8273 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + -(2
· π)) = (𝐴
− (2 · π))) |
19 | 17, 18 | eqtrd 2210 |
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + (-1
· (2 · π))) = (𝐴 − (2 ·
π))) |
20 | 19 | fveq2d 5519 |
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘(𝐴
+ (-1 · (2 · π)))) = (cos‘(𝐴 − (2 ·
π)))) |
21 | | neg1z 9284 |
. . . 4
⊢ -1 ∈
ℤ |
22 | | cosper 14201 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ -1 ∈
ℤ) → (cos‘(𝐴 + (-1 · (2 · π)))) =
(cos‘𝐴)) |
23 | 8, 21, 22 | sylancl 413 |
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘(𝐴
+ (-1 · (2 · π)))) = (cos‘𝐴)) |
24 | 15, 20, 23 | 3eqtr2d 2216 |
. 2
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) =
(cos‘𝐴)) |
25 | | 0xr 8003 |
. . . . 5
⊢ 0 ∈
ℝ* |
26 | 1 | rexri 8014 |
. . . . 5
⊢ π
∈ ℝ* |
27 | | 0re 7956 |
. . . . . . 7
⊢ 0 ∈
ℝ |
28 | | pipos 14179 |
. . . . . . 7
⊢ 0 <
π |
29 | 27, 1, 28 | ltleii 8059 |
. . . . . 6
⊢ 0 ≤
π |
30 | 29 | a1i 9 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ≤ π) |
31 | | lbicc2 9983 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ 0 ≤
π) → 0 ∈ (0[,]π)) |
32 | 25, 26, 30, 31 | mp3an12i 1341 |
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ∈ (0[,]π)) |
33 | 3 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (2 · π) ∈ ℝ) |
34 | 7, 33 | resubcld 8337 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 − (2
· π)) ∈ ℝ) |
35 | 34 | renegcld 8336 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ∈ ℝ) |
36 | 27 | a1i 9 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ∈ ℝ) |
37 | 6 | simp3bi 1014 |
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 < (2
· π)) |
38 | 7, 33 | posdifd 8488 |
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 < (2
· π) ↔ 0 < ((2 · π) − 𝐴))) |
39 | 37, 38 | mpbid 147 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 < ((2 · π) − 𝐴)) |
40 | 8, 12 | negsubdi2d 8283 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) = ((2 · π) − 𝐴)) |
41 | 39, 40 | breqtrrd 4031 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 < -(𝐴
− (2 · π))) |
42 | 36, 35, 41 | ltled 8075 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ≤ -(𝐴
− (2 · π))) |
43 | 1 | a1i 9 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → π ∈ ℝ) |
44 | | ax-1cn 7903 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
45 | 9, 44, 10 | subdiri 8364 |
. . . . . . . . 9
⊢ ((2
− 1) · π) = ((2 · π) − (1 ·
π)) |
46 | | 2m1e1 9036 |
. . . . . . . . . . 11
⊢ (2
− 1) = 1 |
47 | 46 | oveq1i 5884 |
. . . . . . . . . 10
⊢ ((2
− 1) · π) = (1 · π) |
48 | 10 | mullidi 7959 |
. . . . . . . . . 10
⊢ (1
· π) = π |
49 | 47, 48 | eqtri 2198 |
. . . . . . . . 9
⊢ ((2
− 1) · π) = π |
50 | 48 | oveq2i 5885 |
. . . . . . . . 9
⊢ ((2
· π) − (1 · π)) = ((2 · π) −
π) |
51 | 45, 49, 50 | 3eqtr3ri 2207 |
. . . . . . . 8
⊢ ((2
· π) − π) = π |
52 | 6 | simp2bi 1013 |
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → π ≤ 𝐴) |
53 | 51, 52 | eqbrtrid 4038 |
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → ((2 · π) − π) ≤ 𝐴) |
54 | 33, 43, 7, 53 | subled 8504 |
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → ((2 · π) − 𝐴) ≤ π) |
55 | 40, 54 | eqbrtrd 4025 |
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ≤ π) |
56 | 27, 1 | elicc2i 9938 |
. . . . 5
⊢ (-(𝐴 − (2 · π))
∈ (0[,]π) ↔ (-(𝐴 − (2 · π)) ∈ ℝ
∧ 0 ≤ -(𝐴 − (2
· π)) ∧ -(𝐴
− (2 · π)) ≤ π)) |
57 | 35, 42, 55, 56 | syl3anbrc 1181 |
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ∈ (0[,]π)) |
58 | 32, 57, 41 | cosordlem 14240 |
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) <
(cos‘0)) |
59 | | cos0 11737 |
. . 3
⊢
(cos‘0) = 1 |
60 | 58, 59 | breqtrdi 4044 |
. 2
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) <
1) |
61 | 24, 60 | eqbrtrrd 4027 |
1
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘𝐴)
< 1) |