Metamath Proof Explorer

Theorem itschlc0xyqsol1

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0yqsol.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itschlc0xyqsol1 
|- ( ( ( ( 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 = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itsclc0yqsol.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
3 animorr 
 |-  ( ( A = 0 /\ B =/= 0 ) -> ( A =/= 0 \/ B =/= 0 ) )
4 3 anim2i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) )
5 1 2 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 ) ) ) )
6 4 5 syl3an1 
 |-  ( ( ( ( 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 ) ) ) )
7 6 imp 
 |-  ( ( ( ( ( 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 ) ) )
8 oveq1 
 |-  ( A = 0 -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
9 8 adantr 
 |-  ( ( A = 0 /\ B =/= 0 ) -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
10 9 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
11 10 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
12 rpcn 
 |-  ( R e. RR+ -> R e. CC )
13 12 adantr 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. CC )
14 13 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> R e. CC )
15 14 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( R ^ 2 ) e. CC )
16 1 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
17 16 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. CC )
18 17 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. CC )
19 18 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> Q e. CC )
20 19 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. CC )
21 15 20 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( R ^ 2 ) x. Q ) e. CC )
22 simpll3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. RR )
23 22 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. CC )
24 23 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( C ^ 2 ) e. CC )
25 21 24 subcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. CC )
26 2 25 eqeltrid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. CC )
27 26 sqrtcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( sqrt ` D ) e. CC )
28 27 mul02d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 0 x. ( sqrt ` D ) ) = 0 )
29 11 28 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) = 0 )
30 29 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) = ( ( B x. C ) - 0 ) )
31 simpll2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. RR )
32 31 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. CC )
33 32 23 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. C ) e. CC )
34 33 subid1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) - 0 ) = ( B x. C ) )
35 30 34 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) = ( B x. C ) )
36 sq0i 
 |-  ( A = 0 -> ( A ^ 2 ) = 0 )
37 36 adantr 
 |-  ( ( A = 0 /\ B =/= 0 ) -> ( A ^ 2 ) = 0 )
38 37 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( A ^ 2 ) = 0 )
39 38 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A ^ 2 ) = 0 )
40 39 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 0 + ( B ^ 2 ) ) )
41 32 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) e. CC )
42 41 addid2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 0 + ( B ^ 2 ) ) = ( B ^ 2 ) )
43 40 42 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( B ^ 2 ) )
44 1 43 syl5eq 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q = ( B ^ 2 ) )
45 recn 
 |-  ( B e. RR -> B e. CC )
46 45 sqvald 
 |-  ( B e. RR -> ( B ^ 2 ) = ( B x. B ) )
47 46 3ad2ant2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) = ( B x. B ) )
48 47 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( B ^ 2 ) = ( B x. B ) )
49 48 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) = ( B x. B ) )
50 44 49 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q = ( B x. B ) )
51 35 50 oveq12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) = ( ( B x. C ) / ( B x. B ) ) )
52 simplrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B =/= 0 )
53 23 32 32 52 52 divcan5d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) / ( B x. B ) ) = ( C / B ) )
54 51 53 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) = ( C / B ) )
55 54 eqeq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( C / B ) ) )
56 55 biimpd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> Y = ( C / B ) ) )
57 29 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) = ( ( B x. C ) + 0 ) )
58 33 addid1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) + 0 ) = ( B x. C ) )
59 57 58 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) = ( B x. C ) )
60 59 44 oveq12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) = ( ( B x. C ) / ( B ^ 2 ) ) )
61 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
62 61 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
63 62 sqvald 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) = ( B x. B ) )
64 63 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( B ^ 2 ) = ( B x. B ) )
65 64 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( B x. C ) / ( B ^ 2 ) ) = ( ( B x. C ) / ( B x. B ) ) )
66 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> C e. RR )
67 66 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> C e. CC )
68 62 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> B e. CC )
69 simpr 
 |-  ( ( A = 0 /\ B =/= 0 ) -> B =/= 0 )
70 69 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> B =/= 0 )
71 67 68 68 70 70 divcan5d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( B x. C ) / ( B x. B ) ) = ( C / B ) )
72 65 71 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( B x. C ) / ( B ^ 2 ) ) = ( C / B ) )
73 72 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. C ) / ( B ^ 2 ) ) = ( C / B ) )
74 60 73 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) = ( C / B ) )
75 74 eqeq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) <-> Y = ( C / B ) ) )
76 75 biimpd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> Y = ( C / B ) ) )
77 56 76 jaod 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> Y = ( C / B ) ) )
78 77 3adant3 
 |-  ( ( ( ( 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 ) - ( A x. ( sqrt ` D ) ) ) / Q ) \/ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> Y = ( C / B ) ) )
79 78 adantr 
 |-  ( ( ( ( ( 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 ) ) -> Y = ( C / B ) ) )
80 oveq1 
 |-  ( Y = ( C / B ) -> ( Y ^ 2 ) = ( ( C / B ) ^ 2 ) )
81 80 oveq2d 
 |-  ( Y = ( C / B ) -> ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( ( X ^ 2 ) + ( ( C / B ) ^ 2 ) ) )
82 81 eqeq1d 
 |-  ( Y = ( C / B ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) <-> ( ( X ^ 2 ) + ( ( C / B ) ^ 2 ) ) = ( R ^ 2 ) ) )
83 15 3adant3 
 |-  ( ( ( ( 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 )
84 23 3adant3 
 |-  ( ( ( ( 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 )
85 32 3adant3 
 |-  ( ( ( ( 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 )
86 simp1rr 
 |-  ( ( ( ( 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 =/= 0 )
87 84 85 86 divcld 
 |-  ( ( ( ( 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 / B ) e. CC )
88 87 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 / B ) ^ 2 ) e. CC )
89 simp3l 
 |-  ( ( ( ( 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 e. RR )
90 89 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 ) ) -> X e. CC )
91 90 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 ) ) -> ( X ^ 2 ) e. CC )
92 83 88 91 subadd2d 
 |-  ( ( ( ( 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 ) - ( ( C / B ) ^ 2 ) ) = ( X ^ 2 ) <-> ( ( X ^ 2 ) + ( ( C / B ) ^ 2 ) ) = ( R ^ 2 ) ) )
93 23 32 52 sqdivd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( C / B ) ^ 2 ) = ( ( C ^ 2 ) / ( B ^ 2 ) ) )
94 93 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( R ^ 2 ) - ( ( C / B ) ^ 2 ) ) = ( ( R ^ 2 ) - ( ( C ^ 2 ) / ( B ^ 2 ) ) ) )
95 31 resqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) e. RR )
96 31 52 sqgt0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 0 < ( B ^ 2 ) )
97 95 96 elrpd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) e. RR+ )
98 97 rpcnne0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) e. CC /\ ( B ^ 2 ) =/= 0 ) )
99 subdivcomb1 
 |-  ( ( ( R ^ 2 ) e. CC /\ ( C ^ 2 ) e. CC /\ ( ( B ^ 2 ) e. CC /\ ( B ^ 2 ) =/= 0 ) ) -> ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( ( R ^ 2 ) - ( ( C ^ 2 ) / ( B ^ 2 ) ) ) )
100 15 24 98 99 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( ( R ^ 2 ) - ( ( C ^ 2 ) / ( B ^ 2 ) ) ) )
101 94 100 eqtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( R ^ 2 ) - ( ( C / B ) ^ 2 ) ) = ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) )
102 101 eqeq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( R ^ 2 ) - ( ( C / B ) ^ 2 ) ) = ( X ^ 2 ) <-> ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) ) )
103 102 3adant3 
 |-  ( ( ( ( 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 ) - ( ( C / B ) ^ 2 ) ) = ( X ^ 2 ) <-> ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) ) )
104 41 3adant3 
 |-  ( ( ( ( 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 ^ 2 ) e. CC )
105 104 83 mulcomd 
 |-  ( ( ( ( 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 ^ 2 ) x. ( R ^ 2 ) ) = ( ( R ^ 2 ) x. ( B ^ 2 ) ) )
106 44 3adant3 
 |-  ( ( ( ( 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 = ( B ^ 2 ) )
107 106 eqcomd 
 |-  ( ( ( ( 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 ^ 2 ) = Q )
108 107 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 ) ) -> ( ( R ^ 2 ) x. ( B ^ 2 ) ) = ( ( R ^ 2 ) x. Q ) )
109 105 108 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 ) ) -> ( ( B ^ 2 ) x. ( R ^ 2 ) ) = ( ( R ^ 2 ) x. Q ) )
110 109 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 ) ) -> ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) )
111 110 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 ) ) -> ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) )
112 111 eqeq1d 
 |-  ( ( ( ( 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 ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) <-> ( ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) ) )
113 2 oveq1i 
 |-  ( D / ( B ^ 2 ) ) = ( ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) / ( B ^ 2 ) )
114 113 eqeq1i 
 |-  ( ( D / ( B ^ 2 ) ) = ( X ^ 2 ) <-> ( ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) )
115 eqcom 
 |-  ( ( D / ( B ^ 2 ) ) = ( X ^ 2 ) <-> ( X ^ 2 ) = ( D / ( B ^ 2 ) ) )
116 26 3adant3 
 |-  ( ( ( ( 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 )
117 sqrtth 
 |-  ( D e. CC -> ( ( sqrt ` D ) ^ 2 ) = D )
118 117 eqcomd 
 |-  ( D e. CC -> D = ( ( sqrt ` D ) ^ 2 ) )
119 116 118 syl 
 |-  ( ( ( ( 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 = ( ( sqrt ` D ) ^ 2 ) )
120 119 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 ) ) -> ( D / ( B ^ 2 ) ) = ( ( ( sqrt ` D ) ^ 2 ) / ( B ^ 2 ) ) )
121 27 3adant3 
 |-  ( ( ( ( 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 )
122 121 85 86 sqdivd 
 |-  ( ( ( ( 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 ) / B ) ^ 2 ) = ( ( ( sqrt ` D ) ^ 2 ) / ( B ^ 2 ) ) )
123 120 122 eqtr4d 
 |-  ( ( ( ( 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 / ( B ^ 2 ) ) = ( ( ( sqrt ` D ) / B ) ^ 2 ) )
124 123 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 ) ) -> ( ( X ^ 2 ) = ( D / ( B ^ 2 ) ) <-> ( X ^ 2 ) = ( ( ( sqrt ` D ) / B ) ^ 2 ) ) )
125 121 85 86 divcld 
 |-  ( ( ( ( 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 ) / B ) e. CC )
126 90 125 jca 
 |-  ( ( ( ( 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 e. CC /\ ( ( sqrt ` D ) / B ) e. CC ) )
127 sqeqor 
 |-  ( ( X e. CC /\ ( ( sqrt ` D ) / B ) e. CC ) -> ( ( X ^ 2 ) = ( ( ( sqrt ` D ) / B ) ^ 2 ) <-> ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) ) )
128 126 127 syl 
 |-  ( ( ( ( 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 ) = ( ( ( sqrt ` D ) / B ) ^ 2 ) <-> ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) ) )
129 orcom 
 |-  ( ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) <-> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) )
130 129 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 ) ) -> ( ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) <-> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
131 124 128 130 3bitrd 
 |-  ( ( ( ( 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 ) = ( D / ( B ^ 2 ) ) <-> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
132 131 biimpd 
 |-  ( ( ( ( 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 ) = ( D / ( B ^ 2 ) ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
133 115 132 syl5bi 
 |-  ( ( ( ( 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 / ( B ^ 2 ) ) = ( X ^ 2 ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
134 114 133 syl5bir 
 |-  ( ( ( ( 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 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
135 112 134 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 ) ) -> ( ( ( ( ( B ^ 2 ) x. ( R ^ 2 ) ) - ( C ^ 2 ) ) / ( B ^ 2 ) ) = ( X ^ 2 ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
136 103 135 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 ) ) -> ( ( ( R ^ 2 ) - ( ( C / B ) ^ 2 ) ) = ( X ^ 2 ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
137 92 136 sylbird 
 |-  ( ( ( ( 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 ) + ( ( C / B ) ^ 2 ) ) = ( R ^ 2 ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
138 137 com12 
 |-  ( ( ( X ^ 2 ) + ( ( C / B ) ^ 2 ) ) = ( R ^ 2 ) -> ( ( ( ( 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 = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
139 82 138 syl6bi 
 |-  ( Y = ( C / B ) -> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) -> ( ( ( ( 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 = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )
140 139 com13 
 |-  ( ( ( ( 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 ) -> ( Y = ( C / B ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )
141 140 adantrd 
 |-  ( ( ( ( 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 = ( C / B ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )
142 141 imp 
 |-  ( ( ( ( ( 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 = ( C / B ) -> ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
143 142 ancld 
 |-  ( ( ( ( ( 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 = ( C / B ) -> ( Y = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )
144 79 143 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 ) ) -> ( Y = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )
145 7 144 mpd 
 |-  ( ( ( ( ( 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 = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) )
146 145 ex 
 |-  ( ( ( ( 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 = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) ) )