Metamath Proof Explorer

Theorem itschlc0xyqsol

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, 8-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0yqsol.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itschlc0xyqsol 
|- ( ( ( ( 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 ) -> ( ( 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 1 2 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 ) ) ) ) )
4 orcom 
 |-  ( ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) <-> ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) )
5 oveq1 
 |-  ( A = 0 -> ( A x. C ) = ( 0 x. C ) )
6 5 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( A x. C ) = ( 0 x. C ) )
7 6 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) = ( 0 x. C ) )
8 simpll3 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. RR )
9 8 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. CC )
10 9 mul02d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 0 x. C ) = 0 )
11 7 10 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. C ) = 0 )
12 11 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) = ( 0 + ( B x. ( sqrt ` D ) ) ) )
13 simpll2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. RR )
14 13 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. CC )
15 rpre 
 |-  ( R e. RR+ -> R e. RR )
16 15 adantr 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR )
17 16 recnd 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. CC )
18 17 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> R e. CC )
19 18 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( R ^ 2 ) e. CC )
20 1 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
21 20 recnd 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. CC )
22 21 3adant3 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> Q e. CC )
23 22 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> Q e. CC )
24 23 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. CC )
25 19 24 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 )
26 9 sqcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( C ^ 2 ) e. CC )
27 25 26 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 )
28 2 27 eqeltrid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. CC )
29 28 sqrtcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( sqrt ` D ) e. CC )
30 14 29 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. ( sqrt ` D ) ) e. CC )
31 30 addid2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 0 + ( B x. ( sqrt ` D ) ) ) = ( B x. ( sqrt ` D ) ) )
32 12 31 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) = ( B x. ( sqrt ` D ) ) )
33 32 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) = ( ( B x. ( sqrt ` D ) ) / Q ) )
34 sq0i 
 |-  ( A = 0 -> ( A ^ 2 ) = 0 )
35 34 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( A ^ 2 ) = 0 )
36 35 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 0 + ( B ^ 2 ) ) )
37 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. RR )
38 37 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> B e. CC )
39 38 sqcld 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) e. CC )
40 39 addid2d 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 0 + ( B ^ 2 ) ) = ( B ^ 2 ) )
41 38 sqvald 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B ^ 2 ) = ( B x. B ) )
42 40 41 eqtrd 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( 0 + ( B ^ 2 ) ) = ( B x. B ) )
43 42 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( 0 + ( B ^ 2 ) ) = ( B x. B ) )
44 36 43 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( B x. B ) )
45 1 44 syl5eq 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> Q = ( B x. B ) )
46 45 adantr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q = ( B x. B ) )
47 46 oveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( sqrt ` D ) ) / Q ) = ( ( B x. ( sqrt ` D ) ) / ( B x. B ) ) )
48 simplrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B =/= 0 )
49 29 14 14 48 48 divcan5d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( sqrt ` D ) ) / ( B x. B ) ) = ( ( sqrt ` D ) / B ) )
50 47 49 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. ( sqrt ` D ) ) / Q ) = ( ( sqrt ` D ) / B ) )
51 33 50 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) = ( ( sqrt ` D ) / B ) )
52 51 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 ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) = ( ( sqrt ` D ) / B ) )
53 52 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 ) ) /\ Y = ( C / B ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) = ( ( sqrt ` D ) / B ) )
54 53 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 ) ) /\ Y = ( C / B ) ) -> ( ( sqrt ` D ) / B ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) )
55 54 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 = ( C / B ) ) -> ( X = ( ( sqrt ` D ) / B ) <-> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
56 55 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 ) ) /\ Y = ( C / B ) ) -> ( X = ( ( sqrt ` D ) / B ) -> X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ) )
57 oveq1 
 |-  ( A = 0 -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
58 57 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( A x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
59 58 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 ) ) )
60 29 mul02d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( 0 x. ( sqrt ` D ) ) = 0 )
61 59 60 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A x. ( sqrt ` D ) ) = 0 )
62 61 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 ) )
63 14 9 mulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. C ) e. CC )
64 63 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 ) )
65 62 64 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 ) )
66 65 46 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 ) ) )
67 66 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 x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) = ( ( B x. C ) / ( B x. B ) ) )
68 9 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 )
69 14 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 )
70 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 )
71 68 69 69 70 70 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 ) ) -> ( ( B x. C ) / ( B x. B ) ) = ( C / B ) )
72 67 71 eqtr2d 
 |-  ( ( ( ( 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 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) )
73 72 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 = ( C / B ) <-> Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) )
74 73 biimpa 
 |-  ( ( ( ( ( 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 = ( C / B ) ) -> Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) )
75 56 74 jctird 
 |-  ( ( ( ( ( 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 = ( C / B ) ) -> ( X = ( ( sqrt ` D ) / B ) -> ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
76 14 29 mulneg2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B x. -u ( sqrt ` D ) ) = -u ( B x. ( sqrt ` D ) ) )
77 76 eqcomd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> -u ( B x. ( sqrt ` D ) ) = ( B x. -u ( sqrt ` D ) ) )
78 77 46 oveq12d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( -u ( B x. ( sqrt ` D ) ) / Q ) = ( ( B x. -u ( sqrt ` D ) ) / ( B x. B ) ) )
79 29 negcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> -u ( sqrt ` D ) e. CC )
80 79 14 14 48 48 divcan5d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( B x. -u ( sqrt ` D ) ) / ( B x. B ) ) = ( -u ( sqrt ` D ) / B ) )
81 78 80 eqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( -u ( B x. ( sqrt ` D ) ) / Q ) = ( -u ( sqrt ` D ) / B ) )
82 11 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) = ( 0 - ( B x. ( sqrt ` D ) ) ) )
83 df-neg 
 |-  -u ( B x. ( sqrt ` D ) ) = ( 0 - ( B x. ( sqrt ` D ) ) )
84 82 83 eqtr4di 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) = -u ( B x. ( sqrt ` D ) ) )
85 84 oveq1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) = ( -u ( B x. ( sqrt ` D ) ) / Q ) )
86 29 14 48 divnegd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> -u ( ( sqrt ` D ) / B ) = ( -u ( sqrt ` D ) / B ) )
87 81 85 86 3eqtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) = -u ( ( sqrt ` D ) / B ) )
88 87 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 ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) = -u ( ( sqrt ` D ) / B ) )
89 88 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 ) ) /\ Y = ( C / B ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) = -u ( ( sqrt ` D ) / B ) )
90 89 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 ) ) /\ Y = ( C / B ) ) -> -u ( ( sqrt ` D ) / B ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) )
91 90 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 = ( C / B ) ) -> ( X = -u ( ( sqrt ` D ) / B ) <-> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
92 91 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 ) ) /\ Y = ( C / B ) ) -> ( X = -u ( ( sqrt ` D ) / B ) -> X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ) )
93 58 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 x. ( sqrt ` D ) ) = ( 0 x. ( sqrt ` D ) ) )
94 17 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 )
95 94 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 )
96 23 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. CC )
97 95 96 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 ) ) -> ( ( R ^ 2 ) x. Q ) e. CC )
98 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 )
99 98 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 ) ) -> C e. CC )
100 99 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 )
101 97 100 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 ) ) -> ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) ) e. CC )
102 2 101 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. CC )
103 102 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 )
104 103 mul02d 
 |-  ( ( ( ( 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 x. ( sqrt ` D ) ) = 0 )
105 93 104 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 ) ) -> ( A x. ( sqrt ` D ) ) = 0 )
106 105 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 ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) = ( ( B x. C ) + 0 ) )
107 simp1l2 
 |-  ( ( ( ( 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. RR )
108 107 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 ) ) -> B e. CC )
109 108 99 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 )
110 109 addid1d 
 |-  ( ( ( ( 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 ) + 0 ) = ( B x. C ) )
111 106 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 ) ) -> ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) = ( B x. C ) )
112 45 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 = ( B x. B ) )
113 111 112 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 ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) = ( ( B x. C ) / ( B x. B ) ) )
114 99 108 108 70 70 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 ) ) -> ( ( B x. C ) / ( B x. B ) ) = ( C / B ) )
115 113 114 eqtr2d 
 |-  ( ( ( ( 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 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) )
116 115 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 = ( C / B ) <-> Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) )
117 116 biimpa 
 |-  ( ( ( ( ( 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 = ( C / B ) ) -> Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) )
118 92 117 jctird 
 |-  ( ( ( ( ( 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 = ( C / B ) ) -> ( X = -u ( ( sqrt ` D ) / B ) -> ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) )
119 75 118 orim12d 
 |-  ( ( ( ( ( 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 = ( C / B ) ) -> ( ( X = ( ( sqrt ` D ) / B ) \/ X = -u ( ( sqrt ` D ) / B ) ) -> ( ( 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 ) ) ) ) )
120 4 119 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 ) ) /\ Y = ( C / B ) ) -> ( ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) -> ( ( 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 ) ) ) ) )
121 120 expimpd 
 |-  ( ( ( ( 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 = ( C / B ) /\ ( X = -u ( ( sqrt ` D ) / B ) \/ X = ( ( sqrt ` D ) / B ) ) ) -> ( ( 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 ) ) ) ) )
122 3 121 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 ) -> ( ( 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 ) ) ) ) )