Proof of Theorem cosq34lt1
| Step | Hyp | Ref
 | Expression | 
| 1 |   | pire 15022 | 
. . . . . . . 8
⊢ π
∈ ℝ | 
| 2 |   | 2re 9060 | 
. . . . . . . . . 10
⊢ 2 ∈
ℝ | 
| 3 | 2, 1 | remulcli 8040 | 
. . . . . . . . 9
⊢ (2
· π) ∈ ℝ | 
| 4 | 3 | rexri 8084 | 
. . . . . . . 8
⊢ (2
· π) ∈ ℝ* | 
| 5 |   | elico2 10012 | 
. . . . . . . 8
⊢ ((π
∈ ℝ ∧ (2 · π) ∈ ℝ*) →
(𝐴 ∈ (π[,)(2
· π)) ↔ (𝐴
∈ ℝ ∧ π ≤ 𝐴 ∧ 𝐴 < (2 · π)))) | 
| 6 | 1, 4, 5 | mp2an 426 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) ↔ (𝐴 ∈
ℝ ∧ π ≤ 𝐴
∧ 𝐴 < (2 ·
π))) | 
| 7 | 6 | simp1bi 1014 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 ∈
ℝ) | 
| 8 | 7 | recnd 8055 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 ∈
ℂ) | 
| 9 |   | 2cn 9061 | 
. . . . . . 7
⊢ 2 ∈
ℂ | 
| 10 |   | picn 15023 | 
. . . . . . 7
⊢ π
∈ ℂ | 
| 11 | 9, 10 | mulcli 8031 | 
. . . . . 6
⊢ (2
· π) ∈ ℂ | 
| 12 | 11 | a1i 9 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (2 · π) ∈ ℂ) | 
| 13 | 8, 12 | subcld 8337 | 
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 − (2
· π)) ∈ ℂ) | 
| 14 |   | cosneg 11892 | 
. . . 4
⊢ ((𝐴 − (2 · π))
∈ ℂ → (cos‘-(𝐴 − (2 · π))) =
(cos‘(𝐴 − (2
· π)))) | 
| 15 | 13, 14 | syl 14 | 
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) =
(cos‘(𝐴 − (2
· π)))) | 
| 16 | 12 | mulm1d 8436 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (-1 · (2 · π)) = -(2 ·
π)) | 
| 17 | 16 | oveq2d 5938 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + (-1
· (2 · π))) = (𝐴 + -(2 · π))) | 
| 18 | 8, 12 | negsubd 8343 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + -(2
· π)) = (𝐴
− (2 · π))) | 
| 19 | 17, 18 | eqtrd 2229 | 
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 + (-1
· (2 · π))) = (𝐴 − (2 ·
π))) | 
| 20 | 19 | fveq2d 5562 | 
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘(𝐴
+ (-1 · (2 · π)))) = (cos‘(𝐴 − (2 ·
π)))) | 
| 21 |   | neg1z 9358 | 
. . . 4
⊢ -1 ∈
ℤ | 
| 22 |   | cosper 15046 | 
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ -1 ∈
ℤ) → (cos‘(𝐴 + (-1 · (2 · π)))) =
(cos‘𝐴)) | 
| 23 | 8, 21, 22 | sylancl 413 | 
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘(𝐴
+ (-1 · (2 · π)))) = (cos‘𝐴)) | 
| 24 | 15, 20, 23 | 3eqtr2d 2235 | 
. 2
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) =
(cos‘𝐴)) | 
| 25 |   | 0xr 8073 | 
. . . . 5
⊢ 0 ∈
ℝ* | 
| 26 | 1 | rexri 8084 | 
. . . . 5
⊢ π
∈ ℝ* | 
| 27 |   | 0re 8026 | 
. . . . . . 7
⊢ 0 ∈
ℝ | 
| 28 |   | pipos 15024 | 
. . . . . . 7
⊢ 0 <
π | 
| 29 | 27, 1, 28 | ltleii 8129 | 
. . . . . 6
⊢ 0 ≤
π | 
| 30 | 29 | a1i 9 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ≤ π) | 
| 31 |   | lbicc2 10059 | 
. . . . 5
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ* ∧ 0 ≤
π) → 0 ∈ (0[,]π)) | 
| 32 | 25, 26, 30, 31 | mp3an12i 1352 | 
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ∈ (0[,]π)) | 
| 33 | 3 | a1i 9 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (2 · π) ∈ ℝ) | 
| 34 | 7, 33 | resubcld 8407 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 − (2
· π)) ∈ ℝ) | 
| 35 | 34 | renegcld 8406 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ∈ ℝ) | 
| 36 | 27 | a1i 9 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ∈ ℝ) | 
| 37 | 6 | simp3bi 1016 | 
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 𝐴 < (2
· π)) | 
| 38 | 7, 33 | posdifd 8559 | 
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (𝐴 < (2
· π) ↔ 0 < ((2 · π) − 𝐴))) | 
| 39 | 37, 38 | mpbid 147 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 < ((2 · π) − 𝐴)) | 
| 40 | 8, 12 | negsubdi2d 8353 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) = ((2 · π) − 𝐴)) | 
| 41 | 39, 40 | breqtrrd 4061 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 < -(𝐴
− (2 · π))) | 
| 42 | 36, 35, 41 | ltled 8145 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → 0 ≤ -(𝐴
− (2 · π))) | 
| 43 | 1 | a1i 9 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → π ∈ ℝ) | 
| 44 |   | ax-1cn 7972 | 
. . . . . . . . . 10
⊢ 1 ∈
ℂ | 
| 45 | 9, 44, 10 | subdiri 8434 | 
. . . . . . . . 9
⊢ ((2
− 1) · π) = ((2 · π) − (1 ·
π)) | 
| 46 |   | 2m1e1 9108 | 
. . . . . . . . . . 11
⊢ (2
− 1) = 1 | 
| 47 | 46 | oveq1i 5932 | 
. . . . . . . . . 10
⊢ ((2
− 1) · π) = (1 · π) | 
| 48 | 10 | mullidi 8029 | 
. . . . . . . . . 10
⊢ (1
· π) = π | 
| 49 | 47, 48 | eqtri 2217 | 
. . . . . . . . 9
⊢ ((2
− 1) · π) = π | 
| 50 | 48 | oveq2i 5933 | 
. . . . . . . . 9
⊢ ((2
· π) − (1 · π)) = ((2 · π) −
π) | 
| 51 | 45, 49, 50 | 3eqtr3ri 2226 | 
. . . . . . . 8
⊢ ((2
· π) − π) = π | 
| 52 | 6 | simp2bi 1015 | 
. . . . . . . 8
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → π ≤ 𝐴) | 
| 53 | 51, 52 | eqbrtrid 4068 | 
. . . . . . 7
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → ((2 · π) − π) ≤ 𝐴) | 
| 54 | 33, 43, 7, 53 | subled 8575 | 
. . . . . 6
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → ((2 · π) − 𝐴) ≤ π) | 
| 55 | 40, 54 | eqbrtrd 4055 | 
. . . . 5
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ≤ π) | 
| 56 | 27, 1 | elicc2i 10014 | 
. . . . 5
⊢ (-(𝐴 − (2 · π))
∈ (0[,]π) ↔ (-(𝐴 − (2 · π)) ∈ ℝ
∧ 0 ≤ -(𝐴 − (2
· π)) ∧ -(𝐴
− (2 · π)) ≤ π)) | 
| 57 | 35, 42, 55, 56 | syl3anbrc 1183 | 
. . . 4
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → -(𝐴 −
(2 · π)) ∈ (0[,]π)) | 
| 58 | 32, 57, 41 | cosordlem 15085 | 
. . 3
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) <
(cos‘0)) | 
| 59 |   | cos0 11895 | 
. . 3
⊢
(cos‘0) = 1 | 
| 60 | 58, 59 | breqtrdi 4074 | 
. 2
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘-(𝐴 − (2 · π))) <
1) | 
| 61 | 24, 60 | eqbrtrrd 4057 | 
1
⊢ (𝐴 ∈ (π[,)(2 ·
π)) → (cos‘𝐴)
< 1) |