Theorem efifolem4 8659

Description: Lemma for efifo 8663.

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		1re 5415	. . . . . . . 8 |- 1 e. RR
2	1	renegcl 5396	. . . . . . 7 |- -u1 e. RR
3		elioo2t 6324	. . . . . . . 8 |- ((-u1 e. RR* /\ 1 e. RR*) -> (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1)))
4		rexrt 5479	. . . . . . . 8 |- (-u1 e. RR -> -u1 e. RR*)
5		rexrt 5479	. . . . . . . 8 |- (1 e. RR -> 1 e. RR*)
6	3, 4, 5	syl2an 454	. . . . . . 7 |- ((-u1 e. RR /\ 1 e. RR) -> (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1)))
7	2, 1, 6	mp2an 696	. . . . . 6 |- (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1))
8	7	biimp 151	. . . . 5 |- (X e. (-u1(,)1) -> (X e. RR /\ -u1 < X /\ X < 1))
9	8	3simp1d 793	. . . 4 |- (X e. (-u1(,)1) -> X e. RR)
10		efifolem3 8658	. . . . . . . . . . . 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))))
11	10	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)))))
12	11	3expia 834	. . . . . . . . . 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))))))
13	12	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))))))
14	13	3impia 829	. . . . . . . 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)))))
15	14	r19.23adv 1743	. . . . . . 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))))
16		eqid 1473	. . . . . . . . 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, < )
17	16	efifolem1 8656	. . . . . . . 8 |- (X e. (-u1(,)1) -> E.z e. (0(,)pi)X = (cos` z))
18		0re 5420	. . . . . . . . . 10 |- 0 e. RR
19		pire 8615	. . . . . . . . . 10 |- pi e. RR
20		2re 5934	. . . . . . . . . . 11 |- 2 e. RR
21	20, 19	remulcl 5315	. . . . . . . . . 10 |- (2 x. pi) e. RR
22	19	recn 5294	. . . . . . . . . . . . . 14 |- pi e. CC
23	22	mulid2 5313	. . . . . . . . . . . . 13 |- (1 x. pi) = pi
24		1lt2 5983	. . . . . . . . . . . . . . 15 |- 1 < 2
25	1, 20, 24	ltlei 5562	. . . . . . . . . . . . . 14 |- 1 <_ 2
26		pipos 8616	. . . . . . . . . . . . . . 15 |- 0 < pi
27	1, 20, 19	lemul1 5799	. . . . . . . . . . . . . . 15 |- (0 < pi -> (1 <_ 2 <-> (1 x. pi) <_ (2 x. pi)))
28	26, 27	ax-mp 7	. . . . . . . . . . . . . 14 |- (1 <_ 2 <-> (1 x. pi) <_ (2 x. pi))
29	25, 28	mpbi 189	. . . . . . . . . . . . 13 |- (1 x. pi) <_ (2 x. pi)
30	23, 29	eqbrtrr 2631	. . . . . . . . . . . 12 |- pi <_ (2 x. pi)
31		iooss2 6319	. . . . . . . . . . . 12 |- (((0 e. RR* /\ pi e. RR* /\ (2 x. pi) e. RR*) /\ pi <_ (2 x. pi)) -> (0(,)pi) (_ (0(,)(2 x. pi)))
32	30, 31	mpan2 695	. . . . . . . . . . 11 |- ((0 e. RR* /\ pi e. RR* /\ (2 x. pi) e. RR*) -> (0(,)pi) (_ (0(,)(2 x. pi)))
33		rexrt 5479	. . . . . . . . . . 11 |- (0 e. RR -> 0 e. RR*)
34		rexrt 5479	. . . . . . . . . . 11 |- (pi e. RR -> pi e. RR*)
35		rexrt 5479	. . . . . . . . . . 11 |- ((2 x. pi) e. RR -> (2 x. pi) e. RR*)
36	32, 33, 34, 35	syl3an 867	. . . . . . . . . 10 |- ((0 e. RR /\ pi e. RR /\ (2 x. pi) e. RR) -> (0(,)pi) (_ (0(,)(2 x. pi)))
37	18, 19, 21, 36	mp3an 914	. . . . . . . . 9 |- (0(,)pi) (_ (0(,)(2 x. pi))
38		ssrexv 2111	. . . . . . . . 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)))
39	37, 38	ax-mp 7	. . . . . . . 8 |- (E.z e. (0(,)pi)X = (cos` z) -> E.z e. (0(,)(2 x. pi))X = (cos` z))
40	17, 39	syl 10	. . . . . . 7 |- (X e. (-u1(,)1) -> E.z e. (0(,)(2 x. pi))X = (cos` z))
41	15, 40	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))))
42	41	3expib 835	. . . . 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)))))
43	42	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)))))
44	9, 43	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))))
45	44	3impib 830	. 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)))
46		ltlet 5501	. . . . . . . . 9 |- ((0 e. RR /\ z e. RR) -> (0 < z -> 0 <_ z))
47	18, 46	mpan 694	. . . . . . . 8 |- (z e. RR -> (0 < z -> 0 <_ z))
48	47	imdistani 443	. . . . . . 7 |- ((z e. RR /\ 0 < z) -> (z e. RR /\ 0 <_ z))
49	48	anim1i 334	. . . . . 6 |- (((z e. RR /\ 0 < z) /\ z < (2 x. pi)) -> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
50	49	3impa 827	. . . . 5 |- ((z e. RR /\ 0 < z /\ z < (2 x. pi)) -> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
51		elioo2t 6324	. . . . . . 7 |- ((0 e. RR* /\ (2 x. pi) e. RR*) -> (z e. (0(,)(2 x. pi)) <-> (z e. RR /\ 0 < z /\ z < (2 x. pi))))
52	51, 33, 35	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))))
53	18, 21, 52	mp2an 696	. . . . 5 |- (z e. (0(,)(2 x. pi)) <-> (z e. RR /\ 0 < z /\ z < (2 x. pi)))
54		elico2t 6331	. . . . . . 7 |- ((0 e. RR /\ (2 x. pi) e. RR) -> (z e. (0[,)(2 x. pi)) <-> (z e. RR /\ 0 <_ z /\ z < (2 x. pi))))
55	18, 21, 54	mp2an 696	. . . . . 6 |- (z e. (0[,)(2 x. pi)) <-> (z e. RR /\ 0 <_ z /\ z < (2 x. pi)))
56		df-3an 776	. . . . . 6 |- ((z e. RR /\ 0 <_ z /\ z < (2 x. pi)) <-> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
57	55, 56	bitr 173	. . . . 5 |- (z e. (0[,)(2 x. pi)) <-> ((z e. RR /\ 0 <_ z) /\ z < (2 x. pi)))
58	50, 53, 57	3imtr4 219	. . . 4 |- (z e. (0(,)(2 x. pi)) -> z e. (0[,)(2 x. pi)))
59	58	ssriv 2065	. . 3 |- (0(,)(2 x. pi)) (_ (0[,)(2 x. pi))
60		ssrexv 2111	. . 3 |- ((0(,)(2 x. pi)) (_ (0[,)(2 x. pi)) -> (E.a e. (0(,)(2