Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sineq0ALT Structured version   Unicode version

Theorem sineq0ALT 29223
Description: A complex number whose sine is zero is an integer multiple of  pi. The Virtual Deduction form of the proof is http://www.virtualdeduction.com/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 29223. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 20467. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of http://www.virtualdeduction.com/sineq0altro.html is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.)
Assertion
Ref Expression
sineq0ALT  |-  ( A  e.  CC  ->  (
( sin `  A
)  =  0  <->  ( A  /  pi )  e.  ZZ ) )

Proof of Theorem sineq0ALT
StepHypRef Expression
1 pire 20410 . . . . 5  |-  pi  e.  RR
2 pipos 20411 . . . . 5  |-  0  <  pi
31, 2elrpii 10653 . . . 4  |-  pi  e.  RR+
4 2ne0 10121 . . . . . 6  |-  2  =/=  0
54a1i 11 . . . . 5  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
2  =/=  0 )
6 2cn 10108 . . . . . . 7  |-  2  e.  CC
7 2re 10107 . . . . . . . 8  |-  2  e.  RR
87a1i 11 . . . . . . 7  |-  ( 2  e.  CC  ->  2  e.  RR )
96, 8ax-mp 5 . . . . . 6  |-  2  e.  RR
109a1i 11 . . . . 5  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
2  e.  RR )
11 id 21 . . . . . 6  |-  ( A  e.  CC  ->  A  e.  CC )
1211adantr 453 . . . . 5  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  A  e.  CC )
136a1i 11 . . . . . . 7  |-  ( A  e.  CC  ->  2  e.  CC )
1413, 11mulcld 9146 . . . . . 6  |-  ( A  e.  CC  ->  (
2  x.  A )  e.  CC )
15 axicn 9063 . . . . . . . . . . . . . . 15  |-  _i  e.  CC
1615a1i 11 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  _i  e.  CC )
1713, 16, 11mul12d 9313 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
2  x.  ( _i  x.  A ) )  =  ( _i  x.  ( 2  x.  A
) ) )
1816, 11mulcld 9146 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
_i  x.  A )  e.  CC )
19182timesd 10248 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
2  x.  ( _i  x.  A ) )  =  ( ( _i  x.  A )  +  ( _i  x.  A
) ) )
2017, 19eqtr3d 2477 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
_i  x.  ( 2  x.  A ) )  =  ( ( _i  x.  A )  +  ( _i  x.  A
) ) )
2120fveq2d 5767 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  ( exp `  ( _i  x.  ( 2  x.  A
) ) )  =  ( exp `  (
( _i  x.  A
)  +  ( _i  x.  A ) ) ) )
22 efadd 12734 . . . . . . . . . . . 12  |-  ( ( ( _i  x.  A
)  e.  CC  /\  ( _i  x.  A
)  e.  CC )  ->  ( exp `  (
( _i  x.  A
)  +  ( _i  x.  A ) ) )  =  ( ( exp `  ( _i  x.  A ) )  x.  ( exp `  (
_i  x.  A )
) ) )
2318, 18, 22syl2anc 644 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  ( exp `  ( ( _i  x.  A )  +  ( _i  x.  A
) ) )  =  ( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( _i  x.  A
) ) ) )
2421, 23eqtrd 2475 . . . . . . . . . 10  |-  ( A  e.  CC  ->  ( exp `  ( _i  x.  ( 2  x.  A
) ) )  =  ( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( _i  x.  A
) ) ) )
2524adantr 453 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  (
_i  x.  ( 2  x.  A ) ) )  =  ( ( exp `  ( _i  x.  A ) )  x.  ( exp `  (
_i  x.  A )
) ) )
26 sinval 12761 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  ( sin `  A )  =  ( ( ( exp `  ( _i  x.  A
) )  -  ( exp `  ( -u _i  x.  A ) ) )  /  ( 2  x.  _i ) ) )
27 id 21 . . . . . . . . . . . . . . 15  |-  ( ( sin `  A )  =  0  ->  ( sin `  A )  =  0 )
2826, 27sylan9req 2496 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( ( exp `  ( _i  x.  A
) )  -  ( exp `  ( -u _i  x.  A ) ) )  /  ( 2  x.  _i ) )  =  0 )
29 efcl 12723 . . . . . . . . . . . . . . . . . 18  |-  ( ( _i  x.  A )  e.  CC  ->  ( exp `  ( _i  x.  A ) )  e.  CC )
3018, 29syl 16 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  ( exp `  ( _i  x.  A ) )  e.  CC )
3115negcli 9406 . . . . . . . . . . . . . . . . . . . 20  |-  -u _i  e.  CC
3231a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  CC  ->  -u _i  e.  CC )
3332, 11mulcld 9146 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  CC  ->  ( -u _i  x.  A )  e.  CC )
34 efcl 12723 . . . . . . . . . . . . . . . . . 18  |-  ( (
-u _i  x.  A
)  e.  CC  ->  ( exp `  ( -u _i  x.  A ) )  e.  CC )
3533, 34syl 16 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  ( exp `  ( -u _i  x.  A ) )  e.  CC )
3630, 35subcld 9449 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
( exp `  (
_i  x.  A )
)  -  ( exp `  ( -u _i  x.  A ) ) )  e.  CC )
376, 15mulcli 9133 . . . . . . . . . . . . . . . . 17  |-  ( 2  x.  _i )  e.  CC
3837a1i 11 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
2  x.  _i )  e.  CC )
39 ine0 9507 . . . . . . . . . . . . . . . . . 18  |-  _i  =/=  0
406, 15, 4, 39mulne0i 9703 . . . . . . . . . . . . . . . . 17  |-  ( 2  x.  _i )  =/=  0
4140a1i 11 . . . . . . . . . . . . . . . 16  |-  ( A  e.  CC  ->  (
2  x.  _i )  =/=  0 )
4236, 38, 41diveq0ad 9838 . . . . . . . . . . . . . . 15  |-  ( A  e.  CC  ->  (
( ( ( exp `  ( _i  x.  A
) )  -  ( exp `  ( -u _i  x.  A ) ) )  /  ( 2  x.  _i ) )  =  0  <->  ( ( exp `  ( _i  x.  A
) )  -  ( exp `  ( -u _i  x.  A ) ) )  =  0 ) )
4342adantr 453 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( ( ( exp `  ( _i  x.  A ) )  -  ( exp `  ( -u _i  x.  A ) ) )  /  (
2  x.  _i ) )  =  0  <->  (
( exp `  (
_i  x.  A )
)  -  ( exp `  ( -u _i  x.  A ) ) )  =  0 ) )
4428, 43mpbid 203 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( exp `  (
_i  x.  A )
)  -  ( exp `  ( -u _i  x.  A ) ) )  =  0 )
4530, 35subeq0ad 9459 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
( ( exp `  (
_i  x.  A )
)  -  ( exp `  ( -u _i  x.  A ) ) )  =  0  <->  ( exp `  ( _i  x.  A
) )  =  ( exp `  ( -u _i  x.  A ) ) ) )
4645adantr 453 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( ( exp `  ( _i  x.  A
) )  -  ( exp `  ( -u _i  x.  A ) ) )  =  0  <->  ( exp `  ( _i  x.  A
) )  =  ( exp `  ( -u _i  x.  A ) ) ) )
4744, 46mpbid 203 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  (
_i  x.  A )
)  =  ( exp `  ( -u _i  x.  A ) ) )
4847oveq2d 6133 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( _i  x.  A
) ) )  =  ( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( -u _i  x.  A ) ) ) )
49 efadd 12734 . . . . . . . . . . . . 13  |-  ( ( ( _i  x.  A
)  e.  CC  /\  ( -u _i  x.  A
)  e.  CC )  ->  ( exp `  (
( _i  x.  A
)  +  ( -u _i  x.  A ) ) )  =  ( ( exp `  ( _i  x.  A ) )  x.  ( exp `  ( -u _i  x.  A ) ) ) )
5018, 33, 49syl2anc 644 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  ( exp `  ( ( _i  x.  A )  +  ( -u _i  x.  A ) ) )  =  ( ( exp `  ( _i  x.  A
) )  x.  ( exp `  ( -u _i  x.  A ) ) ) )
5150adantr 453 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  (
( _i  x.  A
)  +  ( -u _i  x.  A ) ) )  =  ( ( exp `  ( _i  x.  A ) )  x.  ( exp `  ( -u _i  x.  A ) ) ) )
5248, 51eqtr4d 2478 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( _i  x.  A
) ) )  =  ( exp `  (
( _i  x.  A
)  +  ( -u _i  x.  A ) ) ) )
5315negidi 9407 . . . . . . . . . . . . . . 15  |-  ( _i  +  -u _i )  =  0
5453oveq1i 6127 . . . . . . . . . . . . . 14  |-  ( ( _i  +  -u _i )  x.  A )  =  ( 0  x.  A )
5516, 32, 11adddird 9151 . . . . . . . . . . . . . 14  |-  ( A  e.  CC  ->  (
( _i  +  -u _i )  x.  A
)  =  ( ( _i  x.  A )  +  ( -u _i  x.  A ) ) )
5654, 55syl5reqr 2490 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
( _i  x.  A
)  +  ( -u _i  x.  A ) )  =  ( 0  x.  A ) )
5711mul02d 9302 . . . . . . . . . . . . 13  |-  ( A  e.  CC  ->  (
0  x.  A )  =  0 )
5856, 57eqtrd 2475 . . . . . . . . . . . 12  |-  ( A  e.  CC  ->  (
( _i  x.  A
)  +  ( -u _i  x.  A ) )  =  0 )
5958fveq2d 5767 . . . . . . . . . . 11  |-  ( A  e.  CC  ->  ( exp `  ( ( _i  x.  A )  +  ( -u _i  x.  A ) ) )  =  ( exp `  0
) )
6059adantr 453 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  (
( _i  x.  A
)  +  ( -u _i  x.  A ) ) )  =  ( exp `  0 ) )
61 ef0 12731 . . . . . . . . . . 11  |-  ( exp `  0 )  =  1
6261a1i 11 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  0
)  =  1 )
6352, 60, 623eqtrd 2479 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( exp `  (
_i  x.  A )
)  x.  ( exp `  ( _i  x.  A
) ) )  =  1 )
6425, 63eqtrd 2475 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( exp `  (
_i  x.  ( 2  x.  A ) ) )  =  1 )
6564fveq2d 5767 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( exp `  ( _i  x.  ( 2  x.  A
) ) ) )  =  ( abs `  1
) )
66 abs1 12140 . . . . . . 7  |-  ( abs `  1 )  =  1
6765, 66syl6eq 2491 . . . . . 6  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( exp `  ( _i  x.  ( 2  x.  A
) ) ) )  =  1 )
68 absefib 12837 . . . . . . . 8  |-  ( ( 2  x.  A )  e.  CC  ->  (
( 2  x.  A
)  e.  RR  <->  ( abs `  ( exp `  (
_i  x.  ( 2  x.  A ) ) ) )  =  1 ) )
6968biimparc 475 . . . . . . 7  |-  ( ( ( abs `  ( exp `  ( _i  x.  ( 2  x.  A
) ) ) )  =  1  /\  (
2  x.  A )  e.  CC )  -> 
( 2  x.  A
)  e.  RR )
7069ancoms 441 . . . . . 6  |-  ( ( ( 2  x.  A
)  e.  CC  /\  ( abs `  ( exp `  ( _i  x.  (
2  x.  A ) ) ) )  =  1 )  ->  (
2  x.  A )  e.  RR )
7114, 67, 70eel121 28992 . . . . 5  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( 2  x.  A
)  e.  RR )
72 mulre 11964 . . . . . . 7  |-  ( ( A  e.  CC  /\  2  e.  RR  /\  2  =/=  0 )  ->  ( A  e.  RR  <->  ( 2  x.  A )  e.  RR ) )
73724animp1 28752 . . . . . 6  |-  ( ( ( ( A  e.  CC  /\  2  e.  RR )  /\  2  =/=  0 )  /\  (
2  x.  A )  e.  RR )  ->  A  e.  RR )
74734an31 28753 . . . . 5  |-  ( ( ( ( 2  =/=  0  /\  2  e.  RR )  /\  A  e.  CC )  /\  (
2  x.  A )  e.  RR )  ->  A  e.  RR )
755, 10, 12, 71, 74eel1111 29004 . . . 4  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  A  e.  RR )
763a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  pi  e.  RR+ )
7775, 76modcld 11292 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  mod  pi )  e.  RR )
7877recnd 9152 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  mod  pi )  e.  CC )
7978sincld 12769 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( sin `  ( A  mod  pi ) )  e.  CC )
801a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  pi  e.  RR )
81 0re 9129 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  RR
8281, 1, 2ltleii 9234 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <_  pi
83 gt0ne0 9531 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( pi  e.  RR  /\  0  <  pi )  ->  pi  =/=  0 )
84833adant3 978 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( pi  e.  RR  /\  0  <  pi  /\  0  <_  pi )  ->  pi  =/=  0 )
85843com23 1160 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( pi  e.  RR  /\  0  <_  pi  /\  0  <  pi )  ->  pi  =/=  0 )
861, 82, 2, 85mp3an 1280 . . . . . . . . . . . . . . . . . . . 20  |-  pi  =/=  0
8786a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  pi  =/=  0 )
8875, 80, 87redivcld 9880 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  /  pi )  e.  RR )
8988flcld 11245 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( |_ `  ( A  /  pi ) )  e.  ZZ )
9089znegcld 10415 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -u ( |_ `  ( A  /  pi ) )  e.  ZZ )
91 abssinper 20464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  -u ( |_ `  ( A  /  pi ) )  e.  ZZ )  -> 
( abs `  ( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) )  =  ( abs `  ( sin `  A ) ) )
9291eqcomd 2448 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  -u ( |_ `  ( A  /  pi ) )  e.  ZZ )  -> 
( abs `  ( sin `  A ) )  =  ( abs `  ( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) ) )
9392ex 425 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  CC  ->  ( -u ( |_ `  ( A  /  pi ) )  e.  ZZ  ->  ( abs `  ( sin `  A
) )  =  ( abs `  ( sin `  ( A  +  (
-u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) ) ) )
9493adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( -u ( |_ `  ( A  /  pi ) )  e.  ZZ  ->  ( abs `  ( sin `  A ) )  =  ( abs `  ( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) ) ) )
9590, 94mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  A ) )  =  ( abs `  ( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) ) )
9689zcnd 10414 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( |_ `  ( A  /  pi ) )  e.  CC )
9796negcld 9436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -u ( |_ `  ( A  /  pi ) )  e.  CC )
981recni 9140 . . . . . . . . . . . . . . . . . . . . 21  |-  pi  e.  CC
9998a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  pi  e.  CC )
10097, 99mulcld 9146 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( -u ( |_ `  ( A  /  pi ) )  x.  pi )  e.  CC )
10199, 96mulcld 9146 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( pi  x.  ( |_ `  ( A  /  pi ) ) )  e.  CC )
102101negcld 9436 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -u ( pi  x.  ( |_ `  ( A  /  pi ) ) )  e.  CC )
10396, 99mulneg1d 9524 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( -u ( |_ `  ( A  /  pi ) )  x.  pi )  =  -u ( ( |_ `  ( A  /  pi ) )  x.  pi ) )
10496, 99mulcomd 9147 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( |_ `  ( A  /  pi ) )  x.  pi )  =  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) )
105104negeqd 9338 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -u ( ( |_ `  ( A  /  pi ) )  x.  pi )  =  -u ( pi  x.  ( |_ `  ( A  /  pi ) ) ) )
106103, 105eqtrd 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( -u ( |_ `  ( A  /  pi ) )  x.  pi )  =  -u ( pi  x.  ( |_ `  ( A  /  pi ) ) ) )
107 oveq2 6125 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
-u ( |_ `  ( A  /  pi ) )  x.  pi )  =  -u ( pi  x.  ( |_ `  ( A  /  pi ) ) )  -> 
( A  +  (
-u ( |_ `  ( A  /  pi ) )  x.  pi ) )  =  ( A  +  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
108107ad3antrrr 712 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( -u ( |_ `  ( A  /  pi ) )  x.  pi )  = 
-u ( pi  x.  ( |_ `  ( A  /  pi ) ) )  /\  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) )  e.  CC )  /\  ( -u ( |_ `  ( A  /  pi ) )  x.  pi )  e.  CC )  /\  A  e.  CC )  ->  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) )  =  ( A  +  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
1091084an4132 28754 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( A  e.  CC  /\  ( -u ( |_ `  ( A  /  pi ) )  x.  pi )  e.  CC )  /\  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) )  e.  CC )  /\  ( -u ( |_ `  ( A  /  pi ) )  x.  pi )  = 
-u ( pi  x.  ( |_ `  ( A  /  pi ) ) ) )  ->  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) )  =  ( A  +  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
11012, 100, 102, 106, 109eel1111 29004 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  +  (
-u ( |_ `  ( A  /  pi ) )  x.  pi ) )  =  ( A  +  -u (
pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
11112, 101negsubd 9455 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  +  -u ( pi  x.  ( |_ `  ( A  /  pi ) ) ) )  =  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
112110, 111eqtrd 2475 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  +  (
-u ( |_ `  ( A  /  pi ) )  x.  pi ) )  =  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
113112fveq2d 5767 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) )  =  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) )
114113fveq2d 5767 . . . . . . . . . . . . . . 15  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  ( A  +  ( -u ( |_ `  ( A  /  pi ) )  x.  pi ) ) ) )  =  ( abs `  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) ) )
11595, 114eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  A ) )  =  ( abs `  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) ) )
116 modval 11290 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  ( A  mod  pi )  =  ( A  -  (
pi  x.  ( |_ `  ( A  /  pi ) ) ) ) )
117116fveq2d 5767 . . . . . . . . . . . . . . . . 17  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  ( sin `  ( A  mod  pi ) )  =  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) )
118117fveq2d 5767 . . . . . . . . . . . . . . . 16  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  ( abs `  ( sin `  ( A  mod  pi ) ) )  =  ( abs `  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) ) )
1193, 118mpan2 654 . . . . . . . . . . . . . . 15  |-  ( A  e.  RR  ->  ( abs `  ( sin `  ( A  mod  pi ) ) )  =  ( abs `  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) ) )
12075, 119syl 16 . . . . . . . . . . . . . 14  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  ( A  mod  pi ) ) )  =  ( abs `  ( sin `  ( A  -  ( pi  x.  ( |_ `  ( A  /  pi ) ) ) ) ) ) )
121115, 120eqtr4d 2478 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  A ) )  =  ( abs `  ( sin `  ( A  mod  pi ) ) ) )
12227fveq2d 5767 . . . . . . . . . . . . . . 15  |-  ( ( sin `  A )  =  0  ->  ( abs `  ( sin `  A
) )  =  ( abs `  0 ) )
123 abs0 12128 . . . . . . . . . . . . . . 15  |-  ( abs `  0 )  =  0
124122, 123syl6eq 2491 . . . . . . . . . . . . . 14  |-  ( ( sin `  A )  =  0  ->  ( abs `  ( sin `  A
) )  =  0 )
125124adantl 454 . . . . . . . . . . . . 13  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  A ) )  =  0 )
126121, 125eqtr3d 2477 . . . . . . . . . . . 12  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( abs `  ( sin `  ( A  mod  pi ) ) )  =  0 )
12779, 126abs00d 12286 . . . . . . . . . . 11  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( sin `  ( A  mod  pi ) )  =  0 )
128 notnot 284 . . . . . . . . . . . . 13  |-  ( ( sin `  ( A  mod  pi ) )  =  0  <->  -.  -.  ( sin `  ( A  mod  pi ) )  =  0 )
129128bicomi 195 . . . . . . . . . . . 12  |-  ( -. 
-.  ( sin `  ( A  mod  pi ) )  =  0  <->  ( sin `  ( A  mod  pi ) )  =  0 )
130 ltne 9208 . . . . . . . . . . . . . . . 16  |-  ( ( 0  e.  RR  /\  0  <  ( sin `  ( A  mod  pi ) ) )  ->  ( sin `  ( A  mod  pi ) )  =/=  0
)
131130neneqd 2624 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  0  <  ( sin `  ( A  mod  pi ) ) )  ->  -.  ( sin `  ( A  mod  pi ) )  =  0 )
132131expcom 426 . . . . . . . . . . . . . 14  |-  ( 0  <  ( sin `  ( A  mod  pi ) )  ->  ( 0  e.  RR  ->  -.  ( sin `  ( A  mod  pi ) )  =  0 ) )
13381, 132mpi 17 . . . . . . . . . . . . 13  |-  ( 0  <  ( sin `  ( A  mod  pi ) )  ->  -.  ( sin `  ( A  mod  pi ) )  =  0 )
134133con3i 130 . . . . . . . . . . . 12  |-  ( -. 
-.  ( sin `  ( A  mod  pi ) )  =  0  ->  -.  0  <  ( sin `  ( A  mod  pi ) ) )
135129, 134sylbir 206 . . . . . . . . . . 11  |-  ( ( sin `  ( A  mod  pi ) )  =  0  ->  -.  0  <  ( sin `  ( A  mod  pi ) ) )
136127, 135syl 16 . . . . . . . . . 10  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -.  0  <  ( sin `  ( A  mod  pi ) ) )
137 sinq12gt0 20453 . . . . . . . . . 10  |-  ( ( A  mod  pi )  e.  ( 0 (,) pi )  ->  0  <  ( sin `  ( A  mod  pi ) ) )
138136, 137nsyl 116 . . . . . . . . 9  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -.  ( A  mod  pi )  e.  ( 0 (,) pi ) )
13981rexri 9175 . . . . . . . . . . 11  |-  0  e.  RR*
1401rexri 9175 . . . . . . . . . . 11  |-  pi  e.  RR*
141 elioo2 10995 . . . . . . . . . . 11  |-  ( ( 0  e.  RR*  /\  pi  e.  RR* )  ->  (
( A  mod  pi )  e.  ( 0 (,) pi )  <->  ( ( A  mod  pi )  e.  RR  /\  0  < 
( A  mod  pi )  /\  ( A  mod  pi )  <  pi ) ) )
142139, 140, 141mp2an 655 . . . . . . . . . 10  |-  ( ( A  mod  pi )  e.  ( 0 (,) pi )  <->  ( ( A  mod  pi )  e.  RR  /\  0  < 
( A  mod  pi )  /\  ( A  mod  pi )  <  pi ) )
143142notbii 289 . . . . . . . . 9  |-  ( -.  ( A  mod  pi )  e.  ( 0 (,) pi )  <->  -.  (
( A  mod  pi )  e.  RR  /\  0  <  ( A  mod  pi )  /\  ( A  mod  pi )  <  pi ) )
144138, 143sylib 190 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -.  ( ( A  mod  pi )  e.  RR  /\  0  <  ( A  mod  pi )  /\  ( A  mod  pi )  <  pi ) )
145 3anan12 950 . . . . . . . . 9  |-  ( ( ( A  mod  pi )  e.  RR  /\  0  <  ( A  mod  pi )  /\  ( A  mod  pi )  <  pi )  <-> 
( 0  <  ( A  mod  pi )  /\  ( ( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  <  pi ) ) )
146145notbii 289 . . . . . . . 8  |-  ( -.  ( ( A  mod  pi )  e.  RR  /\  0  <  ( A  mod  pi )  /\  ( A  mod  pi )  <  pi )  <->  -.  (
0  <  ( A  mod  pi )  /\  (
( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  < 
pi ) ) )
147144, 146sylib 190 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -.  ( 0  <  ( A  mod  pi )  /\  ( ( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  <  pi ) ) )
148 modlt 11296 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  ( A  mod  pi )  < 
pi )
149148ancoms 441 . . . . . . . . 9  |-  ( ( pi  e.  RR+  /\  A  e.  RR )  ->  ( A  mod  pi )  < 
pi )
1503, 75, 149sylancr 646 . . . . . . . 8  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  mod  pi )  <  pi )
15177, 150jca 520 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( ( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  <  pi ) )
152 not12an2impnot1 28831 . . . . . . 7  |-  ( ( -.  ( 0  < 
( A  mod  pi )  /\  ( ( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  < 
pi ) )  /\  ( ( A  mod  pi )  e.  RR  /\  ( A  mod  pi )  <  pi ) )  ->  -.  0  <  ( A  mod  pi ) )
153147, 151, 152syl2anc 644 . . . . . 6  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  ->  -.  0  <  ( A  mod  pi ) )
154 modge0 11295 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  0  <_  ( A  mod  pi ) )
155154ancoms 441 . . . . . . . 8  |-  ( ( pi  e.  RR+  /\  A  e.  RR )  ->  0  <_  ( A  mod  pi ) )
1563, 75, 155sylancr 646 . . . . . . 7  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
0  <_  ( A  mod  pi ) )
157 leloe 9199 . . . . . . . . 9  |-  ( ( 0  e.  RR  /\  ( A  mod  pi )  e.  RR )  -> 
( 0  <_  ( A  mod  pi )  <->  ( 0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) ) ) )
158157biimp3a 1284 . . . . . . . 8  |-  ( ( 0  e.  RR  /\  ( A  mod  pi )  e.  RR  /\  0  <_  ( A  mod  pi ) )  ->  (
0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) ) )
159158idi 2 . . . . . . 7  |-  ( ( 0  e.  RR  /\  ( A  mod  pi )  e.  RR  /\  0  <_  ( A  mod  pi ) )  ->  (
0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) ) )
16081, 77, 156, 159eel011 28982 . . . . . 6  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( 0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) ) )
161 pm2.53 364 . . . . . . . 8  |-  ( ( 0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) )  ->  ( -.  0  <  ( A  mod  pi )  ->  0  =  ( A  mod  pi ) ) )
162161imp 420 . . . . . . 7  |-  ( ( ( 0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) )  /\  -.  0  < 
( A  mod  pi ) )  ->  0  =  ( A  mod  pi ) )
163162ancoms 441 . . . . . 6  |-  ( ( -.  0  <  ( A  mod  pi )  /\  ( 0  <  ( A  mod  pi )  \/  0  =  ( A  mod  pi ) ) )  ->  0  =  ( A  mod  pi ) )
164153, 160, 163syl2anc 644 . . . . 5  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
0  =  ( A  mod  pi ) )
165164eqcomd 2448 . . . 4  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  mod  pi )  =  0 )
166 mod0 11293 . . . . . 6  |-  ( ( A  e.  RR  /\  pi  e.  RR+ )  ->  (
( A  mod  pi )  =  0  <->  ( A  /  pi )  e.  ZZ ) )
167166biimp3a 1284 . . . . 5  |-  ( ( A  e.  RR  /\  pi  e.  RR+  /\  ( A  mod  pi )  =  0 )  ->  ( A  /  pi )  e.  ZZ )
1681673com12 1158 . . . 4  |-  ( ( pi  e.  RR+  /\  A  e.  RR  /\  ( A  mod  pi )  =  0 )  ->  ( A  /  pi )  e.  ZZ )
1693, 75, 165, 168eel011 28982 . . 3  |-  ( ( A  e.  CC  /\  ( sin `  A )  =  0 )  -> 
( A  /  pi )  e.  ZZ )
170169ex 425 . 2  |-  ( A  e.  CC  ->  (
( sin `  A
)  =  0  -> 
( A  /  pi )  e.  ZZ )
)
17198a1i 11 . . . . . 6  |-  ( A  e.  CC  ->  pi  e.  CC )
17286a1i 11 . . . . . 6  |-  ( A  e.  CC  ->  pi  =/=  0 )
17311, 171, 172divcan1d 9829 . . . . 5  |-  ( A  e.  CC  ->  (
( A  /  pi )  x.  pi )  =  A )
174173fveq2d 5767 . . . 4  |-  ( A  e.  CC  ->  ( sin `  ( ( A  /  pi )  x.  pi ) )  =  ( sin `  A
) )
175 id 21 . . . . 5  |-  ( ( A  /  pi )  e.  ZZ  ->  ( A  /  pi )  e.  ZZ )
176 sinkpi 20465 . . . . 5  |-  ( ( A  /  pi )  e.  ZZ  ->  ( sin `  ( ( A  /  pi )  x.  pi ) )  =  0 )
177175, 176syl 16 . . . 4  |-  ( ( A  /  pi )  e.  ZZ  ->  ( sin `  ( ( A  /  pi )  x.  pi ) )  =  0 )
178174, 177sylan9req 2496 . . 3  |-  ( ( A  e.  CC  /\  ( A  /  pi )  e.  ZZ )  ->  ( sin `  A
)  =  0 )
179178ex 425 . 2  |-  ( A  e.  CC  ->  (
( A  /  pi )  e.  ZZ  ->  ( sin `  A )  =  0 ) )
180170, 179impbid 185 1  |-  ( A  e.  CC  ->  (
( sin `  A
)  =  0  <->  ( A  /  pi )  e.  ZZ ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    \/ wo 359    /\ wa 360    /\ w3a 937    = wceq 1654    e. wcel 1728    =/= wne 2606   class class class wbr 4243   ` cfv 5489  (class class class)co 6117   CCcc 9026   RRcr 9027   0cc0 9028   1c1 9029   _ici 9030    + caddc 9031    x. cmul 9033   RR*cxr 9157    < clt 9158    <_ cle 9159    - cmin 9329   -ucneg 9330    / cdiv 9715   2c2 10087   ZZcz 10320   RR+crp 10650   (,)cioo 10954   |_cfl 11239    mod cmo 11288   abscabs 12077   expce 12702   sincsin 12704   picpi 12707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4351  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-un 4736  ax-inf2 7632  ax-cnex 9084  ax-resscn 9085  ax-1cn 9086  ax-icn 9087  ax-addcl 9088  ax-addrcl 9089  ax-mulcl 9090  ax-mulrcl 9091  ax-mulcom 9092  ax-addass 9093  ax-mulass 9094  ax-distr 9095  ax-i2m1 9096  ax-1ne0 9097  ax-1rid 9098  ax-rnegex 9099  ax-rrecex 9100  ax-cnre 9101  ax-pre-lttri 9102  ax-pre-lttrn 9103  ax-pre-ltadd 9104  ax-pre-mulgt0 9105  ax-pre-sup 9106  ax-addf 9107  ax-mulf 9108
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-fal 1330  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-tp 3851  df-op 3852  df-uni 4045  df-int 4080  df-iun 4124  df-iin 4125  df-br 4244  df-opab 4298  df-mpt 4299  df-tr 4334  df-eprel 4529  df-id 4533  df-po 4538  df-so 4539  df-fr 4576  df-se 4577  df-we 4578  df-ord 4619  df-on 4620  df-lim 4621  df-suc 4622  df-om 4881  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-f1 5494  df-fo 5495  df-f1o 5496  df-fv 5497  df-isom 5498  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-of 6341  df-1st 6385  df-2nd 6386  df-riota 6585  df-recs 6669  df-rdg 6704  df-1o 6760  df-2o 6761  df-oadd 6764  df-omul 6765  df-er 6941  df-ec 6943  df-qs 6947  df-map 7056  df-pm 7057  df-ixp 7100  df-en 7146  df-dom 7147  df-sdom 7148  df-fin 7149  df-fi 7452  df-sup 7482  df-oi 7515  df-card 7864  df-cda 8086  df-ni 8787  df-pli 8788  df-mi 8789  df-lti 8790  df-plpq 8823  df-mpq 8824  df-ltpq 8825  df-enq 8826  df-nq 8827  df-erq 8828  df-plq 8829  df-mq 8830  df-1nq 8831  df-rq 8832  df-ltnq 8833  df-np 8896  df-1p 8897  df-plp 8898  df-enr 8972  df-nr 8973  df-0r 8977  df-1r 8978  df-c 9034  df-i 9037  df-pnf 9160  df-mnf 9161  df-xr 9162  df-ltxr 9163  df-le 9164  df-sub 9331  df-neg 9332  df-div 9716  df-nn 10039  df-2 10096  df-3 10097  df-4 10098  df-5 10099  df-6 10100  df-7 10101  df-8 10102  df-9 10103  df-10 10104  df-n0 10260  df-z 10321  df-dec 10421  df-uz 10527  df-q 10613  df-rp 10651  df-xneg 10748  df-xadd 10749  df-xmul 10750  df-ioo 10958  df-ioc 10959  df-ico 10960  df-icc 10961  df-fz 11082  df-fzo 11174  df-fl 11240  df-mod 11289  df-seq 11362  df-exp 11421  df-fac 11605  df-bc 11632  df-hash 11657  df-shft 11920  df-cj 11942  df-re 11943  df-im 11944  df-sqr 12078  df-abs 12079  df-limsup 12303  df-clim 12320  df-rlim 12321  df-sum 12518  df-ef 12708  df-sin 12710  df-cos 12711  df-pi 12713  df-struct 13509  df-ndx 13510  df-slot 13511  df-base 13512  df-sets 13513  df-ress 13514  df-plusg 13580  df-mulr 13581  df-starv 13582  df-sca 13583  df-vsca 13584  df-tset 13586  df-ple 13587  df-ds 13589  df-unif 13590  df-hom 13591  df-cco 13592  df-rest 13688  df-topn 13689  df-topgen 13705  df-pt 13706  df-prds 13709  df-xrs 13764  df-0g 13765  df-gsum 13766  df-qtop 13771  df-imas 13772  df-xps 13774  df-mre 13849  df-mrc 13850  df-acs 13852  df-mnd 14728  df-submnd 14777  df-mulg 14853  df-cntz 15154  df-cmn 15452  df-psmet 16732  df-xmet 16733  df-met 16734  df-bl 16735  df-mopn 16736  df-fbas 16737  df-fg 16738  df-cnfld 16742  df-top 17001  df-bases 17003  df-topon 17004  df-topsp 17005  df-cld 17121  df-ntr 17122  df-cls 17123  df-nei 17200  df-lp 17238  df-perf 17239  df-cn 17329  df-cnp 17330  df-haus 17417  df-tx 17632  df-hmeo 17825  df-fil 17916  df-fm 18008  df-flim 18009  df-flf 18010  df-xms 18388  df-ms 18389  df-tms 18390  df-cncf 18946  df-limc 19791  df-dv 19792
  Copyright terms: Public domain W3C validator