sinperlem

	Ref	Expression
Hypotheses	sinperlem.1	$⊢ A \in ℂ \to F (A) = \frac{e^{i A} O e^{(- i) A}}{D}$
	sinperlem.2	$⊢ A + K 2 π \in ℂ \to F (A + K 2 π) = \frac{e^{i (A + K 2 π)} O e^{(- i) (A + K 2 π)}}{D}$
Assertion	sinperlem	$⊢ (A \in ℂ \land K \in ℤ) \to F (A + K 2 π) = F (A)$

Proof

Step	Hyp	Ref	Expression
1		sinperlem.1	$⊢ A \in ℂ \to F (A) = \frac{e^{i A} O e^{(- i) A}}{D}$
2		sinperlem.2	$⊢ A + K 2 π \in ℂ \to F (A + K 2 π) = \frac{e^{i (A + K 2 π)} O e^{(- i) (A + K 2 π)}}{D}$
3		zcn	$⊢ K \in ℤ \to K \in ℂ$
4		2cn	$⊢ 2 \in ℂ$
5		picn	$⊢ π \in ℂ$
6	4 5	mulcli	$⊢ 2 π \in ℂ$
7		mulcl	$⊢ (K \in ℂ \land 2 π \in ℂ) \to K 2 π \in ℂ$
8	3 6 7	sylancl	$⊢ K \in ℤ \to K 2 π \in ℂ$
9		ax-icn	$⊢ i \in ℂ$
10		adddi	$⊢ (i \in ℂ \land A \in ℂ \land K 2 π \in ℂ) \to i (A + K 2 π) = i A + i K 2 π$
11	9 10	mp3an1	$⊢ (A \in ℂ \land K 2 π \in ℂ) \to i (A + K 2 π) = i A + i K 2 π$
12	8 11	sylan2	$⊢ (A \in ℂ \land K \in ℤ) \to i (A + K 2 π) = i A + i K 2 π$
13		mul12	$⊢ (i \in ℂ \land K \in ℂ \land 2 π \in ℂ) \to i K 2 π = K i 2 π$
14	9 6 13	mp3an13	$⊢ K \in ℂ \to i K 2 π = K i 2 π$
15	3 14	syl	$⊢ K \in ℤ \to i K 2 π = K i 2 π$
16	9 6	mulcli	$⊢ i 2 π \in ℂ$
17		mulcom	$⊢ (K \in ℂ \land i 2 π \in ℂ) \to K i 2 π = i 2 π K$
18	3 16 17	sylancl	$⊢ K \in ℤ \to K i 2 π = i 2 π K$
19	15 18	eqtrd	$⊢ K \in ℤ \to i K 2 π = i 2 π K$
20	19	adantl	$⊢ (A \in ℂ \land K \in ℤ) \to i K 2 π = i 2 π K$
21	20	oveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to i A + i K 2 π = i A + i 2 π K$
22	12 21	eqtrd	$⊢ (A \in ℂ \land K \in ℤ) \to i (A + K 2 π) = i A + i 2 π K$
23	22	fveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to e^{i (A + K 2 π)} = e^{i A + i 2 π K}$
24		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
25	9 24	mpan	$⊢ A \in ℂ \to i A \in ℂ$
26		efper	$⊢ (i A \in ℂ \land K \in ℤ) \to e^{i A + i 2 π K} = e^{i A}$
27	25 26	sylan	$⊢ (A \in ℂ \land K \in ℤ) \to e^{i A + i 2 π K} = e^{i A}$
28	23 27	eqtrd	$⊢ (A \in ℂ \land K \in ℤ) \to e^{i (A + K 2 π)} = e^{i A}$
29		negicn	$⊢ - i \in ℂ$
30		adddi	$⊢ (- i \in ℂ \land A \in ℂ \land K 2 π \in ℂ) \to (- i) (A + K 2 π) = (- i) A + (- i) K 2 π$
31	29 30	mp3an1	$⊢ (A \in ℂ \land K 2 π \in ℂ) \to (- i) (A + K 2 π) = (- i) A + (- i) K 2 π$
32	8 31	sylan2	$⊢ (A \in ℂ \land K \in ℤ) \to (- i) (A + K 2 π) = (- i) A + (- i) K 2 π$
33	19	negeqd	$⊢ K \in ℤ \to - i K 2 π = - i 2 π K$
34		mulneg1	$⊢ (i \in ℂ \land K 2 π \in ℂ) \to (- i) K 2 π = - i K 2 π$
35	9 8 34	sylancr	$⊢ K \in ℤ \to (- i) K 2 π = - i K 2 π$
36		mulneg2	$⊢ (i 2 π \in ℂ \land K \in ℂ) \to i 2 π (- K) = - i 2 π K$
37	16 3 36	sylancr	$⊢ K \in ℤ \to i 2 π (- K) = - i 2 π K$
38	33 35 37	3eqtr4d	$⊢ K \in ℤ \to (- i) K 2 π = i 2 π (- K)$
39	38	adantl	$⊢ (A \in ℂ \land K \in ℤ) \to (- i) K 2 π = i 2 π (- K)$
40	39	oveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to (- i) A + (- i) K 2 π = (- i) A + i 2 π (- K)$
41	32 40	eqtrd	$⊢ (A \in ℂ \land K \in ℤ) \to (- i) (A + K 2 π) = (- i) A + i 2 π (- K)$
42	41	fveq2d	$⊢ (A \in ℂ \land K \in ℤ) \to e^{(- i) (A + K 2 π)} = e^{(- i) A + i 2 π (- K)}$
43		mulcl	$⊢ (- i \in ℂ \land A \in ℂ) \to (- i) A \in ℂ$
44	29 43	mpan	$⊢ A \in ℂ \to (- i) A \in ℂ$
45		znegcl	$⊢ K \in ℤ \to - K \in ℤ$
46		efper	$⊢ ((- i) A \in ℂ \land - K \in ℤ) \to e^{(- i) A + i 2 π (- K)} = e^{(- i) A}$
47	44 45 46	syl2an	$⊢ (A \in ℂ \land K \in ℤ) \to e^{(- i) A + i 2 π (- K)} = e^{(- i) A}$
48	42 47	eqtrd	$⊢ (A \in ℂ \land K \in ℤ) \to e^{(- i) (A + K 2 π)} = e^{(- i) A}$
49	28 48	oveq12d	$⊢ (A \in ℂ \land K \in ℤ) \to e^{i (A + K 2 π)} O e^{(- i) (A + K 2 π)} = e^{i A} O e^{(- i) A}$
50	49	oveq1d	$⊢ (A \in ℂ \land K \in ℤ) \to \frac{e^{i (A + K 2 π)} O e^{(- i) (A + K 2 π)}}{D} = \frac{e^{i A} O e^{(- i) A}}{D}$
51		addcl	$⊢ (A \in ℂ \land K 2 π \in ℂ) \to A + K 2 π \in ℂ$
52	8 51	sylan2	$⊢ (A \in ℂ \land K \in ℤ) \to A + K 2 π \in ℂ$
53	52 2	syl	$⊢ (A \in ℂ \land K \in ℤ) \to F (A + K 2 π) = \frac{e^{i (A + K 2 π)} O e^{(- i) (A + K 2 π)}}{D}$
54	1	adantr	$⊢ (A \in ℂ \land K \in ℤ) \to F (A) = \frac{e^{i A} O e^{(- i) A}}{D}$
55	50 53 54	3eqtr4d	$⊢ (A \in ℂ \land K \in ℤ) \to F (A + K 2 π) = F (A)$

Metamath Proof Explorer

Theorem sinperlem

Proof