itscnhlc0yqe - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > itscnhlc0yqe		Structured version Visualization version GIF version

Theorem itscnhlc0yqe 44144

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

**Hypotheses**
Ref	Expression
itscnhlc0yqe.q	⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
itscnhlc0yqe.t	⊢ 𝑇 = -(2 · (𝐵 · 𝐶))
itscnhlc0yqe.u	⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))

**Assertion**
Ref	Expression
itscnhlc0yqe	⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))

**Proof of Theorem itscnhlc0yqe**
Step	Hyp	Ref	Expression
1		recn 10424	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	adantr 473	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1114	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
4	3	3ad2ant1 1114	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
5		simp2 1118	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
6	5	3ad2ant1 1114	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
7		simpr 477	. . . . . . 7 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ∈ ℝ)
8	7	3ad2ant3 1116	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℝ)
9	6, 8	remulcld 10469	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℝ)
10	9	recnd 10467	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℂ)
11		recn 10424	. . . . . 6 ⊢ (𝑋 ∈ ℝ → 𝑋 ∈ ℂ)
12	11	adantr 473	. . . . 5 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑋 ∈ ℂ)
13	12	3ad2ant3 1116	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
14		simp3 1119	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
15	14	recnd 10467	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
16	15	3ad2ant1 1114	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
17		simp11r 1266	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
18	4, 10, 13, 16, 17	lineq 11277	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)))
19	18	anbi2d 620	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴))))
20		oveq1 6982	. . . . . 6 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → (𝑋↑2) = (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2))
21	20	oveq1d 6990	. . . . 5 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → ((𝑋↑2) + (𝑌↑2)) = ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)))
22	21	eqeq1d 2775	. . . 4 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2)))
23	22	biimpac 471	. . 3 ⊢ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2))
24		simpl 475	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ)
25	24	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
26	25	resqcld 13425	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
27	26	recnd 10467	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
28	27	3ad2ant1 1114	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
29	14	3ad2ant1 1114	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
30	29, 9	resubcld 10868	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℝ)
31	25	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
32	30, 31, 17	redivcld 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌)) / 𝐴) ∈ ℝ)
33	32	resqcld 13425	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℝ)
34	33	recnd 10467	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℂ)
35	7	resqcld 13425	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℝ)
36	35	recnd 10467	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℂ)
37	36	3ad2ant3 1116	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
38	28, 34, 37	adddid 10463	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = (((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) + ((𝐴↑2) · (𝑌↑2))))
39	30	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℂ)
40	24	recnd 10467	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
41	40	3ad2ant1 1114	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
42	41	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
43	39, 42, 17	sqdivd 13337	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) = (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2)))
44	43	oveq2d 6991	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))))
45	30	resqcld 13425	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℝ)
46	45	recnd 10467	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℂ)
47	24	resqcld 13425	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ)
48	47	recnd 10467	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℂ)
49	48	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
50	49	3ad2ant1 1114	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
51		sqne0 13303	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
52	1, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
53	52	biimpar 470	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ≠ 0)
54	53	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ≠ 0)
55	54	3ad2ant1 1114	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ≠ 0)
56	46, 50, 55	divcan2d 11218	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))) = ((𝐶 − (𝐵 · 𝑌))↑2))
57	44, 56	eqtrd 2809	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐶 − (𝐵 · 𝑌))↑2))
58	57	oveq1d 6990	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))))
59	38, 58	eqtrd 2809	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))))
60	59	eqeq1d 2775	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
61	8	resqcld 13425	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℝ)
62	33, 61	readdcld 10468	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℝ)
63	62	recnd 10467	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℂ)
64		rpre 12211	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
65	64	resqcld 13425	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
66	65	recnd 10467	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
67	66	3ad2ant2 1115	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℂ)
68	47	3ad2ant1 1114	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
69	68	3ad2ant1 1114	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
70	69	recnd 10467	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
71	63, 67, 70, 55	mulcand 11073	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2)))
72		binom2sub 13395	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ (𝐵 · 𝑌) ∈ ℂ) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
73	16, 10, 72	syl2anc 576	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
74	73	oveq1d 6990	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))))
75	74	eqeq1d 2775	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
76	14	resqcld 13425	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶↑2) ∈ ℝ)
77	76	3ad2ant1 1114	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℝ)
78		2re 11513	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
79	78	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℝ)
80	29, 9	remulcld 10469	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) ∈ ℝ)
81	79, 80	remulcld 10469	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) ∈ ℝ)
82	77, 81	resubcld 10868	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℝ)
83	9	resqcld 13425	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℝ)
84	82, 83	readdcld 10468	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) ∈ ℝ)
85	69, 61	remulcld 10469	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℝ)
86	84, 85	readdcld 10468	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℝ)
87	86	recnd 10467	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℂ)
88	65	3ad2ant2 1115	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℝ)
89	69, 88	remulcld 10469	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℝ)
90	89	recnd 10467	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℂ)
91	87, 90, 90	subcan2ad 10842	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
92	82	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℂ)
93	83	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℂ)
94	85	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℂ)
95	92, 93, 94	addassd 10461	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2)))))
96	29	recnd 10467	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
97	5	recnd 10467	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
98	97	3ad2ant1 1114	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
99	8	recnd 10467	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℂ)
100	96, 98, 99	mulassd 10462	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = (𝐶 · (𝐵 · 𝑌)))
101	15, 97	mulcomd 10460	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
102	101	3ad2ant1 1114	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
103	102	oveq1d 6990	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = ((𝐵 · 𝐶) · 𝑌))
104	100, 103	eqtr3d 2811	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) = ((𝐵 · 𝐶) · 𝑌))
105	104	oveq2d 6991	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = (2 · ((𝐵 · 𝐶) · 𝑌)))
106	79	recnd 10467	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℂ)
107	5, 14	remulcld 10469	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐶) ∈ ℝ)
108	107	3ad2ant1 1114	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
109	108	recnd 10467	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
110	106, 109, 99	mulassd 10462	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) = (2 · ((𝐵 · 𝐶) · 𝑌)))
111	105, 110	eqtr4d 2812	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = ((2 · (𝐵 · 𝐶)) · 𝑌))
112	111	oveq2d 6991	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) = ((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
113	98, 99	sqmuld 13336	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) = ((𝐵↑2) · (𝑌↑2)))
114	113	oveq1d 6990	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2))) = (((𝐵↑2) · (𝑌↑2)) + ((𝐴↑2) · (𝑌↑2))))
115	6	resqcld 13425	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℝ)
116	115	recnd 10467	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℂ)
117	31	resqcld 13425	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
118	117	recnd 10467	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
119	61	recnd 10467	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
120	116, 118, 119	adddird 10464	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) = (((𝐵↑2) · (𝑌↑2)) + ((𝐴↑2) · (𝑌↑2))))
121	114, 120	eqtr4d 2812	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2))) = (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)))
122	112, 121	oveq12d 6993	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2)))) = (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))))
123	95, 122	eqtrd 2809	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))))
124	123	oveq1d 6990	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))))
125	77	recnd 10467	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℂ)
126	5	resqcld 13425	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℝ)
127	126, 68	readdcld 10468	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
128	127	3ad2ant1 1114	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
129	128, 61	remulcld 10469	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℝ)
130	6, 29	remulcld 10469	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
131	79, 130	remulcld 10469	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℝ)
132	131, 8	remulcld 10469	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
133	129, 132	resubcld 10868	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℝ)
134	133	recnd 10467	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℂ)
135	132	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
136	129	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℂ)
137	125, 135, 136	subadd23d 10819	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = ((𝐶↑2) + ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌))))
138	125, 134, 137	comraddd 10653	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)))
139	138	oveq1d 6990	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))))
140	134, 125, 90	addsubassd 10817	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
141	136, 135	negsubd 10803	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
142	141	eqcomd 2779	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)))
143	142	oveq1d 6990	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
144	132	renegcld 10867	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
145	144	recnd 10467	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
146	77, 89	resubcld 10868	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℝ)
147	146	recnd 10467	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℂ)
148	136, 145, 147	addassd 10461	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
149	140, 143, 148	3eqtrd 2813	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
150	124, 139, 149	3eqtrd 2813	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
151	90	subidd 10785	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) = 0)
152	150, 151	eqeq12d 2788	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) ↔ ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0))
153	75, 91, 152	3bitr2d 299	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0))
154	60, 71, 153	3bitr3d 301	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2) ↔ ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0))
155		itscnhlc0yqe.q	. . . . . . . . . . 11 ⊢ 𝑄 = ((𝐴↑2) + (𝐵↑2))
156	155	a1i 11	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 = ((𝐴↑2) + (𝐵↑2)))
157	118, 116, 156	comraddd 10653	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 = ((𝐵↑2) + (𝐴↑2)))
158	157	oveq1d 6990	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · (𝑌↑2)) = (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)))
159		itscnhlc0yqe.t	. . . . . . . . . . . 12 ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))
160	159	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑇 = -(2 · (𝐵 · 𝐶)))
161	160	oveq1d 6990	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑇 · 𝑌) = (-(2 · (𝐵 · 𝐶)) · 𝑌))
162	131	recnd 10467	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℂ)
163	162, 99	mulneg1d 10893	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (-(2 · (𝐵 · 𝐶)) · 𝑌) = -((2 · (𝐵 · 𝐶)) · 𝑌))
164	161, 163	eqtrd 2809	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑇 · 𝑌) = -((2 · (𝐵 · 𝐶)) · 𝑌))
165		itscnhlc0yqe.u	. . . . . . . . . 10 ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))
166	165	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))
167	164, 166	oveq12d 6993	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑇 · 𝑌) + 𝑈) = (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
168	158, 167	oveq12d 6993	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
169	168	eqcomd 2779	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)))
170	169	eqeq1d 2775	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
171	170	biimpd 221	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
172	154, 171	sylbid 232	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
173	23, 172	syl5 34	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
174	19, 173	sylbid 232	1 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 ∧ w3a 1069 = wceq 1508 ∈ wcel 2051 ≠ wne 2962 (class class class)co 6975 ℂcc 10332 ℝcr 10333 0cc0 10334 + caddc 10337 · cmul 10339 − cmin 10669 -cneg 10670 / cdiv 11097 2c2 11494 ℝ⁺crp 12203 ↑cexp 13243

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 ax-cnex 10390 ax-resscn 10391 ax-1cn 10392 ax-icn 10393 ax-addcl 10394 ax-addrcl 10395 ax-mulcl 10396 ax-mulrcl 10397 ax-mulcom 10398 ax-addass 10399 ax-mulass 10400 ax-distr 10401 ax-i2m1 10402 ax-1ne0 10403 ax-1rid 10404 ax-rnegex 10405 ax-rrecex 10406 ax-cnre 10407 ax-pre-lttri 10408 ax-pre-lttrn 10409 ax-pre-ltadd 10410 ax-pre-mulgt0 10411

This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ne 2963 df-nel 3069 df-ral 3088 df-rex 3089 df-reu 3090 df-rmo 3091 df-rab 3092 df-v 3412 df-sbc 3677 df-csb 3782 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-pss 3840 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-tp 4441 df-op 4443 df-uni 4710 df-iun 4791 df-br 4927 df-opab 4989 df-mpt 5006 df-tr 5028 df-id 5309 df-eprel 5314 df-po 5323 df-so 5324 df-fr 5363 df-we 5365 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-pred 5984 df-ord 6030 df-on 6031 df-lim 6032 df-suc 6033 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-riota 6936 df-ov 6978 df-oprab 6979 df-mpo 6980 df-om 7396 df-2nd 7501 df-wrecs 7749 df-recs 7811 df-rdg 7849 df-er 8088 df-en 8306 df-dom 8307 df-sdom 8308 df-pnf 10475 df-mnf 10476 df-xr 10477 df-ltxr 10478 df-le 10479 df-sub 10671 df-neg 10672 df-div 11098 df-nn 11439 df-2 11502 df-n0 11707 df-z 11793 df-uz 12058 df-rp 12204 df-seq 13184 df-exp 13244

This theorem is referenced by: itsclc0yqe 44146 itsclquadb 44161

W3C validator