Metamath Proof Explorer

Theorem itsclquadeu

Description: Quadratic equation for the y-coordinate of the intersection points of a line and a circle. (Contributed by AV, 23-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 itsclquadeu 
|- ( ( ( ( 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 oveq1 
 |-  ( x = z -> ( x ^ 2 ) = ( z ^ 2 ) )
5 4 oveq1d 
 |-  ( x = z -> ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( ( z ^ 2 ) + ( Y ^ 2 ) ) )
6 5 eqeq1d 
 |-  ( x = z -> ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) <-> ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) ) )
7 oveq2 
 |-  ( x = z -> ( A x. x ) = ( A x. z ) )
8 7 oveq1d 
 |-  ( x = z -> ( ( A x. x ) + ( B x. Y ) ) = ( ( A x. z ) + ( B x. Y ) ) )
9 8 eqeq1d 
 |-  ( x = z -> ( ( ( A x. x ) + ( B x. Y ) ) = C <-> ( ( A x. z ) + ( B x. Y ) ) = C ) )
10 6 9 anbi12d 
 |-  ( x = z -> ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) ) )
11 10 reu8 
 |-  ( E! x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) <-> E. x e. RR ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) /\ A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) )
12 11 a1i 
 |-  ( ( ( ( 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 ) <-> E. x e. RR ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) /\ A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) ) )
13 id 
 |-  ( C = ( ( A x. x ) + ( B x. Y ) ) -> C = ( ( A x. x ) + ( B x. Y ) ) )
14 13 eqcoms 
 |-  ( ( ( A x. x ) + ( B x. Y ) ) = C -> C = ( ( A x. x ) + ( B x. Y ) ) )
15 14 eqeq2d 
 |-  ( ( ( A x. x ) + ( B x. Y ) ) = C -> ( ( ( A x. z ) + ( B x. Y ) ) = C <-> ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) ) )
16 15 adantl 
 |-  ( ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> ( ( ( A x. z ) + ( B x. Y ) ) = C <-> ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) ) )
17 simp11l 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> A e. RR )
18 17 ad2antrr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> A e. RR )
19 simpr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> z e. RR )
20 18 19 remulcld 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( A x. z ) e. RR )
21 20 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( A x. z ) e. CC )
22 17 adantr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> A e. RR )
23 simpr 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> x e. RR )
24 22 23 remulcld 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> ( A x. x ) e. RR )
25 24 adantr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( A x. x ) e. RR )
26 25 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( A x. x ) e. CC )
27 simp12 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> B e. RR )
28 simp3 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> Y e. RR )
29 27 28 remulcld 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> ( B x. Y ) e. RR )
30 29 ad2antrr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( B x. Y ) e. RR )
31 30 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( B x. Y ) e. CC )
32 21 26 31 addcan2d 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) <-> ( A x. z ) = ( A x. x ) ) )
33 19 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> z e. CC )
34 simplr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> x e. RR )
35 34 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> x e. CC )
36 18 recnd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> A e. CC )
37 simp11r 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) -> A =/= 0 )
38 37 ad2antrr 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> A =/= 0 )
39 33 35 36 38 mulcand 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( ( A x. z ) = ( A x. x ) <-> z = x ) )
40 equcom 
 |-  ( z = x <-> x = z )
41 40 a1i 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( z = x <-> x = z ) )
42 32 39 41 3bitrd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) <-> x = z ) )
43 42 biimpd 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) -> ( ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) -> x = z ) )
44 43 adantr 
 |-  ( ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> ( ( ( A x. z ) + ( B x. Y ) ) = ( ( A x. x ) + ( B x. Y ) ) -> x = z ) )
45 16 44 sylbid 
 |-  ( ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ z e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> ( ( ( A x. z ) + ( B x. Y ) ) = C -> x = z ) )
46 45 an32s 
 |-  ( ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) /\ z e. RR ) -> ( ( ( A x. z ) + ( B x. Y ) ) = C -> x = z ) )
47 46 adantld 
 |-  ( ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) /\ z e. RR ) -> ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) )
48 47 ralrimiva 
 |-  ( ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) -> A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) )
49 48 ex 
 |-  ( ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ Y e. RR ) /\ x e. RR ) -> ( ( ( A x. x ) + ( B x. Y ) ) = C -> A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) )
50 49 adantld 
 |-  ( ( ( ( ( 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 ) -> A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) )
51 50 pm4.71d 
 |-  ( ( ( ( ( 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 ) <-> ( ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) /\ A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) ) )
52 51 bicomd 
 |-  ( ( ( ( ( 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 ) /\ A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) <-> ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) ) )
53 52 rexbidva 
 |-  ( ( ( ( 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 ) /\ A. z e. RR ( ( ( ( z ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. z ) + ( B x. Y ) ) = C ) -> x = z ) ) <-> E. x e. RR ( ( ( x ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. x ) + ( B x. Y ) ) = C ) ) )
54 1 2 3 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 ) )
55 12 53 54 3bitrd 
 |-  ( ( ( ( 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 ) )