Metamath Proof Explorer

Theorem itsclc0yqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0yqsol.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itsclc0yqsol 
|- ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itsclc0yqsol.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
3 eqid 
 |-  -u ( 2 x. ( B x. C ) ) = -u ( 2 x. ( B x. C ) )
4 eqid 
 |-  ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
5 1 3 4 itsclc0yqe 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
6 5 3adant1r 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
7 6 3adant2r 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 ) )
8 3simpa 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ B e. RR ) )
9 8 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( A e. RR /\ B e. RR ) )
10 1 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
11 9 10 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> Q e. RR )
12 11 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q e. RR )
13 12 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q e. CC )
14 simpr1 
 |-  ( ( A =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> A e. RR )
15 simpl 
 |-  ( ( A =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> A =/= 0 )
16 simpr2 
 |-  ( ( A =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> B e. RR )
17 1 resum2sqgt0 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> 0 < Q )
18 14 15 16 17 syl21anc 
 |-  ( ( A =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> 0 < Q )
19 18 ex 
 |-  ( A =/= 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> 0 < Q ) )
20 simpr2 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> B e. RR )
21 simpl 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> B =/= 0 )
22 simpr1 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> A e. RR )
23 eqid 
 |-  ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) )
24 23 resum2sqgt0 
 |-  ( ( ( B e. RR /\ B =/= 0 ) /\ A e. RR ) -> 0 < ( ( B ^ 2 ) + ( A ^ 2 ) ) )
25 20 21 22 24 syl21anc 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> 0 < ( ( B ^ 2 ) + ( A ^ 2 ) ) )
26 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. RR )
27 26 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
28 27 sqcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A ^ 2 ) e. CC )
29 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
30 29 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
31 30 sqcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) e. CC )
32 28 31 addcomd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
33 32 adantl 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
34 1 33 eqtrid 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> Q = ( ( B ^ 2 ) + ( A ^ 2 ) ) )
35 25 34 breqtrrd 
 |-  ( ( B =/= 0 /\ ( A e. RR /\ B e. RR /\ C e. RR ) ) -> 0 < Q )
36 35 ex 
 |-  ( B =/= 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> 0 < Q ) )
37 19 36 jaoi 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> 0 < Q ) )
38 37 impcom 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q )
39 38 gt0ne0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> Q =/= 0 )
40 39 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q =/= 0 )
41 2cnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> 2 e. CC )
42 recn 
 |-  ( B e. RR -> B e. CC )
43 42 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
44 43 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> B e. CC )
45 44 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. CC )
46 recn 
 |-  ( C e. RR -> C e. CC )
47 46 3ad2ant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> C e. CC )
48 47 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> C e. CC )
49 48 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> C e. CC )
50 45 49 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. C ) e. CC )
51 41 50 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( B x. C ) ) e. CC )
52 51 negcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> -u ( 2 x. ( B x. C ) ) e. CC )
53 49 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( C ^ 2 ) e. CC )
54 recn 
 |-  ( A e. RR -> A e. CC )
55 54 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> A e. CC )
56 55 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> A e. CC )
57 56 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. CC )
58 57 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A ^ 2 ) e. CC )
59 simpl 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR+ )
60 59 rpcnd 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. CC )
61 60 3ad2ant2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> R e. CC )
62 61 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( R ^ 2 ) e. CC )
63 58 62 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( A ^ 2 ) x. ( R ^ 2 ) ) e. CC )
64 53 63 subcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
65 recn 
 |-  ( Y e. RR -> Y e. CC )
66 65 adantl 
 |-  ( ( X e. RR /\ Y e. RR ) -> Y e. CC )
67 66 3ad2ant3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Y e. CC )
68 eqidd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) = ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) )
69 13 40 52 64 67 68 quad 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 <-> ( Y = ( ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) \/ Y = ( ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) ) ) )
70 54 abscld 
 |-  ( A e. RR -> ( abs ` A ) e. RR )
71 70 recnd 
 |-  ( A e. RR -> ( abs ` A ) e. CC )
72 71 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( abs ` A ) e. CC )
73 72 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( abs ` A ) e. CC )
74 73 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( abs ` A ) e. CC )
75 59 rpred 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR )
76 75 3ad2ant2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> R e. RR )
77 76 resqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( R ^ 2 ) e. RR )
78 77 12 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( R ^ 2 ) x. Q ) e. RR )
79 simp1l3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> C e. RR )
80 79 resqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( C ^ 2 ) e. RR )
81 78 80 resubcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. RR )
82 2 81 eqeltrid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> D e. RR )
83 82 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> D e. CC )
84 83 sqrtcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( sqrt ` D ) e. CC )
85 41 74 84 mulassd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) = ( 2 x. ( ( abs ` A ) x. ( sqrt ` D ) ) ) )
86 85 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( B x. C ) ) + ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) ) = ( ( 2 x. ( B x. C ) ) + ( 2 x. ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
87 51 negnegd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> -u -u ( 2 x. ( B x. C ) ) = ( 2 x. ( B x. C ) ) )
88 simpl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
89 88 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
90 simp2r 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> 0 <_ D )
91 1 3 4 2 itsclc0yqsollem2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR /\ 0 <_ D ) -> ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) = ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) )
92 89 76 90 91 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) = ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) )
93 87 92 oveq12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( ( 2 x. ( B x. C ) ) + ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) ) )
94 74 84 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( abs ` A ) x. ( sqrt ` D ) ) e. CC )
95 41 50 94 adddid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) = ( ( 2 x. ( B x. C ) ) + ( 2 x. ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
96 86 93 95 3eqtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( 2 x. ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
97 96 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) = ( ( 2 x. ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) / ( 2 x. Q ) ) )
98 50 94 addcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) e. CC )
99 2ne0 
 |-  2 =/= 0
100 99 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> 2 =/= 0 )
101 98 13 41 40 100 divcan5d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) / ( 2 x. Q ) ) = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) )
102 97 101 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) )
103 102 eqeq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Y = ( ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) <-> Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) )
104 85 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( B x. C ) ) - ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) ) = ( ( 2 x. ( B x. C ) ) - ( 2 x. ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
105 87 92 oveq12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( ( 2 x. ( B x. C ) ) - ( ( 2 x. ( abs ` A ) ) x. ( sqrt ` D ) ) ) )
106 41 50 94 subdid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) = ( ( 2 x. ( B x. C ) ) - ( 2 x. ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
107 104 105 106 3eqtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) = ( 2 x. ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) )
108 107 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) = ( ( 2 x. ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) / ( 2 x. Q ) ) )
109 50 94 subcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) e. CC )
110 109 13 41 40 100 divcan5d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) ) / ( 2 x. Q ) ) = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) )
111 108 110 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) )
112 111 eqeq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Y = ( ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) <-> Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) )
113 103 112 orbi12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Y = ( ( -u -u ( 2 x. ( B x. C ) ) + ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) \/ Y = ( ( -u -u ( 2 x. ( B x. C ) ) - ( sqrt ` ( ( -u ( 2 x. ( B x. C ) ) ^ 2 ) - ( 4 x. ( Q x. ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) ) ) ) / ( 2 x. Q ) ) ) <-> ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) ) )
114 69 113 bitrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 <-> ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) ) )
115 absid 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( abs ` A ) = A )
116 115 ex 
 |-  ( A e. RR -> ( 0 <_ A -> ( abs ` A ) = A ) )
117 116 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 0 <_ A -> ( abs ` A ) = A ) )
118 117 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( 0 <_ A -> ( abs ` A ) = A ) )
119 118 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( 0 <_ A -> ( abs ` A ) = A ) )
120 119 impcom 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( abs ` A ) = A )
121 120 oveq1d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( abs ` A ) x. ( sqrt ` D ) ) = ( A x. ( sqrt ` D ) ) )
122 121 oveq2d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) )
123 122 oveq1d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) )
124 123 eqeq2d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
125 121 oveq2d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) )
126 125 oveq1d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) )
127 126 eqeq2d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
128 124 127 orbi12d 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) <-> ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
129 pm1.4 
 |-  ( ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
130 128 129 biimtrdi 
 |-  ( ( 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
131 50 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( B x. C ) e. CC )
132 94 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( abs ` A ) x. ( sqrt ` D ) ) e. CC )
133 131 132 subnegd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) - -u ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) )
134 74 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( abs ` A ) e. CC )
135 84 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( sqrt ` D ) e. CC )
136 134 135 mulneg1d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( -u ( abs ` A ) x. ( sqrt ` D ) ) = -u ( ( abs ` A ) x. ( sqrt ` D ) ) )
137 89 simp1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. RR )
138 137 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> A e. RR )
139 id 
 |-  ( A e. RR -> A e. RR )
140 0red 
 |-  ( A e. RR -> 0 e. RR )
141 139 140 ltnled 
 |-  ( A e. RR -> ( A < 0 <-> -. 0 <_ A ) )
142 ltle 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 -> A <_ 0 ) )
143 140 142 mpdan 
 |-  ( A e. RR -> ( A < 0 -> A <_ 0 ) )
144 141 143 sylbird 
 |-  ( A e. RR -> ( -. 0 <_ A -> A <_ 0 ) )
145 144 3ad2ant1 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( -. 0 <_ A -> A <_ 0 ) )
146 145 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( -. 0 <_ A -> A <_ 0 ) )
147 146 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( -. 0 <_ A -> A <_ 0 ) )
148 147 impcom 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> A <_ 0 )
149 138 148 absnidd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( abs ` A ) = -u A )
150 149 negeqd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> -u ( abs ` A ) = -u -u A )
151 57 adantl 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> A e. CC )
152 151 negnegd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> -u -u A = A )
153 150 152 eqtrd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> -u ( abs ` A ) = A )
154 153 oveq1d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( -u ( abs ` A ) x. ( sqrt ` D ) ) = ( A x. ( sqrt ` D ) ) )
155 136 154 eqtr3d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> -u ( ( abs ` A ) x. ( sqrt ` D ) ) = ( A x. ( sqrt ` D ) ) )
156 155 oveq2d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) - -u ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) )
157 133 156 eqtr3d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) )
158 157 oveq1d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) )
159 158 eqeq2d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
160 131 132 negsubd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) + -u ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) )
161 155 oveq2d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) + -u ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) )
162 160 161 eqtr3d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) = ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) )
163 162 oveq1d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) )
164 163 eqeq2d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
165 159 164 orbi12d 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) <-> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
166 165 biimpd 
 |-  ( ( -. 0 <_ A /\ ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
167 130 166 pm2.61ian 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Y = ( ( ( B x. C ) + ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) - ( ( abs ` A ) x. ( sqrt ` D ) ) ) / Q ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
168 114 167 sylbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) = 0 -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
169 7 168 syld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )