Proof of Theorem coseq0negpitopi
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
(-π(,]π)) |
| 2 | | pire 26500 |
. . . . . . . 8
⊢ π
∈ ℝ |
| 3 | 2 | renegcli 11570 |
. . . . . . 7
⊢ -π
∈ ℝ |
| 4 | 3 | rexri 11319 |
. . . . . 6
⊢ -π
∈ ℝ* |
| 5 | | elioc2 13450 |
. . . . . 6
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ) → (𝐴 ∈ (-π(,]π) ↔ (𝐴 ∈ ℝ ∧ -π <
𝐴 ∧ 𝐴 ≤ π))) |
| 6 | 4, 2, 5 | mp2an 692 |
. . . . 5
⊢ (𝐴 ∈ (-π(,]π) ↔
(𝐴 ∈ ℝ ∧
-π < 𝐴 ∧ 𝐴 ≤ π)) |
| 7 | 1, 6 | sylib 218 |
. . . 4
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 ∈ ℝ ∧
-π < 𝐴 ∧ 𝐴 ≤ π)) |
| 8 | 7 | simp1d 1143 |
. . 3
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
ℝ) |
| 9 | | 0re 11263 |
. . . 4
⊢ 0 ∈
ℝ |
| 10 | 9 | a1i 11 |
. . 3
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) → 0
∈ ℝ) |
| 11 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℝ) |
| 12 | 11 | recnd 11289 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℂ) |
| 13 | 8 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
ℂ) |
| 14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ∈
ℂ) |
| 15 | | cosneg 16183 |
. . . . . . . . 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 2777 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
(cos‘-𝐴) =
0) |
| 19 | 8 | renegcld 11690 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 ∈
ℝ) |
| 20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ∈
ℝ) |
| 21 | | simpr 484 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 ≤ 0) |
| 22 | 11 | le0neg1d 11834 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → (𝐴 ≤ 0 ↔ 0 ≤ -𝐴)) |
| 23 | 21, 22 | mpbid 232 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 0 ≤
-𝐴) |
| 24 | 2 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
π ∈ ℝ) |
| 25 | 7 | simp2d 1144 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-π < 𝐴) |
| 26 | 24, 8, 25 | ltnegcon1d 11843 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 <
π) |
| 27 | 19, 24, 26 | ltled 11409 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
-𝐴 ≤
π) |
| 28 | 27 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ≤ π) |
| 29 | 9, 2 | elicc2i 13453 |
. . . . . . . . 9
⊢ (-𝐴 ∈ (0[,]π) ↔
(-𝐴 ∈ ℝ ∧ 0
≤ -𝐴 ∧ -𝐴 ≤ π)) |
| 30 | 20, 23, 28, 29 | syl3anbrc 1344 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 ∈
(0[,]π)) |
| 31 | | coseq00topi 26544 |
. . . . . . . 8
⊢ (-𝐴 ∈ (0[,]π) →
((cos‘-𝐴) = 0 ↔
-𝐴 = (π /
2))) |
| 32 | 30, 31 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) →
((cos‘-𝐴) = 0 ↔
-𝐴 = (π /
2))) |
| 33 | 18, 32 | mpbid 232 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -𝐴 = (π / 2)) |
| 34 | 12, 33 | negcon1ad 11615 |
. . . . 5
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → -(π /
2) = 𝐴) |
| 35 | 34 | eqcomd 2743 |
. . . 4
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 ≤ 0) → 𝐴 = -(π / 2)) |
| 36 | | halfpire 26506 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
| 37 | 36 | renegcli 11570 |
. . . . 5
⊢ -(π /
2) ∈ ℝ |
| 38 | | prid2g 4761 |
. . . . 5
⊢ (-(π /
2) ∈ ℝ → -(π / 2) ∈ {(π / 2), -(π /
2)}) |
| 39 | | eleq1a 2836 |
. . . . 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 480 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ∈
ℝ) |
| 44 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 0 ≤ 𝐴) |
| 45 | 7 | simp3d 1145 |
. . . . . . . 8
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ≤
π) |
| 46 | 45 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ≤ π) |
| 47 | 9, 2 | elicc2i 13453 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ π)) |
| 48 | 43, 44, 46, 47 | syl3anbrc 1344 |
. . . . . 6
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 ∈
(0[,]π)) |
| 49 | | coseq00topi 26544 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]π) →
((cos‘𝐴) = 0 ↔
𝐴 = (π /
2))) |
| 50 | 48, 49 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) →
((cos‘𝐴) = 0 ↔
𝐴 = (π /
2))) |
| 51 | 42, 50 | mpbid 232 |
. . . 4
⊢ (((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) ∧ 0
≤ 𝐴) → 𝐴 = (π / 2)) |
| 52 | | prid1g 4760 |
. . . . 5
⊢ ((π /
2) ∈ ℝ → (π / 2) ∈ {(π / 2), -(π /
2)}) |
| 53 | | eleq1a 2836 |
. . . . 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 11367 |
. 2
⊢ ((𝐴 ∈ (-π(,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈ {(π / 2),
-(π / 2)}) |
| 57 | | elpri 4649 |
. . . 4
⊢ (𝐴 ∈ {(π / 2), -(π /
2)} → (𝐴 = (π / 2)
∨ 𝐴 = -(π /
2))) |
| 58 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
(cos‘(π / 2))) |
| 59 | | coshalfpi 26511 |
. . . . . 6
⊢
(cos‘(π / 2)) = 0 |
| 60 | 58, 59 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
0) |
| 61 | | fveq2 6906 |
. . . . . 6
⊢ (𝐴 = -(π / 2) →
(cos‘𝐴) =
(cos‘-(π / 2))) |
| 62 | | cosneghalfpi 26512 |
. . . . . 6
⊢
(cos‘-(π / 2)) = 0 |
| 63 | 61, 62 | eqtrdi 2793 |
. . . . 5
⊢ (𝐴 = -(π / 2) →
(cos‘𝐴) =
0) |
| 64 | 60, 63 | jaoi 858 |
. . . 4
⊢ ((𝐴 = (π / 2) ∨ 𝐴 = -(π / 2)) →
(cos‘𝐴) =
0) |
| 65 | 57, 64 | syl 17 |
. . 3
⊢ (𝐴 ∈ {(π / 2), -(π /
2)} → (cos‘𝐴) =
0) |
| 66 | 65 | adantl 481 |
. 2
⊢ ((𝐴 ∈ (-π(,]π) ∧
𝐴 ∈ {(π / 2),
-(π / 2)}) → (cos‘𝐴) = 0) |
| 67 | 56, 66 | impbida 801 |
1
⊢ (𝐴 ∈ (-π(,]π) →
((cos‘𝐴) = 0 ↔
𝐴 ∈ {(π / 2),
-(π / 2)})) |