| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0xr |
⊢ 0 ∈ ℝ* |
| 2 |
1
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → 0 ∈ ℝ* ) |
| 3 |
|
2re |
⊢ 2 ∈ ℝ |
| 4 |
|
pire |
⊢ π ∈ ℝ |
| 5 |
3 4
|
remulcli |
⊢ ( 2 · π ) ∈ ℝ |
| 6 |
5
|
rexri |
⊢ ( 2 · π ) ∈ ℝ* |
| 7 |
6
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → ( 2 · π ) ∈ ℝ* ) |
| 8 |
4
|
renegcli |
⊢ - π ∈ ℝ |
| 9 |
8
|
a1i |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - π ∈ ℝ ) |
| 10 |
4
|
a1i |
⊢ ( 𝐴 ∈ ( - π [,] π ) → π ∈ ℝ ) |
| 11 |
|
id |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ∈ ( - π [,] π ) ) |
| 12 |
|
eliccre |
⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ 𝐴 ∈ ( - π [,] π ) ) → 𝐴 ∈ ℝ ) |
| 13 |
9 10 11 12
|
syl3anc |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ∈ ℝ ) |
| 14 |
13
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ℝ ) |
| 15 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → 0 < 𝐴 ) |
| 16 |
5
|
a1i |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 2 · π ) ∈ ℝ ) |
| 17 |
9
|
rexrd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - π ∈ ℝ* ) |
| 18 |
10
|
rexrd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → π ∈ ℝ* ) |
| 19 |
|
iccleub |
⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ ( - π [,] π ) ) → 𝐴 ≤ π ) |
| 20 |
17 18 11 19
|
syl3anc |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ≤ π ) |
| 21 |
|
pirp |
⊢ π ∈ ℝ+ |
| 22 |
|
2timesgt |
⊢ ( π ∈ ℝ+ → π < ( 2 · π ) ) |
| 23 |
21 22
|
ax-mp |
⊢ π < ( 2 · π ) |
| 24 |
23
|
a1i |
⊢ ( 𝐴 ∈ ( - π [,] π ) → π < ( 2 · π ) ) |
| 25 |
13 10 16 20 24
|
lelttrd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 < ( 2 · π ) ) |
| 26 |
25
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → 𝐴 < ( 2 · π ) ) |
| 27 |
2 7 14 15 26
|
eliood |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ) |
| 28 |
27
|
adantlr |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ 0 < 𝐴 ) → 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ) |
| 29 |
|
sinaover2ne0 |
⊢ ( 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |
| 30 |
28 29
|
syl |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ 0 < 𝐴 ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |
| 31 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → 𝐴 ∈ ( - π [,] π ) ) |
| 32 |
31 13
|
syl |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → 𝐴 ∈ ℝ ) |
| 33 |
|
0red |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → 0 ∈ ℝ ) |
| 34 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → 𝐴 ≠ 0 ) |
| 35 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → ¬ 0 < 𝐴 ) |
| 36 |
32 33 34 35
|
lttri5d |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → 𝐴 < 0 ) |
| 37 |
13
|
recnd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 𝐴 ∈ ℂ ) |
| 38 |
37
|
halfcld |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 𝐴 / 2 ) ∈ ℂ ) |
| 39 |
|
sinneg |
⊢ ( ( 𝐴 / 2 ) ∈ ℂ → ( sin ‘ - ( 𝐴 / 2 ) ) = - ( sin ‘ ( 𝐴 / 2 ) ) ) |
| 40 |
38 39
|
syl |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( sin ‘ - ( 𝐴 / 2 ) ) = - ( sin ‘ ( 𝐴 / 2 ) ) ) |
| 41 |
|
2cnd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 2 ∈ ℂ ) |
| 42 |
|
2ne0 |
⊢ 2 ≠ 0 |
| 43 |
42
|
a1i |
⊢ ( 𝐴 ∈ ( - π [,] π ) → 2 ≠ 0 ) |
| 44 |
37 41 43
|
divnegd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - ( 𝐴 / 2 ) = ( - 𝐴 / 2 ) ) |
| 45 |
44
|
fveq2d |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( sin ‘ - ( 𝐴 / 2 ) ) = ( sin ‘ ( - 𝐴 / 2 ) ) ) |
| 46 |
40 45
|
eqtr3d |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - ( sin ‘ ( 𝐴 / 2 ) ) = ( sin ‘ ( - 𝐴 / 2 ) ) ) |
| 47 |
46
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - ( sin ‘ ( 𝐴 / 2 ) ) = ( sin ‘ ( - 𝐴 / 2 ) ) ) |
| 48 |
1
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → 0 ∈ ℝ* ) |
| 49 |
6
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( 2 · π ) ∈ ℝ* ) |
| 50 |
13
|
renegcld |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - 𝐴 ∈ ℝ ) |
| 51 |
50
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - 𝐴 ∈ ℝ ) |
| 52 |
|
simpr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → 𝐴 < 0 ) |
| 53 |
13
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → 𝐴 ∈ ℝ ) |
| 54 |
53
|
lt0neg1d |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( 𝐴 < 0 ↔ 0 < - 𝐴 ) ) |
| 55 |
52 54
|
mpbid |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → 0 < - 𝐴 ) |
| 56 |
5
|
renegcli |
⊢ - ( 2 · π ) ∈ ℝ |
| 57 |
56
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - ( 2 · π ) ∈ ℝ ) |
| 58 |
8
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - π ∈ ℝ ) |
| 59 |
4 5
|
ltnegi |
⊢ ( π < ( 2 · π ) ↔ - ( 2 · π ) < - π ) |
| 60 |
23 59
|
mpbi |
⊢ - ( 2 · π ) < - π |
| 61 |
60
|
a1i |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - ( 2 · π ) < - π ) |
| 62 |
|
iccgelb |
⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ ( - π [,] π ) ) → - π ≤ 𝐴 ) |
| 63 |
17 18 11 62
|
syl3anc |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - π ≤ 𝐴 ) |
| 64 |
63
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - π ≤ 𝐴 ) |
| 65 |
57 58 53 61 64
|
ltletrd |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - ( 2 · π ) < 𝐴 ) |
| 66 |
57 53
|
ltnegd |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( - ( 2 · π ) < 𝐴 ↔ - 𝐴 < - - ( 2 · π ) ) ) |
| 67 |
65 66
|
mpbid |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - 𝐴 < - - ( 2 · π ) ) |
| 68 |
16
|
recnd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( 2 · π ) ∈ ℂ ) |
| 69 |
68
|
negnegd |
⊢ ( 𝐴 ∈ ( - π [,] π ) → - - ( 2 · π ) = ( 2 · π ) ) |
| 70 |
69
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - - ( 2 · π ) = ( 2 · π ) ) |
| 71 |
67 70
|
breqtrd |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - 𝐴 < ( 2 · π ) ) |
| 72 |
48 49 51 55 71
|
eliood |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - 𝐴 ∈ ( 0 (,) ( 2 · π ) ) ) |
| 73 |
|
sinaover2ne0 |
⊢ ( - 𝐴 ∈ ( 0 (,) ( 2 · π ) ) → ( sin ‘ ( - 𝐴 / 2 ) ) ≠ 0 ) |
| 74 |
72 73
|
syl |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( sin ‘ ( - 𝐴 / 2 ) ) ≠ 0 ) |
| 75 |
47 74
|
eqnetrd |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → - ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |
| 76 |
75
|
neneqd |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ¬ - ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) |
| 77 |
38
|
sincld |
⊢ ( 𝐴 ∈ ( - π [,] π ) → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ ) |
| 78 |
77
|
adantr |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( sin ‘ ( 𝐴 / 2 ) ) ∈ ℂ ) |
| 79 |
78
|
negeq0d |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( ( sin ‘ ( 𝐴 / 2 ) ) = 0 ↔ - ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) ) |
| 80 |
76 79
|
mtbird |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ¬ ( sin ‘ ( 𝐴 / 2 ) ) = 0 ) |
| 81 |
80
|
neqned |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 < 0 ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |
| 82 |
31 36 81
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) ∧ ¬ 0 < 𝐴 ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |
| 83 |
30 82
|
pm2.61dan |
⊢ ( ( 𝐴 ∈ ( - π [,] π ) ∧ 𝐴 ≠ 0 ) → ( sin ‘ ( 𝐴 / 2 ) ) ≠ 0 ) |