Metamath Proof Explorer

Theorem itscnhlc0yqe

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

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itscnhlc0yqe.t 
|- T = -u ( 2 x. ( B x. C ) )
itscnhlc0yqe.u 
|- U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
Assertion 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 ) )

Proof

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