Theorem sineq0ALT 45380

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

Assertion

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

Proof of Theorem sineq0ALT

Step	Hyp	Ref	Expression
1		pire 26439	. . . . 5 ⊢ π ∈ ℝ
2		pipos 26441	. . . . 5 ⊢ 0 < π
3	1, 2	elrpii 12936	. . . 4 ⊢ π ∈ ℝ+
4		2ne0 12276	. . . . . 6 ⊢ 2 ≠ 0
5	4	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ≠ 0)
6		2cn 12247	. . . . . . 7 ⊢ 2 ∈ ℂ
7		2re 12246	. . . . . . . 8 ⊢ 2 ∈ ℝ
8	7	a1i 11	. . . . . . 7 ⊢ (2 ∈ ℂ → 2 ∈ ℝ)
9	6, 8	ax-mp 5	. . . . . 6 ⊢ 2 ∈ ℝ
10	9	a1i 11	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ∈ ℝ)
11		id 22	. . . . . 6 ⊢ (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
12	11	adantr 481	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℂ)
13	6	a1i 11	. . . . . . 7 ⊢ (𝐴 ∈ ℂ → 2 ∈ ℂ)
14	13, 11	mulcld 11156	. . . . . 6 ⊢ (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
15		ax-icn 11088	. . . . . . . . . . . . . . 15 ⊢ i ∈ ℂ
16	15	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → i ∈ ℂ)
17	13, 16, 11	mul12d 11346	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = (i · (2 · 𝐴)))
18	16, 11	mulcld 11156	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (i · 𝐴) ∈ ℂ)
19	18	2timesd 12411	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
20	17, 19	eqtr3d 2776	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
21	20	fveq2d 6831	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴))))
22		efadd 16050	. . . . . . . . . . . 12 ⊢ (((i · 𝐴) ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
23	18, 18, 22	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
24	21, 23	eqtrd 2774	. . . . . . . . . 10 ⊢ (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
25	24	adantr 481	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
26		sinval 16080	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
27		id 22	. . . . . . . . . . . . . . 15 ⊢ ((sin‘𝐴) = 0 → (sin‘𝐴) = 0)
28	26, 27	sylan9req 2795	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0)
29		efcl 16038	. . . . . . . . . . . . . . . . . 18 ⊢ ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
30	18, 29	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
31		negicn 11385	. . . . . . . . . . . . . . . . . . . 20 ⊢ -i ∈ ℂ
32	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℂ → -i ∈ ℂ)
33	32, 11	mulcld 11156	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ)
34		efcl 16038	. . . . . . . . . . . . . . . . . 18 ⊢ ((-i · 𝐴) ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
35	33, 34	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
36	30, 35	subcld 11496	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ)
37		2mulicn 12392	. . . . . . . . . . . . . . . . 17 ⊢ (2 · i) ∈ ℂ
38	37	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (2 · i) ∈ ℂ)
39		2muline0 12393	. . . . . . . . . . . . . . . . 17 ⊢ (2 · i) ≠ 0
40	39	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 ∈ ℂ → (2 · i) ≠ 0)
41	36, 38, 40	diveq0ad 11932	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
42	41	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
43	28, 42	mpbid 233	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)
44	30, 35	subeq0ad 11506	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
45	44	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
46	43, 45	mpbid 233	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))
47	46	oveq2d 7372	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
48		efadd 16050	. . . . . . . . . . . . 13 ⊢ (((i · 𝐴) ∈ ℂ ∧ (-i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
49	18, 33, 48	syl2anc 590	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
50	49	adantr 481	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
51	47, 50	eqtr4d 2777	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴))))
52	16, 32, 11	adddird 11161	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴)))
53	15	negidi 11454	. . . . . . . . . . . . . . 15 ⊢ (i + -i) = 0
54	53	oveq1i 7366	. . . . . . . . . . . . . 14 ⊢ ((i + -i) · 𝐴) = (0 · 𝐴)
55	52, 54	eqtr3di 2789	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴))
56	11	mul02d 11335	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
57	55, 56	eqtrd 2774	. . . . . . . . . . . 12 ⊢ (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = 0)
58	57	fveq2d 6831	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
59	58	adantr 481	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
60		ef0 16047	. . . . . . . . . . 11 ⊢ (exp‘0) = 1
61	60	a1i 11	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘0) = 1)
62	51, 59, 61	3eqtrd 2778	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1)
63	25, 62	eqtrd 2774	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = 1)
64	63	fveq2d 6831	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1))
65		abs1 15250	. . . . . . 7 ⊢ (abs‘1) = 1
66	64, 65	eqtrdi 2790	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = 1)
67		absefib 16156	. . . . . . . 8 ⊢ ((2 · 𝐴) ∈ ℂ → ((2 · 𝐴) ∈ ℝ ↔ (abs‘(exp‘(i · (2 · 𝐴)))) = 1))
68	67	biimparc 480	. . . . . . 7 ⊢ (((abs‘(exp‘(i · (2 · 𝐴)))) = 1 ∧ (2 · 𝐴) ∈ ℂ) → (2 · 𝐴) ∈ ℝ)
69	68	ancoms 459	. . . . . 6 ⊢ (((2 · 𝐴) ∈ ℂ ∧ (abs‘(exp‘(i · (2 · 𝐴)))) = 1) → (2 · 𝐴) ∈ ℝ)
70	14, 66, 69	syl2an2r 691	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (2 · 𝐴) ∈ ℝ)
71		mulre 15074	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0) → (𝐴 ∈ ℝ ↔ (2 · 𝐴) ∈ ℝ))
72	71	4animp1 44941	. . . . . 6 ⊢ ((((𝐴 ∈ ℂ ∧ 2 ∈ ℝ) ∧ 2 ≠ 0) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
73	72	4an31 44942	. . . . 5 ⊢ ((((2 ≠ 0 ∧ 2 ∈ ℝ) ∧ 𝐴 ∈ ℂ) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
74	5, 10, 12, 70, 73	syl1111anc 846	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
75	3	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℝ+)
76	74, 75	modcld 13825	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) ∈ ℝ)
77	76	recnd 11164	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) ∈ ℂ)
78	77	sincld 16088	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod π)) ∈ ℂ)
79	1	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℝ)
80		0re 11137	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 0 ∈ ℝ
81	80, 1, 2	ltleii 11260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ≤ π
82		gt0ne0 11606	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((π ∈ ℝ ∧ 0 < π) → π ≠ 0)
83	82	3adant3 1138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((π ∈ ℝ ∧ 0 < π ∧ 0 ≤ π) → π ≠ 0)
84	83	3com23 1132	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((π ∈ ℝ ∧ 0 ≤ π ∧ 0 < π) → π ≠ 0)
85	1, 81, 2, 84	mp3an 1469	. . . . . . . . . . . . . . . . . . . 20 ⊢ π ≠ 0
86	85	a1i 11	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ≠ 0)
87	74, 79, 86	redivcld 11974	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / π) ∈ ℝ)
88	87	flcld 13748	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / π)) ∈ ℤ)
89	88	znegcld 12626	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / π)) ∈ ℤ)
90		abssinper 26503	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / π)) ∈ ℤ) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))) = (abs‘(sin‘𝐴)))
91	90	eqcomd 2745	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / π)) ∈ ℤ) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))))
92	91	ex 413	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∈ ℂ → (-(⌊‘(𝐴 / π)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))))))
93	92	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))))))
94	89, 93	mpd 15	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))))
95	88	zcnd 12625	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / π)) ∈ ℂ)
96	95	negcld 11483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / π)) ∈ ℂ)
97	1	recni 11150	. . . . . . . . . . . . . . . . . . . . 21 ⊢ π ∈ ℂ
98	97	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℂ)
99	96, 98	mulcld 11156	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) ∈ ℂ)
100	98, 95	mulcld 11156	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (π · (⌊‘(𝐴 / π))) ∈ ℂ)
101	100	negcld 11483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(π · (⌊‘(𝐴 / π))) ∈ ℂ)
102	95, 98	mulneg1d 11594	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) = -((⌊‘(𝐴 / π)) · π))
103	95, 98	mulcomd 11157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((⌊‘(𝐴 / π)) · π) = (π · (⌊‘(𝐴 / π))))
104	103	negeqd 11378	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -((⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))))
105	102, 104	eqtrd 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))))
106		oveq2 7364	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
107	106	ad3antrrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))) ∧ -(π · (⌊‘(𝐴 / π))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / π)) · π) ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
108	107	4an4132 44943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ ℂ ∧ (-(⌊‘(𝐴 / π)) · π) ∈ ℂ) ∧ -(π · (⌊‘(𝐴 / π))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π)))) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
109	12, 99, 101, 105, 108	syl1111anc 846	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
110	12, 100	negsubd 11502	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + -(π · (⌊‘(𝐴 / π)))) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
111	109, 110	eqtrd 2774	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
112	111	fveq2d 6831	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))) = (sin‘(𝐴 − (π · (⌊‘(𝐴 / π))))))
113	112	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
114	94, 113	eqtrd 2774	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
115		modval 13821	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (𝐴 mod π) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
116	115	fveq2d 6831	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (sin‘(𝐴 mod π)) = (sin‘(𝐴 − (π · (⌊‘(𝐴 / π))))))
117	116	fveq2d 6831	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
118	3, 117	mpan2 697	. . . . . . . . . . . . . . 15 ⊢ (𝐴 ∈ ℝ → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
119	74, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
120	114, 119	eqtr4d 2777	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod π))))
121	27	fveq2d 6831	. . . . . . . . . . . . . . 15 ⊢ ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = (abs‘0))
122		abs0 15238	. . . . . . . . . . . . . . 15 ⊢ (abs‘0) = 0
123	121, 122	eqtrdi 2790	. . . . . . . . . . . . . 14 ⊢ ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = 0)
124	123	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = 0)
125	120, 124	eqtr3d 2776	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod π))) = 0)
126	78, 125	abs00d 15402	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod π)) = 0)
127		notnotb 316	. . . . . . . . . . . . 13 ⊢ ((sin‘(𝐴 mod π)) = 0 ↔ ¬ ¬ (sin‘(𝐴 mod π)) = 0)
128	127	bicomi 225	. . . . . . . . . . . 12 ⊢ (¬ ¬ (sin‘(𝐴 mod π)) = 0 ↔ (sin‘(𝐴 mod π)) = 0)
129		ltne 11234	. . . . . . . . . . . . . . . 16 ⊢ ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod π))) → (sin‘(𝐴 mod π)) ≠ 0)
130	129	neneqd 2939	. . . . . . . . . . . . . . 15 ⊢ ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod π))) → ¬ (sin‘(𝐴 mod π)) = 0)
131	130	expcom 414	. . . . . . . . . . . . . 14 ⊢ (0 < (sin‘(𝐴 mod π)) → (0 ∈ ℝ → ¬ (sin‘(𝐴 mod π)) = 0))
132	80, 131	mpi 20	. . . . . . . . . . . . 13 ⊢ (0 < (sin‘(𝐴 mod π)) → ¬ (sin‘(𝐴 mod π)) = 0)
133	132	con3i 154	. . . . . . . . . . . 12 ⊢ (¬ ¬ (sin‘(𝐴 mod π)) = 0 → ¬ 0 < (sin‘(𝐴 mod π)))
134	128, 133	sylbir 236	. . . . . . . . . . 11 ⊢ ((sin‘(𝐴 mod π)) = 0 → ¬ 0 < (sin‘(𝐴 mod π)))
135	126, 134	syl 17	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (sin‘(𝐴 mod π)))
136		sinq12gt0 26489	. . . . . . . . . 10 ⊢ ((𝐴 mod π) ∈ (0(,)π) → 0 < (sin‘(𝐴 mod π)))
137	135, 136	nsyl 140	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (𝐴 mod π) ∈ (0(,)π))
138	80	rexri 11194	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ*
139	1	rexri 11194	. . . . . . . . . . 11 ⊢ π ∈ ℝ*
140		elioo2 13330	. . . . . . . . . . 11 ⊢ ((0 ∈ ℝ* ∧ π ∈ ℝ*) → ((𝐴 mod π) ∈ (0(,)π) ↔ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π)))
141	138, 139, 140	mp2an 698	. . . . . . . . . 10 ⊢ ((𝐴 mod π) ∈ (0(,)π) ↔ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
142	141	notbii 321	. . . . . . . . 9 ⊢ (¬ (𝐴 mod π) ∈ (0(,)π) ↔ ¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
143	137, 142	sylib 219	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
144		3anan12 1101	. . . . . . . . 9 ⊢ (((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π) ↔ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
145	144	notbii 321	. . . . . . . 8 ⊢ (¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π) ↔ ¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
146	143, 145	sylib 219	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
147		modlt 13830	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (𝐴 mod π) < π)
148	147	ancoms 459	. . . . . . . . 9 ⊢ ((π ∈ ℝ+ ∧ 𝐴 ∈ ℝ) → (𝐴 mod π) < π)
149	3, 74, 148	sylancr 593	. . . . . . . 8 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) < π)
150	76, 149	jca 516	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π))
151		not12an2impnot1 45012	. . . . . . 7 ⊢ ((¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)) → ¬ 0 < (𝐴 mod π))
152	146, 150, 151	syl2anc 590	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod π))
153		modge0 13829	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → 0 ≤ (𝐴 mod π))
154	153	ancoms 459	. . . . . . . 8 ⊢ ((π ∈ ℝ+ ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 mod π))
155	3, 74, 154	sylancr 593	. . . . . . 7 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 ≤ (𝐴 mod π))
156		leloe 11223	. . . . . . . . 9 ⊢ ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ) → (0 ≤ (𝐴 mod π) ↔ (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π))))
157	156	biimp3a 1477	. . . . . . . 8 ⊢ ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ ∧ 0 ≤ (𝐴 mod π)) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
158	157	idiALT 44922	. . . . . . 7 ⊢ ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ ∧ 0 ≤ (𝐴 mod π)) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
159	80, 76, 155, 158	mp3an2i 1474	. . . . . 6 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
160		pm2.53 857	. . . . . . . 8 ⊢ ((0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)) → (¬ 0 < (𝐴 mod π) → 0 = (𝐴 mod π)))
161	160	imp 407	. . . . . . 7 ⊢ (((0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)) ∧ ¬ 0 < (𝐴 mod π)) → 0 = (𝐴 mod π))
162	161	ancoms 459	. . . . . 6 ⊢ ((¬ 0 < (𝐴 mod π) ∧ (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π))) → 0 = (𝐴 mod π))
163	152, 159, 162	syl2anc 590	. . . . 5 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 = (𝐴 mod π))
164	163	eqcomd 2745	. . . 4 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) = 0)
165		mod0 13826	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → ((𝐴 mod π) = 0 ↔ (𝐴 / π) ∈ ℤ))
166	165	biimp3a 1477	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ π ∈ ℝ+ ∧ (𝐴 mod π) = 0) → (𝐴 / π) ∈ ℤ)
167	166	3com12 1129	. . . 4 ⊢ ((π ∈ ℝ+ ∧ 𝐴 ∈ ℝ ∧ (𝐴 mod π) = 0) → (𝐴 / π) ∈ ℤ)
168	3, 74, 164, 167	mp3an2i 1474	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / π) ∈ ℤ)
169	168	ex 413	. 2 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 → (𝐴 / π) ∈ ℤ))
170	97	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → π ∈ ℂ)
171	85	a1i 11	. . . . . 6 ⊢ (𝐴 ∈ ℂ → π ≠ 0)
172	11, 170, 171	divcan1d 11923	. . . . 5 ⊢ (𝐴 ∈ ℂ → ((𝐴 / π) · π) = 𝐴)
173	172	fveq2d 6831	. . . 4 ⊢ (𝐴 ∈ ℂ → (sin‘((𝐴 / π) · π)) = (sin‘𝐴))
174		id 22	. . . . 5 ⊢ ((𝐴 / π) ∈ ℤ → (𝐴 / π) ∈ ℤ)
175		sinkpi 26504	. . . . 5 ⊢ ((𝐴 / π) ∈ ℤ → (sin‘((𝐴 / π) · π)) = 0)
176	174, 175	syl 17	. . . 4 ⊢ ((𝐴 / π) ∈ ℤ → (sin‘((𝐴 / π) · π)) = 0)
177	173, 176	sylan9req 2795	. . 3 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴 / π) ∈ ℤ) → (sin‘𝐴) = 0)
178	177	ex 413	. 2 ⊢ (𝐴 ∈ ℂ → ((𝐴 / π) ∈ ℤ → (sin‘𝐴) = 0))
179	169, 178	impbid 213	1 ⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119   ≠ wne 2934   class class class wbr 5072  ‘cfv 6485  (class class class)co 7356  ℂcc 11027  ℝcr 11028  0cc0 11029  1c1 11030  ici 11031   + caddc 11032   · cmul 11034  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171   − cmin 11368  -cneg 11369   / cdiv 11798  2c2 12227  ℤcz 12515  ℝ⁺crp 12933  (,)cioo 13289  ⌊cfl 13740   mod cmo 13819  abscabs 15187  expce 16017  sincsin 16019  πcpi 16022

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-inf2 9553  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-pre-sup 11107  ax-addf 11108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9265  df-fi 9314  df-sup 9345  df-inf 9346  df-oi 9415  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-div 11799  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-q 12890  df-rp 12934  df-xneg 13054  df-xadd 13055  df-xmul 13056  df-ioo 13293  df-ioc 13294  df-ico 13295  df-icc 13296  df-fz 13453  df-fzo 13600  df-fl 13742  df-mod 13820  df-seq 13955  df-exp 14015  df-fac 14227  df-bc 14256  df-hash 14284  df-shft 15020  df-cj 15052  df-re 15053  df-im 15054  df-sqrt 15188  df-abs 15189  df-limsup 15424  df-clim 15441  df-rlim 15442  df-sum 15640  df-ef 16023  df-sin 16025  df-cos 16026  df-pi 16028  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-hom 17235  df-cco 17236  df-rest 17376  df-topn 17377  df-0g 17395  df-gsum 17396  df-topgen 17397  df-pt 17398  df-prds 17401  df-xrs 17457  df-qtop 17462  df-imas 17463  df-xps 17465  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-submnd 18743  df-mulg 19035  df-cntz 19283  df-cmn 19748  df-psmet 21339  df-xmet 21340  df-met 21341  df-bl 21342  df-mopn 21343  df-fbas 21344  df-fg 21345  df-cnfld 21348  df-top 22877  df-topon 22894  df-topsp 22916  df-bases 22929  df-cld 23002  df-ntr 23003  df-cls 23004  df-nei 23081  df-lp 23119  df-perf 23120  df-cn 23210  df-cnp 23211  df-haus 23298  df-tx 23545  df-hmeo 23738  df-fil 23829  df-fm 23921  df-flim 23922  df-flf 23923  df-xms 24303  df-ms 24304  df-tms 24305  df-cncf 24863  df-limc 25851  df-dv 25852

This theorem is referenced by: (None)