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 ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
Assertion itschlc0yqe ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q ⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itscnhlc0yqe.t ⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) )
3 itscnhlc0yqe.u ⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) )
4 oveq2 ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( 𝐵 · 𝐶 ) = ( 𝐵 · ( 𝐵 · 𝑌 ) ) )
5 4 oveq2d ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( 2 · ( 𝐵 · 𝐶 ) ) = ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) )
6 5 oveq1d ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) )
7 6 negeqd ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) )
8 oveq1 ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( 𝐶 ↑ 2 ) = ( ( 𝐵 · 𝑌 ) ↑ 2 ) )
9 7 8 oveq12d ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) = ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) )
10 9 oveq2d ⊢ ( 𝐶 = ( 𝐵 · 𝑌 ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) )
11 10 eqcoms ⊢ ( ( 𝐵 · 𝑌 ) = 𝐶 → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) = ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) )
12 simp12 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
13 12 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
14 simp3r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℝ )
15 14 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℂ )
16 13 15 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝑌 ) ∈ ℂ )
17 16 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑌 ) ↑ 2 ) ∈ ℂ )
18 2cnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 2 ∈ ℂ )
19 13 16 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · ( 𝐵 · 𝑌 ) ) ∈ ℂ )
20 18 19 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) ∈ ℂ )
21 20 15 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ∈ ℂ )
22 21 negcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ∈ ℂ )
23 add32r ⊢ ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) ∈ ℂ ∧ - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ∈ ℂ ∧ ( ( 𝐵 · 𝑌 ) ↑ 2 ) ∈ ℂ ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) = ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) + - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) )
24 17 22 17 23 syl3anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) = ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) + - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) )
25 17 17 addcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ∈ ℂ )
26 25 21 negsubd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) + - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) = ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) − ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) )
27 18 19 15 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) = ( 2 · ( ( 𝐵 · ( 𝐵 · 𝑌 ) ) · 𝑌 ) ) )
28 13 16 15 mul32d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( 𝐵 · 𝑌 ) ) · 𝑌 ) = ( ( 𝐵 · 𝑌 ) · ( 𝐵 · 𝑌 ) ) )
29 16 sqvald ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑌 ) ↑ 2 ) = ( ( 𝐵 · 𝑌 ) · ( 𝐵 · 𝑌 ) ) )
30 28 29 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · ( 𝐵 · 𝑌 ) ) · 𝑌 ) = ( ( 𝐵 · 𝑌 ) ↑ 2 ) )
31 30 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( ( 𝐵 · ( 𝐵 · 𝑌 ) ) · 𝑌 ) ) = ( 2 · ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) )
32 17 2timesd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) = ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) )
33 27 31 32 3eqtrrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) = ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) )
34 25 33 subeq0bd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) − ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) = 0 )
35 26 34 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) + - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) ) = 0 )
36 24 35 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · ( 𝐵 · 𝑌 ) ) ) · 𝑌 ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) = 0 )
37 11 36 sylan9eqr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) ∧ ( 𝐵 · 𝑌 ) = 𝐶 ) → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) = 0 )
38 37 ex ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑌 ) = 𝐶 → ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) = 0 ) )
39 simp3l ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℝ )
40 39 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℂ )
41 40 mul02d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 0 · 𝑋 ) = 0 )
42 41 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( 0 + ( 𝐵 · 𝑌 ) ) )
43 16 addlidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 0 + ( 𝐵 · 𝑌 ) ) = ( 𝐵 · 𝑌 ) )
44 42 43 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( 𝐵 · 𝑌 ) )
45 44 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( 𝐵 · 𝑌 ) = 𝐶 ) )
46 13 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
47 46 addlidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 0 + ( 𝐵 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
48 47 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) )
49 13 15 sqmuld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑌 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) )
50 48 49 eqtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( 𝐵 · 𝑌 ) ↑ 2 ) )
51 simp13 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
52 51 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
53 13 52 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
54 18 53 mulcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ )
55 54 15 mulneg1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
56 rpcn ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℂ )
57 56 sqcld ⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℂ )
58 57 mul02d ⊢ ( 𝑅 ∈ ℝ+ → ( 0 · ( 𝑅 ↑ 2 ) ) = 0 )
59 58 oveq2d ⊢ ( 𝑅 ∈ ℝ+ → ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) − 0 ) )
60 59 3ad2ant2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) − 0 ) )
61 52 sqcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
62 61 subid1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) − 0 ) = ( 𝐶 ↑ 2 ) )
63 60 62 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) = ( 𝐶 ↑ 2 ) )
64 55 63 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) = ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) )
65 50 64 oveq12d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) )
66 65 eqeq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ↔ ( ( ( 𝐵 · 𝑌 ) ↑ 2 ) + ( - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( 𝐶 ↑ 2 ) ) ) = 0 ) )
67 38 45 66 3imtr4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
68 67 3exp ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑅 ∈ ℝ+ → ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) ) )
69 68 3adant1r ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑅 ∈ ℝ+ → ( ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) → ( ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) ) )
70 69 3imp ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
71 70 adantld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
72 oveq1 ⊢ ( 𝐴 = 0 → ( 𝐴 · 𝑋 ) = ( 0 · 𝑋 ) )
73 72 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) )
74 73 eqeq1d ⊢ ( 𝐴 = 0 → ( ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) )
75 74 anbi2d ⊢ ( 𝐴 = 0 → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) )
76 sq0i ⊢ ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )
77 76 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 0 + ( 𝐵 ↑ 2 ) ) )
78 1 77 eqtrid ⊢ ( 𝐴 = 0 → 𝑄 = ( 0 + ( 𝐵 ↑ 2 ) ) )
79 78 oveq1d ⊢ ( 𝐴 = 0 → ( 𝑄 · ( 𝑌 ↑ 2 ) ) = ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) )
80 2 oveq1i ⊢ ( 𝑇 · 𝑌 ) = ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 )
81 80 a1i ⊢ ( 𝐴 = 0 → ( 𝑇 · 𝑌 ) = ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) )
82 76 oveq1d ⊢ ( 𝐴 = 0 → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) = ( 0 · ( 𝑅 ↑ 2 ) ) )
83 82 oveq2d ⊢ ( 𝐴 = 0 → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) )
84 3 83 eqtrid ⊢ ( 𝐴 = 0 → 𝑈 = ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) )
85 81 84 oveq12d ⊢ ( 𝐴 = 0 → ( ( 𝑇 · 𝑌 ) + 𝑈 ) = ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) )
86 79 85 oveq12d ⊢ ( 𝐴 = 0 → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) )
87 86 eqeq1d ⊢ ( 𝐴 = 0 → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ↔ ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) )
88 75 87 imbi12d ⊢ ( 𝐴 = 0 → ( ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ↔ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
89 88 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) → ( ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ↔ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
90 89 3ad2ant1 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ↔ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
91 90 3ad2ant1 ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ↔ ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 0 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( ( 0 + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( 0 · ( 𝑅 ↑ 2 ) ) ) ) ) = 0 ) ) )
92 71 91 mpbird ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 = 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑋 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) )