Metamath Proof Explorer

Theorem itsclquadb

Description: Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 22-Feb-2023)

Ref Expression
Hypotheses itsclquadb.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclquadb.t 
|- T = -u ( 2 x. ( B x. C ) )
itsclquadb.u 
|- U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
Assertion itsclquadb 
|- ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 itsclquadb.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itsclquadb.t 
 |-  T = -u ( 2 x. ( B x. C ) )
3 itsclquadb.u 
 |-  U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
4 simpl1 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) )
5 simp2 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> R e. RR+ )
6 5 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> R e. RR+ )
7 simp3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> Y e. RR )
8 7 anim1ci 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> ( x e. RR /\ Y e. RR ) )
9 1 2 3 itscnhlc0yqe 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ 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 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
10 4 6 8 9 syl3anc 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
11 10 rexlimdva 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
12 simp3 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> C e. RR )
13 12 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> C e. RR )
14 simp2 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> B e. RR )
15 14 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> B e. RR )
16 15 7 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B x. Y ) e. RR )
17 13 16 resubcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C - ( B x. Y ) ) e. RR )
18 simp11l 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> A e. RR )
19 simp11r 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> A =/= 0 )
20 17 18 19 redivcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C - ( B x. Y ) ) / A ) e. RR )
21 20 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( C - ( B x. Y ) ) / A ) e. RR )
22 oveq1 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( x ^ 2 ) = ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) )
23 22 oveq1d 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) )
24 23 eqeq1d 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) <-> ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) ) )
25 oveq2 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( A x. x ) = ( A x. ( ( C - ( B x. Y ) ) / A ) ) )
26 25 oveq1d 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( ( A x. x ) + ( B x. Y ) ) = ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) )
27 26 eqeq1d 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( ( ( A x. x ) + ( B x. Y ) ) = C <-> ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C ) )
28 24 27 anbi12d 
 |-  ( x = ( ( C - ( B x. Y ) ) / A ) -> ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> ( ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C ) ) )
29 28 adantl 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) /\ x = ( ( C - ( B x. Y ) ) / A ) ) -> ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> ( ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C ) ) )
30 17 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C - ( B x. Y ) ) e. CC )
31 18 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> A e. CC )
32 30 31 19 sqdivd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) = ( ( ( C - ( B x. Y ) ) ^ 2 ) / ( A ^ 2 ) ) )
33 13 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> C e. CC )
34 16 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B x. Y ) e. CC )
35 binom2sub 
 |-  ( ( C e. CC /\ ( B x. Y ) e. CC ) -> ( ( C - ( B x. Y ) ) ^ 2 ) = ( ( ( C ^ 2 ) - ( 2 x. ( C x. ( B x. Y ) ) ) ) + ( ( B x. Y ) ^ 2 ) ) )
36 33 34 35 syl2anc 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C - ( B x. Y ) ) ^ 2 ) = ( ( ( C ^ 2 ) - ( 2 x. ( C x. ( B x. Y ) ) ) ) + ( ( B x. Y ) ^ 2 ) ) )
37 13 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C ^ 2 ) e. RR )
38 37 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C ^ 2 ) e. CC )
39 2re 
 |-  2 e. RR
40 39 a1i 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> 2 e. RR )
41 13 16 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C x. ( B x. Y ) ) e. RR )
42 40 41 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( C x. ( B x. Y ) ) ) e. RR )
43 42 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( C x. ( B x. Y ) ) ) e. CC )
44 38 43 negsubd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + -u ( 2 x. ( C x. ( B x. Y ) ) ) ) = ( ( C ^ 2 ) - ( 2 x. ( C x. ( B x. Y ) ) ) ) )
45 15 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> B e. CC )
46 7 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> Y e. CC )
47 33 45 46 mulassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C x. B ) x. Y ) = ( C x. ( B x. Y ) ) )
48 47 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C x. ( B x. Y ) ) = ( ( C x. B ) x. Y ) )
49 48 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( C x. ( B x. Y ) ) ) = ( 2 x. ( ( C x. B ) x. Y ) ) )
50 2cnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> 2 e. CC )
51 13 15 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C x. B ) e. RR )
52 51 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C x. B ) e. CC )
53 50 52 46 mulassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( 2 x. ( C x. B ) ) x. Y ) = ( 2 x. ( ( C x. B ) x. Y ) ) )
54 53 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( ( C x. B ) x. Y ) ) = ( ( 2 x. ( C x. B ) ) x. Y ) )
55 33 45 mulcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( C x. B ) = ( B x. C ) )
56 55 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( C x. B ) ) = ( 2 x. ( B x. C ) ) )
57 56 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( 2 x. ( C x. B ) ) x. Y ) = ( ( 2 x. ( B x. C ) ) x. Y ) )
58 49 54 57 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( C x. ( B x. Y ) ) ) = ( ( 2 x. ( B x. C ) ) x. Y ) )
59 58 negeqd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> -u ( 2 x. ( C x. ( B x. Y ) ) ) = -u ( ( 2 x. ( B x. C ) ) x. Y ) )
60 59 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + -u ( 2 x. ( C x. ( B x. Y ) ) ) ) = ( ( C ^ 2 ) + -u ( ( 2 x. ( B x. C ) ) x. Y ) ) )
61 44 60 eqtr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) - ( 2 x. ( C x. ( B x. Y ) ) ) ) = ( ( C ^ 2 ) + -u ( ( 2 x. ( B x. C ) ) x. Y ) ) )
62 45 46 sqmuld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( B x. Y ) ^ 2 ) = ( ( B ^ 2 ) x. ( Y ^ 2 ) ) )
63 61 62 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) - ( 2 x. ( C x. ( B x. Y ) ) ) ) + ( ( B x. Y ) ^ 2 ) ) = ( ( ( C ^ 2 ) + -u ( ( 2 x. ( B x. C ) ) x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) )
64 15 13 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B x. C ) e. RR )
65 40 64 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( B x. C ) ) e. RR )
66 65 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( 2 x. ( B x. C ) ) e. CC )
67 66 46 mulneg1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( -u ( 2 x. ( B x. C ) ) x. Y ) = -u ( ( 2 x. ( B x. C ) ) x. Y ) )
68 2 eqcomi 
 |-  -u ( 2 x. ( B x. C ) ) = T
69 68 oveq1i 
 |-  ( -u ( 2 x. ( B x. C ) ) x. Y ) = ( T x. Y )
70 69 a1i 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( -u ( 2 x. ( B x. C ) ) x. Y ) = ( T x. Y ) )
71 67 70 eqtr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> -u ( ( 2 x. ( B x. C ) ) x. Y ) = ( T x. Y ) )
72 71 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + -u ( ( 2 x. ( B x. C ) ) x. Y ) ) = ( ( C ^ 2 ) + ( T x. Y ) ) )
73 72 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + -u ( ( 2 x. ( B x. C ) ) x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) = ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) )
74 36 63 73 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C - ( B x. Y ) ) ^ 2 ) = ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) )
75 74 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C - ( B x. Y ) ) ^ 2 ) / ( A ^ 2 ) ) = ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) )
76 32 75 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) = ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) )
77 resqcl 
 |-  ( Y e. RR -> ( Y ^ 2 ) e. RR )
78 77 recnd 
 |-  ( Y e. RR -> ( Y ^ 2 ) e. CC )
79 78 3ad2ant3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( Y ^ 2 ) e. CC )
80 18 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( A ^ 2 ) e. RR )
81 80 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( A ^ 2 ) e. CC )
82 recn 
 |-  ( A e. RR -> A e. CC )
83 sqne0 
 |-  ( A e. CC -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
84 82 83 syl 
 |-  ( A e. RR -> ( ( A ^ 2 ) =/= 0 <-> A =/= 0 ) )
85 84 biimpar 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( A ^ 2 ) =/= 0 )
86 85 3ad2ant1 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( A ^ 2 ) =/= 0 )
87 86 3ad2ant1 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( A ^ 2 ) =/= 0 )
88 79 81 87 divcan2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) = ( Y ^ 2 ) )
89 88 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( Y ^ 2 ) = ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) )
90 76 89 oveq12d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) + ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) ) )
91 81 79 81 87 divassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( A ^ 2 ) x. ( Y ^ 2 ) ) / ( A ^ 2 ) ) = ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) )
92 91 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) = ( ( ( A ^ 2 ) x. ( Y ^ 2 ) ) / ( A ^ 2 ) ) )
93 92 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) + ( ( A ^ 2 ) x. ( ( Y ^ 2 ) / ( A ^ 2 ) ) ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( Y ^ 2 ) ) / ( A ^ 2 ) ) ) )
94 65 renegcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> -u ( 2 x. ( B x. C ) ) e. RR )
95 2 94 eqeltrid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> T e. RR )
96 95 7 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( T x. Y ) e. RR )
97 37 96 readdcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + ( T x. Y ) ) e. RR )
98 15 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B ^ 2 ) e. RR )
99 7 resqcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( Y ^ 2 ) e. RR )
100 98 99 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( B ^ 2 ) x. ( Y ^ 2 ) ) e. RR )
101 97 100 readdcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) e. RR )
102 101 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) e. CC )
103 80 99 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( Y ^ 2 ) ) e. RR )
104 103 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( Y ^ 2 ) ) e. CC )
105 102 104 81 87 divdird 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( Y ^ 2 ) ) / ( A ^ 2 ) ) ) )
106 105 eqcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) + ( ( ( A ^ 2 ) x. ( Y ^ 2 ) ) / ( A ^ 2 ) ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) )
107 90 93 106 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) )
108 107 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) )
109 97 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + ( T x. Y ) ) e. CC )
110 100 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( B ^ 2 ) x. ( Y ^ 2 ) ) e. CC )
111 109 110 104 addassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) = ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( ( B ^ 2 ) x. ( Y ^ 2 ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) ) )
112 98 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B ^ 2 ) e. CC )
113 99 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( Y ^ 2 ) e. CC )
114 112 81 113 adddird 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( B ^ 2 ) + ( A ^ 2 ) ) x. ( Y ^ 2 ) ) = ( ( ( B ^ 2 ) x. ( Y ^ 2 ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) )
115 112 81 addcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( B ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
116 115 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( B ^ 2 ) + ( A ^ 2 ) ) x. ( Y ^ 2 ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) )
117 114 116 eqtr3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( B ^ 2 ) x. ( Y ^ 2 ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) )
118 117 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( ( B ^ 2 ) x. ( Y ^ 2 ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) ) = ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) )
119 96 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( T x. Y ) e. CC )
120 80 98 readdcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. RR )
121 120 99 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) e. RR )
122 121 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) e. CC )
123 38 119 122 addassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) = ( ( C ^ 2 ) + ( ( T x. Y ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) ) )
124 119 122 addcomd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( T x. Y ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) )
125 124 oveq2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + ( ( T x. Y ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) ) = ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) )
126 123 125 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) ) = ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) )
127 111 118 126 3eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) = ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) )
128 127 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) = ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) )
129 128 oveq1d 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( ( ( C ^ 2 ) + ( T x. Y ) ) + ( ( B ^ 2 ) x. ( Y ^ 2 ) ) ) + ( ( A ^ 2 ) x. ( Y ^ 2 ) ) ) / ( A ^ 2 ) ) = ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) )
130 1 oveq1i 
 |-  ( Q x. ( Y ^ 2 ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) )
131 3 oveq2i 
 |-  ( ( T x. Y ) + U ) = ( ( T x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) )
132 130 131 oveq12i 
 |-  ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( T x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
133 rpre 
 |-  ( R e. RR+ -> R e. RR )
134 133 resqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. RR )
135 134 3ad2ant2 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( R ^ 2 ) e. RR )
136 80 135 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( R ^ 2 ) ) e. RR )
137 37 136 resubcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) e. RR )
138 137 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) e. CC )
139 122 119 138 addassd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( T x. Y ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) ) )
140 132 139 eqtr4id 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
141 140 eqeq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 <-> ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = 0 ) )
142 121 96 readdcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) e. RR )
143 142 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) e. CC )
144 addeq0 
 |-  ( ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) e. CC /\ ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) e. CC ) -> ( ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = 0 <-> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
145 143 138 144 syl2anc 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) + ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = 0 <-> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
146 141 145 bitrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 <-> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
147 oveq2 
 |-  ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) -> ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) = ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
148 147 oveq1d 
 |-  ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) -> ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) = ( ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) / ( A ^ 2 ) ) )
149 38 138 negsubd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( C ^ 2 ) - ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) )
150 136 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A ^ 2 ) x. ( R ^ 2 ) ) e. CC )
151 38 150 nncand 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) - ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
152 149 151 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) = ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
153 152 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) / ( A ^ 2 ) ) = ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) / ( A ^ 2 ) ) )
154 135 recnd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( R ^ 2 ) e. CC )
155 154 81 87 divcan3d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( A ^ 2 ) x. ( R ^ 2 ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) )
156 153 155 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( C ^ 2 ) + -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) )
157 148 156 sylan9eqr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) ) -> ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) )
158 157 ex 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) = -u ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) -> ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) ) )
159 146 158 sylbid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 -> ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) ) )
160 159 imp 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( C ^ 2 ) + ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( T x. Y ) ) ) / ( A ^ 2 ) ) = ( R ^ 2 ) )
161 108 129 160 3eqtrd 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) )
162 30 31 19 divcan2d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( A x. ( ( C - ( B x. Y ) ) / A ) ) = ( C - ( B x. Y ) ) )
163 162 oveq1d 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = ( ( C - ( B x. Y ) ) + ( B x. Y ) ) )
164 33 34 npcand 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( C - ( B x. Y ) ) + ( B x. Y ) ) = C )
165 163 164 eqtrd 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C )
166 165 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C )
167 161 166 jca 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> ( ( ( ( ( C - ( B x. Y ) ) / A ) ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( ( C - ( B x. Y ) ) / A ) ) + ( B x. Y ) ) = C ) )
168 21 29 167 rspcedvd 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) -> E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) )
169 168 ex 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 -> E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) ) )
170 11 169 impbid 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )