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) → 𝐴 ∈ ℝ)
StepHypRefExpression
1   sinval (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
2   id ((sin‘𝐴) = 0 → (sin‘𝐴) = 0)
31, 2 sylan9req ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0)
4   axicn i ∈ ℂ
5   2cn 2 ∈ ℂ
65, 4 mulcli (2 · i) ∈ ℂ
7   id (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
d14 a1i (𝐴 ∈ ℂ → i ∈ ℂ)
8d1, 7 mulcld (𝐴 ∈ ℂ → (i · 𝐴) ∈ ℂ)
d3   efcl ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
98, d3 syl (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
104 negcli -i ∈ ℂ
d410 a1i (𝐴 ∈ ℂ → -i ∈ ℂ)
11d4, 7 mulcld (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ)
d6   efcl ((-i · 𝐴) ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
1211, d6 syl (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
139, 12 subcld (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ)
14   ine0 i ≠ 0
15   2ne0 2 ≠ 0
165, 4, 15, 14 mulne0i (2 · i) ≠ 0
d76 a1i (𝐴 ∈ ℂ → (2 · i) ∈ ℂ)
d816 a1i (𝐴 ∈ ℂ → (2 · i) ≠ 0)
1713, d7, d8 diveq0ad (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
d1017 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
183, d10 mpbid ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)
199, 12 subeq0ad (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
d1219 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
2018, d12 mpbid ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))
2120 oveq2d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
d14   efadd (((i · 𝐴) ∈ ℂ ∧ (-i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
228, 11, d14 syl2anc (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
234 negidi (i + -i) = 0
2423 oveq1i ((i + -i) · 𝐴) = (0 · 𝐴)
25d1, d4, 7 adddird (𝐴 ∈ ℂ → ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴)))
2624, 25 syl5reqr (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴))
277 mul02d (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
2826, 27 eqtrd (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = 0)
2928 fveq2d (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
30   ef0 (exp‘0) = 1
d1622 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
3121, d16 eqtr4d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴))))
d1830 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘0) = 1)
d1929 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
3231, d19, d18 3eqtrd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1)
d21   efadd (((i · 𝐴) ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
338, 8, d21 syl2anc (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
348 2timesd (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
d225 a1i (𝐴 ∈ ℂ → 2 ∈ ℂ)
35d22, d1, 7 mul12d (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = (i · (2 · 𝐴)))
3635, 34 eqtr3d (𝐴 ∈ ℂ → (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
3736 fveq2d (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴))))
3837, 33 eqtrd (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
d2438 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
39d24, 32 eqtrd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = 1)
4039 fveq2d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1))
41   abs1 (abs‘1) = 1
4240, 41 syl6eq ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = 1)
43d22, 7 mulcld (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
d138   absefib ((2 · 𝐴) ∈ ℂ → ((2 · 𝐴) ∈ ℝ ↔ (abs‘(exp‘(i · (2 · 𝐴)))) = 1))
d63d138 biimparc (((abs‘(exp‘(i · (2 · 𝐴)))) = 1 ∧ (2 · 𝐴) ∈ ℂ) → (2 · 𝐴) ∈ ℝ)
d27d63 ancoms (((2 · 𝐴) ∈ ℂ ∧ (abs‘(exp‘(i · (2 · 𝐴)))) = 1) → (2 · 𝐴) ∈ ℝ)
4443, 42, d27 eel121 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (2 · 𝐴) ∈ ℝ)
d139   2re 2 ∈ ℝ
d65d139 a1i (2 ∈ ℂ → 2 ∈ ℝ)
455, d65 ax-mp 2 ∈ ℝ
d2815 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ≠ 0)
d2945 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ∈ ℝ)
d307 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℂ)
d140   mulre ((𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0) → (𝐴 ∈ ℝ ↔ (2 · 𝐴) ∈ ℝ))
d84d140 4animp1 ((((𝐴 ∈ ℂ ∧ 2 ∈ ℝ) ∧ 2 ≠ 0) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
d32d84 4an31 ((((2 ≠ 0 ∧ 2 ∈ ℝ) ∧ 𝐴 ∈ ℂ) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
lemma1d28, d29, d30, 44, d32 eel1111 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
Proof of lemma2
((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
StepHypRefExpression
47   pire 𝜋 ∈ ℝ
48   pipos 0 < 𝜋
49   0re 0 ∈ ℝ
5049, 47, 48 ltleii 0 ≤ 𝜋
d141   gt0ne0 ((𝜋 ∈ ℝ ∧ 0 < 𝜋) → 𝜋 ≠ 0)
d93d141 3adant3 ((𝜋 ∈ ℝ ∧ 0 < 𝜋 ∧ 0 ≤ 𝜋) → 𝜋 ≠ 0)
d33d93 3com23 ((𝜋 ∈ ℝ ∧ 0 ≤ 𝜋 ∧ 0 < 𝜋) → 𝜋 ≠ 0)
5147, 50, 48, d33 mp3an 𝜋 ≠ 0
d3447 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℝ)
d3551 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ≠ 0)
52lemma1, d34, d35 redivcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / 𝜋) ∈ ℝ)
5352 flcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / 𝜋)) ∈ ℤ)
5453 zcnd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / 𝜋)) ∈ ℂ)
5547 recni 𝜋 ∈ ℂ
d3755 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℂ)
5654, d37 mulneg1d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -((⌊‘(𝐴 / 𝜋)) · 𝜋))
5754, d37 mulcomd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((⌊‘(𝐴 / 𝜋)) · 𝜋) = (𝜋 · (⌊‘(𝐴 / 𝜋))))
5857 negeqd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -((⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))))
5956, 58 eqtrd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))))
60d37, 54 mulcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ)
61d30, 60 negsubd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
6260 negcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ)
6354 negcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / 𝜋)) ∈ ℂ)
6463, d37 mulcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ)
d142   oveq2 ((-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
d96d142 ad3antrrr (((((-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∧ -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
d46d96 4an4132 ((((𝐴 ∈ ℂ ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) ∈ ℂ) ∧ -(𝜋 · (⌊‘(𝐴 / 𝜋))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / 𝜋)) · 𝜋) = -(𝜋 · (⌊‘(𝐴 / 𝜋)))) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
65d30, 64, 62, 59, d46 eel1111 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 + -(𝜋 · (⌊‘(𝐴 / 𝜋)))))
6665, 61 eqtrd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
6766 fveq2d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))
lemma267 fveq2d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
Proof of lemma3
((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) = 0)
StepHypRefExpression
69   modval ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (𝐴 mod 𝜋) = (𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))
7069 fveq2d ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (sin‘(𝐴 mod 𝜋)) = (sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋))))))
7170 fveq2d ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
d143   abssinper ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / 𝜋)) ∈ ℤ) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))) = (abs‘(sin‘𝐴)))
72d143 eqcomd ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / 𝜋)) ∈ ℤ) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))
7372 ex (𝐴 ∈ ℂ → (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))))
7453 znegcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / 𝜋)) ∈ ℤ)
d4773 adantr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / 𝜋)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋))))))
7574, d47 mpd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / 𝜋)) · 𝜋)))))
7647, 48 elrpii 𝜋 ∈ ℝ+
7776, 71 mpan2 (𝐴 ∈ ℝ → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
78lemma1, 77 syl ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod 𝜋))) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
7975, lemma2 eqtrd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (𝜋 · (⌊‘(𝐴 / 𝜋)))))))
8079, 78 eqtr4d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod 𝜋))))
812 fveq2d ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = (abs‘0))
82   abs0 (abs‘0) = 0
8381, 82 syl6eq ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = 0)
d4983 adantl ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = 0)
8480, d49 eqtr3d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod 𝜋))) = 0)
d5176 a1i ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝜋 ∈ ℝ+)
85lemma1, d51 modcld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) ∈ ℝ)
8685 recnd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) ∈ ℂ)
8786 sincld ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) ∈ ℂ)
lemma387, 84 abs00d ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod 𝜋)) = 0)
Proof of lemma4
((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod 𝜋))
StepHypRefExpression
89   ltne ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod 𝜋))) → (sin‘(𝐴 mod 𝜋)) ≠ 0)
9089 neneqd ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod 𝜋))) → ¬ (sin‘(𝐴 mod 𝜋)) = 0)
9190 expcom (0 < (sin‘(𝐴 mod 𝜋)) → (0 ∈ ℝ → ¬ (sin‘(𝐴 mod 𝜋)) = 0))
9249, 91 mpi (0 < (sin‘(𝐴 mod 𝜋)) → ¬ (sin‘(𝐴 mod 𝜋)) = 0)
9392 con3i (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
d144   notnot ((sin‘(𝐴 mod 𝜋)) = 0 ↔ ¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0)
94d144 bicomi (¬ ¬ (sin‘(𝐴 mod 𝜋)) = 0 ↔ (sin‘(𝐴 mod 𝜋)) = 0)
9594, 93 sylbir ((sin‘(𝐴 mod 𝜋)) = 0 → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
96lemma3, 95 syl ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (sin‘(𝐴 mod 𝜋)))
97   sinq12gt0 ((𝐴 mod 𝜋) ∈ (0(,)𝜋) → 0 < (sin‘(𝐴 mod 𝜋)))
9896, 97 nsyl ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋))
9949 rexri 0 ∈ ℝ*
10047 rexri 𝜋 ∈ ℝ*
d53   elioo2 ((0 ∈ ℝ* ∧ 𝜋 ∈ ℝ*) → ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋)))
10199, 100, d53 mp2an ((𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
102101 notbii (¬ (𝐴 mod 𝜋) ∈ (0(,)𝜋) ↔ ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
10398, 102 sylib ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋))
104   3anan12 (((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
105104 notbii (¬ ((𝐴 mod 𝜋) ∈ ℝ ∧ 0 < (𝐴 mod 𝜋) ∧ (𝐴 mod 𝜋) < 𝜋) ↔ ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
106103, 105 sylib ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)))
d120   modlt ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → (𝐴 mod 𝜋) < 𝜋)
d54d120 ancoms ((𝜋 ∈ ℝ+𝐴 ∈ ℝ) → (𝐴 mod 𝜋) < 𝜋)
10776, lemma1, d54 sylancr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) < 𝜋)
10885, 107 jca ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋))
d55   not12an2impnot1 ((¬ (0 < (𝐴 mod 𝜋) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)) ∧ ((𝐴 mod 𝜋) ∈ ℝ ∧ (𝐴 mod 𝜋) < 𝜋)) → ¬ 0 < (𝐴 mod 𝜋))
lemma4106, 108, d55 syl2anc ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod 𝜋))
Proof of sineq0ALTRO
(𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))
StepHypRefExpression
d122   modge0 ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → 0 ≤ (𝐴 mod 𝜋))
d56d122 ancoms ((𝜋 ∈ ℝ+𝐴 ∈ ℝ) → 0 ≤ (𝐴 mod 𝜋))
11076, lemma1, d56 sylancr ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 ≤ (𝐴 mod 𝜋))
d145   leloe ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ) → (0 ≤ (𝐴 mod 𝜋) ↔ (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))))
d129d145 biimp3a ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ ∧ 0 ≤ (𝐴 mod 𝜋)) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
d57d129 idi ((0 ∈ ℝ ∧ (𝐴 mod 𝜋) ∈ ℝ ∧ 0 ≤ (𝐴 mod 𝜋)) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
11149, 85, 110, d57 eel011 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)))
d146   pm2.53 ((0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)) → (¬ 0 < (𝐴 mod 𝜋) → 0 = (𝐴 mod 𝜋)))
d130d146 imp (((0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋)) ∧ ¬ 0 < (𝐴 mod 𝜋)) → 0 = (𝐴 mod 𝜋))
d58d130 ancoms ((¬ 0 < (𝐴 mod 𝜋) ∧ (0 < (𝐴 mod 𝜋) ∨ 0 = (𝐴 mod 𝜋))) → 0 = (𝐴 mod 𝜋))
112lemma4, 111, d58 syl2anc ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 = (𝐴 mod 𝜋))
113112 eqcomd ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod 𝜋) = 0)
d147   mod0 ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+) → ((𝐴 mod 𝜋) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))
d136d147 biimp3a ((𝐴 ∈ ℝ ∧ 𝜋 ∈ ℝ+ ∧ (𝐴 mod 𝜋) = 0) → (𝐴 / 𝜋) ∈ ℤ)
d59d136 3com12 ((𝜋 ∈ ℝ+𝐴 ∈ ℝ ∧ (𝐴 mod 𝜋) = 0) → (𝐴 / 𝜋) ∈ ℤ)
11476, lemma1, 113, d59 eel011 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / 𝜋) ∈ ℤ)
115114 ex (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 → (𝐴 / 𝜋) ∈ ℤ))
116   id ((𝐴 / 𝜋) ∈ ℤ → (𝐴 / 𝜋) ∈ ℤ)
d60   sinkpi ((𝐴 / 𝜋) ∈ ℤ → (sin‘((𝐴 / 𝜋) · 𝜋)) = 0)
117116, d60 syl ((𝐴 / 𝜋) ∈ ℤ → (sin‘((𝐴 / 𝜋) · 𝜋)) = 0)
d6155 a1i (𝐴 ∈ ℂ → 𝜋 ∈ ℂ)
d6251 a1i (𝐴 ∈ ℂ → 𝜋 ≠ 0)
1187, d61, d62 divcan1d (𝐴 ∈ ℂ → ((𝐴 / 𝜋) · 𝜋) = 𝐴)
119118 fveq2d (𝐴 ∈ ℂ → (sin‘((𝐴 / 𝜋) · 𝜋)) = (sin‘𝐴))
120119, 117 sylan9req ((𝐴 ∈ ℂ ∧ (𝐴 / 𝜋) ∈ ℤ) → (sin‘𝐴) = 0)
121120 ex (𝐴 ∈ ℂ → ((𝐴 / 𝜋) ∈ ℤ → (sin‘𝐴) = 0))
qed115, 121 impbid (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / 𝜋) ∈ ℤ))
 Copyright terms: Public domain W3C validator