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 47609

Description: Lemma for itsclc0 47621. 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 11206	. . . . . . 7 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
2	1	adantr 480	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
3	2	3ad2ant1 1132	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
4	3	3ad2ant1 1132	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
5		simp2 1136	. . . . . . 7 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
6	5	3ad2ant1 1132	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℝ)
7		simpr 484	. . . . . . 7 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ∈ ℝ)
8	7	3ad2ant3 1134	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℝ)
9	6, 8	remulcld 11251	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℝ)
10	9	recnd 11249	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝑌) ∈ ℂ)
11		recn 11206	. . . . . 6 ⊢ (𝑋 ∈ ℝ → 𝑋 ∈ ℂ)
12	11	adantr 480	. . . . 5 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑋 ∈ ℂ)
13	12	3ad2ant3 1134	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑋 ∈ ℂ)
14		simp3 1137	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
15	14	recnd 11249	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℂ)
16	15	3ad2ant1 1132	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
17		simp11r 1284	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ≠ 0)
18	4, 10, 13, 16, 17	lineq 12058	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶 ↔ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)))
19	18	anbi2d 628	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) ↔ (((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴))))
20		oveq1 7419	. . . . . 6 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → (𝑋↑2) = (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2))
21	20	oveq1d 7427	. . . . 5 ⊢ (𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴) → ((𝑋↑2) + (𝑌↑2)) = ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)))
22	21	eqeq1d 2733	. . . 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 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
26	25	resqcld 14097	. . . . . . . . . 10 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
27	26	recnd 11249	. . . . . . . . 9 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
28	27	3ad2ant1 1132	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
29	14	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℝ)
30	29, 9	resubcld 11649	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℝ)
31	25	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℝ)
32	30, 31, 17	redivcld 12049	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌)) / 𝐴) ∈ ℝ)
33	32	resqcld 14097	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℝ)
34	33	recnd 11249	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) ∈ ℂ)
35	7	resqcld 14097	. . . . . . . . . 10 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℝ)
36	35	recnd 11249	. . . . . . . . 9 ⊢ ((𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ) → (𝑌↑2) ∈ ℂ)
37	36	3ad2ant3 1134	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
38	28, 34, 37	adddid 11245	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = (((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) + ((𝐴↑2) · (𝑌↑2))))
39	30	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 − (𝐵 · 𝑌)) ∈ ℂ)
40	24	recnd 11249	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → 𝐴 ∈ ℂ)
41	40	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℂ)
42	41	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐴 ∈ ℂ)
43	39, 42, 17	sqdivd 14131	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) = (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2)))
44	43	oveq2d 7428	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))))
45	30	resqcld 14097	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℝ)
46	45	recnd 11249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) ∈ ℂ)
47	24	resqcld 14097	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℝ)
48	47	recnd 11249	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ∈ ℂ)
49	48	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℂ)
50	49	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
51		sqne0 14095	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ ℂ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
52	1, 51	syl 17	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ ℝ → ((𝐴↑2) ≠ 0 ↔ 𝐴 ≠ 0))
53	52	biimpar 477	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → (𝐴↑2) ≠ 0)
54	53	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ≠ 0)
55	54	3ad2ant1 1132	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ≠ 0)
56	46, 50, 55	divcan2d 11999	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌))↑2) / (𝐴↑2))) = ((𝐶 − (𝐵 · 𝑌))↑2))
57	44, 56	eqtrd 2771	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2)) = ((𝐶 − (𝐵 · 𝑌))↑2))
58	57	oveq1d 7427	. . . . . . 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 2733	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
61	8	resqcld 14097	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℝ)
62	33, 61	readdcld 11250	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℝ)
63	62	recnd 11249	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) ∈ ℂ)
64		rpre 12989	. . . . . . . . 9 ⊢ (𝑅 ∈ ℝ⁺ → 𝑅 ∈ ℝ)
65	64	resqcld 14097	. . . . . . . 8 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℝ)
66	65	recnd 11249	. . . . . . 7 ⊢ (𝑅 ∈ ℝ⁺ → (𝑅↑2) ∈ ℂ)
67	66	3ad2ant2 1133	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℂ)
68	47	3ad2ant1 1132	. . . . . . . 8 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴↑2) ∈ ℝ)
69	68	3ad2ant1 1132	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
70	69	recnd 11249	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
71	63, 67, 70, 55	mulcand 11854	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2)))
72		binom2sub 14190	. . . . . . . . 9 ⊢ ((𝐶 ∈ ℂ ∧ (𝐵 · 𝑌) ∈ ℂ) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
73	16, 10, 72	syl2anc 583	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 − (𝐵 · 𝑌))↑2) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)))
74	73	oveq1d 7427	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))))
75	74	eqeq1d 2733	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶 − (𝐵 · 𝑌))↑2) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2)) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
76	14	resqcld 14097	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶↑2) ∈ ℝ)
77	76	3ad2ant1 1132	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℝ)
78		2re 12293	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℝ
79	78	a1i 11	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℝ)
80	29, 9	remulcld 11251	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) ∈ ℝ)
81	79, 80	remulcld 11251	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) ∈ ℝ)
82	77, 81	resubcld 11649	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℝ)
83	9	resqcld 14097	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℝ)
84	82, 83	readdcld 11250	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) ∈ ℝ)
85	69, 61	remulcld 11251	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℝ)
86	84, 85	readdcld 11250	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℝ)
87	86	recnd 11249	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) ∈ ℂ)
88	65	3ad2ant2 1133	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑅↑2) ∈ ℝ)
89	69, 88	remulcld 11251	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℝ)
90	89	recnd 11249	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑅↑2)) ∈ ℂ)
91	87, 90, 90	subcan2ad 11623	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) ↔ ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = ((𝐴↑2) · (𝑅↑2))))
92	82	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) ∈ ℂ)
93	83	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) ∈ ℂ)
94	85	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐴↑2) · (𝑌↑2)) ∈ ℂ)
95	92, 93, 94	addassd 11243	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) = (((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2)))))
96	29	recnd 11249	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐶 ∈ ℂ)
97	5	recnd 11249	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℂ)
98	97	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝐵 ∈ ℂ)
99	8	recnd 11249	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑌 ∈ ℂ)
100	96, 98, 99	mulassd 11244	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = (𝐶 · (𝐵 · 𝑌)))
101	15, 97	mulcomd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
102	101	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · 𝐵) = (𝐵 · 𝐶))
103	102	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶 · 𝐵) · 𝑌) = ((𝐵 · 𝐶) · 𝑌))
104	100, 103	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶 · (𝐵 · 𝑌)) = ((𝐵 · 𝐶) · 𝑌))
105	104	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = (2 · ((𝐵 · 𝐶) · 𝑌)))
106	79	recnd 11249	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 2 ∈ ℂ)
107	5, 14	remulcld 11251	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 · 𝐶) ∈ ℝ)
108	107	3ad2ant1 1132	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
109	108	recnd 11249	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℂ)
110	106, 109, 99	mulassd 11244	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) = (2 · ((𝐵 · 𝐶) · 𝑌)))
111	105, 110	eqtr4d 2774	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐶 · (𝐵 · 𝑌))) = ((2 · (𝐵 · 𝐶)) · 𝑌))
112	111	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) = ((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
113	98, 99	sqmuld 14130	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵 · 𝑌)↑2) = ((𝐵↑2) · (𝑌↑2)))
114	113	oveq1d 7427	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵 · 𝑌)↑2) + ((𝐴↑2) · (𝑌↑2))) = (((𝐵↑2) · (𝑌↑2)) + ((𝐴↑2) · (𝑌↑2))))
115	6	resqcld 14097	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℝ)
116	115	recnd 11249	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵↑2) ∈ ℂ)
117	31	resqcld 14097	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℝ)
118	117	recnd 11249	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐴↑2) ∈ ℂ)
119	61	recnd 11249	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑌↑2) ∈ ℂ)
120	116, 118, 119	adddird 11246	. . . . . . . . . . . 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 7430	. . . . . . . . . 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 7427	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶↑2) − (2 · (𝐶 · (𝐵 · 𝑌)))) + ((𝐵 · 𝑌)↑2)) + ((𝐴↑2) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))))
125	77	recnd 11249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐶↑2) ∈ ℂ)
126	5	resqcld 14097	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵↑2) ∈ ℝ)
127	126, 68	readdcld 11250	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
128	127	3ad2ant1 1132	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐵↑2) + (𝐴↑2)) ∈ ℝ)
129	128, 61	remulcld 11251	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℝ)
130	6, 29	remulcld 11251	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝐵 · 𝐶) ∈ ℝ)
131	79, 130	remulcld 11251	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℝ)
132	131, 8	remulcld 11251	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
133	129, 132	resubcld 11649	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℝ)
134	133	recnd 11249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) ∈ ℂ)
135	132	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
136	129	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) ∈ ℂ)
137	125, 135, 136	subadd23d 11600	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = ((𝐶↑2) + ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌))))
138	125, 134, 137	comraddd 11435	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)))
139	138	oveq1d 7427	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐶↑2) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2))) − ((𝐴↑2) · (𝑅↑2))) = ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))))
140	134, 125, 90	addsubassd 11598	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + (𝐶↑2)) − ((𝐴↑2) · (𝑅↑2))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
141	136, 135	negsubd 11584	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)))
142	141	eqcomd 2737	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)))
143	142	oveq1d 7427	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) − ((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))) = (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + -((2 · (𝐵 · 𝐶)) · 𝑌)) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
144	132	renegcld 11648	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℝ)
145	144	recnd 11249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → -((2 · (𝐵 · 𝐶)) · 𝑌) ∈ ℂ)
146	77, 89	resubcld 11649	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℝ)
147	146	recnd 11249	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))) ∈ ℂ)
148	136, 145, 147	addassd 11243	. . . . . . . . 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 11566	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((𝐴↑2) · (𝑅↑2)) − ((𝐴↑2) · (𝑅↑2))) = 0)
152	150, 151	eqeq12d 2747	. . . . . 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 11435	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑄 = ((𝐵↑2) + (𝐴↑2)))
158	157	oveq1d 7427	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑄 · (𝑌↑2)) = (((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)))
159		itscnhlc0yqe.t	. . . . . . . . . . . 12 ⊢ 𝑇 = -(2 · (𝐵 · 𝐶))
160	159	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → 𝑇 = -(2 · (𝐵 · 𝐶)))
161	160	oveq1d 7427	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (𝑇 · 𝑌) = (-(2 · (𝐵 · 𝐶)) · 𝑌))
162	131	recnd 11249	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (2 · (𝐵 · 𝐶)) ∈ ℂ)
163	162, 99	mulneg1d 11674	. . . . . . . . . 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 7430	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑇 · 𝑌) + 𝑈) = (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2)))))
168	158, 167	oveq12d 7430	. . . . . . 7 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))))
169	168	eqcomd 2737	. . . . . 6 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)))
170	169	eqeq1d 2733	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 ↔ ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
171	170	biimpd 228	. . . 4 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐵↑2) + (𝐴↑2)) · (𝑌↑2)) + (-((2 · (𝐵 · 𝐶)) · 𝑌) + ((𝐶↑2) − ((𝐴↑2) · (𝑅↑2))))) = 0 → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
172	154, 171	sylbid 239	. . 3 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → (((((𝐶 − (𝐵 · 𝑌)) / 𝐴)↑2) + (𝑌↑2)) = (𝑅↑2) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
173	23, 172	syl5 34	. 2 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ 𝑋 = ((𝐶 − (𝐵 · 𝑌)) / 𝐴)) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))
174	19, 173	sylbid 239	1 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝑅 ∈ ℝ⁺ ∧ (𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ)) → ((((𝑋↑2) + (𝑌↑2)) = (𝑅↑2) ∧ ((𝐴 · 𝑋) + (𝐵 · 𝑌)) = 𝐶) → ((𝑄 · (𝑌↑2)) + ((𝑇 · 𝑌) + 𝑈)) = 0))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 (class class class)co 7412 ℂcc 11114 ℝcr 11115 0cc0 11116 + caddc 11119 · cmul 11121 − cmin 11451 -cneg 11452 / cdiv 11878 2c2 12274 ℝ⁺crp 12981 ↑cexp 14034

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11172 ax-resscn 11173 ax-1cn 11174 ax-icn 11175 ax-addcl 11176 ax-addrcl 11177 ax-mulcl 11178 ax-mulrcl 11179 ax-mulcom 11180 ax-addass 11181 ax-mulass 11182 ax-distr 11183 ax-i2m1 11184 ax-1ne0 11185 ax-1rid 11186 ax-rnegex 11187 ax-rrecex 11188 ax-cnre 11189 ax-pre-lttri 11190 ax-pre-lttrn 11191 ax-pre-ltadd 11192 ax-pre-mulgt0 11193

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-2nd 7980 df-frecs 8272 df-wrecs 8303 df-recs 8377 df-rdg 8416 df-er 8709 df-en 8946 df-dom 8947 df-sdom 8948 df-pnf 11257 df-mnf 11258 df-xr 11259 df-ltxr 11260 df-le 11261 df-sub 11453 df-neg 11454 df-div 11879 df-nn 12220 df-2 12282 df-n0 12480 df-z 12566 df-uz 12830 df-rp 12982 df-seq 13974 df-exp 14035

This theorem is referenced by: itsclc0yqe 47611 itsclquadb 47626

W3C validator