Metamath Proof Explorer

Theorem itschlc0yqe

Description: Lemma for itsclc0 . Quadratic equation for the y-coordinate of the intersection points of a horizontal line and a circle. (Contributed by AV, 25-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 itschlc0yqe 
|- ( ( ( ( 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 oveq2 
 |-  ( C = ( B x. Y ) -> ( B x. C ) = ( B x. ( B x. Y ) ) )
5 4 oveq2d 
 |-  ( C = ( B x. Y ) -> ( 2 x. ( B x. C ) ) = ( 2 x. ( B x. ( B x. Y ) ) ) )
6 5 oveq1d 
 |-  ( C = ( B x. Y ) -> ( ( 2 x. ( B x. C ) ) x. Y ) = ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) )
7 6 negeqd 
 |-  ( C = ( B x. Y ) -> -u ( ( 2 x. ( B x. C ) ) x. Y ) = -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) )
8 oveq1 
 |-  ( C = ( B x. Y ) -> ( C ^ 2 ) = ( ( B x. Y ) ^ 2 ) )
9 7 8 oveq12d 
 |-  ( C = ( B x. Y ) -> ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) = ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) )
10 9 oveq2d 
 |-  ( C = ( B x. Y ) -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) = ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) ) )
11 10 eqcoms 
 |-  ( ( B x. Y ) = C -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) = ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) ) )
12 simp12 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> B e. RR )
13 12 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> B e. CC )
14 simp3r 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> Y e. RR )
15 14 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> Y e. CC )
16 13 15 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. Y ) e. CC )
17 16 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. Y ) ^ 2 ) e. CC )
18 2cnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> 2 e. CC )
19 13 16 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. ( B x. Y ) ) e. CC )
20 18 19 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( B x. ( B x. Y ) ) ) e. CC )
21 20 15 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) e. CC )
22 21 negcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) e. CC )
23 add32r 
 |-  ( ( ( ( B x. Y ) ^ 2 ) e. CC /\ -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) e. CC /\ ( ( B x. Y ) ^ 2 ) e. CC ) -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) ) = ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) + -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) )
24 17 22 17 23 syl3anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) ) = ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) + -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) )
25 17 17 addcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) e. CC )
26 25 21 negsubd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) + -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) = ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) - ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) )
27 18 19 15 mulassd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) = ( 2 x. ( ( B x. ( B x. Y ) ) x. Y ) ) )
28 13 16 15 mul32d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( B x. Y ) ) x. Y ) = ( ( B x. Y ) x. ( B x. Y ) ) )
29 16 sqvald 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. Y ) ^ 2 ) = ( ( B x. Y ) x. ( B x. Y ) ) )
30 28 29 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. ( B x. Y ) ) x. Y ) = ( ( B x. Y ) ^ 2 ) )
31 30 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( ( B x. ( B x. Y ) ) x. Y ) ) = ( 2 x. ( ( B x. Y ) ^ 2 ) ) )
32 17 2timesd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( ( B x. Y ) ^ 2 ) ) = ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) )
33 27 31 32 3eqtrrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) = ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) )
34 25 33 subeq0bd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) - ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) = 0 )
35 26 34 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( B x. Y ) ^ 2 ) + ( ( B x. Y ) ^ 2 ) ) + -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) ) = 0 )
36 24 35 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. ( B x. Y ) ) ) x. Y ) + ( ( B x. Y ) ^ 2 ) ) ) = 0 )
37 11 36 sylan9eqr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) /\ ( B x. Y ) = C ) -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) = 0 )
38 37 ex 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. Y ) = C -> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) = 0 ) )
39 simp3l 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> X e. RR )
40 39 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> X e. CC )
41 40 mul02d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 0 x. X ) = 0 )
42 41 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 0 x. X ) + ( B x. Y ) ) = ( 0 + ( B x. Y ) ) )
43 16 addlidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 0 + ( B x. Y ) ) = ( B x. Y ) )
44 42 43 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 0 x. X ) + ( B x. Y ) ) = ( B x. Y ) )
45 44 eqeq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( 0 x. X ) + ( B x. Y ) ) = C <-> ( B x. Y ) = C ) )
46 13 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( B ^ 2 ) e. CC )
47 46 addlidd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 0 + ( B ^ 2 ) ) = ( B ^ 2 ) )
48 47 oveq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) = ( ( B ^ 2 ) x. ( Y ^ 2 ) ) )
49 13 15 sqmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( B x. Y ) ^ 2 ) = ( ( B ^ 2 ) x. ( Y ^ 2 ) ) )
50 48 49 eqtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) = ( ( B x. Y ) ^ 2 ) )
51 simp13 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> C e. RR )
52 51 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> C e. CC )
53 13 52 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( B x. C ) e. CC )
54 18 53 mulcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( 2 x. ( B x. C ) ) e. CC )
55 54 15 mulneg1d 
 |-  ( ( ( A e. RR /\ 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 ) )
56 rpcn 
 |-  ( R e. RR+ -> R e. CC )
57 56 sqcld 
 |-  ( R e. RR+ -> ( R ^ 2 ) e. CC )
58 57 mul02d 
 |-  ( R e. RR+ -> ( 0 x. ( R ^ 2 ) ) = 0 )
59 58 oveq2d 
 |-  ( R e. RR+ -> ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) = ( ( C ^ 2 ) - 0 ) )
60 59 3ad2ant2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) = ( ( C ^ 2 ) - 0 ) )
61 52 sqcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( C ^ 2 ) e. CC )
62 61 subid1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( C ^ 2 ) - 0 ) = ( C ^ 2 ) )
63 60 62 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) = ( C ^ 2 ) )
64 55 63 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) = ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) )
65 50 64 oveq12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) )
66 65 eqeq1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 <-> ( ( ( B x. Y ) ^ 2 ) + ( -u ( ( 2 x. ( B x. C ) ) x. Y ) + ( C ^ 2 ) ) ) = 0 ) )
67 38 45 66 3imtr4d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( 0 x. X ) + ( B x. Y ) ) = C -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) )
68 67 3exp 
 |-  ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( R e. RR+ -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( 0 x. X ) + ( B x. Y ) ) = C -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) ) )
69 68 3adant1r 
 |-  ( ( ( A e. RR /\ A = 0 ) /\ B e. RR /\ C e. RR ) -> ( R e. RR+ -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( 0 x. X ) + ( B x. Y ) ) = C -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) ) )
70 69 3imp 
 |-  ( ( ( ( A e. RR /\ A = 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( 0 x. X ) + ( B x. Y ) ) = C -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) )
71 70 adantld 
 |-  ( ( ( ( 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 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) )
72 oveq1 
 |-  ( A = 0 -> ( A x. X ) = ( 0 x. X ) )
73 72 oveq1d 
 |-  ( A = 0 -> ( ( A x. X ) + ( B x. Y ) ) = ( ( 0 x. X ) + ( B x. Y ) ) )
74 73 eqeq1d 
 |-  ( A = 0 -> ( ( ( A x. X ) + ( B x. Y ) ) = C <-> ( ( 0 x. X ) + ( B x. Y ) ) = C ) )
75 74 anbi2d 
 |-  ( A = 0 -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) <-> ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) ) )
76 sq0i 
 |-  ( A = 0 -> ( A ^ 2 ) = 0 )
77 76 oveq1d 
 |-  ( A = 0 -> ( ( A ^ 2 ) + ( B ^ 2 ) ) = ( 0 + ( B ^ 2 ) ) )
78 1 77 eqtrid 
 |-  ( A = 0 -> Q = ( 0 + ( B ^ 2 ) ) )
79 78 oveq1d 
 |-  ( A = 0 -> ( Q x. ( Y ^ 2 ) ) = ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) )
80 2 oveq1i 
 |-  ( T x. Y ) = ( -u ( 2 x. ( B x. C ) ) x. Y )
81 80 a1i 
 |-  ( A = 0 -> ( T x. Y ) = ( -u ( 2 x. ( B x. C ) ) x. Y ) )
82 76 oveq1d 
 |-  ( A = 0 -> ( ( A ^ 2 ) x. ( R ^ 2 ) ) = ( 0 x. ( R ^ 2 ) ) )
83 82 oveq2d 
 |-  ( A = 0 -> ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) ) = ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) )
84 3 83 eqtrid 
 |-  ( A = 0 -> U = ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) )
85 81 84 oveq12d 
 |-  ( A = 0 -> ( ( T x. Y ) + U ) = ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) )
86 79 85 oveq12d 
 |-  ( A = 0 -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) )
87 86 eqeq1d 
 |-  ( A = 0 -> ( ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 <-> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) )
88 75 87 imbi12d 
 |-  ( A = 0 -> ( ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) <-> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
89 88 adantl 
 |-  ( ( A e. RR /\ A = 0 ) -> ( ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) <-> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
90 89 3ad2ant1 
 |-  ( ( ( A e. RR /\ A = 0 ) /\ B e. RR /\ C e. RR ) -> ( ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) <-> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
91 90 3ad2ant1 
 |-  ( ( ( ( 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 ) <-> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( 0 x. X ) + ( B x. Y ) ) = C ) -> ( ( ( 0 + ( B ^ 2 ) ) x. ( Y ^ 2 ) ) + ( ( -u ( 2 x. ( B x. C ) ) x. Y ) + ( ( C ^ 2 ) - ( 0 x. ( R ^ 2 ) ) ) ) ) = 0 ) ) )
92 71 91 mpbird 
 |-  ( ( ( ( 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 ) )