Proof of Theorem sinq12gt0
Step | Hyp | Ref
| Expression |
1 | | 0xr 10767 |
. . 3
⊢ 0 ∈
ℝ* |
2 | | pire 25203 |
. . . 4
⊢ π
∈ ℝ |
3 | 2 | rexri 10778 |
. . 3
⊢ π
∈ ℝ* |
4 | | elioo2 12863 |
. . 3
⊢ ((0
∈ ℝ* ∧ π ∈ ℝ*) → (𝐴 ∈ (0(,)π) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π))) |
5 | 1, 3, 4 | mp2an 692 |
. 2
⊢ (𝐴 ∈ (0(,)π) ↔ (𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π)) |
6 | | rehalfcl 11943 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℝ) |
7 | 6 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (𝐴 / 2) ∈ ℝ) |
8 | | halfpos2 11946 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ 0 < (𝐴 / 2))) |
9 | 8 | biimpa 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (𝐴 / 2)) |
10 | 9 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (𝐴 / 2)) |
11 | | 2re 11791 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
12 | | 2pos 11820 |
. . . . . . . . 9
⊢ 0 <
2 |
13 | 11, 12 | pm3.2i 474 |
. . . . . . . 8
⊢ (2 ∈
ℝ ∧ 0 < 2) |
14 | | ltdiv1 11583 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
15 | 2, 13, 14 | mp3an23 1454 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
16 | 15 | adantr 484 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 < π ↔ (𝐴 / 2) < (π /
2))) |
17 | 16 | biimp3a 1470 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (𝐴 / 2) < (π / 2)) |
18 | | sincosq1lem 25242 |
. . . . 5
⊢ (((𝐴 / 2) ∈ ℝ ∧ 0
< (𝐴 / 2) ∧ (𝐴 / 2) < (π / 2)) → 0
< (sin‘(𝐴 /
2))) |
19 | 7, 10, 17, 18 | syl3anc 1372 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘(𝐴 / 2))) |
20 | | resubcl 11029 |
. . . . . . . . 9
⊢ ((π
∈ ℝ ∧ 𝐴
∈ ℝ) → (π − 𝐴) ∈ ℝ) |
21 | 2, 20 | mpan 690 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (π
− 𝐴) ∈
ℝ) |
22 | | rehalfcl 11943 |
. . . . . . . 8
⊢ ((π
− 𝐴) ∈ ℝ
→ ((π − 𝐴) /
2) ∈ ℝ) |
23 | 21, 22 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) / 2) ∈
ℝ) |
24 | 23 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((π − 𝐴) / 2) ∈
ℝ) |
25 | | posdif 11212 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ) → (𝐴
< π ↔ 0 < (π − 𝐴))) |
26 | 2, 25 | mpan2 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ 0 < (π
− 𝐴))) |
27 | | halfpos2 11946 |
. . . . . . . . . 10
⊢ ((π
− 𝐴) ∈ ℝ
→ (0 < (π − 𝐴) ↔ 0 < ((π − 𝐴) / 2))) |
28 | 21, 27 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 <
(π − 𝐴) ↔ 0
< ((π − 𝐴) /
2))) |
29 | 26, 28 | bitrd 282 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 < π ↔ 0 < ((π
− 𝐴) /
2))) |
30 | 29 | adantr 484 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → (𝐴 < π ↔ 0 < ((π
− 𝐴) /
2))) |
31 | 30 | biimp3a 1470 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < ((π −
𝐴) / 2)) |
32 | | ltsubpos 11211 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ π
∈ ℝ) → (0 < 𝐴 ↔ (π − 𝐴) < π)) |
33 | 2, 32 | mpan2 691 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ (π −
𝐴) <
π)) |
34 | | ltdiv1 11583 |
. . . . . . . . . . 11
⊢ (((π
− 𝐴) ∈ ℝ
∧ π ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((π − 𝐴) < π
↔ ((π − 𝐴) /
2) < (π / 2))) |
35 | 2, 13, 34 | mp3an23 1454 |
. . . . . . . . . 10
⊢ ((π
− 𝐴) ∈ ℝ
→ ((π − 𝐴)
< π ↔ ((π − 𝐴) / 2) < (π / 2))) |
36 | 21, 35 | syl 17 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) < π ↔
((π − 𝐴) / 2) <
(π / 2))) |
37 | 33, 36 | bitrd 282 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (0 <
𝐴 ↔ ((π −
𝐴) / 2) < (π /
2))) |
38 | 37 | biimpa 480 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → ((π −
𝐴) / 2) < (π /
2)) |
39 | 38 | 3adant3 1133 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((π − 𝐴) / 2) < (π /
2)) |
40 | | sincosq1lem 25242 |
. . . . . 6
⊢ ((((π
− 𝐴) / 2) ∈
ℝ ∧ 0 < ((π − 𝐴) / 2) ∧ ((π − 𝐴) / 2) < (π / 2)) → 0
< (sin‘((π − 𝐴) / 2))) |
41 | 24, 31, 39, 40 | syl3anc 1372 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘((π
− 𝐴) /
2))) |
42 | | recn 10706 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
43 | | picn 25204 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
44 | | 2cnne0 11927 |
. . . . . . . . . 10
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
45 | | divsubdir 11413 |
. . . . . . . . . 10
⊢ ((π
∈ ℂ ∧ 𝐴
∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((π −
𝐴) / 2) = ((π / 2)
− (𝐴 /
2))) |
46 | 43, 44, 45 | mp3an13 1453 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → ((π
− 𝐴) / 2) = ((π /
2) − (𝐴 /
2))) |
47 | 42, 46 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → ((π
− 𝐴) / 2) = ((π /
2) − (𝐴 /
2))) |
48 | 47 | fveq2d 6679 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π − 𝐴) / 2)) = (sin‘((π / 2) −
(𝐴 / 2)))) |
49 | 6 | recnd 10748 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 / 2) ∈
ℂ) |
50 | | sinhalfpim 25238 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘((π / 2) − (𝐴 / 2))) = (cos‘(𝐴 / 2))) |
51 | 49, 50 | syl 17 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(sin‘((π / 2) − (𝐴 / 2))) = (cos‘(𝐴 / 2))) |
52 | 48, 51 | eqtrd 2773 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
(sin‘((π − 𝐴) / 2)) = (cos‘(𝐴 / 2))) |
53 | 52 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (sin‘((π −
𝐴) / 2)) =
(cos‘(𝐴 /
2))) |
54 | 41, 53 | breqtrd 5057 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (cos‘(𝐴 / 2))) |
55 | | resincl 15586 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ →
(sin‘(𝐴 / 2)) ∈
ℝ) |
56 | | recoscl 15587 |
. . . . . . . 8
⊢ ((𝐴 / 2) ∈ ℝ →
(cos‘(𝐴 / 2)) ∈
ℝ) |
57 | 55, 56 | jca 515 |
. . . . . . 7
⊢ ((𝐴 / 2) ∈ ℝ →
((sin‘(𝐴 / 2)) ∈
ℝ ∧ (cos‘(𝐴
/ 2)) ∈ ℝ)) |
58 | | axmulgt0 10794 |
. . . . . . 7
⊢
(((sin‘(𝐴 /
2)) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
59 | 6, 57, 58 | 3syl 18 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
60 | | remulcl 10701 |
. . . . . . . . 9
⊢
(((sin‘(𝐴 /
2)) ∈ ℝ ∧ (cos‘(𝐴 / 2)) ∈ ℝ) →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
61 | 6, 57, 60 | 3syl 18 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ →
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) ∈ ℝ) |
62 | | axmulgt0 10794 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))) ∈ ℝ) →
((0 < 2 ∧ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
63 | 11, 61, 62 | sylancr 590 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → ((0 <
2 ∧ 0 < ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))) → 0 < (2
· ((sin‘(𝐴 /
2)) · (cos‘(𝐴
/ 2)))))) |
64 | 12, 63 | mpani 696 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (0 <
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))) → 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
65 | 59, 64 | syld 47 |
. . . . 5
⊢ (𝐴 ∈ ℝ → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
66 | 65 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → ((0 <
(sin‘(𝐴 / 2)) ∧ 0
< (cos‘(𝐴 / 2)))
→ 0 < (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2)))))) |
67 | 19, 54, 66 | mp2and 699 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
68 | | 2cn 11792 |
. . . . . . . 8
⊢ 2 ∈
ℂ |
69 | | 2ne0 11821 |
. . . . . . . 8
⊢ 2 ≠
0 |
70 | | divcan2 11385 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (2 · (𝐴 / 2)) = 𝐴) |
71 | 68, 69, 70 | mp3an23 1454 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → (2
· (𝐴 / 2)) = 𝐴) |
72 | 42, 71 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → (2
· (𝐴 / 2)) = 𝐴) |
73 | 72 | fveq2d 6679 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(sin‘(2 · (𝐴 /
2))) = (sin‘𝐴)) |
74 | | sin2t 15623 |
. . . . . 6
⊢ ((𝐴 / 2) ∈ ℂ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
75 | 49, 74 | syl 17 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(sin‘(2 · (𝐴 /
2))) = (2 · ((sin‘(𝐴 / 2)) · (cos‘(𝐴 / 2))))) |
76 | 73, 75 | eqtr3d 2775 |
. . . 4
⊢ (𝐴 ∈ ℝ →
(sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
77 | 76 | 3ad2ant1 1134 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → (sin‘𝐴) = (2 ·
((sin‘(𝐴 / 2))
· (cos‘(𝐴 /
2))))) |
78 | 67, 77 | breqtrrd 5059 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴 ∧ 𝐴 < π) → 0 < (sin‘𝐴)) |
79 | 5, 78 | sylbi 220 |
1
⊢ (𝐴 ∈ (0(,)π) → 0 <
(sin‘𝐴)) |