Theorem sineq0ALTRO

Description: A complex number whose sine is zero is an integer multiple of 𝜋. The Virtual Deduction form of the proof is sineq0ALTVD. 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 sineq0ALTRO is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 6-Jun-2018.)

Assertion

Ref	Expression
sineq0ALTRO	⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))

Proof of Theorem sineq0ALTRO

			⊢
⊢
Proof of lemma1
⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
Step	Hyp	Ref	Expression
1		sinval	⊢ (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
2		id	⊢ ((sin‘𝐴) = 0 → (sin‘𝐴) = 0)
3	1, 2	sylan9req	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0)
4		axicn	⊢ i ∈ ℂ
5		2cn	⊢ 2 ∈ ℂ
6	5, 4	mulcli	⊢ (2 · i) ∈ ℂ
7		id	⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
d1	4	a1i	⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
8	d1, 7	mulcld	⊢ (𝐴 ∈ ℂ → (i · 𝐴) ∈ ℂ)
d3		efcl	⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
9	8, d3	syl	⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
10	4	negcli	⊢ -i ∈ ℂ
d4	10	a1i	⊢ (𝐴 ∈ ℂ → -i ∈ ℂ)
11	d4, 7	mulcld	⊢ (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ)
d6		efcl	⊢ ((-i · 𝐴) ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
12	11, d6	syl	⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
13	9, 12	subcld	⊢ (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ)
14		ine0	⊢ i ≠ 0
15		2ne0	⊢ 2 ≠ 0
16	5, 4, 15, 14	mulne0i	⊢ (2 · i) ≠ 0
d7	6	a1i	⊢ (𝐴 ∈ ℂ → (2 · i) ∈ ℂ)
d8	16	a1i	⊢ (𝐴 ∈ ℂ → (2 · i) ≠ 0)
17	13, d7, d8	diveq0ad	⊢ (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
d10	17	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
18	3, d10	mpbid	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)
19	9, 12	subeq0ad	⊢ (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
d12	19	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
20	18, d12	mpbid	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))
21	20	oveq2d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
d14		efadd	⊢ (((i · 𝐴) ∈ ℂ ∧ (-i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
22	8, 11, d14	syl2anc	⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
23	4	negidi	⊢ (i + -i) = 0
24	23	oveq1i	⊢ ((i + -i) · 𝐴) = (0 · 𝐴)
25	d1, d4, 7	adddird	⊢ (𝐴 ∈ ℂ → ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴)))
26	24, 25	syl5reqr	⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴))
27	7	mul02d	⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
28	26, 27	eqtrd	⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = 0)
29	28	fveq2d	⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
30		ef0	⊢ (exp‘0) = 1
d16	22	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
31	21, d16	eqtr4d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴))))
d18	30	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘0) = 1)
d19	29	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
32	31, d19, d18	3eqtrd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1)
d21		efadd	⊢ (((i · 𝐴) ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
33	8, 8, d21	syl2anc	⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
34	8	2timesd	⊢ (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
d22	5	a1i	⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
35	d22, d1, 7	mul12d	⊢ (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = (i · (2 · 𝐴)))
36	35, 34	eqtr3d	⊢ (𝐴 ∈ ℂ → (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
37	36	fveq2d	⊢ (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴))))
38	37, 33	eqtrd	⊢ (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
d24	38	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
39	d24, 32	eqtrd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = 1)
40	39	fveq2d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1))
41		abs1	⊢ (abs‘1) = 1
42	40, 41	syl6eq	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = 1)
43	d22, 7	mulcld	⊢ (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
d138		absefib	⊢ ((2 · 𝐴) ∈ ℂ → ((2 · 𝐴) ∈ ℝ ↔ (abs‘(exp‘(i · (2 · 𝐴)))) = 1))
d63	d138	biimparc	⊢ (((abs‘(exp‘(i · (2 · 𝐴)))) = 1 ∧ (2 · 𝐴) ∈ ℂ) → (2 · 𝐴) ∈ ℝ)
d27	d63	ancoms	⊢ (((2 · 𝐴) ∈ ℂ ∧ (abs‘(exp‘(i · (2 · 𝐴)))) = 1) → (2 · 𝐴) ∈ ℝ)
44	43, 42, d27	eel121	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (2 · 𝐴) ∈ ℝ)
d139		2re	⊢ 2 ∈ ℝ
d65	d139	a1i	⊢ (2 ∈ ℂ → 2 ∈ ℝ)
45	5, d65	ax-mp	⊢ 2 ∈ ℝ
d28	15	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ≠ 0)
d29	45	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ∈ ℝ)
d30	7	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℂ)
d140		mulre	⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0) → (𝐴 ∈ ℝ ↔ (2 · 𝐴) ∈ ℝ))
d84	d140	4animp1	⊢ ((((𝐴 ∈ ℂ ∧ 2 ∈ ℝ) ∧ 2 ≠ 0) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
d32	d84	4an31	⊢ ((((2 ≠ 0 ∧ 2 ∈ ℝ) ∧ 𝐴 ∈ ℂ) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
lemma1	d28, d29, d30, 44, d32	eel1111	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
⊢
Proof of lemma2
⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
Step	Hyp	Ref	Expression
47		pire	⊢ 𝜋 ∈ ℝ
48		pipos	⊢ 0 < 𝜋
49		0re	⊢ 0 ∈ ℝ
50	49, 47, 48	ltleii	⊢ 0 ≤ 𝜋
d141		gt0ne0	⊢ ((𝜋 ∈ ℝ ∧ 0 < 𝜋) → 𝜋 ≠ 0)
d93	d141	3adant3	⊢ ((𝜋 ∈ ℝ ∧ 0 < 𝜋 ∧ 0 ≤ 𝜋) → 𝜋 ≠ 0)
d33	d93	3com23	⊢ ((𝜋 ∈ ℝ ∧ 0 ≤ 𝜋 ∧ 0 < 𝜋) → 𝜋 ≠ 0)
51	47, 50, 48, d33	mp3an	⊢ 𝜋 ≠ 0
d34	47	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℝ)
d35	51	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ≠ 0)
52	lemma1, d34, d35	redivcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / 𝜋) ∈ ℝ)
53	52	flcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / 𝜋)) ∈ ℤ)
54	53	zcnd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / 𝜋)) ∈ ℂ)
55	47	recni	⊢ 𝜋 ∈ ℂ
d37	55	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℂ)
56	54, d37	mulneg1d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -((⌊‘(𝐴 / 𝜋)) · 𝜋))
57	54, d37	mulcomd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((⌊‘(𝐴 / 𝜋)) · 𝜋) = (𝜋 · (⌊‘(𝐴 / 𝜋))))
58	57	negeqd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -((⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))))
59	56, 58	eqtrd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))))
60	d37, 54	mulcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ)
61	d30, 60	negsubd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
62	60	negcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ)
63	54	negcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / 𝜋)) ∈ ℂ)
64	63, d37	mulcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ)
d142		oveq2	⊢ ((-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
d96	d142	ad3antrrr	⊢ (((((-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∧ -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
d46	d96	4an4132	⊢ ((((𝐴 ∈ ℂ ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ) ∧ -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
65	d30, 64, 62, 59, d46	eel1111	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
66	65, 61	eqtrd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
67	66	fveq2d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))
lemma2	67	fveq2d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
⊢
Proof of lemma3
⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) = 0)
Step	Hyp	Ref	Expression
69		modval	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (𝐴 mod 𝜋) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
70	69	fveq2d	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (sin‘(𝐴 mod 𝜋)) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))
71	70	fveq2d	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
d143		abssinper	⊢ ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / 𝜋)) ∈ ℤ) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘𝐴)))
72	d143	eqcomd	⊢ ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / 𝜋)) ∈ ℤ) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))
73	72	ex	⊢ (𝐴 ∈ ℂ → (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))))
74	53	znegcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / 𝜋)) ∈ ℤ)
d47	73	adantr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))))
75	74, d47	mpd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))
76	47, 48	elrpii	⊢ 𝜋 ∈ ℝ+
77	76, 71	mpan2	⊢ (𝐴 ∈ ℝ → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
78	lemma1, 77	syl	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
79	75, lemma2	eqtrd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
80	79, 78	eqtr4d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod 𝜋))))
81	2	fveq2d	⊢ ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = (abs‘0))
82		abs0	⊢ (abs‘0) = 0
83	81, 82	syl6eq	⊢ ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = 0)
d49	83	adantl	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = 0)
84	80, d49	eqtr3d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod 𝜋))) = 0)
d51	76	a1i	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℝ+)
85	lemma1, d51	modcld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) ∈ ℝ)
86	85	recnd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) ∈ ℂ)
87	86	sincld	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) ∈ ℂ)
lemma3	87, 84	abs00d	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) = 0)
⊢
Proof of lemma4
⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod 𝜋))
Step	Hyp	Ref	Expression
89		ltne	⊢ ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod 𝜋))) → (sin‘(𝐴 mod 𝜋)) ≠ 0)
90	89	neneqd	⊢ ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod 𝜋))) → ¬ (sin‘(𝐴 mod 𝜋)) = 0)
91	90	expcom	⊢ (0 < (sin‘(𝐴 mod 𝜋)) → (0 ∈ ℝ → ¬ (sin‘(𝐴 mod 𝜋)) = 0))
92	49, 91	mpi	⊢ (0 < (sin‘(𝐴 mod 𝜋)) → ¬ (sin‘(𝐴 mod 𝜋)) = 0)
93	92	con3i	⊢ (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
d144		notnot	⊢ ((sin‘(𝐴 mod 𝜋)) = 0 ↔ ¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0)
94	d144	bicomi	⊢ (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 ↔ (sin‘(𝐴 mod 𝜋)) = 0)
95	94, 93	sylbir	⊢ ((sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
96	lemma3, 95	syl	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
97		sinq12gt0	⊢ ((𝐴 mod 𝜋) ∈ (0(,)𝜋) → 0 < (sin‘(𝐴 mod 𝜋)))
98	96, 97	nsyl	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋))
99	49	rexri	⊢ 0 ∈ ℝ*
100	47	rexri	⊢ 𝜋 ∈ ℝ*
d53		elioo2	⊢ ((0 ∈ ℝ* ∧ 𝜋 ∈ ℝ*) → ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋)))
101	99, 100, d53	mp2an	⊢ ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
102	101	notbii	⊢ (¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
103	98, 102	sylib	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
104		3anan12	⊢ (((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
105	104	notbii	⊢ (¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
106	103, 105	sylib	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
d120		modlt	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (𝐴 mod 𝜋) < 𝜋)
d54	d120	ancoms	⊢ ((𝜋 ∈ ℝ+ ∧ 𝐴 ∈ ℝ) → (𝐴 mod 𝜋) < 𝜋)
107	76, lemma1, d54	sylancr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) < 𝜋)
108	85, 107	jca	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋))
d55		not12an2impnot1	⊢ ((¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)) → ¬ 0 < (𝐴 mod 𝜋))
lemma4	106, 108, d55	syl2anc	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod 𝜋))
⊢
Proof of sineq0ALTRO
⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))
Step	Hyp	Ref	Expression
d122		modge0	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝜋))
d56	d122	ancoms	⊢ ((𝜋 ∈ ℝ+ ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 mod 𝜋))
110	76, lemma1, d56	sylancr	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 ≤ (𝐴 mod 𝜋))
d145		leloe	⊢ ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ) → (0 ≤ (𝐴 mod 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))))
d129	d145	biimp3a	⊢ ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ ∧ 0 ≤ (𝐴 mod 𝜋)) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
d57	d129	idi	⊢ ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ ∧ 0 ≤ (𝐴 mod 𝜋)) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
111	49, 85, 110, d57	eel011	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
d146		pm2.53	⊢ ((0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)) → (¬ 0 < (𝐴 mod 𝜋) → 0 = (𝐴 mod 𝜋)))
d130	d146	imp	⊢ (((0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)) ∧ ¬ 0 < (𝐴 mod 𝜋)) → 0 = (𝐴 mod 𝜋))
d58	d130	ancoms	⊢ ((¬ 0 < (𝐴 mod 𝜋) ∧ (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))) → 0 = (𝐴 mod 𝜋))
112	lemma4, 111, d58	syl2anc	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 = (𝐴 mod 𝜋))
113	112	eqcomd	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) = 0)
d147		mod0	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → ((𝐴 mod 𝜋) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))
d136	d147	biimp3a	⊢ ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+ ∧ (𝐴 mod 𝜋) = 0) → (𝐴 / 𝜋) ∈ ℤ)
d59	d136	3com12	⊢ ((𝜋 ∈ ℝ+ ∧ 𝐴 ∈ ℝ ∧ (𝐴 mod 𝜋) = 0) → (𝐴 / 𝜋) ∈ ℤ)
114	76, lemma1, 113, d59	eel011	⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / 𝜋) ∈ ℤ)
115	114	ex	⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 → (𝐴 / 𝜋) ∈ ℤ))
116		id	⊢ ((𝐴 / 𝜋) ∈ ℤ → (𝐴 / 𝜋) ∈ ℤ)
d60		sinkpi	⊢ ((𝐴 / 𝜋) ∈ ℤ → (sin‘((𝐴 / 𝜋) · 𝜋)) = 0)
117	116, d60	syl	⊢ ((𝐴 / 𝜋) ∈ ℤ → (sin‘((𝐴 / 𝜋) · 𝜋)) = 0)
d61	55	a1i	⊢ (𝐴 ∈ ℂ → 𝜋 ∈ ℂ)
d62	51	a1i	⊢ (𝐴 ∈ ℂ → 𝜋 ≠ 0)
118	7, d61, d62	divcan1d	⊢ (𝐴 ∈ ℂ → ((𝐴 / 𝜋) · 𝜋) = 𝐴)
119	118	fveq2d	⊢ (𝐴 ∈ ℂ → (sin‘((𝐴 / 𝜋) · 𝜋)) = (sin‘𝐴))
120	119, 117	sylan9req	⊢ ((𝐴 ∈ ℂ ∧ (𝐴 / 𝜋) ∈ ℤ) → (sin‘𝐴) = 0)
121	120	ex	⊢ (𝐴 ∈ ℂ → ((𝐴 / 𝜋) ∈ ℤ → (sin‘𝐴) = 0))
qed	115, 121	impbid	⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))