Proof of Theorem coseq0q4123
Step | Hyp | Ref
| Expression |
1 | | 0re 7913 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | 1 | ltnri 8005 |
. . . 4
⊢ ¬ 0
< 0 |
3 | | elioore 9862 |
. . . . . . 7
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) → 𝐴 ∈ ℝ) |
4 | 3 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → 𝐴 ∈ ℝ) |
5 | | halfpire 13472 |
. . . . . 6
⊢ (π /
2) ∈ ℝ |
6 | | reaplt 8500 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (π / 2)
∈ ℝ) → (𝐴 #
(π / 2) ↔ (𝐴 <
(π / 2) ∨ (π / 2) < 𝐴))) |
7 | 4, 5, 6 | sylancl 411 |
. . . . 5
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → (𝐴 # (π / 2) ↔ (𝐴 < (π / 2) ∨ (π / 2) < 𝐴))) |
8 | 3 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → 𝐴 ∈ ℝ) |
9 | | neghalfpirx 13474 |
. . . . . . . . . . . . . 14
⊢ -(π /
2) ∈ ℝ* |
10 | | 3re 8945 |
. . . . . . . . . . . . . . . 16
⊢ 3 ∈
ℝ |
11 | 10, 5 | remulcli 7927 |
. . . . . . . . . . . . . . 15
⊢ (3
· (π / 2)) ∈ ℝ |
12 | 11 | rexri 7970 |
. . . . . . . . . . . . . 14
⊢ (3
· (π / 2)) ∈ ℝ* |
13 | | elioo2 9871 |
. . . . . . . . . . . . . 14
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (3 · (π / 2)) ∈
ℝ*) → (𝐴 ∈ (-(π / 2)(,)(3 · (π /
2))) ↔ (𝐴 ∈
ℝ ∧ -(π / 2) < 𝐴 ∧ 𝐴 < (3 · (π /
2))))) |
14 | 9, 12, 13 | mp2an 424 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ↔ (𝐴 ∈ ℝ ∧ -(π / 2) < 𝐴 ∧ 𝐴 < (3 · (π /
2)))) |
15 | 14 | simp2bi 1008 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) → -(π / 2) < 𝐴) |
16 | 15 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → -(π / 2) <
𝐴) |
17 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → 𝐴 < (π / 2)) |
18 | 9 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → -(π / 2) ∈
ℝ*) |
19 | 5 | rexri 7970 |
. . . . . . . . . . . 12
⊢ (π /
2) ∈ ℝ* |
20 | | elioo2 9871 |
. . . . . . . . . . . 12
⊢ ((-(π
/ 2) ∈ ℝ* ∧ (π / 2) ∈ ℝ*)
→ (𝐴 ∈ (-(π /
2)(,)(π / 2)) ↔ (𝐴
∈ ℝ ∧ -(π / 2) < 𝐴 ∧ 𝐴 < (π / 2)))) |
21 | 18, 19, 20 | sylancl 411 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → (𝐴 ∈ (-(π / 2)(,)(π / 2)) ↔
(𝐴 ∈ ℝ ∧
-(π / 2) < 𝐴 ∧
𝐴 < (π /
2)))) |
22 | 8, 16, 17, 21 | mpbir3and 1175 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → 𝐴 ∈ (-(π / 2)(,)(π /
2))) |
23 | | cosq14gt0 13512 |
. . . . . . . . . 10
⊢ (𝐴 ∈ (-(π / 2)(,)(π /
2)) → 0 < (cos‘𝐴)) |
24 | 22, 23 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 < (π / 2)) → 0 <
(cos‘𝐴)) |
25 | 24 | adantlr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ 𝐴 < (π / 2)) → 0 <
(cos‘𝐴)) |
26 | | simplr 525 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ 𝐴 < (π / 2)) → (cos‘𝐴) = 0) |
27 | 25, 26 | breqtrd 4013 |
. . . . . . 7
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ 𝐴 < (π / 2)) → 0 <
0) |
28 | 27 | ex 114 |
. . . . . 6
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → (𝐴 < (π / 2) → 0 <
0)) |
29 | | simplr 525 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ (π / 2) < 𝐴) → (cos‘𝐴) = 0) |
30 | 3 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (π / 2) < 𝐴) → 𝐴 ∈ ℝ) |
31 | | simpr 109 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (π / 2) < 𝐴) → (π / 2) < 𝐴) |
32 | 14 | simp3bi 1009 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) → 𝐴 < (3 · (π /
2))) |
33 | 32 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (π / 2) < 𝐴) → 𝐴 < (3 · (π /
2))) |
34 | | elioo2 9871 |
. . . . . . . . . . . 12
⊢ (((π /
2) ∈ ℝ* ∧ (3 · (π / 2)) ∈
ℝ*) → (𝐴 ∈ ((π / 2)(,)(3 · (π /
2))) ↔ (𝐴 ∈
ℝ ∧ (π / 2) < 𝐴 ∧ 𝐴 < (3 · (π /
2))))) |
35 | 19, 12, 34 | mp2an 424 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ((π / 2)(,)(3
· (π / 2))) ↔ (𝐴 ∈ ℝ ∧ (π / 2) < 𝐴 ∧ 𝐴 < (3 · (π /
2)))) |
36 | 30, 31, 33, 35 | syl3anbrc 1176 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (π / 2) < 𝐴) → 𝐴 ∈ ((π / 2)(,)(3 · (π /
2)))) |
37 | | cosq23lt0 13513 |
. . . . . . . . . 10
⊢ (𝐴 ∈ ((π / 2)(,)(3
· (π / 2))) → (cos‘𝐴) < 0) |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (π / 2) < 𝐴) → (cos‘𝐴) < 0) |
39 | 38 | adantlr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ (π / 2) < 𝐴) → (cos‘𝐴) < 0) |
40 | 29, 39 | eqbrtrrd 4011 |
. . . . . . 7
⊢ (((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) ∧ (π / 2) < 𝐴) → 0 <
0) |
41 | 40 | ex 114 |
. . . . . 6
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → ((π / 2) < 𝐴 → 0 <
0)) |
42 | 28, 41 | jaod 712 |
. . . . 5
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → ((𝐴 < (π / 2) ∨ (π / 2) < 𝐴) → 0 <
0)) |
43 | 7, 42 | sylbid 149 |
. . . 4
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → (𝐴 # (π / 2) → 0 <
0)) |
44 | 2, 43 | mtoi 659 |
. . 3
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → ¬ 𝐴 # (π / 2)) |
45 | 3 | recnd 7941 |
. . . 4
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) → 𝐴 ∈ ℂ) |
46 | | picn 13467 |
. . . . 5
⊢ π
∈ ℂ |
47 | | halfcl 9097 |
. . . . 5
⊢ (π
∈ ℂ → (π / 2) ∈ ℂ) |
48 | 46, 47 | mp1i 10 |
. . . 4
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → (π / 2) ∈
ℂ) |
49 | | apti 8534 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ (π / 2)
∈ ℂ) → (𝐴 =
(π / 2) ↔ ¬ 𝐴 #
(π / 2))) |
50 | 45, 48, 49 | syl2an2r 590 |
. . 3
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → (𝐴 = (π / 2) ↔ ¬ 𝐴 # (π / 2))) |
51 | 44, 50 | mpbird 166 |
. 2
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ (cos‘𝐴) = 0) → 𝐴 = (π / 2)) |
52 | | fveq2 5494 |
. . . 4
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
(cos‘(π / 2))) |
53 | | coshalfpi 13477 |
. . . 4
⊢
(cos‘(π / 2)) = 0 |
54 | 52, 53 | eqtrdi 2219 |
. . 3
⊢ (𝐴 = (π / 2) →
(cos‘𝐴) =
0) |
55 | 54 | adantl 275 |
. 2
⊢ ((𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) ∧ 𝐴 = (π / 2)) → (cos‘𝐴) = 0) |
56 | 51, 55 | impbida 591 |
1
⊢ (𝐴 ∈ (-(π / 2)(,)(3
· (π / 2))) → ((cos‘𝐴) = 0 ↔ 𝐴 = (π / 2))) |