Theorem efifolem3 8639

Description: Lemma for efifo 8644.

Assertion

Ref	Expression
efifolem3	|- ((X e. RR /\ Y e. RR /\ A e. (0(,)(2 x. pi))) -> ((((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 efifolem3

Step	Hyp	Ref	Expression
1		opreq1 3953	. . . . . 6 |- (X = if(X e. RR, X, 0) -> (X^2) = (if(X e. RR, X, 0)^2))
2	1	opreq1d 3960	. . . . 5 |- (X = if(X e. RR, X, 0) -> ((X^2) + (Y^2)) = ((if(X e. RR, X, 0)^2) + (Y^2)))
3	2	eqeq1d 1475	. . . 4 |- (X = if(X e. RR, X, 0) -> (((X^2) + (Y^2)) = 1 <-> ((if(X e. RR, X, 0)^2) + (Y^2)) = 1))
4		eqeq1 1473	. . . 4 |- (X = if(X e. RR, X, 0) -> (X = (cos` A) <-> if(X e. RR, X, 0) = (cos` A)))
5	3, 4	anbi12d 626	. . 3 |- (X = if(X e. RR, X, 0) -> ((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) <-> (((if(X e. RR, X, 0)^2) + (Y^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A))))
6		eqeq1 1473	. . . . 5 |- (X = if(X e. RR, X, 0) -> (X = (cos` a) <-> if(X e. RR, X, 0) = (cos` a)))
7	6	anbi1d 615	. . . 4 |- (X = if(X e. RR, X, 0) -> ((X = (cos` a) /\ Y = (sin` a)) <-> (if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a))))
8	7	rexbidv 1656	. . 3 |- (X = if(X e. RR, X, 0) -> (E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)) <-> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a))))
9	5, 8	imbi12d 624	. 2 |- (X = if(X e. RR, X, 0) -> (((((X^2) + (Y^2)) = 1 /\ X = (cos` A)) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))) <-> ((((if(X e. RR, X, 0)^2) + (Y^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) -> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a)))))
10		opreq1 3953	. . . . . 6 |- (Y = if(Y e. RR, Y, 0) -> (Y^2) = (if(Y e. RR, Y, 0)^2))
11	10	opreq2d 3961	. . . . 5 |- (Y = if(Y e. RR, Y, 0) -> ((if(X e. RR, X, 0)^2) + (Y^2)) = ((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)))
12	11	eqeq1d 1475	. . . 4 |- (Y = if(Y e. RR, Y, 0) -> (((if(X e. RR, X, 0)^2) + (Y^2)) = 1 <-> ((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1))
13	12	anbi1d 615	. . 3 |- (Y = if(Y e. RR, Y, 0) -> ((((if(X e. RR, X, 0)^2) + (Y^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) <-> (((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A))))
14		eqeq1 1473	. . . . 5 |- (Y = if(Y e. RR, Y, 0) -> (Y = (sin` a) <-> if(Y e. RR, Y, 0) = (sin` a)))
15	14	anbi2d 614	. . . 4 |- (Y = if(Y e. RR, Y, 0) -> ((if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a)) <-> (if(X e. RR, X, 0) = (cos` a) /\ if(Y e. RR, Y, 0) = (sin` a))))
16	15	rexbidv 1656	. . 3 |- (Y = if(Y e. RR, Y, 0) -> (E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a)) <-> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ if(Y e. RR, Y, 0) = (sin` a))))
17	13, 16	imbi12d 624	. 2 |- (Y = if(Y e. RR, Y, 0) -> (((((if(X e. RR, X, 0)^2) + (Y^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) -> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ Y = (sin` a))) <-> ((((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) -> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ if(Y e. RR, Y, 0) = (sin` a)))))
18		fveq2 3709	. . . . 5 |- (A = if(A e. (0(,)(2 x. pi)), A, pi) -> (cos` A) = (cos` if(A e. (0(,)(2 x. pi)), A, pi)))
19	18	eqeq2d 1478	. . . 4 |- (A = if(A e. (0(,)(2 x. pi)), A, pi) -> (if(X e. RR, X, 0) = (cos` A) <-> if(X e. RR, X, 0) = (cos` if(A e. (0(,)(2 x. pi)), A, pi))))
20	19	anbi2d 614	. . 3 |- (A = if(A e. (0(,)(2 x. pi)), A, pi) -> ((((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) <-> (((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` if(A e. (0(,)(2 x. pi)), A, pi)))))
21	20	imbi1d 611	. 2 |- (A = if(A e. (0(,)(2 x. pi)), A, pi) -> (((((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` A)) -> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ if(Y e. RR, Y, 0) = (sin` a))) <-> ((((if(X e. RR, X, 0)^2) + (if(Y e. RR, Y, 0)^2)) = 1 /\ if(X e. RR, X, 0) = (cos` if(A e. (0(,)(2 x. pi)), A, pi))) -> E.a e. (0(,)(2 x. pi))(if(X e. RR, X, 0) = (cos` a) /\ if(Y e. RR, Y, 0) = (sin` a)))))
22		pire 8596	. . . . 5 |- pi e. RR
23		pipos 8597	. . . . 5 |- 0 < pi
24	22	recn 5286	. . . . . . 7 |- pi e. CC
25	24	mulid2 5305	. . . . . 6 |- (1 x. pi) = pi
26		1lt2 5975	. . . . . . 7 |- 1 < 2
27		1re 5407	. . . . . . . 8 |- 1 e. RR
28		2re 5926	. . . . . . . 8 |- 2 e. RR
29	27, 28, 22, 23	ltmul1i 5777	. . . . . . 7 |- (1 < 2 <-> (1 x. pi) < (2 x. pi))
30	26, 29	mpbi 189	. . . . . 6 |- (1 x. pi) < (2 x. pi)
31	25, 30	eqbrtrr 2626	. . . . 5 |- pi < (2 x. pi)
32		0re 5412	. . . . . . 7 |- 0 e. RR
33	28, 22	remulcl 5307	. . . . . . 7 |- (2 x. pi) e. RR
34		elioo2t 6316	. . . . . . . 8 |- ((0 e. RR* /\ (2 x. pi) e. RR*) -> (pi e. (0(,)(2 x. pi)) <-> (pi e. RR /\ 0 < pi /\ pi < (2 x. pi))))
35		rexrt 5471	. . . . . . . 8 |- (0 e. RR -> 0 e. RR*)
36		rexrt 5471	. . . . . . . 8 |- ((2 x. pi) e. RR -> (2 x. pi) e. RR*)
37	34, 35, 36	syl2an 454	. . . . . . 7 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (pi e. (0(,)(2 x. pi