Step |
Hyp |
Ref |
Expression |
1 |
|
picn |
|- _pi e. CC |
2 |
1
|
a1i |
|- ( A e. CC -> _pi e. CC ) |
3 |
2
|
halfcld |
|- ( A e. CC -> ( _pi / 2 ) e. CC ) |
4 |
|
id |
|- ( A e. CC -> A e. CC ) |
5 |
3 4
|
addcld |
|- ( A e. CC -> ( ( _pi / 2 ) + A ) e. CC ) |
6 |
|
sineq0 |
|- ( ( ( _pi / 2 ) + A ) e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ ) ) |
7 |
5 6
|
syl |
|- ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ ) ) |
8 |
|
sinhalfpip |
|- ( A e. CC -> ( sin ` ( ( _pi / 2 ) + A ) ) = ( cos ` A ) ) |
9 |
8
|
eqeq1d |
|- ( A e. CC -> ( ( sin ` ( ( _pi / 2 ) + A ) ) = 0 <-> ( cos ` A ) = 0 ) ) |
10 |
|
pire |
|- _pi e. RR |
11 |
|
pipos |
|- 0 < _pi |
12 |
10 11
|
gt0ne0ii |
|- _pi =/= 0 |
13 |
12
|
a1i |
|- ( A e. CC -> _pi =/= 0 ) |
14 |
3 4 2 13
|
divdird |
|- ( A e. CC -> ( ( ( _pi / 2 ) + A ) / _pi ) = ( ( ( _pi / 2 ) / _pi ) + ( A / _pi ) ) ) |
15 |
|
2cnd |
|- ( A e. CC -> 2 e. CC ) |
16 |
|
2ne0 |
|- 2 =/= 0 |
17 |
16
|
a1i |
|- ( A e. CC -> 2 =/= 0 ) |
18 |
2 15 2 17 13
|
divdiv32d |
|- ( A e. CC -> ( ( _pi / 2 ) / _pi ) = ( ( _pi / _pi ) / 2 ) ) |
19 |
2 13
|
dividd |
|- ( A e. CC -> ( _pi / _pi ) = 1 ) |
20 |
19
|
oveq1d |
|- ( A e. CC -> ( ( _pi / _pi ) / 2 ) = ( 1 / 2 ) ) |
21 |
18 20
|
eqtrd |
|- ( A e. CC -> ( ( _pi / 2 ) / _pi ) = ( 1 / 2 ) ) |
22 |
21
|
oveq1d |
|- ( A e. CC -> ( ( ( _pi / 2 ) / _pi ) + ( A / _pi ) ) = ( ( 1 / 2 ) + ( A / _pi ) ) ) |
23 |
|
1cnd |
|- ( A e. CC -> 1 e. CC ) |
24 |
23
|
halfcld |
|- ( A e. CC -> ( 1 / 2 ) e. CC ) |
25 |
4 2 13
|
divcld |
|- ( A e. CC -> ( A / _pi ) e. CC ) |
26 |
24 25
|
addcomd |
|- ( A e. CC -> ( ( 1 / 2 ) + ( A / _pi ) ) = ( ( A / _pi ) + ( 1 / 2 ) ) ) |
27 |
14 22 26
|
3eqtrd |
|- ( A e. CC -> ( ( ( _pi / 2 ) + A ) / _pi ) = ( ( A / _pi ) + ( 1 / 2 ) ) ) |
28 |
27
|
eleq1d |
|- ( A e. CC -> ( ( ( ( _pi / 2 ) + A ) / _pi ) e. ZZ <-> ( ( A / _pi ) + ( 1 / 2 ) ) e. ZZ ) ) |
29 |
7 9 28
|
3bitr3d |
|- ( A e. CC -> ( ( cos ` A ) = 0 <-> ( ( A / _pi ) + ( 1 / 2 ) ) e. ZZ ) ) |