Theorem efifolem2 8718

Description: Lemma for efifo 8724.

Hypotheses

Ref	Expression
efifolem2.1	|- A e. (0(,)(2 x. pi))
efifolem2.2	|- X e. RR
efifolem2.3	|- Y e. RR

Assertion

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

Distinct variable groups:   A,a   X,a   Y,a

Proof of Theorem efifolem2

Step	Hyp	Ref	Expression
1		ax1cn 5281	. . . . . . . . . . 11 |- 1 e. CC
2		efifolem2.2	. . . . . . . . . . . . 13 |- X e. RR
3	2	recn 5326	. . . . . . . . . . . 12 |- X e. CC
4	3	sqcl 6616	. . . . . . . . . . 11 |- (X^2) e. CC
5		efifolem2.3	. . . . . . . . . . . . 13 |- Y e. RR
6	5	recn 5326	. . . . . . . . . . . 12 |- Y e. CC
7	6	sqcl 6616	. . . . . . . . . . 11 |- (Y^2) e. CC
8	1, 4, 7	subadd 5383	. . . . . . . . . 10 |- ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1)
9	8	biimpr 152	. . . . . . . . 9 |- (((X^2) + (Y^2)) = 1 -> (1 - (X^2)) = (Y^2))
10		opreq1 3974	. . . . . . . . . 10 |- (X = (cos` A) -> (X^2) = ((cos` A)^2))
11	10	opreq2d 3982	. . . . . . . . 9 |- (X = (cos` A) -> (1 - (X^2)) = (1 - ((cos` A)^2)))
12	9, 11	sylan9req 1531	. . . . . . . 8 |- ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> (Y^2) = (1 - ((cos` A)^2)))
13		efifolem2.1	. . . . . . . . . . . . 13 |- A e. (0(,)(2 x. pi))
14		0re 5452	. . . . . . . . . . . . . 14 |- 0 e. RR
15		2re 5981	. . . . . . . . . . . . . . 15 |- 2 e. RR
16		pire 8672	. . . . . . . . . . . . . . 15 |- pi e. RR
17	15, 16	remulcl 5347	. . . . . . . . . . . . . 14 |- (2 x. pi) e. RR
18		elioo2t 6380	. . . . . . . . . . . . . . 15 |- ((0 e. RR* /\ (2 x. pi) e. RR*) -> (A e. (0(,)(2 x. pi)) <-> (A e. RR /\ 0 < A /\ A < (2 x. pi))))
19		rexrt 5511	. . . . . . . . . . . . . . 15 |- (0 e. RR -> 0 e. RR*)
20		rexrt 5511	. . . . . . . . . . . . . . 15 |- ((2 x. pi) e. RR -> (2 x. pi) e. RR*)
21	18, 19, 20	syl2an 456	. . . . . . . . . . . . . 14 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (A e. (0(,)(2 x. pi)) <-> (A e. RR /\ 0 < A /\ A < (2 x. pi))))
22	14, 17, 21	mp2an 699	. . . . . . . . . . . . 13 |- (A e. (0(,)(2 x. pi)) <-> (A e. RR /\ 0 < A /\ A < (2 x. pi)))
23	13, 22	mpbi 189	. . . . . . . . . . . 12 |- (A e. RR /\ 0 < A /\ A < (2 x. pi))
24	23	3simp1i 793	. . . . . . . . . . 11 |- A e. RR
25	24	recn 5326	. . . . . . . . . 10 |- A e. CC
26		sincossqt 7461	. . . . . . . . . 10 |- (A e. CC -> (((sin` A)^2) + ((cos` A)^2)) = 1)
27	25, 26	ax-mp 7	. . . . . . . . 9 |- (((sin` A)^2) + ((cos` A)^2)) = 1
28		cosclt 7432	. . . . . . . . . . . 12 |- (A e. CC -> (cos` A) e. CC)
29	25, 28	ax-mp 7	. . . . . . . . . . 11 |- (cos` A) e. CC
30	29	sqcl 6616	. . . . . . . . . 10 |- ((cos` A)^2) e. CC
31		sinclt 7431	. . . . . . . . . . . 12 |- (A e. CC -> (sin` A) e. CC)
32	25, 31	ax-mp 7	. . . . . . . . . . 11 |- (sin` A) e. CC
33	32	sqcl 6616	. . . . . . . . . 10 |- ((sin` A)^2) e. CC
34	1, 30, 33	subadd2 5385	. . . . . . . . 9 |- ((1 - ((cos` A)^2)) = ((sin` A)^2) <-> (((sin` A)^2) + ((cos` A)^2)) = 1)
35	27, 34	mpbir 190	. . . . . . . 8 |- (1 - ((cos` A)^2)) = ((sin` A)^2)
36	12, 35	syl6eq 1526	. . . . . . 7 |- ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> (Y^2) = ((sin` A)^2))
37	6, 32	sqeqor 6648	. . . . . . 7 |- ((Y^2) = ((sin` A)^2) <-> (Y = (sin` A) \/ Y = -u(sin` A)))
38	36, 37	sylib 198	. . . . . 6 |- ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> (Y = (sin` A) \/ Y = -u(sin` A)))
39	38	ex 373	. . . . 5 |- (((X^2) + (Y^2)) = 1 -> (X = (cos` A) -> (Y = (sin` A) \/ Y = -u(sin` A))))
40	39	ancld 298	. . . 4 |- (((X^2) + (Y^2)) = 1 -> (X = (cos` A) -> (X = (cos` A) /\ (Y = (sin` A) \/ Y = -u(sin` A)))))
41	40	imp 350	. . 3 |- ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> (X = (cos` A) /\ (Y = (sin` A) \/ Y = -u(sin` A))))
42		andi 606	. . 3 |- ((X = (cos` A) /\ (Y = (sin` A) \/ Y = -u(sin` A))) <-> ((X = (cos` A) /\ Y = (sin` A)) \/ (X = (cos` A) /\ Y = -u(sin` A))))
43	41, 42	sylib 198	. 2 |- ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> ((X = (cos` A) /\ Y = (sin` A)) \/ (X = (cos` A) /\ Y = -u(sin` A))))
44		fveq2 3730	. . . . . . 7 |- (a = A -> (cos` a) = (cos` A))
45	44	eqeq2d 1489	. . . . . 6 |- (a = A -> (X = (cos` a) <-> X = (cos` A)))
46		fveq2 3730	. . . . . . 7 |- (a = A -> (sin` a) = (sin` A))
47	46	eqeq2d 1489	. . . . . 6 |- (a = A -> (Y = (sin` a) <-> Y = (sin` A)))
48	45, 47	anbi12d 630	. . . . 5 |- (a = A -> ((X = (cos` a) /\ Y = (sin` a)) <-> (X = (cos` A) /\ Y = (sin` A))))
49	48	rcla4ev 1880	. . . 4 |- ((A e. (0(,)(2 x. pi)) /\ (X = (cos` A) /\ Y = (sin` A))) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
50	13, 49	mpan 697	. . 3 |- ((X = (cos` A) /\ Y = (sin` A)) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
51		3ancomb 785	. . . . . . . 8 |- ((A e. RR /\ A < (2 x. pi) /\ 0 < A) <-> (A e. RR /\ 0 < A /\ A < (2 x. pi)))
52	17, 24	resubcl 5451	. . . . . . . . . 10 |- ((2 x. pi) - A) e. RR
53	24, 52	2th 720	. . . . . . . . 9 |- (A e. RR <-> ((2 x. pi) - A) e. RR)
54	24, 17	posdif 5677	. . . . . . . . 9 |- (A < (2 x. pi) <-> 0 < ((2 x. pi) - A))
55		ltsubpost 5665	. . . . . . . . . 10 |- ((A e. RR /\ (2 x. pi) e. RR) -> (0 < A <-> ((2 x. pi) - A) < (2 x. pi)))
56	24, 17, 55	mp2an 699	. . . . . . . . 9 |- (0 < A <-> ((2 x. pi) - A) < (2 x. pi))
57	53, 54, 56	3anbi123i 824	. . . . . . . 8 |- ((A e. RR /\ A < (2 x. pi) /\ 0 < A) <-> (((2 x. pi) - A) e. RR /\ 0 < ((2 x. pi) - A) /\ ((2 x. pi) - A) < (2 x. pi)))
58	51, 57	bitr3 175	. . . . . . 7 |- ((A e. RR /\ 0 < A /\ A < (2 x. pi)) <-> (((2 x. pi) - A) e. RR /\ 0 < ((2 x. pi) - A) /\ ((2 x. pi) - A) < (2 x. pi)))
59		elioo2t 6380	. . . . . . . . 9 |- ((0 e. RR* /\ (2 x. pi) e. RR*) -> (((2 x. pi) - A) e. (0(,)(2 x. pi)) <-> (((2 x. pi) - A) e. RR /\ 0 < ((2 x. pi) - A) /\ ((2 x. pi) - A) < (2 x. pi))))
60	59, 19, 20	syl2an 456	. . . . . . . 8 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (((2 x. pi) - A) e. (0(,)(2 x. pi)) <-> (((2 x. pi) - A) e. RR /\ 0 < ((2 x. pi) - A) /\ ((2 x. pi) - A) < (2 x. pi))))
61	14, 17, 60	mp2an 699	. . . . . . 7 |- (((2 x. pi) - A) e. (0(,)(2 x. pi)) <-> (((2 x. pi) - A) e. RR /\ 0 < ((2 x. pi) - A) /\ ((2 x. pi) - A) < (2 x. pi)))
62	58, 22, 61	3bitr4 183	. . . . . 6 |- (A e. (0(,)(2 x. pi)) <-> ((2 x. pi) - A) e. (0(,)(2 x. pi)))
63	13, 62	mpbi 189	. . . . 5 |- ((2 x. pi) - A) e. (0(,)(2 x. pi))
64		fveq2 3730	. . . . . . . 8 |- (a = ((2 x. pi) - A) -> (cos` a) = (cos` ((2 x. pi) - A)))
65	64	eqeq2d 1489	. . . . . . 7 |- (a = ((2 x. pi) - A) -> (X = (cos` a) <-> X = (cos` ((2 x. pi) - A))))
66		fveq2 3730	. . . . . . . 8 |- (