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 48706

Description: Lemma for itsclc0 48718. 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 11224	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1133	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
4	3	3ad2ant1 1133	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
5		simp2 1137	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
6	5	3ad2ant1 1133	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
7		simpr 484	. . . . . . 7 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ∈ ℝ)
8	7	3ad2ant3 1135	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℝ)
9	6, 8	remulcld 11270	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℝ)
10	9	recnd 11268	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℂ)
11		recn 11224	. . . . . 6 ⊢ (𝑋 ∈ ℝ → 𝑋 ∈ ℂ)
12	11	adantr 480	. . . . 5 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑋 ∈ ℂ)
13	12	3ad2ant3 1135	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
14		simp3 1138	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
15	14	recnd 11268	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
16	15	3ad2ant1 1133	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
17		simp11r 1286	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
18	4, 10, 13, 16, 17	lineq 12083	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)))
19	18	anbi2d 630	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴))))
20		oveq1 7417	. . . . . 6 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → (𝑋↑2) = (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2))
21	20	oveq1d 7425	. . . . 5 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → ((𝑋↑2) + (𝑌↑2)) = ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)))
22	21	eqeq1d 2738	. . . 4 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ↔ ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2)))
23	22	biimpac 478	. . 3 ⊢ ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2))
24		simpl 482	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℝ)
25	24	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
26	25	resqcld 14148	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
27	26	recnd 11268	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
28	27	3ad2ant1 1133	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
29	14	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
30	29, 9	resubcld 11670	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℝ)
31	25	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
32	30, 31, 17	redivcld 12074	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌)) / 𝐴) ∈ ℝ)
33	32	resqcld 14148	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℝ)
34	33	recnd 11268	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℂ)
35	7	resqcld 14148	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℝ)
36	35	recnd 11268	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℂ)
37	36	3ad2ant3 1135	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
38	28, 34, 37	adddid 11264	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = (((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) + ((𝐴↑2) · (𝑌↑2))))
39	30	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℂ)
40	24	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
41	40	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
42	41	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
43	39, 42, 17	sqdivd 14182	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) = (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2)))
44	43	oveq2d 7426	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))))
45	30	resqcld 14148	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℝ)
46	45	recnd 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℂ)
47	24	resqcld 14148	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ)
48	47	recnd 11268	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℂ)
49	48	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
50	49	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
51		sqne0 14146	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
52	1, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
53	52	biimpar 477	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ≠ 0)
54	53	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ≠ 0)
55	54	3ad2ant1 1133	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ≠ 0)
56	46, 50, 55	divcan2d 12024	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))) = ((𝐶 − (𝐵 · 𝑌))↑2))
57	44, 56	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐶 − (𝐵 · 𝑌))↑2))
58	57	oveq1d 7425	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))))
59	38, 58	eqtrd 2771	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))))
60	59	eqeq1d 2738	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
61	8	resqcld 14148	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℝ)
62	33, 61	readdcld 11269	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℝ)
63	62	recnd 11268	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℂ)
64		rpre 13022	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
65	64	resqcld 14148	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
66	65	recnd 11268	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
67	66	3ad2ant2 1134	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℂ)
68	47	3ad2ant1 1133	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
69	68	3ad2ant1 1133	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
70	69	recnd 11268	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
71	63, 67, 70, 55	mulcand 11875	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2)))
72		binom2sub 14243	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ (𝐵 · 𝑌) ∈ ℂ) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
73	16, 10, 72	syl2anc 584	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
74	73	oveq1d 7425	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))))
75	74	eqeq1d 2738	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
76	14	resqcld 14148	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶↑2) ∈ ℝ)
77	76	3ad2ant1 1133	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℝ)
78		2re 12319	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
79	78	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℝ)
80	29, 9	remulcld 11270	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) ∈ ℝ)
81	79, 80	remulcld 11270	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) ∈ ℝ)
82	77, 81	resubcld 11670	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℝ)
83	9	resqcld 14148	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℝ)
84	82, 83	readdcld 11269	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) ∈ ℝ)
85	69, 61	remulcld 11270	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℝ)
86	84, 85	readdcld 11269	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℝ)
87	86	recnd 11268	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℂ)
88	65	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℝ)
89	69, 88	remulcld 11270	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℝ)
90	89	recnd 11268	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℂ)
91	87, 90, 90	subcan2ad 11644	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
92	82	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℂ)
93	83	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℂ)
94	85	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℂ)
95	92, 93, 94	addassd 11262	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2)))))
96	29	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
97	5	recnd 11268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
98	97	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
99	8	recnd 11268	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℂ)
100	96, 98, 99	mulassd 11263	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = (𝐶 · (𝐵 · 𝑌)))
101	15, 97	mulcomd 11261	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
102	101	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
103	102	oveq1d 7425	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = ((𝐵 · 𝐶) · 𝑌))
104	100, 103	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) = ((𝐵 · 𝐶) · 𝑌))
105	104	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = (2 · ((𝐵 · 𝐶) · 𝑌)))
106	79	recnd 11268	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℂ)
107	5, 14	remulcld 11270	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐶) ∈ ℝ)
108	107	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
109	108	recnd 11268	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
110	106, 109, 99	mulassd 11263	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) = (2 · ((𝐵 · 𝐶) · 𝑌)))
111	105, 110	eqtr4d 2774	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = ((2 · (𝐵 · 𝐶)) · 𝑌))
112	111	oveq2d 7426	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) = ((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
113	98, 99	sqmuld 14181	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) = ((𝐵↑2) · (𝑌↑2)))
114	113	oveq1d 7425	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2))) = (((𝐵↑2) · (𝑌↑2)) + ((𝐴↑2) · (𝑌↑2))))
115	6	resqcld 14148	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℝ)
116	115	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℂ)
117	31	resqcld 14148	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
118	117	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
119	61	recnd 11268	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
120	116, 118, 119	adddird 11265	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) = (((𝐵↑2) · (𝑌↑2)) + ((𝐴↑2) · (𝑌↑2))))
121	114, 120	eqtr4d 2774	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2))) = (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)))
122	112, 121	oveq12d 7428	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2)))) = (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))))
123	95, 122	eqtrd 2771	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))))
124	123	oveq1d 7425	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))))
125	77	recnd 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℂ)
126	5	resqcld 14148	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℝ)
127	126, 68	readdcld 11269	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
128	127	3ad2ant1 1133	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
129	128, 61	remulcld 11270	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℝ)
130	6, 29	remulcld 11270	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
131	79, 130	remulcld 11270	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℝ)
132	131, 8	remulcld 11270	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
133	129, 132	resubcld 11670	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℝ)
134	133	recnd 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℂ)
135	132	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
136	129	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℂ)
137	125, 135, 136	subadd23d 11621	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = ((𝐶↑2) + ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌))))
138	125, 134, 137	comraddd 11454	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)))
139	138	oveq1d 7425	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))))
140	134, 125, 90	addsubassd 11619	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
141	136, 135	negsubd 11605	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
142	141	eqcomd 2742	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)))
143	142	oveq1d 7425	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
144	132	renegcld 11669	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
145	144	recnd 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
146	77, 89	resubcld 11670	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℝ)
147	146	recnd 11268	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℂ)
148	136, 145, 147	addassd 11262	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
149	140, 143, 148	3eqtrd 2775	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
150	124, 139, 149	3eqtrd 2775	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
151	90	subidd 11587	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) = 0)
152	150, 151	eqeq12d 2752	. . . . . 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 307	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0))
154	60, 71, 153	3bitr3d 309	. . . 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 11454	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 = ((𝐵↑2) + (𝐴↑2)))
158	157	oveq1d 7425	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · (𝑌↑2)) = (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)))
159		itscnhlc0yqe.t	. . . . . . . . . . . 12 ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))
160	159	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑇 = -(2 · (𝐵 · 𝐶)))
161	160	oveq1d 7425	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑇 · 𝑌) = (-(2 · (𝐵 · 𝐶)) · 𝑌))
162	131	recnd 11268	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℂ)
163	162, 99	mulneg1d 11695	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (-(2 · (𝐵 · 𝐶)) · 𝑌) = -((2 · (𝐵 · 𝐶)) · 𝑌))
164	161, 163	eqtrd 2771	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑇 · 𝑌) = -((2 · (𝐵 · 𝐶)) · 𝑌))
165		itscnhlc0yqe.u	. . . . . . . . . 10 ⊢ 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))
166	165	a1i 11	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑈 = ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))
167	164, 166	oveq12d 7428	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑇 · 𝑌) + 𝑈) = (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
168	158, 167	oveq12d 7428	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
169	168	eqcomd 2742	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)))
170	169	eqeq1d 2738	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
171	170	biimpd 229	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
172	154, 171	sylbid 240	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
173	23, 172	syl5 34	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
174	19, 173	sylbid 240	1 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2933 (class class class)co 7410 ℂcc 11132 ℝcr 11133 0cc0 11134 + caddc 11137 · cmul 11139 − cmin 11471 -cneg 11472 / cdiv 11899 2c2 12300 ℝ⁺crp 13013 ↑cexp 14084

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2708 ax-sep 5271 ax-nul 5281 ax-pow 5340 ax-pr 5407 ax-un 7734 ax-cnex 11190 ax-resscn 11191 ax-1cn 11192 ax-icn 11193 ax-addcl 11194 ax-addrcl 11195 ax-mulcl 11196 ax-mulrcl 11197 ax-mulcom 11198 ax-addass 11199 ax-mulass 11200 ax-distr 11201 ax-i2m1 11202 ax-1ne0 11203 ax-1rid 11204 ax-rnegex 11205 ax-rrecex 11206 ax-cnre 11207 ax-pre-lttri 11208 ax-pre-lttrn 11209 ax-pre-ltadd 11210 ax-pre-mulgt0 11211

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2810 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3062 df-rmo 3364 df-reu 3365 df-rab 3421 df-v 3466 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-op 4613 df-uni 4889 df-iun 4974 df-br 5125 df-opab 5187 df-mpt 5207 df-tr 5235 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6295 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7867 df-2nd 7994 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-er 8724 df-en 8965 df-dom 8966 df-sdom 8967 df-pnf 11276 df-mnf 11277 df-xr 11278 df-ltxr 11279 df-le 11280 df-sub 11473 df-neg 11474 df-div 11900 df-nn 12246 df-2 12308 df-n0 12507 df-z 12594 df-uz 12858 df-rp 13014 df-seq 14025 df-exp 14085

This theorem is referenced by: itsclc0yqe 48708 itsclquadb 48723

W3C validator