Theorem efif1lem5 8734

Description: Lemma for efif1 8737.

Hypotheses

Ref	Expression
efif1lem5.1	|- A e. (0[,)pi)
efif1lem5.2	|- B e. (pi[,)(2 x. pi))

Assertion

Ref	Expression
efif1lem5	|- -. (exp` (i x. A)) = (exp` (i x. B))

Proof of Theorem efif1lem5

Step	Hyp	Ref	Expression
1		efif1lem5.1	. . . 4 |- A e. (0[,)pi)
2		0re 5440	. . . . . . 7 |- 0 e. RR
3		pire 8677	. . . . . . 7 |- pi e. RR
4		pipos 8678	. . . . . . 7 |- 0 < pi
5		snunioo 6415	. . . . . . 7 |- ((0 e. RR /\ pi e. RR /\ 0 < pi) -> ({0} u. (0(,)pi)) = (0[,)pi))
6	2, 3, 4, 5	mp3an 916	. . . . . 6 |- ({0} u. (0(,)pi)) = (0[,)pi)
7	6	eleq2i 1538	. . . . 5 |- (A e. ({0} u. (0(,)pi)) <-> A e. (0[,)pi))
8		elun 2173	. . . . 5 |- (A e. ({0} u. (0(,)pi)) <-> (A e. {0} \/ A e. (0(,)pi)))
9	7, 8	bitr3 175	. . . 4 |- (A e. (0[,)pi) <-> (A e. {0} \/ A e. (0(,)pi)))
10	1, 9	mpbi 189	. . 3 |- (A e. {0} \/ A e. (0(,)pi))
11		elsnc2g 2436	. . . . 5 |- (0 e. RR -> (A e. {0} <-> A = 0))
12	2, 11	ax-mp 7	. . . 4 |- (A e. {0} <-> A = 0)
13	12	orbi1i 256	. . 3 |- ((A e. {0} \/ A e. (0(,)pi)) <-> (A = 0 \/ A e. (0(,)pi)))
14	10, 13	mpbi 189	. 2 |- (A = 0 \/ A e. (0(,)pi))
15		efif1lem5.2	. . . 4 |- B e. (pi[,)(2 x. pi))
16		2re 5979	. . . . . . . 8 |- 2 e. RR
17	16, 3	remulcl 5335	. . . . . . 7 |- (2 x. pi) e. RR
18		1lt2 6028	. . . . . . . 8 |- 1 < 2
19		ltmulgt12t 5847	. . . . . . . . 9 |- ((pi e. RR /\ 2 e. RR /\ 0 < pi) -> (1 < 2 <-> pi < (2 x. pi)))
20	3, 16, 4, 19	mp3an 916	. . . . . . . 8 |- (1 < 2 <-> pi < (2 x. pi))
21	18, 20	mpbi 189	. . . . . . 7 |- pi < (2 x. pi)
22		snunioo 6415	. . . . . . 7 |- ((pi e. RR /\ (2 x. pi) e. RR /\ pi < (2 x. pi)) -> ({pi} u. (pi(,)(2 x. pi))) = (pi[,)(2 x. pi)))
23	3, 17, 21, 22	mp3an 916	. . . . . 6 |- ({pi} u. (pi(,)(2 x. pi))) = (pi[,)(2 x. pi))
24	23	eleq2i 1538	. . . . 5 |- (B e. ({pi} u. (pi(,)(2 x. pi))) <-> B e. (pi[,)(2 x. pi)))
25		elun 2173	. . . . 5 |- (B e. ({pi} u. (pi(,)(2 x. pi))) <-> (B e. {pi} \/ B e. (pi(,)(2 x. pi))))
26	24, 25	bitr3 175	. . . 4 |- (B e. (pi[,)(2 x. pi)) <-> (B e. {pi} \/ B e. (pi(,)(2 x. pi))))
27	15, 26	mpbi 189	. . 3 |- (B e. {pi} \/ B e. (pi(,)(2 x. pi)))
28		elsnc2g 2436	. . . . 5 |- (pi e. RR -> (B e. {pi} <-> B = pi))
29	3, 28	ax-mp 7	. . . 4 |- (B e. {pi} <-> B = pi)
30	29	orbi1i 256	. . 3 |- ((B e. {pi} \/ B e. (pi(,)(2 x. pi))) <-> (B = pi \/ B e. (pi(,)(2 x. pi))))
31	27, 30	mpbi 189	. 2 |- (B = pi \/ B e. (pi(,)(2 x. pi)))
32		ax1ne0 5280	. . . . . 6 |- 1 =/= 0
33		df-ne 1587	. . . . . 6 |- (1 =/= 0 <-> -. 1 = 0)
34	32, 33	mpbi 189	. . . . 5 |- -. 1 = 0
35		fveq2 3724	. . . . . . . 8 |- (A = 0 -> (cos` A) = (cos` 0))
36		cos0 7446	. . . . . . . 8 |- (cos` 0) = 1
37	35, 36	syl6eq 1523	. . . . . . 7 |- (A = 0 -> (cos` A) = 1)
38		fveq2 3724	. . . . . . . 8 |- (B = pi -> (cos` B) = (cos` pi))
39		cospi 8682	. . . . . . . 8 |- (cos` pi) = -u1
40	38, 39	syl6eq 1523	. . . . . . 7 |- (B = pi -> (cos` B) = -u1)
41	37, 40	eqeqan12d 1490	. . . . . 6 |- ((A = 0 /\ B = pi) -> ((cos` A) = (cos` B) <-> 1 = -u1))
42		ax1cn 5269	. . . . . . 7 |- 1 e. CC
43	42	eqneg 5804	. . . . . 6 |- (1 = -u1 <-> 1 = 0)
44	41, 43	syl6bb 536	. . . . 5 |- ((A = 0 /\ B = pi) -> ((cos` A) = (cos` B) <-> 1 = 0))
45	34, 44	mtbiri 717	. . . 4 |- ((A = 0 /\ B = pi) -> -. (cos` A) = (cos` B))
46		orc 269	. . . . . 6 |- (-. (cos` A) = (cos` B) -> (-. (cos` A) = (cos` B) \/ -. (sin` A) = (sin` B)))
47		ianor 305	. . . . . 6 |- (-. ((cos` A) = (cos` B) /\ (sin` A) = (sin` B)) <-> (-. (cos` A) = (cos` B) \/ -. (sin` A) = (sin` B)))
48	46, 47	sylibr 200	. . . . 5 |- (-. (cos` A) = (cos` B) -> -. ((cos` A) = (cos` B) /\ (sin` A) = (sin` B)))
49		elico2t 6391	. . . . . . . . . 10 |- ((0 e. RR /\ pi e. RR) -> (A e. (0[,)pi) <-> (A e. RR /\ 0 <_ A /\ A < pi)))
50	2, 3, 49	mp2an 697	. . . . . . . . 9 |- (A e. (0[,)pi) <-> (A e. RR /\ 0 <_ A /\ A < pi))
51	1, 50	mpbi 189	. . . . . . . 8 |- (A e. RR /\ 0 <_ A /\ A < pi)
52	51	3simp1i 791	. . . . . . 7 |- A e. RR
53		elico2t 6391	. . . . . . . . . 10 |- ((pi e. RR /\ (2 x. pi) e. RR) -> (B e. (pi[,)(2 x. pi)) <-> (B e. RR /\ pi <_ B /\ B < (2 x. pi))))
54	3, 17, 53	mp2an 697	. . . . . . . . 9 |- (B e. (pi[,)(2 x. pi)) <-> (B e. RR /\ pi <_ B /\ B < (2 x. pi)))
55	15, 54	mpbi 189	. . . . . . . 8 |- (B e. RR /\ pi <_ B /\ B < (2 x. pi))
56	55	3simp1i 791	. . . . . . 7 |- B e. RR
57		efieq 7450	. . . . . . 7 |- ((A e. RR /\ B e. RR) -> ((exp` (i x. A)) = (exp` (i x. B)) <-> ((cos` A) = (cos` B) /\ (sin` A) = (sin` B))))
58	52, 56, 57	mp2an 697	. . . . . 6 |- ((exp` (i x. A)) = (exp` (i x. B)) <-> ((cos` A) = (cos` B) /\ (sin` A) = (sin` B)))
59	58	negbii 187	. . . . 5 |- (-. (exp` (i x. A)) = (exp` (i x. B)) <-> -. ((cos` A) = (cos` B) /\ (sin` A) = (sin` B)))
60	48, 59	sylibr 200	. . . 4 |- (-. (cos` A) = (cos` B) -> -. (exp` (i x. A)) = (exp` (i x. B)))
61	45, 60	syl 10	. . 3 |- ((A = 0 /\ B = pi) -> -. (exp` (i x. A)) = (exp` (i x. B)))
62		sinq12gt0t 8708	. . . . . . . 8 |- (A e. (0(,)pi) -> 0 < (sin` A))
63		resinclt 7438	. . . . . . . . . 10 |- (A e. RR -> (sin` A) e. RR)
64	52, 63	ax-mp 7	. . . . . . . . 9 |- (sin` A) e. RR
65	64	gt0ne0 5611	. . . . . . . 8 |- (0 < (sin` A) -> (sin` A) =/= 0)
66	62, 65	syl 10	. . . . . . 7 |- (A e. (0(,)pi) -> (sin` A) =/= 0)
67		df-ne 1587	. . . . . . 7 |- ((sin` A) =/= 0 <-> -. (sin` A) = 0)
68	66, 67	sylib 198	. . . . . 6 |- (A e. (0(,)pi) -> -. (sin` A) = 0)
69	68	adantr 389	. . . . 5 |- ((A e. (0(,)pi) /\ B = pi) -> -. (sin` A) = 0)
70		eqtrt 1492	. . . . . . 7 |- (((sin` A) = (sin` B) /\ (sin` B) = 0) -> (sin` A) = 0)
71		fveq2 3724	. . . . . . . . 9 |- (B = pi -> (sin` B) = (sin` pi))
72		sinpi 8676	. . . . . . . . 9 |- (sin` pi) = 0
73	71, 72	syl6eq 1523	. . . . . . . 8 |- (B = pi -> (sin` B) = 0)
74	73	adantl 388	. . . . . . 7 |- ((A e. (0(,)pi) /\ B = pi) -> (sin` B) = 0)
75	70, 74	sylan2 451	. . . . . 6 |- (((sin` A) = (sin` B) /\ (A e. (0(,)pi) /\ B = pi)) -> (sin` A) = 0)
76	75	expcom 374	. . . . 5 |- ((A e. (0(,)pi) /\ B = pi) -> ((sin` A) = (sin` B) -> (sin` A) = 0))
77	69, 76	mtod 108	. . . 4 |- ((A e. (0(,)pi) /\ B = pi) -> -. (sin` A) = (sin` B))
78		olc 268	. . . . . 6 |- (-. (sin` A) = (sin` B) -> (-. (cos` A) = (cos` B) \/ -. (sin` A) = (sin` B)))
79	78, 47	sylibr 200	. . . . 5 |- (-. (sin` A) = (sin` B) -> -. ((cos` A) = (cos` B) /\ (sin` A) = (sin` B)))
80	79, 59	sylibr 200	. . . 4 |- (-. (sin` A) = (sin` B) -> -. (exp` (i x. A)) = (exp` (i x. B)))
81	77, 80	syl 10	. . 3 |- ((A e. (0(,)pi) /\ B = pi) -> -. (exp` (i x. A)) = (exp` (i x. B)))
82		efif1lem1 8730	. . . . . . . . . 10 |- (B e. (pi(,)(2 x. pi)) -> (B - pi) e. (0(,)pi))
83		sinq12gt0t 8708	. . . . . . . . . 10 |- ((B - pi) e. (0(,)pi) -> 0