Proof of Theorem sinq12gt0
Step | Hyp | Ref
| Expression |
1 | | 0xr 7924 |
. . 3
⊢ 0 ∈
ℝ* |
2 | | pire 13118 |
. . . 4
⊢ π
∈ ℝ |
3 | 2 | rexri 7935 |
. . 3
⊢ π
∈ ℝ* |
4 | | elioo2 9825 |
. . 3
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) → (𝐴 ∈ (0(,)π) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π))) |
5 | 1, 3, 4 | mp2an 423 |
. 2
⊢ (𝐴 ∈ (0(,)π) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π)) |
6 | | rehalfcl 9060 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
7 | 6 | 3ad2ant1 1003 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (𝐴 / 2) ∈ ℝ) |
8 | | halfpos2 9063 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ 0 < (𝐴 / 2))) |
9 | 8 | biimpa 294 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴 / 2)) |
10 | 9 | 3adant3 1002 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (𝐴 / 2)) |
11 | | 2re 8903 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
12 | | 2pos 8924 |
. . . . . . . . 9
⊢ 0 <
2 |
13 | 11, 12 | pm3.2i 270 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 0 < 2) |
14 | | ltdiv1 8739 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
15 | 2, 13, 14 | mp3an23 1311 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
16 | 15 | adantr 274 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
17 | 16 | biimp3a 1327 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (𝐴 / 2) < (π / 2)) |
18 | | sincosq1lem 13157 |
. . . . 5
⊢ (((𝐴 / 2) ∈ ℝ ∧ 0
< (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2)) → 0
< (sin‘(𝐴 /
2))) |
19 | 7, 10, 17, 18 | syl3anc 1220 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘(𝐴 / 2))) |
20 | | resubcl 8139 |
. . . . . . . . 9
⊢ ((π
∈ ℝ ∧ 𝐴
∈ ℝ) → (π − 𝐴) ∈ ℝ) |
21 | 2, 20 | mpan 421 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (π
− 𝐴) ∈
ℝ) |
22 | | rehalfcl 9060 |
. . . . . . . 8
⊢ ((π
− 𝐴) ∈ ℝ
→ ((π − 𝐴) /
2) ∈ ℝ) |
23 | 21, 22 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) / 2) ∈
ℝ) |
24 | 23 | 3ad2ant1 1003 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((π − 𝐴) / 2) ∈
ℝ) |
25 | | posdif 8330 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ) → (𝐴
< π ↔ 0 < (π − 𝐴))) |
26 | 2, 25 | mpan2 422 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ 0 < (π
− 𝐴))) |
27 | | halfpos2 9063 |
. . . . . . . . . 10
⊢ ((π
− 𝐴) ∈ ℝ
→ (0 < (π − 𝐴) ↔ 0 < ((π − 𝐴) / 2))) |
28 | 21, 27 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 <
(π − 𝐴) ↔ 0
< ((π − 𝐴) /
2))) |
29 | 26, 28 | bitrd 187 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ 0 < ((π
− 𝐴) /
2))) |
30 | 29 | adantr 274 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 < π ↔ 0 < ((π
− 𝐴) /
2))) |
31 | 30 | biimp3a 1327 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < ((π −
𝐴) / 2)) |
32 | | ltsubpos 8329 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ) → (0 < 𝐴 ↔ (π − 𝐴) < π)) |
33 | 2, 32 | mpan2 422 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ (π −
𝐴) <
π)) |
34 | | ltdiv1 8739 |
. . . . . . . . . . 11
⊢ (((π
− 𝐴) ∈ ℝ
∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((π − 𝐴) < π
↔ ((π − 𝐴) /
2) < (π / 2))) |
35 | 2, 13, 34 | mp3an23 1311 |
. . . . . . . . . 10
⊢ ((π
− 𝐴) ∈ ℝ
→ ((π − 𝐴)
< π ↔ ((π − 𝐴) / 2) < (π / 2))) |
36 | 21, 35 | syl 14 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) < π ↔
((π − 𝐴) / 2) <
(π / 2))) |
37 | 33, 36 | bitrd 187 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ ((π −
𝐴) / 2) < (π /
2))) |
38 | 37 | biimpa 294 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((π −
𝐴) / 2) < (π /
2)) |
39 | 38 | 3adant3 1002 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((π − 𝐴) / 2) < (π /
2)) |
40 | | sincosq1lem 13157 |
. . . . . 6
⊢ ((((π
− 𝐴) / 2) ∈
ℝ ∧ 0 < ((π − 𝐴) / 2) ∧ ((π − 𝐴) / 2) < (π / 2)) → 0
< (sin‘((π − 𝐴) / 2))) |
41 | 24, 31, 39, 40 | syl3anc 1220 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘((π
− 𝐴) /
2))) |
42 | | recn 7865 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
43 | | picn 13119 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
44 | | 2cn 8904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
45 | | 2ap0 8926 |
. . . . . . . . . . 11
⊢ 2 #
0 |
46 | 44, 45 | pm3.2i 270 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ ∧ 2 # 0) |
47 | | divsubdirap 8581 |
. . . . . . . . . 10
⊢ ((π
∈ ℂ ∧ 𝐴
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((π −
𝐴) / 2) = ((π / 2)
− (𝐴 /
2))) |
48 | 43, 46, 47 | mp3an13 1310 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((π
− 𝐴) / 2) = ((π /
2) − (𝐴 /
2))) |
49 | 42, 48 | syl 14 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) / 2) = ((π /
2) − (𝐴 /
2))) |
50 | 49 | fveq2d 5472 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π − 𝐴) / 2)) = (sin‘((π / 2) −
(𝐴 / 2)))) |
51 | 6 | recnd 7906 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℂ) |
52 | | sinhalfpim 13153 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘((π / 2) − (𝐴 / 2))) = (cos‘(𝐴 / 2))) |
53 | 51, 52 | syl 14 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) − (𝐴 / 2))) = (cos‘(𝐴 / 2))) |
54 | 50, 53 | eqtrd 2190 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(sin‘((π − 𝐴) / 2)) = (cos‘(𝐴 / 2))) |
55 | 54 | 3ad2ant1 1003 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (sin‘((π −
𝐴) / 2)) =
(cos‘(𝐴 /
2))) |
56 | 41, 55 | breqtrd 3990 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (cos‘(𝐴 / 2))) |
57 | | resincl 11617 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ →
(sin‘(𝐴 / 2)) ∈
ℝ) |
58 | | recoscl 11618 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ →
(cos‘(𝐴 / 2)) ∈
ℝ) |
59 | 57, 58 | jca 304 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
((sin‘(𝐴 / 2)) ∈
ℝ ∧ (cos‘(𝐴
/ 2)) ∈ ℝ)) |
60 | | axmulgt0 7949 |
. . . . . . 7
⊢
(((sin‘(𝐴 /
2)) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
61 | 6, 59, 60 | 3syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
62 | | remulcl 7860 |
. . . . . . . . 9
⊢
(((sin‘(𝐴 /
2)) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
63 | 6, 59, 62 | 3syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
64 | | axmulgt0 7949 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℝ) →
((0 < 2 ∧ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
65 | 11, 63, 64 | sylancr 411 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((0 <
2 ∧ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
66 | 12, 65 | mpani 427 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) → 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
67 | 61, 66 | syld 45 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
68 | 67 | 3ad2ant1 1003 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
69 | 19, 56, 68 | mp2and 430 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
70 | | divcanap2 8553 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 # 0) → (2 · (𝐴 / 2)) = 𝐴) |
71 | 44, 45, 70 | mp3an23 1311 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) |
72 | 42, 71 | syl 14 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (2
· (𝐴 / 2)) = 𝐴) |
73 | 72 | fveq2d 5472 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(sin‘(2 · (𝐴 /
2))) = (sin‘𝐴)) |
74 | | sin2t 11646 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
75 | 51, 74 | syl 14 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
76 | 73, 75 | eqtr3d 2192 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
77 | 76 | 3ad2ant1 1003 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
78 | 69, 77 | breqtrrd 3992 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘𝐴)) |
79 | 5, 78 | sylbi 120 |
1
⊢ (𝐴 ∈ (0(,)π) → 0 <
(sin‘𝐴)) |