Theorem efifolem6 8722

Description: Lemma for efifo 8724.

Assertion

Ref	Expression
efifolem6	|- ((X e. RR /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> (Y = 0 -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))

Distinct variable groups:   X,a   Y,a

Proof of Theorem efifolem6

Step	Hyp	Ref	Expression
1		sq0i 6637	. . . . . . . . . . 11 |- (Y = 0 -> (Y^2) = 0)
2	1	opreq2d 3982	. . . . . . . . . 10 |- (Y = 0 -> ((X^2) + (Y^2)) = ((X^2) + 0))
3		recnt 5325	. . . . . . . . . . 11 |- (X e. RR -> X e. CC)
4		sqclt 6612	. . . . . . . . . . 11 |- (X e. CC -> (X^2) e. CC)
5		ax0id 5293	. . . . . . . . . . 11 |- ((X^2) e. CC -> ((X^2) + 0) = (X^2))
6	3, 4, 5	3syl 20	. . . . . . . . . 10 |- (X e. RR -> ((X^2) + 0) = (X^2))
7	2, 6	sylan9eqr 1532	. . . . . . . . 9 |- ((X e. RR /\ Y = 0) -> ((X^2) + (Y^2)) = (X^2))
8	7	eqeq1d 1486	. . . . . . . 8 |- ((X e. RR /\ Y = 0) -> (((X^2) + (Y^2)) = 1 <-> (X^2) = 1))
9		ax1cn 5281	. . . . . . . . . . . 12 |- 1 e. CC
10		sqeqort 6650	. . . . . . . . . . . 12 |- ((X e. CC /\ 1 e. CC) -> ((X^2) = (1^2) <-> (X = 1 \/ X = -u1)))
11	9, 10	mpan2 698	. . . . . . . . . . 11 |- (X e. CC -> ((X^2) = (1^2) <-> (X = 1 \/ X = -u1)))
12	3, 11	syl 10	. . . . . . . . . 10 |- (X e. RR -> ((X^2) = (1^2) <-> (X = 1 \/ X = -u1)))
13		sq1 6638	. . . . . . . . . . 11 |- (1^2) = 1
14	13	eqeq2i 1488	. . . . . . . . . 10 |- ((X^2) = (1^2) <-> (X^2) = 1)
15	12, 14	syl5bbr 536	. . . . . . . . 9 |- (X e. RR -> ((X^2) = 1 <-> (X = 1 \/ X = -u1)))
16	15	adantr 391	. . . . . . . 8 |- ((X e. RR /\ Y = 0) -> ((X^2) = 1 <-> (X = 1 \/ X = -u1)))
17	8, 16	bitrd 530	. . . . . . 7 |- ((X e. RR /\ Y = 0) -> (((X^2) + (Y^2)) = 1 <-> (X = 1 \/ X = -u1)))
18	17	ex 373	. . . . . 6 |- (X e. RR -> (Y = 0 -> (((X^2) + (Y^2)) = 1 <-> (X = 1 \/ X = -u1))))
19	18	pm5.32rd 650	. . . . 5 |- (X e. RR -> ((((X^2) + (Y^2)) = 1 /\ Y = 0) <-> ((X = 1 \/ X = -u1) /\ Y = 0)))
20		0re 5452	. . . . . . . . 9 |- 0 e. RR
21	20	leid 5622	. . . . . . . . 9 |- 0 <_ 0
22		2re 5981	. . . . . . . . . 10 |- 2 e. RR
23		pire 8672	. . . . . . . . . 10 |- pi e. RR
24		2pos 5991	. . . . . . . . . 10 |- 0 < 2
25		pipos 8673	. . . . . . . . . 10 |- 0 < pi
26	22, 23, 24, 25	mulgt0i 5620	. . . . . . . . 9 |- 0 < (2 x. pi)
27	22, 23	remulcl 5347	. . . . . . . . . . 11 |- (2 x. pi) e. RR
28		elico2t 6392	. . . . . . . . . . 11 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (0 e. (0[,)(2 x. pi)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 < (2 x. pi))))
29	20, 27, 28	mp2an 699	. . . . . . . . . 10 |- (0 e. (0[,)(2 x. pi)) <-> (0 e. RR /\ 0 <_ 0 /\ 0 < (2 x. pi)))
30	29	biimpr 152	. . . . . . . . 9 |- ((0 e. RR /\ 0 <_ 0 /\ 0 < (2 x. pi)) -> 0 e. (0[,)(2 x. pi)))
31	20, 21, 26, 30	mp3an 918	. . . . . . . 8 |- 0 e. (0[,)(2 x. pi))
32		fveq2 3730	. . . . . . . . . . 11 |- (a = 0 -> (cos` a) = (cos` 0))
33	32	eqeq2d 1489	. . . . . . . . . 10 |- (a = 0 -> (X = (cos` a) <-> X = (cos` 0)))
34		fveq2 3730	. . . . . . . . . . 11 |- (a = 0 -> (sin` a) = (sin` 0))
35	34	eqeq2d 1489	. . . . . . . . . 10 |- (a = 0 -> (Y = (sin` a) <-> Y = (sin` 0)))
36	33, 35	anbi12d 630	. . . . . . . . 9 |- (a = 0 -> ((X = (cos` a) /\ Y = (sin` a)) <-> (X = (cos` 0) /\ Y = (sin` 0))))
37	36	rcla4ev 1880	. . . . . . . 8 |- ((0 e. (0[,)(2 x. pi)) /\ (X = (cos` 0) /\ Y = (sin` 0))) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
38	31, 37	mpan 697	. . . . . . 7 |- ((X = (cos` 0) /\ Y = (sin` 0)) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
39		cos0 7446	. . . . . . . . 9 |- (cos` 0) = 1
40		eqeq2 1487	. . . . . . . . 9 |- (X = 1 -> ((cos` 0) = X <-> (cos` 0) = 1))
41	39, 40	mpbiri 194	. . . . . . . 8 |- (X = 1 -> (cos` 0) = X)
42	41	eqcomd 1483	. . . . . . 7 |- (X = 1 -> X = (cos` 0))
43		sin0 7444	. . . . . . . . 9 |- (sin` 0) = 0
44		eqeq2 1487	. . . . . . . . 9 |- (Y = 0 -> ((sin` 0) = Y <-> (sin` 0) = 0))
45	43, 44	mpbiri 194	. . . . . . . 8 |- (Y = 0 -> (sin` 0) = Y)
46	45	eqcomd 1483	. . . . . . 7 |- (Y = 0 -> Y = (sin` 0))
47	38, 42, 46	syl2an 456	. . . . . 6 |- ((X = 1 /\ Y = 0) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
48	20, 23, 25	ltlei 5593	. . . . . . . . 9 |- 0 <_ pi
49	23	recn 5326	. . . . . . . . . . 11 |- pi e. CC
50	49	mulid2 5345	. . . . . . . . . 10 |- (1 x. pi) = pi
51		1lt2 6030	. . . . . . . . . . 11 |- 1 < 2
52		1re 5447	. . . . . . . . . . . 12 |- 1 e. RR
53	52, 22, 23, 25	ltmul1i 5823	. . . . . . . . . . 11 |- (1 < 2 <-> (1 x. pi) < (2 x. pi))
54	51, 53	mpbi 189	. . . . . . . . . 10 |- (1 x. pi) < (2 x. pi)
55	50, 54	eqbrtrr 2641	. . . . . . . . 9 |- pi < (2 x. pi)
56		elico2t 6392	. . . . . . . . . . 11 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (pi e. (0[,)(2 x. pi)) <-> (pi e. RR /\ 0 <_ pi /\ pi < (2 x. pi))))
57	20, 27, 56	mp2an 699	. . . . . . . . . 10 |- (pi e. (0[,)(2 x. pi)) <-> (pi e. RR /\ 0 <_ pi /\ pi < (2 x. pi)))
58	57	biimpr 152	. . . . . . . . 9 |- ((pi e. RR /\ 0 <_ pi /\ pi < (2 x. pi)) -> pi e. (0[,)(2 x. pi)))
59	23, 48, 55, 58	mp3an 918	. . . . . . . 8 |- pi e. (0[,)(2 x. pi))
60		fveq2 3730	. . . . . . . . . . 11 |- (a = pi -> (cos` a) = (cos` pi))
61	60	eqeq2d 1489	. . . . . . . . . 10 |- (a = pi -> (X = (cos` a) <-> X = (cos` pi)))
62		fveq2 3730	. . . . . . . . . . 11 |- (a = pi -> (sin` a) = (sin` pi))
63	62	eqeq2d 1489	. . . . . . . . . 10 |- (a = pi -> (Y = (sin` a) <-> Y = (sin` pi)))
64	61, 63	anbi12d 630	. . . . . . . . 9 |- (a = pi -> ((X = (cos` a) /\ Y = (sin` a)) <-> (X = (cos` pi) /\ Y = (sin` pi))))
65	64	rcla4ev 1880	. . . . . . . 8 |- ((pi e. (0[,)(2 x. pi)) /\ (X = (cos` pi) /\ Y = (sin` pi))) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
66	59, 65	mpan 697	. . . . . . 7 |- ((X = (cos` pi) /\ Y = (sin` pi)) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
67		cospi 8677	. . . . . . . . 9 |- (cos` pi) = -u1
68		eqeq2 1487	. . . . . . . . 9 |- (X = -u1 -> ((cos` pi) = X <-> (cos` pi) = -u1))
69	67, 68	mpbiri 194	. . . . . . . 8 |- (X = -u1 -> (cos` pi) = X)
70	69	eqcomd 1483	. . . . . . 7 |- (X = -u1 -> X = (cos` pi))
71		sinpi 8671	. . . . . . . . 9 |- (sin` pi) = 0
72		eqeq2 1487	. . . . . . . . 9 |- (Y = 0 -> ((sin` pi) = Y <-> (sin` pi) = 0))
73	71, 72	mpbiri 194	. . . . . . . 8 |- (Y = 0 -> (sin` pi) = Y)
74	73	eqcomd 1483	. . . . . . 7 |- (Y = 0 -> Y = (sin` pi))
75	66, 70, 74	syl2an 456	. . . . . 6 |- ((X = -u1 /\ Y = 0) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
76	47, 75	jaoian 427	. . . . 5 |- (((X = 1 \/ X = -u1) /\ Y = 0) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
77	19, 76	syl6bi 214	. . . 4 |- (X e. RR -> ((((X^2) + (Y^2)) = 1 /\ Y = 0) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
78	77	3impib 833	. . 3 |- ((X e. RR /\ ((X^2) + (Y^2)) = 1 /\ Y = 0) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
79	78	3expia 837	. 2 |- ((X e. RR /\ ((X^2) + (Y^2)) = 1) -> (Y = 0 -> E.a e. (0[,)(2 x. pi))(X