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 ) )