Theorem efifolem5 8726

Description: Lemma for efifo 8729.

Assertion

Ref	Expression
efifolem5	|- ((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 efifolem5

Step	Hyp	Ref	Expression
1		ax1cn 5269	. . . . . . . . . 10 |- 1 e. CC
2		subaddt 5375	. . . . . . . . . 10 |- ((1 e. CC /\ (X^2) e. CC /\ (Y^2) e. CC) -> ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1))
3	1, 2	mp3an1 903	. . . . . . . . 9 |- (((X^2) e. CC /\ (Y^2) e. CC) -> ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1))
4		recnt 5313	. . . . . . . . 9 |- ((X^2) e. RR -> (X^2) e. CC)
5		recnt 5313	. . . . . . . . 9 |- ((Y^2) e. RR -> (Y^2) e. CC)
6	3, 4, 5	syl2an 454	. . . . . . . 8 |- (((X^2) e. RR /\ (Y^2) e. RR) -> ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1))
7		resqclt 6621	. . . . . . . 8 |- (X e. RR -> (X^2) e. RR)
8		resqclt 6621	. . . . . . . 8 |- (Y e. RR -> (Y^2) e. RR)
9	6, 7, 8	syl2an 454	. . . . . . 7 |- ((X e. RR /\ Y e. RR) -> ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1))
10	9	3adant3 799	. . . . . 6 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> ((1 - (X^2)) = (Y^2) <-> ((X^2) + (Y^2)) = 1))
11		breq2 2623	. . . . . . . . . 10 |- ((1 - (X^2)) = (Y^2) -> (0 < (1 - (X^2)) <-> 0 < (Y^2)))
12		sqgt0t 6622	. . . . . . . . . 10 |- ((Y e. RR /\ Y =/= 0) -> 0 < (Y^2))
13	11, 12	syl5cbir 211	. . . . . . . . 9 |- ((Y e. RR /\ Y =/= 0) -> ((1 - (X^2)) = (Y^2) -> 0 < (1 - (X^2))))
14	13	3adant1 797	. . . . . . . 8 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> ((1 - (X^2)) = (Y^2) -> 0 < (1 - (X^2))))
15		3simp1 788	. . . . . . . 8 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> X e. RR)
16	14, 15	jctild 601	. . . . . . 7 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> ((1 - (X^2)) = (Y^2) -> (X e. RR /\ 0 < (1 - (X^2)))))
17		1re 5435	. . . . . . . . . . . 12 |- 1 e. RR
18		posdift 5654	. . . . . . . . . . . 12 |- (((X^2) e. RR /\ 1 e. RR) -> ((X^2) < 1 <-> 0 < (1 - (X^2))))
19	17, 18	mpan2 696	. . . . . . . . . . 11 |- ((X^2) e. RR -> ((X^2) < 1 <-> 0 < (1 - (X^2))))
20	7, 19	syl 10	. . . . . . . . . 10 |- (X e. RR -> ((X^2) < 1 <-> 0 < (1 - (X^2))))
21	20	biimprd 154	. . . . . . . . 9 |- (X e. RR -> (0 < (1 - (X^2)) -> (X^2) < 1))
22	21	imdistani 443	. . . . . . . 8 |- ((X e. RR /\ 0 < (1 - (X^2))) -> (X e. RR /\ (X^2) < 1))
23		recnt 5313	. . . . . . . . . . . 12 |- (X e. RR -> X e. CC)
24		0re 5440	. . . . . . . . . . . . . . . 16 |- 0 e. RR
25		lt01 5680	. . . . . . . . . . . . . . . 16 |- 0 < 1
26	24, 17, 25	ltlei 5581	. . . . . . . . . . . . . . 15 |- 0 <_ 1
27	17, 26	pm3.2i 285	. . . . . . . . . . . . . 14 |- (1 e. RR /\ 0 <_ 1)
28		lt2sqt 6630	. . . . . . . . . . . . . 14 |- ((((abs` X) e. RR /\ 0 <_ (abs` X)) /\ (1 e. RR /\ 0 <_ 1)) -> ((abs` X) < 1 <-> ((abs` X)^2) < (1^2)))
29	27, 28	mpan2 696	. . . . . . . . . . . . 13 |- (((abs` X) e. RR /\ 0 <_ (abs` X)) -> ((abs` X) < 1 <-> ((abs` X)^2) < (1^2)))
30		absclt 6833	. . . . . . . . . . . . 13 |- (X e. CC -> (abs` X) e. RR)
31		absge0t 6854	. . . . . . . . . . . . 13 |- (X e. CC -> 0 <_ (abs` X))
32	29, 30, 31	sylanc 471	. . . . . . . . . . . 12 |- (X e. CC -> ((abs` X) < 1 <-> ((abs` X)^2) < (1^2)))
33	23, 32	syl 10	. . . . . . . . . . 11 |- (X e. RR -> ((abs` X) < 1 <-> ((abs` X)^2) < (1^2)))
34		absltt 6880	. . . . . . . . . . . 12 |- ((X e. RR /\ 1 e. RR) -> ((abs` X) < 1 <-> (-u1 < X /\ X < 1)))
35	17, 34	mpan2 696	. . . . . . . . . . 11 |- (X e. RR -> ((abs` X) < 1 <-> (-u1 < X /\ X < 1)))
36		absresqt 6867	. . . . . . . . . . . 12 |- (X e. RR -> ((abs` X)^2) = (X^2))
37		sq1 6637	. . . . . . . . . . . . 13 |- (1^2) = 1
38	37	a1i 8	. . . . . . . . . . . 12 |- (X e. RR -> (1^2) = 1)
39	36, 38	breq12d 2631	. . . . . . . . . . 11 |- (X e. RR -> (((abs` X)^2) < (1^2) <-> (X^2) < 1))
40	33, 35, 39	3bitr3rd 549	. . . . . . . . . 10 |- (X e. RR -> ((X^2) < 1 <-> (-u1 < X /\ X < 1)))
41	40	pm5.32i 645	. . . . . . . . 9 |- ((X e. RR /\ (X^2) < 1) <-> (X e. RR /\ (-u1 < X /\ X < 1)))
42	17	renegcl 5416	. . . . . . . . . . . 12 |- -u1 e. RR
43		elioo2t 6379	. . . . . . . . . . . . 13 |- ((-u1 e. RR* /\ 1 e. RR*) -> (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1)))
44		rexrt 5499	. . . . . . . . . . . . 13 |- (-u1 e. RR -> -u1 e. RR*)
45		rexrt 5499	. . . . . . . . . . . . 13 |- (1 e. RR -> 1 e. RR*)
46	43, 44, 45	syl2an 454	. . . . . . . . . . . 12 |- ((-u1 e. RR /\ 1 e. RR) -> (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1)))
47	42, 17, 46	mp2an 697	. . . . . . . . . . 11 |- (X e. (-u1(,)1) <-> (X e. RR /\ -u1 < X /\ X < 1))
48	47	biimpr 152	. . . . . . . . . 10 |- ((X e. RR /\ -u1 < X /\ X < 1) -> X e. (-u1(,)1))
49	48	3expb 834	. . . . . . . . 9 |- ((X e. RR /\ (-u1 < X /\ X < 1)) -> X e. (-u1(,)1))
50	41, 49	sylbi 199	. . . . . . . 8 |- ((X e. RR /\ (X^2) < 1) -> X e. (-u1(,)1))
51	22, 50	syl 10	. . . . . . 7 |- ((X e. RR /\ 0 < (1 - (X^2))) -> X e. (-u1(,)1))
52	16, 51	syl6 22	. . . . . 6 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> ((1 - (X^2)) = (Y^2) -> X e. (-u1(,)1)))
53	10, 52	sylbird 205	. . . . 5 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> (((X^2) + (Y^2)) = 1 -> X e. (-u1(,)1)))
54		efifolem4 8725	. . . . . . . . 9 |- ((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)))
55	54	3expib 836	. . . . . . . 8 |- (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))))
56	55	com12 11	. . . . . . 7 |- ((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))))
57	56	ex 373	. . . . . 6 |- (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)))))
58	57	3ad2ant2 801	. . . . 5 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> (((X^2) + (Y^2)) = 1 -> (X e. (-u1(,)1) -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
59	53, 58	mpdd 46	. . . 4 |- ((X e. RR /\ Y e. RR /\ Y =/= 0) -> (((X^2) + (Y^2)) = 1 -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a))))
60	59	3expia 835	. . 3 |- ((X e. RR /\ Y e. RR) -> (Y =/= 0 -> (((X^2) + (Y^2)) = 1 -> E.a e. (0[,)(2 x. pi))(X = (cos` a) /\ Y = (sin` a)))))
61	60	com23 32	. 2 |- ((X e. RR /\ Y e. RR) -> (((X^2) + (Y^2)) = 1 -> (Y =/= 0 -> E.a e. (0[,