Metamath Proof Explorer

Theorem itscnhlc0xyqsol

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

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0yqsol.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itscnhlc0xyqsol 
|- ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B 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 simpl 
 |-  ( ( A e. RR /\ A =/= 0 ) -> A e. RR )
4 3 3anim1i 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
5 simpr 
 |-  ( ( A e. RR /\ A =/= 0 ) -> A =/= 0 )
6 5 3ad2ant1 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> A =/= 0 )
7 6 orcd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( A =/= 0 \/ B =/= 0 ) )
8 4 7 jca 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) )
9 8 3anim1i 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) )
10 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 ) ) ) )
11 9 10 syl 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) ) ) )
12 11 imp 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) ) )
13 oveq2 
 |-  ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( B x. Y ) = ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
14 13 oveq2d 
 |-  ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( A x. X ) + ( B x. Y ) ) = ( ( A x. X ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
15 14 eqeq1d 
 |-  ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> ( ( A x. X ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
16 simp12 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. RR )
17 16 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> B e. CC )
18 simp13 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> C e. RR )
19 18 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> C e. CC )
20 17 19 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. C ) e. CC )
21 simp11l 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. RR )
22 21 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> A e. CC )
23 rpre 
 |-  ( R e. RR+ -> R e. RR )
24 23 adantr 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR )
25 24 adantl 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> R e. RR )
26 25 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( R ^ 2 ) e. RR )
27 simp1l 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> A e. RR )
28 simp2 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> B e. RR )
29 1 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
30 27 28 29 syl2anc 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> Q e. RR )
31 30 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. RR )
32 26 31 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( R ^ 2 ) x. Q ) e. RR )
33 simpl3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. RR )
34 33 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( C ^ 2 ) e. RR )
35 32 34 resubcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. RR )
36 2 35 eqeltrid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. RR )
37 36 3adant3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> D e. RR )
38 37 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> D e. CC )
39 38 sqrtcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( sqrt ` D ) e. CC )
40 22 39 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A x. ( sqrt ` D ) ) e. CC )
41 20 40 subcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) e. CC )
42 30 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q e. RR )
43 42 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q e. CC )
44 1 resum2sqgt0 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR ) -> 0 < Q )
45 44 3adant3 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> 0 < Q )
46 45 gt0ne0d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> Q =/= 0 )
47 46 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> Q =/= 0 )
48 17 41 43 47 divassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
49 48 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) = ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) )
50 49 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( A x. X ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = ( ( A x. X ) + ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) )
51 19 43 47 divcan3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Q x. C ) / Q ) = C )
52 51 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> C = ( ( Q x. C ) / Q ) )
53 50 52 eqeq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C <-> ( ( A x. X ) + ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) ) )
54 43 19 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Q x. C ) e. CC )
55 17 41 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) e. CC )
56 54 55 43 47 divsubdird 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) )
57 56 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) )
58 57 eqeq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( A x. X ) <-> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) ) )
59 54 43 47 divcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Q x. C ) / Q ) e. CC )
60 55 43 47 divcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) e. CC )
61 simp3l 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> X e. RR )
62 61 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> X e. CC )
63 22 62 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( A x. X ) e. CC )
64 59 60 63 subadd2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( A x. X ) <-> ( ( A x. X ) + ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) ) )
65 eqcom 
 |-  ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) )
66 65 a1i 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) ) )
67 54 55 subcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) e. CC )
68 67 43 47 divcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) e. CC )
69 simp11r 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> A =/= 0 )
70 68 62 22 69 divmul2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) ) )
71 67 43 22 47 69 divdiv1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) )
72 71 eqeq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
73 66 70 72 3bitr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
74 58 64 73 3bitr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
75 53 74 bitrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
76 15 75 sylan9bbr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
77 1 oveq1i 
 |-  ( Q x. C ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. C )
78 27 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> A e. CC )
79 78 sqcld 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( A ^ 2 ) e. CC )
80 28 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> B e. CC )
81 80 sqcld 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) e. CC )
82 simp3 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> C e. RR )
83 82 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> C e. CC )
84 79 81 83 adddird 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. C ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
85 77 84 syl5eq 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( Q x. C ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
86 85 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q x. C ) = ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) )
87 80 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. CC )
88 33 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. CC )
89 87 88 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. C ) e. CC )
90 78 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. CC )
91 36 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. CC )
92 91 sqrtcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( sqrt ` D ) e. CC )
93 90 92 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) e. CC )
94 87 89 93 subdid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) = ( ( B x. ( B x. C ) ) - ( B x. ( A x. ( sqrt ` D ) ) ) ) )
95 80 80 83 mulassd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( B x. B ) x. C ) = ( B x. ( B x. C ) ) )
96 recn 
 |-  ( B e. RR -> B e. CC )
97 96 sqvald 
 |-  ( B e. RR -> ( B ^ 2 ) = ( B x. B ) )
98 97 3ad2ant2 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) = ( B x. B ) )
99 98 eqcomd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( B x. B ) = ( B ^ 2 ) )
100 99 oveq1d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( B x. B ) x. C ) = ( ( B ^ 2 ) x. C ) )
101 95 100 eqtr3d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( B x. ( B x. C ) ) = ( ( B ^ 2 ) x. C ) )
102 101 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( B x. C ) ) = ( ( B ^ 2 ) x. C ) )
103 87 90 92 mul12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( A x. ( sqrt ` D ) ) ) = ( A x. ( B x. ( sqrt ` D ) ) ) )
104 102 103 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( B x. C ) ) - ( B x. ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
105 94 104 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
106 86 105 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) ) )
107 90 sqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A ^ 2 ) e. CC )
108 107 88 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. C ) e. CC )
109 87 sqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B ^ 2 ) e. CC )
110 109 88 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B ^ 2 ) x. C ) e. CC )
111 108 110 addcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) = ( ( ( B ^ 2 ) x. C ) + ( ( A ^ 2 ) x. C ) ) )
112 111 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( ( B ^ 2 ) x. C ) + ( ( A ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) ) )
113 87 92 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( sqrt ` D ) ) e. CC )
114 90 113 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( B x. ( sqrt ` D ) ) ) e. CC )
115 110 108 114 pnncand 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B ^ 2 ) x. C ) + ( ( A ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
116 106 112 115 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
117 116 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) = ( ( ( ( A ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( Q x. A ) ) )
118 78 sqvald 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( A ^ 2 ) = ( A x. A ) )
119 118 oveq1d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( A ^ 2 ) x. C ) = ( ( A x. A ) x. C ) )
120 78 78 83 mulassd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( A x. A ) x. C ) = ( A x. ( A x. C ) ) )
121 119 120 eqtrd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( A ^ 2 ) x. C ) = ( A x. ( A x. C ) ) )
122 121 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A ^ 2 ) x. C ) = ( A x. ( A x. C ) ) )
123 122 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
124 31 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. CC )
125 124 90 mulcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q x. A ) = ( A x. Q ) )
126 123 125 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( Q x. A ) ) = ( ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) )
127 90 88 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) e. CC )
128 90 127 113 adddid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
129 128 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) )
130 129 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) )
131 127 113 addcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) e. CC )
132 46 adantr 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q =/= 0 )
133 simpl1r 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A =/= 0 )
134 131 124 90 132 133 divcan5d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) )
135 130 134 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. ( A x. C ) ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) )
136 117 126 135 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) )
137 136 eqeq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) <-> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
138 137 biimpd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
139 138 3adant3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
140 139 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
141 76 140 sylbid 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
142 141 ex 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
143 142 com23 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> ( Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
144 143 adantld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
145 144 imp 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
146 145 ancrd 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
147 oveq2 
 |-  ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( B x. Y ) = ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
148 147 oveq2d 
 |-  ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( A x. X ) + ( B x. Y ) ) = ( ( A x. X ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
149 148 eqeq1d 
 |-  ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> ( ( A x. X ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C ) )
150 20 40 addcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) e. CC )
151 17 150 43 47 divassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) = ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
152 151 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) = ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) )
153 152 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( A x. X ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = ( ( A x. X ) + ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) )
154 153 52 eqeq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C <-> ( ( A x. X ) + ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) ) )
155 17 150 mulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) e. CC )
156 54 155 43 47 divsubdird 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) )
157 156 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) )
158 157 eqeq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( A x. X ) <-> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) ) )
159 155 43 47 divcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) e. CC )
160 59 159 63 subadd2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) / Q ) - ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( A x. X ) <-> ( ( A x. X ) + ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) ) )
161 eqcom 
 |-  ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) )
162 161 a1i 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) ) )
163 54 155 subcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) e. CC )
164 163 43 47 divcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) e. CC )
165 164 62 22 69 divmul2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = X <-> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) ) )
166 163 43 22 47 69 divdiv1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) )
167 166 eqeq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( X = ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) / A ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
168 162 165 167 3bitr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / Q ) = ( A x. X ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
169 158 160 168 3bitr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) / Q ) ) = ( ( Q x. C ) / Q ) <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
170 154 169 bitrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) = C <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
171 149 170 sylan9bbr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) ) )
172 87 89 93 adddid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) = ( ( B x. ( B x. C ) ) + ( B x. ( A x. ( sqrt ` D ) ) ) ) )
173 102 103 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( B x. C ) ) + ( B x. ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
174 172 173 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) = ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) )
175 86 174 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) ) )
176 111 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) + ( ( B ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( ( B ^ 2 ) x. C ) + ( ( A ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) ) )
177 110 108 114 pnpcand 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( B ^ 2 ) x. C ) + ( ( A ^ 2 ) x. C ) ) - ( ( ( B ^ 2 ) x. C ) + ( A x. ( B x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
178 175 176 177 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) = ( ( ( A ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
179 178 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) = ( ( ( ( A ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( Q x. A ) ) )
180 122 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
181 180 125 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( ( A ^ 2 ) x. C ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( Q x. A ) ) = ( ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) )
182 90 127 113 subdid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) = ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) )
183 182 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) = ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) )
184 183 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) )
185 127 113 subcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) e. CC )
186 185 124 90 132 133 divcan5d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) )
187 184 186 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. ( A x. C ) ) - ( A x. ( B x. ( sqrt ` D ) ) ) ) / ( A x. Q ) ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) )
188 179 181 187 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) )
189 188 eqeq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) <-> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
190 189 biimpd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
191 190 3adant3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
192 191 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( X = ( ( ( Q x. C ) - ( B x. ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) ) ) / ( Q x. A ) ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
193 171 192 sylbid 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
194 193 ex 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
195 194 com23 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( A x. X ) + ( B x. Y ) ) = C -> ( Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
196 195 adantld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) ) )
197 196 imp 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
198 197 ancrd 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) -> ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
199 146 198 orim12d 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( 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 ) ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )
200 12 199 mpd 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) /\ ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
201 200 ex 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )