abssinper

Description: The absolute value of sine has period _pi . (Contributed by NM, 17-Aug-2008)

		Ref	Expression
	Assertion	abssinper	$⊢ (A \in ℂ \land K \in ℤ) \to \|\sin (A + K π)\| = \|\sin A\|$

Proof

Step	Hyp	Ref	Expression
1		zcn	$⊢ K \in ℤ \to K \in ℂ$
2		halfcl	$⊢ K \in ℂ \to \frac{K}{2} \in ℂ$
3		2cn	$⊢ 2 \in ℂ$
4		picn	$⊢ π \in ℂ$
5		mulass	$⊢ (\frac{K}{2} \in ℂ \land 2 \in ℂ \land π \in ℂ) \to (\frac{K}{2}) \cdot 2 π = (\frac{K}{2}) 2 π$
6	3 4 5	mp3an23	$⊢ \frac{K}{2} \in ℂ \to (\frac{K}{2}) \cdot 2 π = (\frac{K}{2}) 2 π$
7	2 6	syl	$⊢ K \in ℂ \to (\frac{K}{2}) \cdot 2 π = (\frac{K}{2}) 2 π$
8		2ne0	$⊢ 2 \neq 0$
9		divcan1	$⊢ (K \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to (\frac{K}{2}) \cdot 2 = K$
10	3 8 9	mp3an23	$⊢ K \in ℂ \to (\frac{K}{2}) \cdot 2 = K$
11	10	oveq1d	$⊢ K \in ℂ \to (\frac{K}{2}) \cdot 2 π = K π$
12	7 11	eqtr3d	$⊢ K \in ℂ \to (\frac{K}{2}) 2 π = K π$
13	1 12	syl	$⊢ K \in ℤ \to (\frac{K}{2}) 2 π = K π$
14	13	adantl	$⊢ (A \in ℂ \land K \in ℤ) \to (\frac{K}{2}) 2 π = K π$
15	14	oveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to A + (\frac{K}{2}) 2 π = A + K π$
16	15	fveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to \sin (A + (\frac{K}{2}) 2 π) = \sin (A + K π)$
17	16	eqcomd	$⊢ (A \in ℂ \land K \in ℤ) \to \sin (A + K π) = \sin (A + (\frac{K}{2}) 2 π)$
18	17	adantr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K}{2} \in ℤ) \to \sin (A + K π) = \sin (A + (\frac{K}{2}) 2 π)$
19		sinper	$⊢ (A \in ℂ \land \frac{K}{2} \in ℤ) \to \sin (A + (\frac{K}{2}) 2 π) = \sin A$
20	19	adantlr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K}{2} \in ℤ) \to \sin (A + (\frac{K}{2}) 2 π) = \sin A$
21	18 20	eqtrd	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K}{2} \in ℤ) \to \sin (A + K π) = \sin A$
22	21	fveq2d	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K}{2} \in ℤ) \to \|\sin (A + K π)\| = \|\sin A\|$
23		peano2cn	$⊢ K \in ℂ \to K + 1 \in ℂ$
24		halfcl	$⊢ K + 1 \in ℂ \to \frac{K + 1}{2} \in ℂ$
25	23 24	syl	$⊢ K \in ℂ \to \frac{K + 1}{2} \in ℂ$
26	3 4	mulcli	$⊢ 2 π \in ℂ$
27		mulcl	$⊢ (\frac{K + 1}{2} \in ℂ \land 2 π \in ℂ) \to (\frac{K + 1}{2}) 2 π \in ℂ$
28	25 26 27	sylancl	$⊢ K \in ℂ \to (\frac{K + 1}{2}) 2 π \in ℂ$
29		subadd23	$⊢ (A \in ℂ \land π \in ℂ \land (\frac{K + 1}{2}) 2 π \in ℂ) \to A - π + (\frac{K + 1}{2}) 2 π = A + (\frac{K + 1}{2}) 2 π - π$
30	4 29	mp3an2	$⊢ (A \in ℂ \land (\frac{K + 1}{2}) 2 π \in ℂ) \to A - π + (\frac{K + 1}{2}) 2 π = A + (\frac{K + 1}{2}) 2 π - π$
31	28 30	sylan2	$⊢ (A \in ℂ \land K \in ℂ) \to A - π + (\frac{K + 1}{2}) 2 π = A + (\frac{K + 1}{2}) 2 π - π$
32		divcan1	$⊢ (K + 1 \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to (\frac{K + 1}{2}) \cdot 2 = K + 1$
33	3 8 32	mp3an23	$⊢ K + 1 \in ℂ \to (\frac{K + 1}{2}) \cdot 2 = K + 1$
34	23 33	syl	$⊢ K \in ℂ \to (\frac{K + 1}{2}) \cdot 2 = K + 1$
35	34	oveq1d	$⊢ K \in ℂ \to (\frac{K + 1}{2}) \cdot 2 π = (K + 1) π$
36		ax-1cn	$⊢ 1 \in ℂ$
37		adddir	$⊢ (K \in ℂ \land 1 \in ℂ \land π \in ℂ) \to (K + 1) π = K π + 1 π$
38	36 4 37	mp3an23	$⊢ K \in ℂ \to (K + 1) π = K π + 1 π$
39	35 38	eqtrd	$⊢ K \in ℂ \to (\frac{K + 1}{2}) \cdot 2 π = K π + 1 π$
40	4	mulid2i	$⊢ 1 π = π$
41	40	oveq2i	$⊢ K π + 1 π = K π + π$
42	39 41	syl6req	$⊢ K \in ℂ \to K π + π = (\frac{K + 1}{2}) \cdot 2 π$
43		mulass	$⊢ (\frac{K + 1}{2} \in ℂ \land 2 \in ℂ \land π \in ℂ) \to (\frac{K + 1}{2}) \cdot 2 π = (\frac{K + 1}{2}) 2 π$
44	3 4 43	mp3an23	$⊢ \frac{K + 1}{2} \in ℂ \to (\frac{K + 1}{2}) \cdot 2 π = (\frac{K + 1}{2}) 2 π$
45	25 44	syl	$⊢ K \in ℂ \to (\frac{K + 1}{2}) \cdot 2 π = (\frac{K + 1}{2}) 2 π$
46	42 45	eqtr2d	$⊢ K \in ℂ \to (\frac{K + 1}{2}) 2 π = K π + π$
47	46	oveq1d	$⊢ K \in ℂ \to (\frac{K + 1}{2}) 2 π - π = K π + π - π$
48		mulcl	$⊢ (K \in ℂ \land π \in ℂ) \to K π \in ℂ$
49	4 48	mpan2	$⊢ K \in ℂ \to K π \in ℂ$
50		pncan	$⊢ (K π \in ℂ \land π \in ℂ) \to K π + π - π = K π$
51	49 4 50	sylancl	$⊢ K \in ℂ \to K π + π - π = K π$
52	47 51	eqtrd	$⊢ K \in ℂ \to (\frac{K + 1}{2}) 2 π - π = K π$
53	52	adantl	$⊢ (A \in ℂ \land K \in ℂ) \to (\frac{K + 1}{2}) 2 π - π = K π$
54	53	oveq2d	$⊢ (A \in ℂ \land K \in ℂ) \to A + (\frac{K + 1}{2}) 2 π - π = A + K π$
55	31 54	eqtr2d	$⊢ (A \in ℂ \land K \in ℂ) \to A + K π = A - π + (\frac{K + 1}{2}) 2 π$
56	1 55	sylan2	$⊢ (A \in ℂ \land K \in ℤ) \to A + K π = A - π + (\frac{K + 1}{2}) 2 π$
57	56	fveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to \sin (A + K π) = \sin (A - π + (\frac{K + 1}{2}) 2 π)$
58	57	adantr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \sin (A + K π) = \sin (A - π + (\frac{K + 1}{2}) 2 π)$
59		subcl	$⊢ (A \in ℂ \land π \in ℂ) \to A - π \in ℂ$
60	4 59	mpan2	$⊢ A \in ℂ \to A - π \in ℂ$
61		sinper	$⊢ (A - π \in ℂ \land \frac{K + 1}{2} \in ℤ) \to \sin (A - π + (\frac{K + 1}{2}) 2 π) = \sin (A - π)$
62	60 61	sylan	$⊢ (A \in ℂ \land \frac{K + 1}{2} \in ℤ) \to \sin (A - π + (\frac{K + 1}{2}) 2 π) = \sin (A - π)$
63	62	adantlr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \sin (A - π + (\frac{K + 1}{2}) 2 π) = \sin (A - π)$
64		sinmpi	$⊢ A \in ℂ \to \sin (A - π) = - \sin A$
65	64	ad2antrr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \sin (A - π) = - \sin A$
66	63 65	eqtrd	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \sin (A - π + (\frac{K + 1}{2}) 2 π) = - \sin A$
67	58 66	eqtrd	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \sin (A + K π) = - \sin A$
68	67	fveq2d	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \|\sin (A + K π)\| = \|- \sin A\|$
69		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
70	69	absnegd	$⊢ A \in ℂ \to \|- \sin A\| = \|\sin A\|$
71	70	ad2antrr	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \|- \sin A\| = \|\sin A\|$
72	68 71	eqtrd	$⊢ ((A \in ℂ \land K \in ℤ) \land \frac{K + 1}{2} \in ℤ) \to \|\sin (A + K π)\| = \|\sin A\|$
73		zeo	$⊢ K \in ℤ \to (\frac{K}{2} \in ℤ \lor \frac{K + 1}{2} \in ℤ)$
74	73	adantl	$⊢ (A \in ℂ \land K \in ℤ) \to (\frac{K}{2} \in ℤ \lor \frac{K + 1}{2} \in ℤ)$
75	22 72 74	mpjaodan	$⊢ (A \in ℂ \land K \in ℤ) \to \|\sin (A + K π)\| = \|\sin A\|$

Metamath Proof Explorer

Theorem abssinper

Proof