Theorem abssinper 8707

Description: The absolute value of sine has period pi.

Assertion

Ref	Expression
abssinper	|- ((A e. CC /\ K e. ZZ) -> (abs` (sin` (A + (K x. pi)))) = (abs` (sin` A)))

Proof of Theorem abssinper

Step	Hyp	Ref	Expression
1		zeot 6201	. . 3 |- (K e. ZZ -> ((K / 2) e. ZZ \/ ((K + 1) / 2) e. ZZ))
2	1	adantl 390	. 2 |- ((A e. CC /\ K e. ZZ) -> ((K / 2) e. ZZ \/ ((K + 1) / 2) e. ZZ))
3		zcnt 6142	. . . . . . . . . . 11 |- (K e. ZZ -> K e. CC)
4		halfclt 6035	. . . . . . . . . . . . 13 |- (K e. CC -> (K / 2) e. CC)
5		2cn 5982	. . . . . . . . . . . . . 14 |- 2 e. CC
6		pire 8672	. . . . . . . . . . . . . . 15 |- pi e. RR
7	6	recn 5326	. . . . . . . . . . . . . 14 |- pi e. CC
8		mulasst 5320	. . . . . . . . . . . . . 14 |- (((K / 2) e. CC /\ 2 e. CC /\ pi e. CC) -> (((K / 2) x. 2) x. pi) = ((K / 2) x. (2 x. pi)))
9	5, 7, 8	mp3an23 910	. . . . . . . . . . . . 13 |- ((K / 2) e. CC -> (((K / 2) x. 2) x. pi) = ((K / 2) x. (2 x. pi)))
10	4, 9	syl 10	. . . . . . . . . . . 12 |- (K e. CC -> (((K / 2) x. 2) x. pi) = ((K / 2) x. (2 x. pi)))
11		2ne0 5992	. . . . . . . . . . . . . 14 |- 2 =/= 0
12		divcan1t 5732	. . . . . . . . . . . . . 14 |- ((K e. CC /\ 2 e. CC /\ 2 =/= 0) -> ((K / 2) x. 2) = K)
13	5, 11, 12	mp3an23 910	. . . . . . . . . . . . 13 |- (K e. CC -> ((K / 2) x. 2) = K)
14	13	opreq1d 3981	. . . . . . . . . . . 12 |- (K e. CC -> (((K / 2) x. 2) x. pi) = (K x. pi))
15	10, 14	eqtr3d 1512	. . . . . . . . . . 11 |- (K e. CC -> ((K / 2) x. (2 x. pi)) = (K x. pi))
16	3, 15	syl 10	. . . . . . . . . 10 |- (K e. ZZ -> ((K / 2) x. (2 x. pi)) = (K x. pi))
17	16	adantl 390	. . . . . . . . 9 |- ((A e. CC /\ K e. ZZ) -> ((K / 2) x. (2 x. pi)) = (K x. pi))
18	17	opreq2d 3982	. . . . . . . 8 |- ((A e. CC /\ K e. ZZ) -> (A + ((K / 2) x. (2 x. pi))) = (A + (K x. pi)))
19	18	fveq2d 3734	. . . . . . 7 |- ((A e. CC /\ K e. ZZ) -> (sin` (A + ((K / 2) x. (2 x. pi)))) = (sin` (A + (K x. pi))))
20	19	eqcomd 1483	. . . . . 6 |- ((A e. CC /\ K e. ZZ) -> (sin` (A + (K x. pi))) = (sin` (A + ((K / 2) x. (2 x. pi)))))
21	20	adantr 391	. . . . 5 |- (((A e. CC /\ K e. ZZ) /\ (K / 2) e. ZZ) -> (sin` (A + (K x. pi))) = (sin` (A + ((K / 2) x. (2 x. pi)))))
22		sinper 8685	. . . . . 6 |- ((A e. CC /\ (K / 2) e. ZZ) -> (sin` (A + ((K / 2) x. (2 x. pi)))) = (sin` A))
23	22	adantlr 395	. . . . 5 |- (((A e. CC /\ K e. ZZ) /\ (K / 2) e. ZZ) -> (sin` (A + ((K / 2) x. (2 x. pi)))) = (sin` A))
24	21, 23	eqtrd 1510	. . . 4 |- (((A e. CC /\ K e. ZZ) /\ (K / 2) e. ZZ) -> (sin` (A + (K x. pi))) = (sin` A))
25	24	fveq2d 3734	. . 3 |- (((A e. CC /\ K e. ZZ) /\ (K / 2) e. ZZ) -> (abs` (sin` (A + (K x. pi)))) = (abs` (sin` A)))
26		subadd23t 5397	. . . . . . . . . . . 12 |- ((A e. CC /\ pi e. CC /\ (((K + 1) / 2) x. (2 x. pi)) e. CC) -> ((A - pi) + (((K + 1) / 2) x. (2 x. pi))) = (A + ((((K + 1) / 2) x. (2 x. pi)) - pi)))
27	7, 26	mp3an2 906	. . . . . . . . . . 11 |- ((A e. CC /\ (((K + 1) / 2) x. (2 x. pi)) e. CC) -> ((A - pi) + (((K + 1) / 2) x. (2 x. pi))) = (A + ((((K + 1) / 2) x. (2 x. pi)) - pi)))
28		peano2cn 5356	. . . . . . . . . . . . 13 |- (K e. CC -> (K + 1) e. CC)
29		halfclt 6035	. . . . . . . . . . . . 13 |- ((K + 1) e. CC -> ((K + 1) / 2) e. CC)
30	28, 29	syl 10	. . . . . . . . . . . 12 |- (K e. CC -> ((K + 1) / 2) e. CC)
31	5, 7	mulcl 5333	. . . . . . . . . . . . 13 |- (2 x. pi) e. CC
32		mulclt 5315	. . . . . . . . . . . . 13 |- ((((K + 1) / 2) e. CC /\ (2 x. pi) e. CC) -> (((K + 1) / 2) x. (2 x. pi)) e. CC)
33	31, 32	mpan2 698	. . . . . . . . . . . 12 |- (((K + 1) / 2) e. CC -> (((K + 1) / 2) x. (2 x. pi)) e. CC)
34	30, 33	syl 10	. . . . . . . . . . 11 |- (K e. CC -> (((K + 1) / 2) x. (2 x. pi)) e. CC)
35	27, 34	sylan2 453	. . . . . . . . . 10 |- ((A e. CC /\ K e. CC) -> ((A - pi) + (((K + 1) / 2) x. (2 x. pi))) = (A + ((((K + 1) / 2) x. (2 x. pi)) - pi)))
36		divcan1t 5732	. . . . . . . . . . . . . . . . . . 19 |- (((K + 1) e. CC /\ 2 e. CC /\ 2 =/= 0) -> (((K + 1) / 2) x. 2) = (K + 1))
37	5, 11, 36	mp3an23 910	. . . . . . . . . . . . . . . . . 18 |- ((K + 1) e. CC -> (((K + 1) / 2) x. 2) = (K + 1))
38	28, 37	syl 10	. . . . . . . . . . . . . . . . 17 |- (K e. CC -> (((K + 1) / 2) x. 2) = (K + 1))
39	38	opreq1d 3981	. . . . . . . . . . . . . . . 16 |- (K e. CC -> ((((K + 1) / 2) x. 2) x. pi) = ((K + 1) x. pi))
40		ax1cn 5281	. . . . . . . . . . . . . . . . 17 |- 1 e. CC
41		adddirt 5331	. . . . . . . . . . . . . . . . 17 |- ((K e. CC /\ 1 e. CC /\ pi e. CC) -> ((K + 1) x. pi) = ((K x. pi) + (1 x. pi)))
42	40, 7, 41	mp3an23 910	. . . . . . . . . . . . . . . 16 |- (K e. CC -> ((K + 1) x. pi) = ((K x. pi) + (1 x. pi)))
43	7	mulid2 5345	. . . . . . . . . . . . . . . . . 18 |- (1 x. pi) = pi
44	43	opreq2i 3978	. . . . . . . . . . . . . . . . 17 |- ((K x. pi) + (1 x. pi)) = ((K x. pi) + pi)
45	44	a1i 8	. . . . . . . . . . . . . . . 16 |- (K e. CC -> ((K x. pi) + (1 x. pi)) = ((K x. pi) + pi))
46	39, 42, 45	3eqtrrd 1515	. . . . . . . . . . . . . . 15 |- (K e. CC -> ((K x. pi) + pi) = ((((K + 1) / 2) x. 2) x. pi))
47		mulasst 5320	. . . . . . . . . . . . . . . . 17 |- ((((K + 1) / 2) e. CC /\ 2 e. CC /\ pi e. CC) -> ((((K + 1) / 2) x. 2) x. pi) = (((K + 1) / 2) x. (2 x. pi)))
48	5, 7, 47	mp3an23 910	. . . . . . . . . . . . . . . 16 |- (((K + 1) / 2) e. CC -> ((((K + 1) / 2) x. 2) x. pi) = (((K + 1) / 2) x. (2 x. pi)))
49	30, 48	syl 10	. . . . . . . . . . . . . . 15 |- (K e. CC -> ((((K + 1) / 2) x. 2) x. pi) = (((K + 1) / 2) x. (2 x. pi)))
50	46, 49	eqtr2d 1511	. . . . . . . . . . . . . 14 |- (K e. CC -> (((K + 1) / 2) x. (2 x. pi)) = ((K x. pi) + pi))
51	50	opreq1d 3981	. . . . . . . . . . . . 13 |- (K e. CC -> ((((K + 1) / 2) x. (2 x. pi)) - pi) = (((K x. pi) + pi) - pi))
52		mulclt 5315	. . . . . . . . . . . . . . 15 |- ((K e. CC /\ pi e. CC) -> (K x. pi) e. CC)
53	7, 52	mpan2 698	. . . . . . . . . . . . . 14 |- (K e. CC -> (K x. pi) e. CC)
54		pncant 5409	. . . . . . . . . . . . . . 15 |- (((K x. pi) e. CC /\ pi e. CC) -> (((K x. pi) + pi) - pi) = (K x. pi))
55	7, 54	mpan2 698	. . . . . . . . . . . . . 14 |- ((K x. pi) e. CC -> (((K x. pi) + pi) - pi) = (K x. pi))
56	53, 55	syl 10	. . . . . . . . . . . . 13 |- (K e. CC -> (((K x. pi) + pi) - pi) = (K x. pi))
57	51, 56	eqtrd 1510	. . . . . . . . . . . 12 |- (K e. CC -> ((((K + 1) / 2) x. (2 x. pi)) - pi) = (K x. pi))
58	57	adantl 390	. . . . . . . . . . 11 |- ((A e. CC /\ K e. CC) -> ((((K + 1) / 2) x. (2 x. pi)) - pi) = (K x. pi))
59	58	opreq2d 3982	. . . . . . . . . 10 |- ((A e. CC /\ K e. CC) -> (A + ((((K + 1) / 2) x. (2 x. pi)) - pi)) = (A + (K x. pi)))
60	35, 59	eqtr2d 1511	. . . . . . . . 9 |- ((A e. CC /\ K e. CC) -> (A + (K x. pi)) = ((A - pi) + (((K + 1) / 2) x. (2 x. pi))))
61	60, 3	sylan2 453	. . . . . . . 8 |- (