efeq1

Description: A complex number whose exponential is one is an integer multiple of 2pi i . (Contributed by NM, 17-Aug-2008) (Revised by Mario Carneiro, 10-May-2014)

		Ref	Expression
	Assertion	efeq1	\|- ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )

Proof

Step	Hyp	Ref	Expression
1		halfcl	\|- ( A e. CC -> ( A / 2 ) e. CC )
2		ax-icn	\|- _i e. CC
3		ine0	\|- _i =/= 0
4		divcl	\|- ( ( ( A / 2 ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( ( A / 2 ) / _i ) e. CC )
5	2 3 4	mp3an23	\|- ( ( A / 2 ) e. CC -> ( ( A / 2 ) / _i ) e. CC )
6	1 5	syl	\|- ( A e. CC -> ( ( A / 2 ) / _i ) e. CC )
7		sineq0	\|- ( ( ( A / 2 ) / _i ) e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ ) )
8	6 7	syl	\|- ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ ) )
9		sinval	\|- ( ( ( A / 2 ) / _i ) e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) )
10	6 9	syl	\|- ( A e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) )
11		divcan2	\|- ( ( ( A / 2 ) e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
12	2 3 11	mp3an23	\|- ( ( A / 2 ) e. CC -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
13	1 12	syl	\|- ( A e. CC -> ( _i x. ( ( A / 2 ) / _i ) ) = ( A / 2 ) )
14	13	fveq2d	\|- ( A e. CC -> ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) = ( exp ` ( A / 2 ) ) )
15		mulneg1	\|- ( ( _i e. CC /\ ( ( A / 2 ) / _i ) e. CC ) -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( _i x. ( ( A / 2 ) / _i ) ) )
16	2 6 15	sylancr	\|- ( A e. CC -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( _i x. ( ( A / 2 ) / _i ) ) )
17	13	negeqd	\|- ( A e. CC -> -u ( _i x. ( ( A / 2 ) / _i ) ) = -u ( A / 2 ) )
18	16 17	eqtrd	\|- ( A e. CC -> ( -u _i x. ( ( A / 2 ) / _i ) ) = -u ( A / 2 ) )
19	18	fveq2d	\|- ( A e. CC -> ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) = ( exp ` -u ( A / 2 ) ) )
20	14 19	oveq12d	\|- ( A e. CC -> ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) = ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) )
21	20	oveq1d	\|- ( A e. CC -> ( ( ( exp ` ( _i x. ( ( A / 2 ) / _i ) ) ) - ( exp ` ( -u _i x. ( ( A / 2 ) / _i ) ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) )
22	10 21	eqtrd	\|- ( A e. CC -> ( sin ` ( ( A / 2 ) / _i ) ) = ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) )
23	22	eqeq1d	\|- ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 ) )
24		efcl	\|- ( ( A / 2 ) e. CC -> ( exp ` ( A / 2 ) ) e. CC )
25	1 24	syl	\|- ( A e. CC -> ( exp ` ( A / 2 ) ) e. CC )
26	1	negcld	\|- ( A e. CC -> -u ( A / 2 ) e. CC )
27		efcl	\|- ( -u ( A / 2 ) e. CC -> ( exp ` -u ( A / 2 ) ) e. CC )
28	26 27	syl	\|- ( A e. CC -> ( exp ` -u ( A / 2 ) ) e. CC )
29	25 28	subcld	\|- ( A e. CC -> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC )
30		2cn	\|- 2 e. CC
31	30 2	mulcli	\|- ( 2 x. _i ) e. CC
32		2ne0	\|- 2 =/= 0
33	30 2 32 3	mulne0i	\|- ( 2 x. _i ) =/= 0
34		diveq0	\|- ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC /\ ( 2 x. _i ) e. CC /\ ( 2 x. _i ) =/= 0 ) -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
35	31 33 34	mp3an23	\|- ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
36	29 35	syl	\|- ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( 2 x. _i ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
37		efne0	\|- ( -u ( A / 2 ) e. CC -> ( exp ` -u ( A / 2 ) ) =/= 0 )
38	26 37	syl	\|- ( A e. CC -> ( exp ` -u ( A / 2 ) ) =/= 0 )
39	25 28 28 38	divsubdird	\|- ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = ( ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) - ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) ) )
40		efsub	\|- ( ( ( A / 2 ) e. CC /\ -u ( A / 2 ) e. CC ) -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
41	1 26 40	syl2anc	\|- ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) )
42	1 1	subnegd	\|- ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = ( ( A / 2 ) + ( A / 2 ) ) )
43		2halves	\|- ( A e. CC -> ( ( A / 2 ) + ( A / 2 ) ) = A )
44	42 43	eqtrd	\|- ( A e. CC -> ( ( A / 2 ) - -u ( A / 2 ) ) = A )
45	44	fveq2d	\|- ( A e. CC -> ( exp ` ( ( A / 2 ) - -u ( A / 2 ) ) ) = ( exp ` A ) )
46	41 45	eqtr3d	\|- ( A e. CC -> ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = ( exp ` A ) )
47	28 38	dividd	\|- ( A e. CC -> ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) = 1 )
48	46 47	oveq12d	\|- ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) - ( ( exp ` -u ( A / 2 ) ) / ( exp ` -u ( A / 2 ) ) ) ) = ( ( exp ` A ) - 1 ) )
49	39 48	eqtrd	\|- ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = ( ( exp ` A ) - 1 ) )
50	49	eqeq1d	\|- ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` A ) - 1 ) = 0 ) )
51	29 28 38	diveq0ad	\|- ( A e. CC -> ( ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) / ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 ) )
52		efcl	\|- ( A e. CC -> ( exp ` A ) e. CC )
53		ax-1cn	\|- 1 e. CC
54		subeq0	\|- ( ( ( exp ` A ) e. CC /\ 1 e. CC ) -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
55	52 53 54	sylancl	\|- ( A e. CC -> ( ( ( exp ` A ) - 1 ) = 0 <-> ( exp ` A ) = 1 ) )
56	50 51 55	3bitr3d	\|- ( A e. CC -> ( ( ( exp ` ( A / 2 ) ) - ( exp ` -u ( A / 2 ) ) ) = 0 <-> ( exp ` A ) = 1 ) )
57	23 36 56	3bitrd	\|- ( A e. CC -> ( ( sin ` ( ( A / 2 ) / _i ) ) = 0 <-> ( exp ` A ) = 1 ) )
58		2cnne0	\|- ( 2 e. CC /\ 2 =/= 0 )
59	2 3	pm3.2i	\|- ( _i e. CC /\ _i =/= 0 )
60		divdiv32	\|- ( ( A e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _i e. CC /\ _i =/= 0 ) ) -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
61	58 59 60	mp3an23	\|- ( A e. CC -> ( ( A / 2 ) / _i ) = ( ( A / _i ) / 2 ) )
62	61	oveq1d	\|- ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( ( ( A / _i ) / 2 ) / _pi ) )
63		divcl	\|- ( ( A e. CC /\ _i e. CC /\ _i =/= 0 ) -> ( A / _i ) e. CC )
64	2 3 63	mp3an23	\|- ( A e. CC -> ( A / _i ) e. CC )
65		picn	\|- _pi e. CC
66		pire	\|- _pi e. RR
67		pipos	\|- 0 < _pi
68	66 67	gt0ne0ii	\|- _pi =/= 0
69	65 68	pm3.2i	\|- ( _pi e. CC /\ _pi =/= 0 )
70		divdiv1	\|- ( ( ( A / _i ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( _pi e. CC /\ _pi =/= 0 ) ) -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
71	58 69 70	mp3an23	\|- ( ( A / _i ) e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
72	64 71	syl	\|- ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( ( A / _i ) / ( 2 x. _pi ) ) )
73	30 65	mulcli	\|- ( 2 x. _pi ) e. CC
74	30 65 32 68	mulne0i	\|- ( 2 x. _pi ) =/= 0
75	73 74	pm3.2i	\|- ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 )
76		divdiv1	\|- ( ( A e. CC /\ ( _i e. CC /\ _i =/= 0 ) /\ ( ( 2 x. _pi ) e. CC /\ ( 2 x. _pi ) =/= 0 ) ) -> ( ( A / _i ) / ( 2 x. _pi ) ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
77	59 75 76	mp3an23	\|- ( A e. CC -> ( ( A / _i ) / ( 2 x. _pi ) ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
78	72 77	eqtrd	\|- ( A e. CC -> ( ( ( A / _i ) / 2 ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
79	62 78	eqtrd	\|- ( A e. CC -> ( ( ( A / 2 ) / _i ) / _pi ) = ( A / ( _i x. ( 2 x. _pi ) ) ) )
80	79	eleq1d	\|- ( A e. CC -> ( ( ( ( A / 2 ) / _i ) / _pi ) e. ZZ <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )
81	8 57 80	3bitr3d	\|- ( A e. CC -> ( ( exp ` A ) = 1 <-> ( A / ( _i x. ( 2 x. _pi ) ) ) e. ZZ ) )

Metamath Proof Explorer

Theorem efeq1

Proof