Theorem sineq0ALTVD

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
sineq0ALTVD	⊢ (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ)   )

Proof of Theorem sineq0ALTVD

		⊢
⊢
Proof of lemma1
⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   𝐴 ∈ ℝ   )
Step	Hyp	Expression
1		⊢ (   𝐴 ∈ ℂ   ▶   (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))   )
2		⊢ (   (sin‘𝐴) = 0   ▶   (sin‘𝐴) = 0   )
3	1, 2	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0   )
4		⊢ i ∈ ℂ
5		⊢ 2 ∈ ℂ
6	4, 5	⊢ (2 · i) ∈ ℂ
7		⊢ (   𝐴 ∈ ℂ   ▶   𝐴 ∈ ℂ   )
8	4, 7	⊢ (   𝐴 ∈ ℂ   ▶   (i · 𝐴) ∈ ℂ   )
9	8	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘(i · 𝐴)) ∈ ℂ   )
10	4	⊢ -i ∈ ℂ
11	10, 7	⊢ (   𝐴 ∈ ℂ   ▶   (-i · 𝐴) ∈ ℂ   )
12	11	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘(-i · 𝐴)) ∈ ℂ   )
13	9, 12	⊢ (   𝐴 ∈ ℂ   ▶   ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ   )
14		⊢ i ≠ 0
15		⊢ 2 ≠ 0
16	5, 4, 14, 15	⊢ (2 · i) ≠ 0
17	13, 6, 16	⊢ (   𝐴 ∈ ℂ   ▶   ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)   )
18	3, 17	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0   )
19	9, 12	⊢ (   𝐴 ∈ ℂ   ▶   (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))   )
20	19, 18	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))   )
21	20	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴)))   )
22	8, 11	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴)))   )
23	4	⊢ (i + -i) = 0
24	23	⊢ ((i + -i) · 𝐴) = (0 · 𝐴)
25	7, 4, 10	⊢ (   𝐴 ∈ ℂ   ▶   ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴))   )
26	24, 25	⊢ (   𝐴 ∈ ℂ   ▶   ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴)   )
27	7	⊢ (   𝐴 ∈ ℂ   ▶   (0 · 𝐴) = 0   )
28	26, 27	⊢ (   𝐴 ∈ ℂ   ▶   ((i · 𝐴) + (-i · 𝐴)) = 0   )
29	28	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0)   )
30		⊢ (exp‘0) = 1
31	22, 21	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴)))   )
32	29, 30, 31	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1   )
33	8, 8	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴)))   )
34	8	⊢ (   𝐴 ∈ ℂ   ▶   (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))   )
35	5, 4, 7	⊢ (   𝐴 ∈ ℂ   ▶   (2 · (i · 𝐴)) = (i · (2 · 𝐴))   )
36	34, 35	⊢ (   𝐴 ∈ ℂ   ▶   (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴))   )
37	36	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴)))   )
38	33, 37	⊢ (   𝐴 ∈ ℂ   ▶   (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴)))   )
39	32, 38	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (exp‘(i · (2 · 𝐴))) = 1   )
40	39	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1)   )
41		⊢ (abs‘1) = 1
42	40, 41	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(exp‘(i · (2 · 𝐴)))) = 1   )
43	7, 5	⊢ (   𝐴 ∈ ℂ   ▶   (2 · 𝐴) ∈ ℂ   )
44	43, 42	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (2 · 𝐴) ∈ ℝ   )
45	5	⊢ 2 ∈ ℝ
lemma1	15, 45, 7, 44	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   𝐴 ∈ ℝ   )
⊢
Proof of lemma2
⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
Step	Hyp	Expression
47		⊢ 𝜋 ∈ ℝ
48		⊢ 0 < 𝜋
49		⊢ 0 ∈ ℝ
50	49, 47, 48	⊢ 0 ≤ 𝜋
51	47, 50, 48	⊢ 𝜋 ≠ 0
52	47, lemma1, 51	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 / 𝜋) ∈ ℝ   )
53	52	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (⌊‘(𝐴 / 𝜋)) ∈ ℤ   )
54	53	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (⌊‘(𝐴 / 𝜋)) ∈ ℂ   )
55	47	⊢ 𝜋 ∈ ℂ
56	54, 55	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -((⌊‘(𝐴 / 𝜋)) · 𝜋)   )
57	54, 55	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((⌊‘(𝐴 / 𝜋)) · 𝜋) = (𝜋 · (⌊‘(𝐴 / 𝜋)))   )
58	57	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -((⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))   )
59	56, 58	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))   )
60	55, 54	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ   )
61	7, 60	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
62	60	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ   )
63	54	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(⌊‘(𝐴 / 𝜋)) ∈ ℂ   )
64	63, 55	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ   )
65	59, 7, 62, 64	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋))))   )
66	65, 61	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
67	66	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))   )
lemma2	67	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
⊢
Proof of lemma3
⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) = 0   )
Step	Hyp	Expression
69		⊢ (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (𝐴 mod 𝜋) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
70	69	⊢ (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (sin‘(𝐴 mod 𝜋)) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))   )
71	70	⊢ (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
72		⊢ (   (   𝐴 ∈ ℂ   ,   -(⌊‘(𝐴 / 𝜋)) ∈ ℤ   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))   )
73	72	⊢ (   𝐴 ∈ ℂ   ▶   (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))   )
74	53	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(⌊‘(𝐴 / 𝜋)) ∈ ℤ   )
75	73, 74	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))   )
76	47, 48	⊢ 𝜋 ∈ ℝ+
77	71, 76	⊢ (   𝐴 ∈ ℝ   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
78	lemma1, 77	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
79	75, lemma2	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
80	79, 78	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod 𝜋)))   )
81	2	⊢ (   (sin‘𝐴) = 0   ▶   (abs‘(sin‘𝐴)) = (abs‘0)   )
82		⊢ (abs‘0) = 0
83	81, 82	⊢ (   (sin‘𝐴) = 0   ▶   (abs‘(sin‘𝐴)) = 0   )
84	80, 83	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = 0   )
85	lemma1, 76	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) ∈ ℝ   )
86	85	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) ∈ ℂ   )
87	86	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) ∈ ℂ   )
lemma3	87, 84	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) = 0   )
⊢
Proof of lemma4
⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (𝐴 mod 𝜋)   )
Step	Hyp	Expression
89		⊢ (   (   0 ∈ ℝ   ,   0 < (sin‘(𝐴 mod 𝜋))   )   ▶   (sin‘(𝐴 mod 𝜋)) ≠ 0   )
90	89	⊢ (   (   0 ∈ ℝ   ,   0 < (sin‘(𝐴 mod 𝜋))   )   ▶   ¬ (sin‘(𝐴 mod 𝜋)) = 0   )
91	90	⊢ (   0 < (sin‘(𝐴 mod 𝜋))   ▶   (0 ∈ ℝ → ¬ (sin‘(𝐴 mod 𝜋)) = 0)   )
92	91, 49	⊢ (   0 < (sin‘(𝐴 mod 𝜋))   ▶   ¬ (sin‘(𝐴 mod 𝜋)) = 0   )
93	92	⊢ (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
94		⊢ (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 ↔ (sin‘(𝐴 mod 𝜋)) = 0)
95	93, 94	⊢ ((sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
96	lemma3, 95	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (sin‘(𝐴 mod 𝜋))   )
97		⊢ ((𝐴 mod 𝜋) ∈ (0(,)𝜋) → 0 < (sin‘(𝐴 mod 𝜋)))
98	96, 97	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋)   )
99	49	⊢ 0 ∈ ℝ*
100	47	⊢ 𝜋 ∈ ℝ*
101	99, 100	⊢ ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
102	101	⊢ (¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
103	98, 102	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋)   )
104		⊢ (((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
105	104	⊢ (¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
106	103, 105	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋))   )
107	76, lemma1	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) < 𝜋   )
108	85, 107	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)   )
lemma4	106, 108	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (𝐴 mod 𝜋)   )
⊢
Proof of sineq0ALTVD
⊢ (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ)   )
Step	Hyp	Expression
110	lemma1, 76	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   0 ≤ (𝐴 mod 𝜋)   )
111	49, 85, 110	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))   )
112	lemma4, 111	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   0 = (𝐴 mod 𝜋)   )
113	112	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) = 0   )
114	lemma1, 76, 113	⊢ (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 / 𝜋) ∈ ℤ   )
115	114	⊢ (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 → (𝐴 / 𝜋) ∈ ℤ)   )
116		⊢ (   (𝐴 / 𝜋) ∈ ℤ   ▶   (𝐴 / 𝜋) ∈ ℤ   )
117	116	⊢ (   (𝐴 / 𝜋) ∈ ℤ   ▶   (sin‘((𝐴 / 𝜋) · 𝜋)) = 0   )
118	7, 55, 51	⊢ (   𝐴 ∈ ℂ   ▶   ((𝐴 / 𝜋) · 𝜋) = 𝐴   )
119	118	⊢ (   𝐴 ∈ ℂ   ▶   (sin‘((𝐴 / 𝜋) · 𝜋)) = (sin‘𝐴)   )
120	117, 119	⊢ (   (   𝐴 ∈ ℂ   ,   (𝐴 / 𝜋) ∈ ℤ   )   ▶   (sin‘𝐴) = 0   )
121	120	⊢ (   𝐴 ∈ ℂ   ▶   ((𝐴 / 𝜋) ∈ ℤ → (sin‘𝐴) = 0)   )
qed	115, 121	⊢ (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ)   )