Theorem efifolem4 8725

Description: Lemma for efifo 8729.

Assertion

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

Distinct variable groups:   X,a   Y,a

Proof of Theorem efifolem4

Step	Hyp	Ref	Expression
1		eliooret 6386	. . . 4 |- (X e. (-u1(,)1) -> X e. RR)
2		efifolem3 8724	. . . . . . . . . . . 12 |- ((X e. RR /\ Y e. RR /\ z e. (0(,)(2 x. pi))) -> ((((X^2) + (Y^2)) = 1 /\ X = (cos` z)) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
3	2	exp3a 375	. . . . . . . . . . 11 |- ((X e. RR /\ Y e. RR /\ z e. (0(,)(2 x. pi))) -> (((X^2) + (Y^2)) = 1 -> (X = (cos` z) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
4	3	3expia 835	. . . . . . . . . 10 |- ((X e. RR /\ Y e. RR) -> (z e. (0(,)(2 x. pi)) -> (((X^2) + (Y^2)) = 1 -> (X = (cos` z) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))))
5	4	com23 32	. . . . . . . . 9 |- ((X e. RR /\ Y e. RR) -> (((X^2) + (Y^2)) = 1 -> (z e. (0(,)(2 x. pi)) -> (X = (cos` z) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))))
6	5	3impia 830	. . . . . . . 8 |- ((X e. RR /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> (z e. (0(,)(2 x. pi)) -> (X = (cos` z) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
7	6	r19.23adv 1746	. . . . . . 7 |- ((X e. RR /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> (E.z e. (0(,)(2 x. pi))X = (cos` z) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
8		eqid 1475	. . . . . . . . 9 |- sup({a e. (0[,]pi) | (cos` a) = if(X e. (-u1(,)1), X, 0)}, RR, < ) = sup({a e. (0[,]pi) | (cos` a) = if(X e. (-u1(,)1), X, 0)}, RR, < )
9	8	efifolem1 8722	. . . . . . . 8 |- (X e. (-u1(,)1) -> E.z e. (0(,)pi)X = (cos` z))
10		0re 5440	. . . . . . . . . 10 |- 0 e. RR
11		pire 8677	. . . . . . . . . 10 |- pi e. RR
12		2re 5979	. . . . . . . . . . 11 |- 2 e. RR
13	12, 11	remulcl 5335	. . . . . . . . . 10 |- (2 x. pi) e. RR
14	11	recn 5314	. . . . . . . . . . . . . 14 |- pi e. CC
15	14	mulid2 5333	. . . . . . . . . . . . 13 |- (1 x. pi) = pi
16		1re 5435	. . . . . . . . . . . . . . 15 |- 1 e. RR
17		1lt2 6028	. . . . . . . . . . . . . . 15 |- 1 < 2
18	16, 12, 17	ltlei 5581	. . . . . . . . . . . . . 14 |- 1 <_ 2
19		pipos 8678	. . . . . . . . . . . . . . 15 |- 0 < pi
20	16, 12, 11	lemul1 5835	. . . . . . . . . . . . . . 15 |- (0 < pi -> (1 <_ 2 <-> (1 x. pi) <_ (2 x. pi)))
21	19, 20	ax-mp 7	. . . . . . . . . . . . . 14 |- (1 <_ 2 <-> (1 x. pi) <_ (2 x. pi))
22	18, 21	mpbi 189	. . . . . . . . . . . . 13 |- (1 x. pi) <_ (2 x. pi)
23	15, 22	eqbrtrr 2636	. . . . . . . . . . . 12 |- pi <_ (2 x. pi)
24		iooss2 6374	. . . . . . . . . . . 12 |- (((0 e. RR* /\ pi e. RR* /\ (2 x. pi) e. RR*) /\ pi <_ (2 x. pi)) -> (0(,)pi) (_ (0(,)(2 x. pi)))
25	23, 24	mpan2 696	. . . . . . . . . . 11 |- ((0 e. RR* /\ pi e. RR* /\ (2 x. pi) e. RR*) -> (0(,)pi) (_ (0(,)(2 x. pi)))
26		rexrt 5499	. . . . . . . . . . 11 |- (0 e. RR -> 0 e. RR*)
27		rexrt 5499	. . . . . . . . . . 11 |- (pi e. RR -> pi e. RR*)
28		rexrt 5499	. . . . . . . . . . 11 |- ((2 x. pi) e. RR -> (2 x. pi) e. RR*)
29	25, 26, 27, 28	syl3an 868	. . . . . . . . . 10 |- ((0 e. RR /\ pi e. RR /\ (2 x. pi) e. RR) -> (0(,)pi) (_ (0(,)(2 x. pi)))
30	10, 11, 13, 29	mp3an 916	. . . . . . . . 9 |- (0(,)pi) (_ (0(,)(2 x. pi))
31		ssrexv 2115	. . . . . . . . 9 |- ((0(,)pi) (_ (0(,)(2 x. pi)) -> (E.z e. (0(,)pi)X = (cos` z) -> E.z e. (0(,)(2 x. pi))X = (cos` z)))
32	30, 31	ax-mp 7	. . . . . . . 8 |- (E.z e. (0(,)pi)X = (cos` z) -> E.z e. (0(,)(2 x. pi))X = (cos` z))
33	9, 32	syl 10	. . . . . . 7 |- (X e. (-u1(,)1) -> E.z e. (0(,)(2 x. pi))X = (cos` z))
34	7, 33	syl5 21	. . . . . 6 |- ((X e. RR /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> (X e. (-u1(,)1) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
35	34	3expib 836	. . . . 5 |- (X e. RR -> ((Y e. RR /\ ((X^2) + (Y^2)) = 1) -> (X e. (-u1(,)1) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
36	35	com3r 35	. . . 4 |- (X e. (-u1(,)1) -> (X e. RR -> ((Y e. RR /\ ((X^2) + (Y^2)) = 1) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
37	1, 36	mpd 26	. . 3 |- (X e. (-u1(,)1) -> ((Y e. RR /\ ((X^2) + (Y^2)) = 1) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
38	37	3impib 831	. 2 |- ((X e. (-u1(,)1) /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> E.a e. (0(,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))
39		ltlet 5520	. . . . . . . . 9 |- ((0 e. RR /\ z e. RR) -> (0 < z -> 0 <_ z))
40	10, 39	mpan 695	. . . . . . . 8 |- (z e. RR -> (0 < z -> 0 <_ z))
41	40	imdistani 443	. . . . . . 7 |- ((z e. RR /\ 0 < z) -> (z e. RR /\ 0 <_ z))
42	41	anim1i 334	. . . . . 6 |- (((z e. RR /\ 0 < z) /\ z < (2 x. pi)) -> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
43	42	3impa 828	. . . . 5 |- ((z e. RR /\ 0 < z /\ z < (2 x. pi)) -> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
44		elioo2t 6379	. . . . . . 7 |- ((0 e. RR* /\ (2 x. pi) e. RR*) -> (z e. (0(,)(2 x. pi)) <-> (z e. RR /\ 0 < z /\ z < (2 x. pi))))
45	44, 26, 28	syl2an 454	. . . . . 6 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (z e. (0(,)(2 x. pi)) <-> (z e. RR /\ 0 < z /\ z < (2 x. pi))))
46	10, 13, 45	mp2an 697	. . . . 5 |- (z e. (0(,)(2 x. pi)) <-> (z e. RR /\ 0 < z /\ z < (2 x. pi)))
47		elico2t 6391	. . . . . . 7 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (z e. (0[,)(2 x. pi)) <-> (z e. RR /\ 0 <_ z /\ z < (2 x. pi))))
48	10, 13, 47	mp2an 697	. . . . . 6 |- (z e. (0[,)(2 x. pi)) <-> (z e. RR /\ 0 <_ z /\ z < (2 x. pi)))
49		df-3an 777	. . . . . 6 |- ((z e. RR /\ 0 <_ z /\ z < (2 x. pi)) <-> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
50	48, 49	bitr 173	. . . . 5 |- (z e. (0[,)(2 x. pi)) <-> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
51	43, 46, 50	3imtr4 219	. . . 4 |- (z e. (0(,)(2 x. pi)) -> z e. (0[,)(2 x. pi)))
52	51	ssriv 2069	. . 3 |- (0(,)(2 x. pi)) (_ (0[,)(2 x. pi))
53		ssrexv 2115	. . 3 |- ((0(,)(2 x. pi)) (_ (0[,)(2 x. pi)) -> (E.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))))
54	52, 53	ax-mp 7	. 2 |- (E.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)))
55	38, 54	syl 10	1 |- ((X e. (-u1(,)1) /\ Y e. RR /\ ((X^2) + (Y^2)) = 1) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))