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