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   )   ▶   𝐴 ∈ ℝ   )
StepHypExpression
1  (   𝐴 ∈ ℂ   ▶   (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i))   )
2  (   (sin‘𝐴) = 0   ▶   (sin‘𝐴) = 0   )
31, 2 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0   )
4  i ∈ ℂ
5  2 ∈ ℂ
64, 5 (2 · i) ∈ ℂ
7  (   𝐴 ∈ ℂ   ▶   𝐴 ∈ ℂ   )
84, 7 (   𝐴 ∈ ℂ   ▶   (i · 𝐴) ∈ ℂ   )
98 (   𝐴 ∈ ℂ   ▶   (exp‘(i · 𝐴)) ∈ ℂ   )
104 -i ∈ ℂ
1110, 7 (   𝐴 ∈ ℂ   ▶   (-i · 𝐴) ∈ ℂ   )
1211 (   𝐴 ∈ ℂ   ▶   (exp‘(-i · 𝐴)) ∈ ℂ   )
139, 12 (   𝐴 ∈ ℂ   ▶   ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ   )
14  i ≠ 0
15  2 ≠ 0
165, 4, 14, 15 (2 · i) ≠ 0
1713, 6, 16 (   𝐴 ∈ ℂ   ▶   ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)   )
183, 17 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0   )
199, 12 (   𝐴 ∈ ℂ   ▶   (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))   )
2019, 18 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))   )
2120 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴)))   )
228, 11 (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴)))   )
234 (i + -i) = 0
2423 ((i + -i) · 𝐴) = (0 · 𝐴)
257, 4, 10 (   𝐴 ∈ ℂ   ▶   ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴))   )
2624, 25 (   𝐴 ∈ ℂ   ▶   ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴)   )
277 (   𝐴 ∈ ℂ   ▶   (0 · 𝐴) = 0   )
2826, 27 (   𝐴 ∈ ℂ   ▶   ((i · 𝐴) + (-i · 𝐴)) = 0   )
2928 (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0)   )
30  (exp‘0) = 1
3122, 21 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴)))   )
3229, 30, 31 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1   )
338, 8 (   𝐴 ∈ ℂ   ▶   (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴)))   )
348 (   𝐴 ∈ ℂ   ▶   (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴))   )
355, 4, 7 (   𝐴 ∈ ℂ   ▶   (2 · (i · 𝐴)) = (i · (2 · 𝐴))   )
3634, 35 (   𝐴 ∈ ℂ   ▶   (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴))   )
3736 (   𝐴 ∈ ℂ   ▶   (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴)))   )
3833, 37 (   𝐴 ∈ ℂ   ▶   (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴)))   )
3932, 38 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (exp‘(i · (2 · 𝐴))) = 1   )
4039 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1)   )
41  (abs‘1) = 1
4240, 41 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(exp‘(i · (2 · 𝐴)))) = 1   )
437, 5 (   𝐴 ∈ ℂ   ▶   (2 · 𝐴) ∈ ℂ   )
4443, 42 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (2 · 𝐴) ∈ ℝ   )
455 2 ∈ ℝ
lemma115, 45, 7, 44 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   𝐴 ∈ ℝ   )
Proof of lemma2
(   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
StepHypExpression
47  𝜋 ∈ ℝ
48  0 < 𝜋
49  0 ∈ ℝ
5049, 47, 48 0 ≤ 𝜋
5147, 50, 48 𝜋 ≠ 0
5247, lemma1, 51 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 / 𝜋) ∈ ℝ   )
5352 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (⌊‘(𝐴 / 𝜋)) ∈ ℤ   )
5453 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (⌊‘(𝐴 / 𝜋)) ∈ ℂ   )
5547 𝜋 ∈ ℂ
5654, 55 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -((⌊‘(𝐴 / 𝜋)) · 𝜋)   )
5754, 55 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((⌊‘(𝐴 / 𝜋)) · 𝜋) = (𝜋 · (⌊‘(𝐴 / 𝜋)))   )
5857 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -((⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))   )
5956, 58 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))   )
6055, 54 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ   )
617, 60 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
6260 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ   )
6354 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(⌊‘(𝐴 / 𝜋)) ∈ ℂ   )
6463, 55 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ   )
6559, 7, 62, 64 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋))))   )
6665, 61 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
6766 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))   )
lemma267 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
Proof of lemma3
(   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) = 0   )
StepHypExpression
69  (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (𝐴 mod 𝜋) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))   )
7069 (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (sin‘(𝐴 mod 𝜋)) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))   )
7170 (   (   𝐴 ∈ ℝ   ,   𝜋 ∈ ℝ+   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
72  (   (   𝐴 ∈ ℂ   ,   -(⌊‘(𝐴 / 𝜋)) ∈ ℤ   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))   )
7372 (   𝐴 ∈ ℂ   ▶   (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))   )
7453 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   -(⌊‘(𝐴 / 𝜋)) ∈ ℤ   )
7573, 74 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))   )
7647, 48 𝜋 ∈ ℝ+
7771, 76 (   𝐴 ∈ ℝ   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
78lemma1, 77 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
7975, lemma2 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))   )
8079, 78 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod 𝜋)))   )
812 (   (sin‘𝐴) = 0   ▶   (abs‘(sin‘𝐴)) = (abs‘0)   )
82  (abs‘0) = 0
8381, 82 (   (sin‘𝐴) = 0   ▶   (abs‘(sin‘𝐴)) = 0   )
8480, 83 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (abs‘(sin‘(𝐴 mod 𝜋))) = 0   )
85lemma1, 76 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) ∈ ℝ   )
8685 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) ∈ ℂ   )
8786 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) ∈ ℂ   )
lemma387, 84 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (sin‘(𝐴 mod 𝜋)) = 0   )
Proof of lemma4
(   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (𝐴 mod 𝜋)   )
StepHypExpression
89  (   (   0 ∈ ℝ   ,   0 < (sin‘(𝐴 mod 𝜋))   )   ▶   (sin‘(𝐴 mod 𝜋)) ≠ 0   )
9089 (   (   0 ∈ ℝ   ,   0 < (sin‘(𝐴 mod 𝜋))   )   ▶   ¬ (sin‘(𝐴 mod 𝜋)) = 0   )
9190 (   0 < (sin‘(𝐴 mod 𝜋))   ▶   (0 ∈ ℝ → ¬ (sin‘(𝐴 mod 𝜋)) = 0)   )
9291, 49 (   0 < (sin‘(𝐴 mod 𝜋))   ▶   ¬ (sin‘(𝐴 mod 𝜋)) = 0   )
9392 (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
94  (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 ↔ (sin‘(𝐴 mod 𝜋)) = 0)
9593, 94 ((sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
96lemma3, 95 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (sin‘(𝐴 mod 𝜋))   )
97  ((𝐴 mod 𝜋) ∈ (0(,)𝜋) → 0 < (sin‘(𝐴 mod 𝜋)))
9896, 97 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋)   )
9949 0 ∈ ℝ*
10047 𝜋 ∈ ℝ*
10199, 100 ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
102101 (¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
10398, 102 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋)   )
104  (((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
105104 (¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
106103, 105 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋))   )
10776, lemma1 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) < 𝜋   )
10885, 107 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)   )
lemma4106, 108 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   ¬ 0 < (𝐴 mod 𝜋)   )
Proof of sineq0ALTVD
(   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ)   )
StepHypExpression
110lemma1, 76 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   0 ≤ (𝐴 mod 𝜋)   )
11149, 85, 110 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))   )
112lemma4, 111 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   0 = (𝐴 mod 𝜋)   )
113112 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 mod 𝜋) = 0   )
114lemma1, 76, 113 (   (   𝐴 ∈ ℂ   ,   (sin‘𝐴) = 0   )   ▶   (𝐴 / 𝜋) ∈ ℤ   )
115114 (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 → (𝐴 / 𝜋) ∈ ℤ)   )
116  (   (𝐴 / 𝜋) ∈ ℤ   ▶   (𝐴 / 𝜋) ∈ ℤ   )
117116 (   (𝐴 / 𝜋) ∈ ℤ   ▶   (sin‘((𝐴 / 𝜋) · 𝜋)) = 0   )
1187, 55, 51 (   𝐴 ∈ ℂ   ▶   ((𝐴 / 𝜋) · 𝜋) = 𝐴   )
119118 (   𝐴 ∈ ℂ   ▶   (sin‘((𝐴 / 𝜋) · 𝜋)) = (sin‘𝐴)   )
120117, 119 (   (   𝐴 ∈ ℂ   ,   (𝐴 / 𝜋) ∈ ℤ   )   ▶   (sin‘𝐴) = 0   )
121120 (   𝐴 ∈ ℂ   ▶   ((𝐴 / 𝜋) ∈ ℤ → (sin‘𝐴) = 0)   )
qed115, 121 (   𝐴 ∈ ℂ   ▶   ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ)   )
 Copyright terms: Public domain W3C validator