Proof of Theorem coseq00topi
| Step | Hyp | Ref
| Expression |
| 1 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) →
(cos‘𝐴) =
0) |
| 2 | | simpl 482 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
(0[,]π)) |
| 3 | | 0re 11263 |
. . . . . . . . . . . . 13
⊢ 0 ∈
ℝ |
| 4 | | pire 26500 |
. . . . . . . . . . . . 13
⊢ π
∈ ℝ |
| 5 | 3, 4 | elicc2i 13453 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (0[,]π) ↔ (𝐴 ∈ ℝ ∧ 0 ≤
𝐴 ∧ 𝐴 ≤ π)) |
| 6 | 2, 5 | sylib 218 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 ∈ ℝ ∧ 0
≤ 𝐴 ∧ 𝐴 ≤ π)) |
| 7 | 6 | simp1d 1143 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ∈
ℝ) |
| 8 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → 𝐴 ∈
ℝ) |
| 9 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → 0 < 𝐴) |
| 10 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → 𝐴 < (π /
2)) |
| 11 | 3 | rexri 11319 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
| 12 | | halfpire 26506 |
. . . . . . . . . . 11
⊢ (π /
2) ∈ ℝ |
| 13 | 12 | rexri 11319 |
. . . . . . . . . 10
⊢ (π /
2) ∈ ℝ* |
| 14 | | elioo2 13428 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ (π / 2) ∈ ℝ*) →
(𝐴 ∈ (0(,)(π / 2))
↔ (𝐴 ∈ ℝ
∧ 0 < 𝐴 ∧ 𝐴 < (π /
2)))) |
| 15 | 11, 13, 14 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐴 ∈ (0(,)(π / 2)) ↔
(𝐴 ∈ ℝ ∧ 0
< 𝐴 ∧ 𝐴 < (π /
2))) |
| 16 | 8, 9, 10, 15 | syl3anbrc 1344 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → 𝐴 ∈ (0(,)(π /
2))) |
| 17 | | sincosq1sgn 26540 |
. . . . . . . 8
⊢ (𝐴 ∈ (0(,)(π / 2)) →
(0 < (sin‘𝐴) ∧
0 < (cos‘𝐴))) |
| 18 | 16, 17 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → (0 <
(sin‘𝐴) ∧ 0 <
(cos‘𝐴))) |
| 19 | 18 | simprd 495 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) → 0 <
(cos‘𝐴)) |
| 20 | 19 | gt0ne0d 11827 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
< 𝐴) →
(cos‘𝐴) ≠
0) |
| 21 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
= 𝐴) → 0 = 𝐴) |
| 22 | 21 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
= 𝐴) → (cos‘0) =
(cos‘𝐴)) |
| 23 | | cos0 16186 |
. . . . . . 7
⊢
(cos‘0) = 1 |
| 24 | 22, 23 | eqtr3di 2792 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
= 𝐴) →
(cos‘𝐴) =
1) |
| 25 | | ax-1ne0 11224 |
. . . . . . 7
⊢ 1 ≠
0 |
| 26 | 25 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
= 𝐴) → 1 ≠
0) |
| 27 | 24, 26 | eqnetrd 3008 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) ∧ 0
= 𝐴) →
(cos‘𝐴) ≠
0) |
| 28 | 6 | simp2d 1144 |
. . . . . . 7
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) → 0
≤ 𝐴) |
| 29 | | 0red 11264 |
. . . . . . . 8
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) → 0
∈ ℝ) |
| 30 | 29, 7 | leloed 11404 |
. . . . . . 7
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(0 ≤ 𝐴 ↔ (0 <
𝐴 ∨ 0 = 𝐴))) |
| 31 | 28, 30 | mpbid 232 |
. . . . . 6
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(0 < 𝐴 ∨ 0 = 𝐴)) |
| 32 | 31 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) →
(0 < 𝐴 ∨ 0 = 𝐴)) |
| 33 | 20, 27, 32 | mpjaodan 961 |
. . . 4
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) →
(cos‘𝐴) ≠
0) |
| 34 | 1, 33 | pm2.21ddne 3026 |
. . 3
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 < (π / 2)) →
𝐴 = (π /
2)) |
| 35 | | simpr 484 |
. . 3
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
𝐴 = (π / 2)) →
𝐴 = (π /
2)) |
| 36 | | simplr 769 |
. . . 4
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) →
(cos‘𝐴) =
0) |
| 37 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) → 𝐴 ∈
ℝ) |
| 38 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) → (π /
2) < 𝐴) |
| 39 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) → 𝐴 < π) |
| 40 | 4 | rexri 11319 |
. . . . . . . . . 10
⊢ π
∈ ℝ* |
| 41 | | elioo2 13428 |
. . . . . . . . . 10
⊢ (((π /
2) ∈ ℝ* ∧ π ∈ ℝ*) →
(𝐴 ∈ ((π /
2)(,)π) ↔ (𝐴 ∈
ℝ ∧ (π / 2) < 𝐴 ∧ 𝐴 < π))) |
| 42 | 13, 40, 41 | mp2an 692 |
. . . . . . . . 9
⊢ (𝐴 ∈ ((π / 2)(,)π)
↔ (𝐴 ∈ ℝ
∧ (π / 2) < 𝐴
∧ 𝐴 <
π)) |
| 43 | 37, 38, 39, 42 | syl3anbrc 1344 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) → 𝐴 ∈ ((π /
2)(,)π)) |
| 44 | | sincosq2sgn 26541 |
. . . . . . . 8
⊢ (𝐴 ∈ ((π / 2)(,)π)
→ (0 < (sin‘𝐴) ∧ (cos‘𝐴) < 0)) |
| 45 | 43, 44 | syl 17 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) → (0 <
(sin‘𝐴) ∧
(cos‘𝐴) <
0)) |
| 46 | 45 | simprd 495 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) →
(cos‘𝐴) <
0) |
| 47 | 46 | lt0ne0d 11828 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 < π) →
(cos‘𝐴) ≠
0) |
| 48 | | simpr 484 |
. . . . . . . 8
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 = π) → 𝐴 = π) |
| 49 | 48 | fveq2d 6910 |
. . . . . . 7
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 = π) →
(cos‘𝐴) =
(cos‘π)) |
| 50 | | cospi 26514 |
. . . . . . 7
⊢
(cos‘π) = -1 |
| 51 | 49, 50 | eqtrdi 2793 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 = π) →
(cos‘𝐴) =
-1) |
| 52 | | neg1ne0 12382 |
. . . . . . 7
⊢ -1 ≠
0 |
| 53 | 52 | a1i 11 |
. . . . . 6
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 = π) → -1 ≠
0) |
| 54 | 51, 53 | eqnetrd 3008 |
. . . . 5
⊢ ((((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) ∧
𝐴 = π) →
(cos‘𝐴) ≠
0) |
| 55 | 6 | simp3d 1145 |
. . . . . . 7
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
𝐴 ≤
π) |
| 56 | 4 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
π ∈ ℝ) |
| 57 | 7, 56 | leloed 11404 |
. . . . . . 7
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 ≤ π ↔ (𝐴 < π ∨ 𝐴 = π))) |
| 58 | 55, 57 | mpbid 232 |
. . . . . 6
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 < π ∨ 𝐴 = π)) |
| 59 | 58 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) →
(𝐴 < π ∨ 𝐴 = π)) |
| 60 | 47, 54, 59 | mpjaodan 961 |
. . . 4
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) →
(cos‘𝐴) ≠
0) |
| 61 | 36, 60 | pm2.21ddne 3026 |
. . 3
⊢ (((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) ∧
(π / 2) < 𝐴) →
𝐴 = (π /
2)) |
| 62 | 56 | rehalfcld 12513 |
. . . 4
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(π / 2) ∈ ℝ) |
| 63 | 7, 62 | lttri4d 11402 |
. . 3
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
(𝐴 < (π / 2) ∨
𝐴 = (π / 2) ∨ (π /
2) < 𝐴)) |
| 64 | 34, 35, 61, 63 | mpjao3dan 1434 |
. 2
⊢ ((𝐴 ∈ (0[,]π) ∧
(cos‘𝐴) = 0) →
𝐴 = (π /
2)) |
| 65 | | fveq2 6906 |
. . . 4
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
(cos‘(π / 2))) |
| 66 | | coshalfpi 26511 |
. . . 4
⊢
(cos‘(π / 2)) = 0 |
| 67 | 65, 66 | eqtrdi 2793 |
. . 3
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
0) |
| 68 | 67 | adantl 481 |
. 2
⊢ ((𝐴 ∈ (0[,]π) ∧ 𝐴 = (π / 2)) →
(cos‘𝐴) =
0) |
| 69 | 64, 68 | impbida 801 |
1
⊢ (𝐴 ∈ (0[,]π) →
((cos‘𝐴) = 0 ↔
𝐴 = (π /
2))) |