Proof of Theorem coseq0negpitopi
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . 5
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
(-π(,]π)) |
2 | | pire 25203 |
. . . . . . . 8
⊢ π
∈ ℝ |
3 | 2 | renegcli 11025 |
. . . . . . 7
⊢ -π
∈ ℝ |
4 | 3 | rexri 10777 |
. . . . . 6
⊢ -π
∈ ℝ* |
5 | | elioc2 12884 |
. . . . . 6
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ) → (𝐴 ∈ (-π(,]π) ↔ (𝐴 ∈ ℝ ∧ -π <
𝐴 ∧ 𝐴 ≤ π))) |
6 | 4, 2, 5 | mp2an 692 |
. . . . 5
⊢ (𝐴 ∈ (-π(,]π) ↔
(𝐴 ∈ ℝ ∧
-π < 𝐴 ∧ 𝐴 ≤ π)) |
7 | 1, 6 | sylib 221 |
. . . 4
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 ∈ ℝ ∧
-π < 𝐴 ∧ 𝐴 ≤ π)) |
8 | 7 | simp1d 1143 |
. . 3
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
ℝ) |
9 | | 0re 10721 |
. . . 4
⊢ 0 ∈
ℝ |
10 | 9 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) → 0
∈ ℝ) |
11 | 8 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℝ) |
12 | 11 | recnd 10747 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℂ) |
13 | 8 | recnd 10747 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
ℂ) |
14 | 13 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℂ) |
15 | | cosneg 15592 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ →
(cos‘-𝐴) =
(cos‘𝐴)) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
(cos‘-𝐴) =
(cos‘𝐴)) |
17 | | simplr 769 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
(cos‘𝐴) =
0) |
18 | 16, 17 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
(cos‘-𝐴) =
0) |
19 | 8 | renegcld 11145 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 ∈
ℝ) |
20 | 19 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ∈
ℝ) |
21 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ≤ 0) |
22 | 11 | le0neg1d 11289 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
23 | 21, 22 | mpbid 235 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 0 ≤
-𝐴) |
24 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
π ∈ ℝ) |
25 | 7 | simp2d 1144 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-π < 𝐴) |
26 | 24, 8, 25 | ltnegcon1d 11298 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 <
π) |
27 | 19, 24, 26 | ltled 10866 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 ≤
π) |
28 | 27 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ≤ π) |
29 | 9, 2 | elicc2i 12887 |
. . . . . . . . 9
⊢ (-𝐴 ∈ (0[,]π) ↔
(-𝐴 ∈ ℝ ∧ 0
≤ -𝐴 ∧ -𝐴 ≤ π)) |
30 | 20, 23, 28, 29 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ∈
(0[,]π)) |
31 | | coseq00topi 25247 |
. . . . . . . 8
⊢ (-𝐴 ∈ (0[,]π) →
((cos‘-𝐴) = 0 ↔
-𝐴 = (π /
2))) |
32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
((cos‘-𝐴) = 0 ↔
-𝐴 = (π /
2))) |
33 | 18, 32 | mpbid 235 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 = (π / 2)) |
34 | 12, 33 | negcon1ad 11070 |
. . . . 5
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -(π /
2) = 𝐴) |
35 | 34 | eqcomd 2744 |
. . . 4
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 = -(π / 2)) |
36 | | halfpire 25209 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
37 | 36 | renegcli 11025 |
. . . . 5
⊢ -(π /
2) ∈ ℝ |
38 | | prid2g 4652 |
. . . . 5
⊢ (-(π /
2) ∈ ℝ → -(π / 2) ∈ {(π / 2), -(π /
2)}) |
39 | | eleq1a 2828 |
. . . . 5
⊢ (-(π /
2) ∈ {(π / 2), -(π / 2)} → (𝐴 = -(π / 2) → 𝐴 ∈ {(π / 2), -(π /
2)})) |
40 | 37, 38, 39 | mp2b 10 |
. . . 4
⊢ (𝐴 = -(π / 2) → 𝐴 ∈ {(π / 2), -(π /
2)}) |
41 | 35, 40 | syl 17 |
. . 3
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈ {(π / 2), -(π /
2)}) |
42 | | simplr 769 |
. . . . 5
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) →
(cos‘𝐴) =
0) |
43 | 8 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ∈
ℝ) |
44 | | simpr 488 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 0 ≤ 𝐴) |
45 | 7 | simp3d 1145 |
. . . . . . . 8
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ≤
π) |
46 | 45 | adantr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ≤ π) |
47 | 9, 2 | elicc2i 12887 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ π)) |
48 | 43, 44, 46, 47 | syl3anbrc 1344 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ∈
(0[,]π)) |
49 | | coseq00topi 25247 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]π) →
((cos‘𝐴) = 0 ↔
𝐴 = (π /
2))) |
50 | 48, 49 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) →
((cos‘𝐴) = 0 ↔
𝐴 = (π /
2))) |
51 | 42, 50 | mpbid 235 |
. . . 4
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 = (π / 2)) |
52 | | prid1g 4651 |
. . . . 5
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈ {(π / 2), -(π /
2)}) |
53 | | eleq1a 2828 |
. . . . 5
⊢ ((π /
2) ∈ {(π / 2), -(π / 2)} → (𝐴 = (π / 2) → 𝐴 ∈ {(π / 2), -(π /
2)})) |
54 | 36, 52, 53 | mp2b 10 |
. . . 4
⊢ (𝐴 = (π / 2) → 𝐴 ∈ {(π / 2), -(π /
2)}) |
55 | 51, 54 | syl 17 |
. . 3
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ∈ {(π / 2), -(π /
2)}) |
56 | 8, 10, 41, 55 | lecasei 10824 |
. 2
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈ {(π / 2),
-(π / 2)}) |
57 | | elpri 4538 |
. . . 4
⊢ (𝐴 ∈ {(π / 2), -(π /
2)} → (𝐴 = (π / 2)
∨ 𝐴 = -(π /
2))) |
58 | | fveq2 6674 |
. . . . . 6
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
(cos‘(π / 2))) |
59 | | coshalfpi 25214 |
. . . . . 6
⊢
(cos‘(π / 2)) = 0 |
60 | 58, 59 | eqtrdi 2789 |
. . . . 5
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
0) |
61 | | fveq2 6674 |
. . . . . 6
⊢ (𝐴 = -(π / 2) →
(cos‘𝐴) =
(cos‘-(π / 2))) |
62 | | cosneghalfpi 25215 |
. . . . . 6
⊢
(cos‘-(π / 2)) = 0 |
63 | 61, 62 | eqtrdi 2789 |
. . . . 5
⊢ (𝐴 = -(π / 2) →
(cos‘𝐴) =
0) |
64 | 60, 63 | jaoi 856 |
. . . 4
⊢ ((𝐴 = (π / 2) ∨ 𝐴 = -(π / 2)) →
(cos‘𝐴) =
0) |
65 | 57, 64 | syl 17 |
. . 3
⊢ (𝐴 ∈ {(π / 2), -(π /
2)} → (cos‘𝐴) =
0) |
66 | 65 | adantl 485 |
. 2
⊢ ((𝐴 ∈ (-π(,]π) ∧
𝐴 ∈ {(π / 2),
-(π / 2)}) → (cos‘𝐴) = 0) |
67 | 56, 66 | impbida 801 |
1
⊢ (𝐴 ∈ (-π(,]π) →
((cos‘𝐴) = 0 ↔
𝐴 ∈ {(π / 2),
-(π / 2)})) |