Step |
Hyp |
Ref |
Expression |
1 |
|
0xr |
⊢ 0 ∈ ℝ* |
2 |
|
pire |
⊢ π ∈ ℝ |
3 |
2
|
rexri |
⊢ π ∈ ℝ* |
4 |
|
elioo2 |
⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( 𝐴 ∈ ( 0 (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) ) ) |
5 |
1 3 4
|
mp2an |
⊢ ( 𝐴 ∈ ( 0 (,) π ) ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) ) |
6 |
|
rehalfcl |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℝ ) |
7 |
6
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( 𝐴 / 2 ) ∈ ℝ ) |
8 |
|
halfpos2 |
⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ 0 < ( 𝐴 / 2 ) ) ) |
9 |
8
|
biimpa |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → 0 < ( 𝐴 / 2 ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( 𝐴 / 2 ) ) |
11 |
|
2re |
⊢ 2 ∈ ℝ |
12 |
|
2pos |
⊢ 0 < 2 |
13 |
11 12
|
pm3.2i |
⊢ ( 2 ∈ ℝ ∧ 0 < 2 ) |
14 |
|
ltdiv1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) ) |
15 |
2 13 14
|
mp3an23 |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) ) |
16 |
15
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 < π ↔ ( 𝐴 / 2 ) < ( π / 2 ) ) ) |
17 |
16
|
biimp3a |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( 𝐴 / 2 ) < ( π / 2 ) ) |
18 |
|
sincosq1lem |
⊢ ( ( ( 𝐴 / 2 ) ∈ ℝ ∧ 0 < ( 𝐴 / 2 ) ∧ ( 𝐴 / 2 ) < ( π / 2 ) ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) ) |
19 |
7 10 17 18
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ ( 𝐴 / 2 ) ) ) |
20 |
|
resubcl |
⊢ ( ( π ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( π − 𝐴 ) ∈ ℝ ) |
21 |
2 20
|
mpan |
⊢ ( 𝐴 ∈ ℝ → ( π − 𝐴 ) ∈ ℝ ) |
22 |
|
rehalfcl |
⊢ ( ( π − 𝐴 ) ∈ ℝ → ( ( π − 𝐴 ) / 2 ) ∈ ℝ ) |
23 |
21 22
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) / 2 ) ∈ ℝ ) |
24 |
23
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( π − 𝐴 ) / 2 ) ∈ ℝ ) |
25 |
|
posdif |
⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( 𝐴 < π ↔ 0 < ( π − 𝐴 ) ) ) |
26 |
2 25
|
mpan2 |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ 0 < ( π − 𝐴 ) ) ) |
27 |
|
halfpos2 |
⊢ ( ( π − 𝐴 ) ∈ ℝ → ( 0 < ( π − 𝐴 ) ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) ) |
28 |
21 27
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( 0 < ( π − 𝐴 ) ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) ) |
29 |
26 28
|
bitrd |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 < π ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) ) |
30 |
29
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐴 < π ↔ 0 < ( ( π − 𝐴 ) / 2 ) ) ) |
31 |
30
|
biimp3a |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( ( π − 𝐴 ) / 2 ) ) |
32 |
|
ltsubpos |
⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ) → ( 0 < 𝐴 ↔ ( π − 𝐴 ) < π ) ) |
33 |
2 32
|
mpan2 |
⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( π − 𝐴 ) < π ) ) |
34 |
|
ltdiv1 |
⊢ ( ( ( π − 𝐴 ) ∈ ℝ ∧ π ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) ) |
35 |
2 13 34
|
mp3an23 |
⊢ ( ( π − 𝐴 ) ∈ ℝ → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) ) |
36 |
21 35
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) < π ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) ) |
37 |
33 36
|
bitrd |
⊢ ( 𝐴 ∈ ℝ → ( 0 < 𝐴 ↔ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) ) |
38 |
37
|
biimpa |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) |
39 |
38
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) |
40 |
|
sincosq1lem |
⊢ ( ( ( ( π − 𝐴 ) / 2 ) ∈ ℝ ∧ 0 < ( ( π − 𝐴 ) / 2 ) ∧ ( ( π − 𝐴 ) / 2 ) < ( π / 2 ) ) → 0 < ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) ) |
41 |
24 31 39 40
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) ) |
42 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
43 |
|
picn |
⊢ π ∈ ℂ |
44 |
|
2cnne0 |
⊢ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) |
45 |
|
divsubdir |
⊢ ( ( π ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ) → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) |
46 |
43 44 45
|
mp3an13 |
⊢ ( 𝐴 ∈ ℂ → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) |
47 |
42 46
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( ( π − 𝐴 ) / 2 ) = ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) |
48 |
47
|
fveq2d |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) ) |
49 |
6
|
recnd |
⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / 2 ) ∈ ℂ ) |
50 |
|
sinhalfpim |
⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) = ( cos ‘ ( 𝐴 / 2 ) ) ) |
51 |
49 50
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π / 2 ) − ( 𝐴 / 2 ) ) ) = ( cos ‘ ( 𝐴 / 2 ) ) ) |
52 |
48 51
|
eqtrd |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( cos ‘ ( 𝐴 / 2 ) ) ) |
53 |
52
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( sin ‘ ( ( π − 𝐴 ) / 2 ) ) = ( cos ‘ ( 𝐴 / 2 ) ) ) |
54 |
41 53
|
breqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) |
55 |
|
resincl |
⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) |
56 |
|
recoscl |
⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) |
57 |
55 56
|
jca |
⊢ ( ( 𝐴 / 2 ) ∈ ℝ → ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) ) |
58 |
|
axmulgt0 |
⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
59 |
6 57 58
|
3syl |
⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
60 |
|
remulcl |
⊢ ( ( ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℝ ∧ ( cos ‘ ( 𝐴 / 2 ) ) ∈ ℝ ) → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ ) |
61 |
6 57 60
|
3syl |
⊢ ( 𝐴 ∈ ℝ → ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ ) |
62 |
|
axmulgt0 |
⊢ ( ( 2 ∈ ℝ ∧ ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ∈ ℝ ) → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) ) |
63 |
11 61 62
|
sylancr |
⊢ ( 𝐴 ∈ ℝ → ( ( 0 < 2 ∧ 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) ) |
64 |
12 63
|
mpani |
⊢ ( 𝐴 ∈ ℝ → ( 0 < ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) ) |
65 |
59 64
|
syld |
⊢ ( 𝐴 ∈ ℝ → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) ) |
66 |
65
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( ( 0 < ( sin ‘ ( 𝐴 / 2 ) ) ∧ 0 < ( cos ‘ ( 𝐴 / 2 ) ) ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) ) |
67 |
19 54 66
|
mp2and |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
68 |
|
2cn |
⊢ 2 ∈ ℂ |
69 |
|
2ne0 |
⊢ 2 ≠ 0 |
70 |
|
divcan2 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 ) |
71 |
68 69 70
|
mp3an23 |
⊢ ( 𝐴 ∈ ℂ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 ) |
72 |
42 71
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( 2 · ( 𝐴 / 2 ) ) = 𝐴 ) |
73 |
72
|
fveq2d |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( sin ‘ 𝐴 ) ) |
74 |
|
sin2t |
⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
75 |
49 74
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ ( 2 · ( 𝐴 / 2 ) ) ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
76 |
73 75
|
eqtr3d |
⊢ ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
77 |
76
|
3ad2ant1 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → ( sin ‘ 𝐴 ) = ( 2 · ( ( sin ‘ ( 𝐴 / 2 ) ) · ( cos ‘ ( 𝐴 / 2 ) ) ) ) ) |
78 |
67 77
|
breqtrrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ∧ 𝐴 < π ) → 0 < ( sin ‘ 𝐴 ) ) |
79 |
5 78
|
sylbi |
⊢ ( 𝐴 ∈ ( 0 (,) π ) → 0 < ( sin ‘ 𝐴 ) ) |