Theorem sineq0

Description: A complex number whose sine is zero is an integer multiple of _pi . (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 10-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		sinval	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) = ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) )
2	1	eqeq1d	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ) )
3		ax-icn	⊢ i ∈ ℂ
4		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
5	3 4	mpan	⊢ ( 𝐴 ∈ ℂ → ( i · 𝐴 ) ∈ ℂ )
6		efcl	⊢ ( ( i · 𝐴 ) ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
7	5 6	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · 𝐴 ) ) ∈ ℂ )
8		negicn	⊢ - i ∈ ℂ
9		mulcl	⊢ ( ( - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( - i · 𝐴 ) ∈ ℂ )
10	8 9	mpan	⊢ ( 𝐴 ∈ ℂ → ( - i · 𝐴 ) ∈ ℂ )
11		efcl	⊢ ( ( - i · 𝐴 ) ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
12	10 11	syl	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( - i · 𝐴 ) ) ∈ ℂ )
13	7 12	subcld	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ )
14		2mulicn	⊢ ( 2 · i ) ∈ ℂ
15		2muline0	⊢ ( 2 · i ) ≠ 0
16		diveq0	⊢ ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
17	14 15 16	mp3an23	⊢ ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
18	13 17	syl	⊢ ( 𝐴 ∈ ℂ → ( ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) / ( 2 · i ) ) = 0 ↔ ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ) )
19	7 12	subeq0ad	⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) − ( exp ‘ ( - i · 𝐴 ) ) ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
20	2 18 19	3bitrd	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) ) )
21		oveq2	⊢ ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
22		2cn	⊢ 2 ∈ ℂ
23		mul12	⊢ ( ( i ∈ ℂ ∧ 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · ( 2 · 𝐴 ) ) = ( 2 · ( i · 𝐴 ) ) )
24	3 22 23	mp3an12	⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · 𝐴 ) ) = ( 2 · ( i · 𝐴 ) ) )
25	5	2timesd	⊢ ( 𝐴 ∈ ℂ → ( 2 · ( i · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
26	24 25	eqtrd	⊢ ( 𝐴 ∈ ℂ → ( i · ( 2 · 𝐴 ) ) = ( ( i · 𝐴 ) + ( i · 𝐴 ) ) )
27	26	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) )
28		efadd	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
29	5 5 28	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) )
30	27 29	eqtr2d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) )
31		efadd	⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ ( - i · 𝐴 ) ∈ ℂ ) → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
32	5 10 31	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) )
33	3	negidi	⊢ ( i + - i ) = 0
34	33	oveq1i	⊢ ( ( i + - i ) · 𝐴 ) = ( 0 · 𝐴 )
35		adddir	⊢ ( ( i ∈ ℂ ∧ - i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( i + - i ) · 𝐴 ) = ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) )
36	3 8 35	mp3an12	⊢ ( 𝐴 ∈ ℂ → ( ( i + - i ) · 𝐴 ) = ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) )
37		mul02	⊢ ( 𝐴 ∈ ℂ → ( 0 · 𝐴 ) = 0 )
38	34 36 37	3eqtr3a	⊢ ( 𝐴 ∈ ℂ → ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) = 0 )
39	38	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = ( exp ‘ 0 ) )
40		ef0	⊢ ( exp ‘ 0 ) = 1
41	39 40	eqtrdi	⊢ ( 𝐴 ∈ ℂ → ( exp ‘ ( ( i · 𝐴 ) + ( - i · 𝐴 ) ) ) = 1 )
42	32 41	eqtr3d	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) = 1 )
43	30 42	eqeq12d	⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) ↔ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = 1 ) )
44		fveq2	⊢ ( ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) = 1 → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) )
45	43 44	biimtrdi	⊢ ( 𝐴 ∈ ℂ → ( ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( i · 𝐴 ) ) ) = ( ( exp ‘ ( i · 𝐴 ) ) · ( exp ‘ ( - i · 𝐴 ) ) ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
46	21 45	syl5	⊢ ( 𝐴 ∈ ℂ → ( ( exp ‘ ( i · 𝐴 ) ) = ( exp ‘ ( - i · 𝐴 ) ) → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
47	20 46	sylbid	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 → ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ) )
48		abs1	⊢ ( abs ‘ 1 ) = 1
49	48	eqeq2i	⊢ ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 )
50		2re	⊢ 2 ∈ ℝ
51		2ne0	⊢ 2 ≠ 0
52		mulre	⊢ ( ( 𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0 ) → ( 𝐴 ∈ ℝ ↔ ( 2 · 𝐴 ) ∈ ℝ ) )
53	50 51 52	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( 2 · 𝐴 ) ∈ ℝ ) )
54		mulcl	⊢ ( ( 2 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 2 · 𝐴 ) ∈ ℂ )
55	22 54	mpan	⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
56		absefib	⊢ ( ( 2 · 𝐴 ) ∈ ℂ → ( ( 2 · 𝐴 ) ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) )
57	55 56	syl	⊢ ( 𝐴 ∈ ℂ → ( ( 2 · 𝐴 ) ∈ ℝ ↔ ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ) )
58	53 57	bitr2d	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = 1 ↔ 𝐴 ∈ ℝ ) )
59	49 58	bitrid	⊢ ( 𝐴 ∈ ℂ → ( ( abs ‘ ( exp ‘ ( i · ( 2 · 𝐴 ) ) ) ) = ( abs ‘ 1 ) ↔ 𝐴 ∈ ℝ ) )
60	47 59	sylibd	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 → 𝐴 ∈ ℝ ) )
61	60	imp	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ℝ )
62		pirp	⊢ π ∈ ℝ+
63		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
64	61 62 63	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
65		picn	⊢ π ∈ ℂ
66		pire	⊢ π ∈ ℝ
67		pipos	⊢ 0 < π
68	66 67	gt0ne0ii	⊢ π ≠ 0
69		redivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ ∧ π ≠ 0 ) → ( 𝐴 / π ) ∈ ℝ )
70	66 68 69	mp3an23	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 / π ) ∈ ℝ )
71	61 70	syl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℝ )
72	71	flcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
73	72	zcnd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ )
74		mulcl	⊢ ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
75	65 73 74	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ )
76		negsub	⊢ ( ( 𝐴 ∈ ℂ ∧ ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ∈ ℂ ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
77	75 76	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 − ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) )
78		mulcom	⊢ ( ( π ∈ ℂ ∧ ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
79	65 73 78	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
80	79	negeqd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
81		mulneg1	⊢ ( ( ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℂ ∧ π ∈ ℂ ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
82	73 65 81	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) = - ( ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
83	80 82	eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) = ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) )
84	83	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 + - ( π · ( ⌊ ‘ ( 𝐴 / π ) ) ) ) = ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) )
85	64 77 84	3eqtr2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) )
86	85	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ ( 𝐴 mod π ) ) = ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) )
87	86	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) )
88	72	znegcld	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ )
89		abssinper	⊢ ( ( 𝐴 ∈ ℂ ∧ - ( ⌊ ‘ ( 𝐴 / π ) ) ∈ ℤ ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )
90	88 89	syldan	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 + ( - ( ⌊ ‘ ( 𝐴 / π ) ) · π ) ) ) ) = ( abs ‘ ( sin ‘ 𝐴 ) ) )
91		simpr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( sin ‘ 𝐴 ) = 0 )
92	91	fveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ 𝐴 ) ) = ( abs ‘ 0 ) )
93	87 90 92	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( abs ‘ 0 ) )
94		abs0	⊢ ( abs ‘ 0 ) = 0
95	93 94	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = 0 )
96		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) ∈ ℝ )
97	61 62 96	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) ∈ ℝ )
98		modlt	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( 𝐴 mod π ) < π )
99	61 62 98	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) < π )
100	97 99	jca	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) )
101	100	biantrurd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) ) )
102		0re	⊢ 0 ∈ ℝ
103		rexr	⊢ ( 0 ∈ ℝ → 0 ∈ ℝ* )
104		rexr	⊢ ( π ∈ ℝ → π ∈ ℝ* )
105		elioo2	⊢ ( ( 0 ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ) )
106	103 104 105	syl2an	⊢ ( ( 0 ∈ ℝ ∧ π ∈ ℝ ) → ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ) )
107	102 66 106	mp2an	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) )
108		3anan32	⊢ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ 0 < ( 𝐴 mod π ) ∧ ( 𝐴 mod π ) < π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) )
109	107 108	bitri	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) ↔ ( ( ( 𝐴 mod π ) ∈ ℝ ∧ ( 𝐴 mod π ) < π ) ∧ 0 < ( 𝐴 mod π ) ) )
110	101 109	bitr4di	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ↔ ( 𝐴 mod π ) ∈ ( 0 (,) π ) ) )
111		sinq12gt0	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 < ( sin ‘ ( 𝐴 mod π ) ) )
112		elioore	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( 𝐴 mod π ) ∈ ℝ )
113	112	resincld	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( sin ‘ ( 𝐴 mod π ) ) ∈ ℝ )
114		ltle	⊢ ( ( 0 ∈ ℝ ∧ ( sin ‘ ( 𝐴 mod π ) ) ∈ ℝ ) → ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) ) )
115	102 113 114	sylancr	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( 0 < ( sin ‘ ( 𝐴 mod π ) ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) ) )
116	111 115	mpd	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 ≤ ( sin ‘ ( 𝐴 mod π ) ) )
117	113 116	absidd	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = ( sin ‘ ( 𝐴 mod π ) ) )
118	111 117	breqtrrd	⊢ ( ( 𝐴 mod π ) ∈ ( 0 (,) π ) → 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) )
119	110 118	biimtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) → 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ) )
120		ltne	⊢ ( ( 0 ∈ ℝ ∧ 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 )
121	102 120	mpan	⊢ ( 0 < ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 )
122	119 121	syl6	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) → ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) ≠ 0 ) )
123	122	necon2bd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( abs ‘ ( sin ‘ ( 𝐴 mod π ) ) ) = 0 → ¬ 0 < ( 𝐴 mod π ) ) )
124	95 123	mpd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ¬ 0 < ( 𝐴 mod π ) )
125		modge0	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → 0 ≤ ( 𝐴 mod π ) )
126	61 62 125	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 ≤ ( 𝐴 mod π ) )
127		leloe	⊢ ( ( 0 ∈ ℝ ∧ ( 𝐴 mod π ) ∈ ℝ ) → ( 0 ≤ ( 𝐴 mod π ) ↔ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) )
128	102 97 127	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 ≤ ( 𝐴 mod π ) ↔ ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) ) )
129	126 128	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 0 < ( 𝐴 mod π ) ∨ 0 = ( 𝐴 mod π ) ) )
130	129	ord	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ¬ 0 < ( 𝐴 mod π ) → 0 = ( 𝐴 mod π ) ) )
131	124 130	mpd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → 0 = ( 𝐴 mod π ) )
132	131	eqcomd	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 mod π ) = 0 )
133		mod0	⊢ ( ( 𝐴 ∈ ℝ ∧ π ∈ ℝ+ ) → ( ( 𝐴 mod π ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )
134	61 62 133	sylancl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( ( 𝐴 mod π ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )
135	132 134	mpbid	⊢ ( ( 𝐴 ∈ ℂ ∧ ( sin ‘ 𝐴 ) = 0 ) → ( 𝐴 / π ) ∈ ℤ )
136		divcan1	⊢ ( ( 𝐴 ∈ ℂ ∧ π ∈ ℂ ∧ π ≠ 0 ) → ( ( 𝐴 / π ) · π ) = 𝐴 )
137	65 68 136	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 / π ) · π ) = 𝐴 )
138	137	fveq2d	⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = ( sin ‘ 𝐴 ) )
139		sinkpi	⊢ ( ( 𝐴 / π ) ∈ ℤ → ( sin ‘ ( ( 𝐴 / π ) · π ) ) = 0 )
140	138 139	sylan9req	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 / π ) ∈ ℤ ) → ( sin ‘ 𝐴 ) = 0 )
141	135 140	impbida	⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) = 0 ↔ ( 𝐴 / π ) ∈ ℤ ) )