Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sineq0ALT Structured version   Visualization version   GIF version

Theorem sineq0ALT 40831
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 40831. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 24796. 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 24796 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
StepHypRef Expression
1 pire 24731 . . . . 5 π ∈ ℝ
2 pipos 24733 . . . . 5 0 < π
31, 2elrpii 12246 . . . 4 π ∈ ℝ+
4 2ne0 11595 . . . . . 6 2 ≠ 0
54a1i 11 . . . . 5 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ≠ 0)
6 2cn 11566 . . . . . . 7 2 ∈ ℂ
7 2re 11565 . . . . . . . 8 2 ∈ ℝ
87a1i 11 . . . . . . 7 (2 ∈ ℂ → 2 ∈ ℝ)
96, 8ax-mp 5 . . . . . 6 2 ∈ ℝ
109a1i 11 . . . . 5 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 2 ∈ ℝ)
11 id 22 . . . . . 6 (𝐴 ∈ ℂ → 𝐴 ∈ ℂ)
1211adantr 481 . . . . 5 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℂ)
136a1i 11 . . . . . . 7 (𝐴 ∈ ℂ → 2 ∈ ℂ)
1413, 11mulcld 10514 . . . . . 6 (𝐴 ∈ ℂ → (2 · 𝐴) ∈ ℂ)
15 ax-icn 10449 . . . . . . . . . . . . . . 15 i ∈ ℂ
1615a1i 11 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → i ∈ ℂ)
1713, 16, 11mul12d 10702 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = (i · (2 · 𝐴)))
1816, 11mulcld 10514 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (i · 𝐴) ∈ ℂ)
19182timesd 11734 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (2 · (i · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
2017, 19eqtr3d 2835 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (i · (2 · 𝐴)) = ((i · 𝐴) + (i · 𝐴)))
2120fveq2d 6549 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = (exp‘((i · 𝐴) + (i · 𝐴))))
22 efadd 15284 . . . . . . . . . . . 12 (((i · 𝐴) ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
2318, 18, 22syl2anc 584 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
2421, 23eqtrd 2833 . . . . . . . . . 10 (𝐴 ∈ ℂ → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
2524adantr 481 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))))
26 sinval 15312 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → (sin‘𝐴) = (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)))
27 id 22 . . . . . . . . . . . . . . 15 ((sin‘𝐴) = 0 → (sin‘𝐴) = 0)
2826, 27sylan9req 2854 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0)
29 efcl 15273 . . . . . . . . . . . . . . . . . 18 ((i · 𝐴) ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
3018, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (exp‘(i · 𝐴)) ∈ ℂ)
31 negicn 10740 . . . . . . . . . . . . . . . . . . . 20 -i ∈ ℂ
3231a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℂ → -i ∈ ℂ)
3332, 11mulcld 10514 . . . . . . . . . . . . . . . . . 18 (𝐴 ∈ ℂ → (-i · 𝐴) ∈ ℂ)
34 efcl 15273 . . . . . . . . . . . . . . . . . 18 ((-i · 𝐴) ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
3533, 34syl 17 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (exp‘(-i · 𝐴)) ∈ ℂ)
3630, 35subcld 10851 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) ∈ ℂ)
37 2mulicn 11714 . . . . . . . . . . . . . . . . 17 (2 · i) ∈ ℂ
3837a1i 11 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (2 · i) ∈ ℂ)
39 2muline0 11715 . . . . . . . . . . . . . . . . 17 (2 · i) ≠ 0
4039a1i 11 . . . . . . . . . . . . . . . 16 (𝐴 ∈ ℂ → (2 · i) ≠ 0)
4136, 38, 40diveq0ad 11280 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℂ → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
4241adantr 481 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) / (2 · i)) = 0 ↔ ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0))
4328, 42mpbid 233 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0)
4430, 35subeq0ad 10861 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
4544adantr 481 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (((exp‘(i · 𝐴)) − (exp‘(-i · 𝐴))) = 0 ↔ (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴))))
4643, 45mpbid 233 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · 𝐴)) = (exp‘(-i · 𝐴)))
4746oveq2d 7039 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
48 efadd 15284 . . . . . . . . . . . . 13 (((i · 𝐴) ∈ ℂ ∧ (-i · 𝐴) ∈ ℂ) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
4918, 33, 48syl2anc 584 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
5049adantr 481 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = ((exp‘(i · 𝐴)) · (exp‘(-i · 𝐴))))
5147, 50eqtr4d 2836 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = (exp‘((i · 𝐴) + (-i · 𝐴))))
5215negidi 10809 . . . . . . . . . . . . . . 15 (i + -i) = 0
5352oveq1i 7033 . . . . . . . . . . . . . 14 ((i + -i) · 𝐴) = (0 · 𝐴)
5416, 32, 11adddird 10519 . . . . . . . . . . . . . 14 (𝐴 ∈ ℂ → ((i + -i) · 𝐴) = ((i · 𝐴) + (-i · 𝐴)))
5553, 54syl5reqr 2848 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = (0 · 𝐴))
5611mul02d 10691 . . . . . . . . . . . . 13 (𝐴 ∈ ℂ → (0 · 𝐴) = 0)
5755, 56eqtrd 2833 . . . . . . . . . . . 12 (𝐴 ∈ ℂ → ((i · 𝐴) + (-i · 𝐴)) = 0)
5857fveq2d 6549 . . . . . . . . . . 11 (𝐴 ∈ ℂ → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
5958adantr 481 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘((i · 𝐴) + (-i · 𝐴))) = (exp‘0))
60 ef0 15281 . . . . . . . . . . 11 (exp‘0) = 1
6160a1i 11 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘0) = 1)
6251, 59, 613eqtrd 2837 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((exp‘(i · 𝐴)) · (exp‘(i · 𝐴))) = 1)
6325, 62eqtrd 2833 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (exp‘(i · (2 · 𝐴))) = 1)
6463fveq2d 6549 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = (abs‘1))
65 abs1 14495 . . . . . . 7 (abs‘1) = 1
6664, 65syl6eq 2849 . . . . . 6 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(exp‘(i · (2 · 𝐴)))) = 1)
67 absefib 15388 . . . . . . . 8 ((2 · 𝐴) ∈ ℂ → ((2 · 𝐴) ∈ ℝ ↔ (abs‘(exp‘(i · (2 · 𝐴)))) = 1))
6867biimparc 480 . . . . . . 7 (((abs‘(exp‘(i · (2 · 𝐴)))) = 1 ∧ (2 · 𝐴) ∈ ℂ) → (2 · 𝐴) ∈ ℝ)
6968ancoms 459 . . . . . 6 (((2 · 𝐴) ∈ ℂ ∧ (abs‘(exp‘(i · (2 · 𝐴)))) = 1) → (2 · 𝐴) ∈ ℝ)
7014, 66, 69syl2an2r 681 . . . . 5 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (2 · 𝐴) ∈ ℝ)
71 mulre 14318 . . . . . . 7 ((𝐴 ∈ ℂ ∧ 2 ∈ ℝ ∧ 2 ≠ 0) → (𝐴 ∈ ℝ ↔ (2 · 𝐴) ∈ ℝ))
72714animp1 40391 . . . . . 6 ((((𝐴 ∈ ℂ ∧ 2 ∈ ℝ) ∧ 2 ≠ 0) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
73724an31 40392 . . . . 5 ((((2 ≠ 0 ∧ 2 ∈ ℝ) ∧ 𝐴 ∈ ℂ) ∧ (2 · 𝐴) ∈ ℝ) → 𝐴 ∈ ℝ)
745, 10, 12, 70, 73syl1111anc 836 . . . 4 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 𝐴 ∈ ℝ)
753a1i 11 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℝ+)
7674, 75modcld 13097 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) ∈ ℝ)
7776recnd 10522 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) ∈ ℂ)
7877sincld 15320 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod π)) ∈ ℂ)
791a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℝ)
80 0re 10496 . . . . . . . . . . . . . . . . . . . . . 22 0 ∈ ℝ
8180, 1, 2ltleii 10616 . . . . . . . . . . . . . . . . . . . . 21 0 ≤ π
82 gt0ne0 10959 . . . . . . . . . . . . . . . . . . . . . . 23 ((π ∈ ℝ ∧ 0 < π) → π ≠ 0)
83823adant3 1125 . . . . . . . . . . . . . . . . . . . . . 22 ((π ∈ ℝ ∧ 0 < π ∧ 0 ≤ π) → π ≠ 0)
84833com23 1119 . . . . . . . . . . . . . . . . . . . . 21 ((π ∈ ℝ ∧ 0 ≤ π ∧ 0 < π) → π ≠ 0)
851, 81, 2, 84mp3an 1453 . . . . . . . . . . . . . . . . . . . 20 π ≠ 0
8685a1i 11 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ≠ 0)
8774, 79, 86redivcld 11322 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / π) ∈ ℝ)
8887flcld 13022 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / π)) ∈ ℤ)
8988znegcld 11943 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / π)) ∈ ℤ)
90 abssinper 24793 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / π)) ∈ ℤ) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))) = (abs‘(sin‘𝐴)))
9190eqcomd 2803 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ -(⌊‘(𝐴 / π)) ∈ ℤ) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))))
9291ex 413 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ ℂ → (-(⌊‘(𝐴 / π)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))))))
9392adantr 481 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) ∈ ℤ → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))))))
9489, 93mpd 15 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))))
9588zcnd 11942 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (⌊‘(𝐴 / π)) ∈ ℂ)
9695negcld 10838 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(⌊‘(𝐴 / π)) ∈ ℂ)
971recni 10508 . . . . . . . . . . . . . . . . . . . . 21 π ∈ ℂ
9897a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → π ∈ ℂ)
9996, 98mulcld 10514 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) ∈ ℂ)
10098, 95mulcld 10514 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (π · (⌊‘(𝐴 / π))) ∈ ℂ)
101100negcld 10838 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -(π · (⌊‘(𝐴 / π))) ∈ ℂ)
10295, 98mulneg1d 10947 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) = -((⌊‘(𝐴 / π)) · π))
10395, 98mulcomd 10515 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((⌊‘(𝐴 / π)) · π) = (π · (⌊‘(𝐴 / π))))
104103negeqd 10733 . . . . . . . . . . . . . . . . . . . 20 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → -((⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))))
105102, 104eqtrd 2833 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))))
106 oveq2 7031 . . . . . . . . . . . . . . . . . . . . 21 ((-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
107106ad3antrrr 726 . . . . . . . . . . . . . . . . . . . 20 (((((-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π))) ∧ -(π · (⌊‘(𝐴 / π))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / π)) · π) ∈ ℂ) ∧ 𝐴 ∈ ℂ) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
1081074an4132 40393 . . . . . . . . . . . . . . . . . . 19 ((((𝐴 ∈ ℂ ∧ (-(⌊‘(𝐴 / π)) · π) ∈ ℂ) ∧ -(π · (⌊‘(𝐴 / π))) ∈ ℂ) ∧ (-(⌊‘(𝐴 / π)) · π) = -(π · (⌊‘(𝐴 / π)))) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
10912, 99, 101, 105, 108syl1111anc 836 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 + -(π · (⌊‘(𝐴 / π)))))
11012, 100negsubd 10857 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + -(π · (⌊‘(𝐴 / π)))) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
111109, 110eqtrd 2833 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 + (-(⌊‘(𝐴 / π)) · π)) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
112111fveq2d 6549 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π))) = (sin‘(𝐴 − (π · (⌊‘(𝐴 / π))))))
113112fveq2d 6549 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 + (-(⌊‘(𝐴 / π)) · π)))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
11494, 113eqtrd 2833 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
115 modval 13093 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (𝐴 mod π) = (𝐴 − (π · (⌊‘(𝐴 / π)))))
116115fveq2d 6549 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (sin‘(𝐴 mod π)) = (sin‘(𝐴 − (π · (⌊‘(𝐴 / π))))))
117116fveq2d 6549 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
1183, 117mpan2 687 . . . . . . . . . . . . . . 15 (𝐴 ∈ ℝ → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
11974, 118syl 17 . . . . . . . . . . . . . 14 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod π))) = (abs‘(sin‘(𝐴 − (π · (⌊‘(𝐴 / π)))))))
120114, 119eqtr4d 2836 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = (abs‘(sin‘(𝐴 mod π))))
12127fveq2d 6549 . . . . . . . . . . . . . . 15 ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = (abs‘0))
122 abs0 14483 . . . . . . . . . . . . . . 15 (abs‘0) = 0
123121, 122syl6eq 2849 . . . . . . . . . . . . . 14 ((sin‘𝐴) = 0 → (abs‘(sin‘𝐴)) = 0)
124123adantl 482 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘𝐴)) = 0)
125120, 124eqtr3d 2835 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (abs‘(sin‘(𝐴 mod π))) = 0)
12678, 125abs00d 14644 . . . . . . . . . . 11 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (sin‘(𝐴 mod π)) = 0)
127 notnotb 316 . . . . . . . . . . . . 13 ((sin‘(𝐴 mod π)) = 0 ↔ ¬ ¬ (sin‘(𝐴 mod π)) = 0)
128127bicomi 225 . . . . . . . . . . . 12 (¬ ¬ (sin‘(𝐴 mod π)) = 0 ↔ (sin‘(𝐴 mod π)) = 0)
129 ltne 10590 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod π))) → (sin‘(𝐴 mod π)) ≠ 0)
130129neneqd 2991 . . . . . . . . . . . . . . 15 ((0 ∈ ℝ ∧ 0 < (sin‘(𝐴 mod π))) → ¬ (sin‘(𝐴 mod π)) = 0)
131130expcom 414 . . . . . . . . . . . . . 14 (0 < (sin‘(𝐴 mod π)) → (0 ∈ ℝ → ¬ (sin‘(𝐴 mod π)) = 0))
13280, 131mpi 20 . . . . . . . . . . . . 13 (0 < (sin‘(𝐴 mod π)) → ¬ (sin‘(𝐴 mod π)) = 0)
133132con3i 157 . . . . . . . . . . . 12 (¬ ¬ (sin‘(𝐴 mod π)) = 0 → ¬ 0 < (sin‘(𝐴 mod π)))
134128, 133sylbir 236 . . . . . . . . . . 11 ((sin‘(𝐴 mod π)) = 0 → ¬ 0 < (sin‘(𝐴 mod π)))
135126, 134syl 17 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (sin‘(𝐴 mod π)))
136 sinq12gt0 24780 . . . . . . . . . 10 ((𝐴 mod π) ∈ (0(,)π) → 0 < (sin‘(𝐴 mod π)))
137135, 136nsyl 142 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (𝐴 mod π) ∈ (0(,)π))
13880rexri 10552 . . . . . . . . . . 11 0 ∈ ℝ*
1391rexri 10552 . . . . . . . . . . 11 π ∈ ℝ*
140 elioo2 12633 . . . . . . . . . . 11 ((0 ∈ ℝ* ∧ π ∈ ℝ*) → ((𝐴 mod π) ∈ (0(,)π) ↔ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π)))
141138, 139, 140mp2an 688 . . . . . . . . . 10 ((𝐴 mod π) ∈ (0(,)π) ↔ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
142141notbii 321 . . . . . . . . 9 (¬ (𝐴 mod π) ∈ (0(,)π) ↔ ¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
143137, 142sylib 219 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π))
144 3anan12 1089 . . . . . . . . 9 (((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π) ↔ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
145144notbii 321 . . . . . . . 8 (¬ ((𝐴 mod π) ∈ ℝ ∧ 0 < (𝐴 mod π) ∧ (𝐴 mod π) < π) ↔ ¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
146143, 145sylib 219 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)))
147 modlt 13102 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → (𝐴 mod π) < π)
148147ancoms 459 . . . . . . . . 9 ((π ∈ ℝ+𝐴 ∈ ℝ) → (𝐴 mod π) < π)
1493, 74, 148sylancr 587 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) < π)
15076, 149jca 512 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π))
151 not12an2impnot1 40462 . . . . . . 7 ((¬ (0 < (𝐴 mod π) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)) ∧ ((𝐴 mod π) ∈ ℝ ∧ (𝐴 mod π) < π)) → ¬ 0 < (𝐴 mod π))
152146, 150, 151syl2anc 584 . . . . . 6 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → ¬ 0 < (𝐴 mod π))
153 modge0 13101 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → 0 ≤ (𝐴 mod π))
154153ancoms 459 . . . . . . . 8 ((π ∈ ℝ+𝐴 ∈ ℝ) → 0 ≤ (𝐴 mod π))
1553, 74, 154sylancr 587 . . . . . . 7 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 ≤ (𝐴 mod π))
156 leloe 10580 . . . . . . . . 9 ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ) → (0 ≤ (𝐴 mod π) ↔ (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π))))
157156biimp3a 1461 . . . . . . . 8 ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ ∧ 0 ≤ (𝐴 mod π)) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
158157idiALT 40371 . . . . . . 7 ((0 ∈ ℝ ∧ (𝐴 mod π) ∈ ℝ ∧ 0 ≤ (𝐴 mod π)) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
15980, 76, 155, 158mp3an2i 1458 . . . . . 6 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)))
160 pm2.53 846 . . . . . . . 8 ((0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)) → (¬ 0 < (𝐴 mod π) → 0 = (𝐴 mod π)))
161160imp 407 . . . . . . 7 (((0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π)) ∧ ¬ 0 < (𝐴 mod π)) → 0 = (𝐴 mod π))
162161ancoms 459 . . . . . 6 ((¬ 0 < (𝐴 mod π) ∧ (0 < (𝐴 mod π) ∨ 0 = (𝐴 mod π))) → 0 = (𝐴 mod π))
163152, 159, 162syl2anc 584 . . . . 5 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → 0 = (𝐴 mod π))
164163eqcomd 2803 . . . 4 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 mod π) = 0)
165 mod0 13098 . . . . . 6 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+) → ((𝐴 mod π) = 0 ↔ (𝐴 / π) ∈ ℤ))
166165biimp3a 1461 . . . . 5 ((𝐴 ∈ ℝ ∧ π ∈ ℝ+ ∧ (𝐴 mod π) = 0) → (𝐴 / π) ∈ ℤ)
1671663com12 1116 . . . 4 ((π ∈ ℝ+𝐴 ∈ ℝ ∧ (𝐴 mod π) = 0) → (𝐴 / π) ∈ ℤ)
1683, 74, 164, 167mp3an2i 1458 . . 3 ((𝐴 ∈ ℂ ∧ (sin‘𝐴) = 0) → (𝐴 / π) ∈ ℤ)
169168ex 413 . 2 (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 → (𝐴 / π) ∈ ℤ))
17097a1i 11 . . . . . 6 (𝐴 ∈ ℂ → π ∈ ℂ)
17185a1i 11 . . . . . 6 (𝐴 ∈ ℂ → π ≠ 0)
17211, 170, 171divcan1d 11271 . . . . 5 (𝐴 ∈ ℂ → ((𝐴 / π) · π) = 𝐴)
173172fveq2d 6549 . . . 4 (𝐴 ∈ ℂ → (sin‘((𝐴 / π) · π)) = (sin‘𝐴))
174 id 22 . . . . 5 ((𝐴 / π) ∈ ℤ → (𝐴 / π) ∈ ℤ)
175 sinkpi 24794 . . . . 5 ((𝐴 / π) ∈ ℤ → (sin‘((𝐴 / π) · π)) = 0)
176174, 175syl 17 . . . 4 ((𝐴 / π) ∈ ℤ → (sin‘((𝐴 / π) · π)) = 0)
177173, 176sylan9req 2854 . . 3 ((𝐴 ∈ ℂ ∧ (𝐴 / π) ∈ ℤ) → (sin‘𝐴) = 0)
178177ex 413 . 2 (𝐴 ∈ ℂ → ((𝐴 / π) ∈ ℤ → (sin‘𝐴) = 0))
179169, 178impbid 213 1 (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 842  w3a 1080   = wceq 1525  wcel 2083  wne 2986   class class class wbr 4968  cfv 6232  (class class class)co 7023  cc 10388  cr 10389  0cc0 10390  1c1 10391  ici 10392   + caddc 10393   · cmul 10395  *cxr 10527   < clt 10528  cle 10529  cmin 10723  -cneg 10724   / cdiv 11151  2c2 11546  cz 11835  +crp 12243  (,)cioo 12592  cfl 13014   mod cmo 13091  abscabs 14431  expce 15252  sincsin 15254  πcpi 15257
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-rep 5088  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-inf2 8957  ax-cnex 10446  ax-resscn 10447  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-mulcom 10454  ax-addass 10455  ax-mulass 10456  ax-distr 10457  ax-i2m1 10458  ax-1ne0 10459  ax-1rid 10460  ax-rnegex 10461  ax-rrecex 10462  ax-cnre 10463  ax-pre-lttri 10464  ax-pre-lttrn 10465  ax-pre-ltadd 10466  ax-pre-mulgt0 10467  ax-pre-sup 10468  ax-addf 10469  ax-mulf 10470
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-fal 1538  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-int 4789  df-iun 4833  df-iin 4834  df-br 4969  df-opab 5031  df-mpt 5048  df-tr 5071  df-id 5355  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-se 5410  df-we 5411  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-pred 6030  df-ord 6076  df-on 6077  df-lim 6078  df-suc 6079  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-isom 6241  df-riota 6984  df-ov 7026  df-oprab 7027  df-mpo 7028  df-of 7274  df-om 7444  df-1st 7552  df-2nd 7553  df-supp 7689  df-wrecs 7805  df-recs 7867  df-rdg 7905  df-1o 7960  df-2o 7961  df-oadd 7964  df-er 8146  df-map 8265  df-pm 8266  df-ixp 8318  df-en 8365  df-dom 8366  df-sdom 8367  df-fin 8368  df-fsupp 8687  df-fi 8728  df-sup 8759  df-inf 8760  df-oi 8827  df-card 9221  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534  df-sub 10725  df-neg 10726  df-div 11152  df-nn 11493  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558  df-7 11559  df-8 11560  df-9 11561  df-n0 11752  df-z 11836  df-dec 11953  df-uz 12098  df-q 12202  df-rp 12244  df-xneg 12361  df-xadd 12362  df-xmul 12363  df-ioo 12596  df-ioc 12597  df-ico 12598  df-icc 12599  df-fz 12747  df-fzo 12888  df-fl 13016  df-mod 13092  df-seq 13224  df-exp 13284  df-fac 13488  df-bc 13517  df-hash 13545  df-shft 14264  df-cj 14296  df-re 14297  df-im 14298  df-sqrt 14432  df-abs 14433  df-limsup 14666  df-clim 14683  df-rlim 14684  df-sum 14881  df-ef 15258  df-sin 15260  df-cos 15261  df-pi 15263  df-struct 16318  df-ndx 16319  df-slot 16320  df-base 16322  df-sets 16323  df-ress 16324  df-plusg 16411  df-mulr 16412  df-starv 16413  df-sca 16414  df-vsca 16415  df-ip 16416  df-tset 16417  df-ple 16418  df-ds 16420  df-unif 16421  df-hom 16422  df-cco 16423  df-rest 16529  df-topn 16530  df-0g 16548  df-gsum 16549  df-topgen 16550  df-pt 16551  df-prds 16554  df-xrs 16608  df-qtop 16613  df-imas 16614  df-xps 16616  df-mre 16690  df-mrc 16691  df-acs 16693  df-mgm 17685  df-sgrp 17727  df-mnd 17738  df-submnd 17779  df-mulg 17986  df-cntz 18192  df-cmn 18639  df-psmet 20223  df-xmet 20224  df-met 20225  df-bl 20226  df-mopn 20227  df-fbas 20228  df-fg 20229  df-cnfld 20232  df-top 21190  df-topon 21207  df-topsp 21229  df-bases 21242  df-cld 21315  df-ntr 21316  df-cls 21317  df-nei 21394  df-lp 21432  df-perf 21433  df-cn 21523  df-cnp 21524  df-haus 21611  df-tx 21858  df-hmeo 22051  df-fil 22142  df-fm 22234  df-flim 22235  df-flf 22236  df-xms 22617  df-ms 22618  df-tms 22619  df-cncf 23173  df-limc 24151  df-dv 24152
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator