Metamath Proof Explorer

Theorem sineq0ALT

Description: A complex number whose sine is zero is an integer multiple of _pi . The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html . The Metamath form of the proof is sineq0ALT . The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 . 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 https://us.metamath.org/other/completeusersproof/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) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sineq0ALT ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 pire ⊢ π ∈ ℝ
2 pipos ⊢ 0 < π
3 1 2 elrpii ⊢ π ∈ ℝ+
4 2ne0 ⊢ 2 ≠ 0
5 4 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 2 ≠ 0 )
6 2cn ⊢ 2 ∈ ℂ
7 2re ⊢ 2 ∈ ℝ
8 7 a1i ⊢ ( 2 ∈ ℂ → 2 ∈ ℝ )
9 6 8 ax-mp ⊢ 2 ∈ ℝ
10 9 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 2 ∈ ℝ )
11 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
12 11 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℂ )
13 6 a1i ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
14 13 11 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
15 ax-icn ⊢ i ∈ ℂ
16 15 a1i ⊢ ( 𝐴 ∈ ℂ → i ∈ ℂ )
17 13 16 11 mul12d ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( i · 𝐴 ) ) = ( i · ( 2 · 𝐴 ) ) )
18 16 11 mulcld ⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
19 18 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
20 17 19 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
21 20 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) )
22 efadd ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
23 18 18 22 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
24 21 23 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
25 24 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
26 sinval ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
27 id ⊢ ( ( sin ‘ 𝐴 ) = 0 → ( sin ‘ 𝐴 ) = 0 )
28 26 27 sylan9req ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 )
29 efcl ⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
30 18 29 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
31 negicn ⊢ - i ∈ ℂ
32 31 a1i ⊢ ( 𝐴 ∈ ℂ → - i ∈ ℂ )
33 32 11 mulcld ⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
34 efcl ⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
35 33 34 syl ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
36 30 35 subcld ⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
37 2mulicn ⊢ ( 2 · i ) ∈ ℂ
38 37 a1i ⊢ ( 𝐴 ∈ ℂ → ( 2 · i ) ∈ ℂ )
39 2muline0 ⊢ ( 2 · i ) ≠ 0
40 39 a1i ⊢ ( 𝐴 ∈ ℂ → ( 2 · i ) ≠ 0 )
41 36 38 40 diveq0ad ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
42 41 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
43 28 42 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 )
44 30 35 subeq0ad ⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
45 44 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
46 43 45 mpbid ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) )
47 46 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
48 efadd ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( - i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
49 18 33 48 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
50 49 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
51 47 50 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) )
52 16 32 11 adddird ⊢ ( 𝐴 ∈ ℂ → ( ( i + - i ) · 𝐴 ) = ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) )
53 15 negidi ⊢ ( i + - i ) = 0
54 53 oveq1i ⊢ ( ( i + - i ) · 𝐴 ) = ( 0 · 𝐴 )
55 52 54 eqtr3di ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) = ( 0 · 𝐴 ) )
56 11 mul02d ⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )
57 55 56 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) = 0 )
58 57 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( exp ‘ 0 ) )
59 58 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( exp ‘ 0 ) )
60 ef0 ⊢ ( exp ‘ 0 ) = 1
61 60 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ 0 ) = 1 )
62 51 59 61 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = 1 )
63 25 62 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = 1 )
64 63 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) )
65 abs1 ⊢ ( abs ‘ 1 ) = 1
66 64 65 eqtrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 )
67 absefib ⊢ ( ( 2 · 𝐴 ) ∈ ℂ → ( ( 2 · 𝐴 ) ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) )
68 67 biimparc ⊢ ( ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ∧ ( 2 · 𝐴 ) ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℝ )
69 68 ancoms ⊢ ( ( ( 2 · 𝐴 ) ∈ ℂ ∧ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) → ( 2 · 𝐴 ) ∈ ℝ )
70 14 66 69 syl2an2r ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 2 · 𝐴 ) ∈ ℝ )
71 mulre ⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( 2 · 𝐴 ) ∈ ℝ ) )
72 71 4animp1 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℝ ) ∧ 2 ≠ 0 ) ∧ ( 2 · 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ )
73 72 4an31 ⊢ ( ( ( ( 2 ≠ 0 ∧ 2 ∈ ℝ ) ∧ 𝐴 ∈ ℂ ) ∧ ( 2 · 𝐴 ) ∈ ℝ ) → 𝐴 ∈ ℝ )
74 5 10 12 70 73 syl1111anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℝ )
75 3 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → π ∈ ℝ+ )
76 74 75 modcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) ∈ ℝ )
77 76 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) ∈ ℂ )
78 77 sincld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ ( 𝐴 mod π ) ) ∈ ℂ )
79 1 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → π ∈ ℝ )
80 0re ⊢ 0 ∈ ℝ
81 80 1 2 ltleii ⊢ 0 ≤ π
82 gt0ne0 ⊢ ( ( π ∈ ℝ ∧ 0 < π ) → π ≠ 0 )
83 82 3adant3 ⊢ ( ( π ∈ ℝ ∧ 0 < π ∧ 0 ≤ π ) → π ≠ 0 )
84 83 3com23 ⊢ ( ( π ∈ ℝ ∧ 0 ≤ π ∧ 0 < π ) → π ≠ 0 )
85 1 81 2 84 mp3an ⊢ π ≠ 0
86 85 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → π ≠ 0 )
87 74 79 86 redivcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℝ )
88 87 flcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
89 88 znegcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
90 abssinper ⊢ ( ( 𝐴 ∈ ℂ ∧ - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )
91 90 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) )
92 91 ex ⊢ ( 𝐴 ∈ ℂ → ( - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) ) )
93 92 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) ) )
94 89 93 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) )
95 88 zcnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ )
96 95 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ )
97 1 recni ⊢ π ∈ ℂ
98 97 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → π ∈ ℂ )
99 96 98 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ∈ ℂ )
100 98 95 mulcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
101 100 negcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
102 95 98 mulneg1d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
103 95 98 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) )
104 103 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) )
105 102 104 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) )
106 oveq2 ⊢ ( ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) → ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) = ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
107 106 ad3antrrr ⊢ ( ( ( ( ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∧ - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ ) ∧ ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ∈ ℂ ) ∧ 𝐴 ∈ ℂ ) → ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) = ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
108 107 4an4132 ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ∈ ℂ ) ∧ - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ ) ∧ ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) → ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) = ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
109 12 99 101 105 108 syl1111anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) = ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
110 12 100 negsubd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
111 109 110 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
112 111 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) = ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) )
113 112 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) ) )
114 94 113 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) ) )
115 modval ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
116 115 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( sin ‘ ( 𝐴 mod π ) ) = ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) )
117 116 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) ) )
118 3 117 mpan2 ⊢ ( 𝐴 ∈ ℝ → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) ) )
119 74 118 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) ) ) )
120 114 119 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) )
121 27 fveq2d ⊢ ( ( sin ‘ 𝐴 ) = 0 → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ 0 ) )
122 abs0 ⊢ ( abs ‘ 0 ) = 0
123 121 122 eqtrdi ⊢ ( ( sin ‘ 𝐴 ) = 0 → ( abs ‘ ( sin ‘ 𝐴 ) ) = 0 )
124 123 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = 0 )
125 120 124 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = 0 )
126 78 125 abs00d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ ( 𝐴 mod π ) ) = 0 )
127 notnotb ⊢ ( ( sin ‘ ( 𝐴 mod π ) ) = 0 ↔ ¬ ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 )
128 127 bicomi ⊢ ( ¬ ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 ↔ ( sin ‘ ( 𝐴 mod π ) ) = 0 )
129 ltne ⊢ ( ( 0 ∈ ℝ ∧ 0 < ( sin ‘ ( 𝐴 mod π ) ) ) → ( sin ‘ ( 𝐴 mod π ) ) ≠ 0 )
130 129 neneqd ⊢ ( ( 0 ∈ ℝ ∧ 0 < ( sin ‘ ( 𝐴 mod π ) ) ) → ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 )
131 130 expcom ⊢ ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → ( 0 ∈ ℝ → ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 ) )
132 80 131 mpi ⊢ ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 )
133 132 con3i ⊢ ( ¬ ¬ ( sin ‘ ( 𝐴 mod π ) ) = 0 → ¬ 0 < ( sin ‘ ( 𝐴 mod π ) ) )
134 128 133 sylbir ⊢ ( ( sin ‘ ( 𝐴 mod π ) ) = 0 → ¬ 0 < ( sin ‘ ( 𝐴 mod π ) ) )
135 126 134 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ 0 < ( sin ‘ ( 𝐴 mod π ) ) )
136 sinq12gt0 ⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( 𝐴 mod π ) ) )
137 135 136 nsyl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ ( 𝐴 mod π ) ∈ ( 0 (,) π ) )
138 80 rexri ⊢ 0 ∈ ℝ*
139 1 rexri ⊢ π ∈ ℝ*
140 elioo2 ⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ) )
141 138 139 140 mp2an ⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) )
142 141 notbii ⊢ ( ¬ ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ¬ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) )
143 137 142 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) )
144 3anan12 ⊢ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ↔ ( 0 < ( 𝐴 mod π ) ∧ ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ) )
145 144 notbii ⊢ ( ¬ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ↔ ¬ ( 0 < ( 𝐴 mod π ) ∧ ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ) )
146 143 145 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ ( 0 < ( 𝐴 mod π ) ∧ ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ) )
147 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) < π )
148 147 ancoms ⊢ ( ( π ∈ ℝ+ ∧ 𝐴 ∈ ℝ ) → ( 𝐴 mod π ) < π )
149 3 74 148 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) < π )
150 76 149 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) )
151 not12an2impnot1 ⊢ ( ( ¬ ( 0 < ( 𝐴 mod π ) ∧ ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ) ∧ ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ) → ¬ 0 < ( 𝐴 mod π ) )
152 146 150 151 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ 0 < ( 𝐴 mod π ) )
153 modge0 ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod π ) )
154 153 ancoms ⊢ ( ( π ∈ ℝ+ ∧ 𝐴 ∈ ℝ ) → 0 ≤ ( 𝐴 mod π ) )
155 3 74 154 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 ≤ ( 𝐴 mod π ) )
156 leloe ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 mod π ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 mod π ) ↔ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) )
157 156 biimp3a ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 mod π ) ∈ ℝ ∧ 0 ≤ ( 𝐴 mod π ) ) → ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) )
158 157 idiALT ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 mod π ) ∈ ℝ ∧ 0 ≤ ( 𝐴 mod π ) ) → ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) )
159 80 76 155 158 mp3an2i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) )
160 pm2.53 ⊢ ( ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) → ( ¬ 0 < ( 𝐴 mod π ) → 0 = ( 𝐴 mod π ) ) )
161 160 imp ⊢ ( ( ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ∧ ¬ 0 < ( 𝐴 mod π ) ) → 0 = ( 𝐴 mod π ) )
162 161 ancoms ⊢ ( ( ¬ 0 < ( 𝐴 mod π ) ∧ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) → 0 = ( 𝐴 mod π ) )
163 152 159 162 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 = ( 𝐴 mod π ) )
164 163 eqcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = 0 )
165 mod0 ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝐴 mod π ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )
166 165 biimp3a ⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ∧ ( 𝐴 mod π ) = 0 ) → ( 𝐴 / π ) ∈ ℤ )
167 166 3com12 ⊢ ( ( π ∈ ℝ+ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 mod π ) = 0 ) → ( 𝐴 / π ) ∈ ℤ )
168 3 74 164 167 mp3an2i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℤ )
169 168 ex ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 → ( 𝐴 / π ) ∈ ℤ ) )
170 97 a1i ⊢ ( 𝐴 ∈ ℂ → π ∈ ℂ )
171 85 a1i ⊢ ( 𝐴 ∈ ℂ → π ≠ 0 )
172 11 170 171 divcan1d ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / π ) · π ) = 𝐴 )
173 172 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = ( sin ‘ 𝐴 ) )
174 id ⊢ ( ( 𝐴 / π ) ∈ ℤ → ( 𝐴 / π ) ∈ ℤ )
175 sinkpi ⊢ ( ( 𝐴 / π ) ∈ ℤ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = 0 )
176 174 175 syl ⊢ ( ( 𝐴 / π ) ∈ ℤ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = 0 )
177 173 176 sylan9req ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 / π ) ∈ ℤ ) → ( sin ‘ 𝐴 ) = 0 )
178 177 ex ⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / π ) ∈ ℤ → ( sin ‘ 𝐴 ) = 0 ) )
179 169 178 impbid ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )