Step |
Hyp |
Ref |
Expression |
1 |
|
itsclquadb.q |
⊢ 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) |
2 |
|
itsclquadb.t |
⊢ 𝑇 = - ( 2 · ( 𝐵 · 𝐶 ) ) |
3 |
|
itsclquadb.u |
⊢ 𝑈 = ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) |
4 |
|
simpl1 |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ) |
5 |
|
simp2 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝑅 ∈ ℝ+ ) |
6 |
5
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → 𝑅 ∈ ℝ+ ) |
7 |
|
simp3 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝑌 ∈ ℝ ) |
8 |
7
|
anim1ci |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) |
9 |
1 2 3
|
itscnhlc0yqe |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ ( 𝑥 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ) |
10 |
4 6 8 9
|
syl3anc |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ) |
11 |
10
|
rexlimdva |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ) |
12 |
|
simp3 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ ) |
13 |
12
|
3ad2ant1 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐶 ∈ ℝ ) |
14 |
|
simp2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐵 ∈ ℝ ) |
15 |
14
|
3ad2ant1 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐵 ∈ ℝ ) |
16 |
15 7
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℝ ) |
17 |
13 16
|
resubcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 − ( 𝐵 · 𝑌 ) ) ∈ ℝ ) |
18 |
|
simp11l |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐴 ∈ ℝ ) |
19 |
|
simp11r |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐴 ≠ 0 ) |
20 |
17 18 19
|
redivcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ∈ ℝ ) |
21 |
20
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ∈ ℝ ) |
22 |
|
oveq1 |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( 𝑥 ↑ 2 ) = ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) ) |
23 |
22
|
oveq1d |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) ) |
24 |
23
|
eqeq1d |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ↔ ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) |
25 |
|
oveq2 |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( 𝐴 · 𝑥 ) = ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) ) |
26 |
25
|
oveq1d |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) ) |
27 |
26
|
eqeq1d |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ↔ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) |
28 |
24 27
|
anbi12d |
⊢ ( 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) ) |
29 |
28
|
adantl |
⊢ ( ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ∧ 𝑥 = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) → ( ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) ) |
30 |
17
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 − ( 𝐵 · 𝑌 ) ) ∈ ℂ ) |
31 |
18
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐴 ∈ ℂ ) |
32 |
30 31 19
|
sqdivd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) = ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) |
33 |
13
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐶 ∈ ℂ ) |
34 |
16
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 · 𝑌 ) ∈ ℂ ) |
35 |
|
binom2sub |
⊢ ( ( 𝐶 ∈ ℂ ∧ ( 𝐵 · 𝑌 ) ∈ ℂ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) |
36 |
33 34 35
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) ) |
37 |
13
|
resqcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℝ ) |
38 |
37
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℂ ) |
39 |
|
2re |
⊢ 2 ∈ ℝ |
40 |
39
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 2 ∈ ℝ ) |
41 |
13 16
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 · ( 𝐵 · 𝑌 ) ) ∈ ℝ ) |
42 |
40 41
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ∈ ℝ ) |
43 |
42
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ∈ ℂ ) |
44 |
38 43
|
negsubd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) ) |
45 |
15
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝐵 ∈ ℂ ) |
46 |
7
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝑌 ∈ ℂ ) |
47 |
33 45 46
|
mulassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 · 𝐵 ) · 𝑌 ) = ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) |
48 |
47
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 · ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) |
49 |
48
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) ) |
50 |
|
2cnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 2 ∈ ℂ ) |
51 |
13 15
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℝ ) |
52 |
51
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) ∈ ℂ ) |
53 |
50 52 46
|
mulassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) = ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) ) |
54 |
53
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( ( 𝐶 · 𝐵 ) · 𝑌 ) ) = ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) ) |
55 |
33 45
|
mulcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) ) |
56 |
55
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · 𝐵 ) ) = ( 2 · ( 𝐵 · 𝐶 ) ) ) |
57 |
56
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 2 · ( 𝐶 · 𝐵 ) ) · 𝑌 ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) |
58 |
49 54 57
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) |
59 |
58
|
negeqd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) = - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) |
60 |
59
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) ) |
61 |
44 60
|
eqtr3d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) ) |
62 |
45 46
|
sqmuld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 · 𝑌 ) ↑ 2 ) = ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) |
63 |
61 62
|
oveq12d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) − ( 2 · ( 𝐶 · ( 𝐵 · 𝑌 ) ) ) ) + ( ( 𝐵 · 𝑌 ) ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) |
64 |
15 13
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 · 𝐶 ) ∈ ℝ ) |
65 |
40 64
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ ) |
66 |
65
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℂ ) |
67 |
66 46
|
mulneg1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) |
68 |
2
|
eqcomi |
⊢ - ( 2 · ( 𝐵 · 𝐶 ) ) = 𝑇 |
69 |
68
|
oveq1i |
⊢ ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 ) |
70 |
69
|
a1i |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( - ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 ) ) |
71 |
67 70
|
eqtr3d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) = ( 𝑇 · 𝑌 ) ) |
72 |
71
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) ) |
73 |
72
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 2 · ( 𝐵 · 𝐶 ) ) · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) |
74 |
36 63 73
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) |
75 |
74
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) ↑ 2 ) / ( 𝐴 ↑ 2 ) ) = ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
76 |
32 75
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) = ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
77 |
|
resqcl |
⊢ ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℝ ) |
78 |
77
|
recnd |
⊢ ( 𝑌 ∈ ℝ → ( 𝑌 ↑ 2 ) ∈ ℂ ) |
79 |
78
|
3ad2ant3 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℂ ) |
80 |
18
|
resqcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℝ ) |
81 |
80
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ∈ ℂ ) |
82 |
|
recn |
⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ ) |
83 |
|
sqne0 |
⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) ) |
84 |
82 83
|
syl |
⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 ↑ 2 ) ≠ 0 ↔ 𝐴 ≠ 0 ) ) |
85 |
84
|
biimpar |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 𝐴 ↑ 2 ) ≠ 0 ) |
86 |
85
|
3ad2ant1 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ≠ 0 ) |
87 |
86
|
3ad2ant1 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 ↑ 2 ) ≠ 0 ) |
88 |
79 81 87
|
divcan2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) = ( 𝑌 ↑ 2 ) ) |
89 |
88
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) |
90 |
76 89
|
oveq12d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) ) |
91 |
81 79 81 87
|
divassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) |
92 |
91
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) |
93 |
92
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( ( 𝑌 ↑ 2 ) / ( 𝐴 ↑ 2 ) ) ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) ) |
94 |
65
|
renegcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → - ( 2 · ( 𝐵 · 𝐶 ) ) ∈ ℝ ) |
95 |
2 94
|
eqeltrid |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → 𝑇 ∈ ℝ ) |
96 |
95 7
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑇 · 𝑌 ) ∈ ℝ ) |
97 |
37 96
|
readdcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) ∈ ℝ ) |
98 |
15
|
resqcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℝ ) |
99 |
7
|
resqcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℝ ) |
100 |
98 99
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ ) |
101 |
97 100
|
readdcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ∈ ℝ ) |
102 |
101
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ∈ ℂ ) |
103 |
80 99
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ ) |
104 |
103
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ ) |
105 |
102 104 81 87
|
divdird |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) ) |
106 |
105
|
eqcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) + ( ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
107 |
90 93 106
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
108 |
107
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
109 |
97
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ ) |
110 |
100
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ ) |
111 |
109 110 104
|
addassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) ) |
112 |
98
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐵 ↑ 2 ) ∈ ℂ ) |
113 |
99
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑌 ↑ 2 ) ∈ ℂ ) |
114 |
112 81 113
|
adddird |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) |
115 |
112 81
|
addcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) |
116 |
115
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) |
117 |
114 116
|
eqtr3d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) |
118 |
117
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) ) |
119 |
96
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑇 · 𝑌 ) ∈ ℂ ) |
120 |
80 98
|
readdcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ∈ ℝ ) |
121 |
120 99
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ∈ ℝ ) |
122 |
121
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ∈ ℂ ) |
123 |
38 119 122
|
addassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) ) ) |
124 |
119 122
|
addcomd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) |
125 |
124
|
oveq2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + ( ( 𝑇 · 𝑌 ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) ) |
126 |
123 125
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) ) |
127 |
111 118 126
|
3eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) ) |
128 |
127
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) ) |
129 |
128
|
oveq1d |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( ( 𝐶 ↑ 2 ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐵 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) + ( ( 𝐴 ↑ 2 ) · ( 𝑌 ↑ 2 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
130 |
1
|
oveq1i |
⊢ ( 𝑄 · ( 𝑌 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) |
131 |
3
|
oveq2i |
⊢ ( ( 𝑇 · 𝑌 ) + 𝑈 ) = ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) |
132 |
130 131
|
oveq12i |
⊢ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
133 |
|
rpre |
⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ ) |
134 |
133
|
resqcld |
⊢ ( 𝑅 ∈ ℝ+ → ( 𝑅 ↑ 2 ) ∈ ℝ ) |
135 |
134
|
3ad2ant2 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ ) |
136 |
80 135
|
remulcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℝ ) |
137 |
37 136
|
resubcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℝ ) |
138 |
137
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ ) |
139 |
122 119 138
|
addassd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) |
140 |
132 139
|
eqtr4id |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
141 |
140
|
eqeq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ↔ ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ) ) |
142 |
121 96
|
readdcld |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℝ ) |
143 |
142
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ ) |
144 |
|
addeq0 |
⊢ ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ∈ ℂ ∧ ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ∈ ℂ ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
145 |
143 138 144
|
syl2anc |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) + ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
146 |
141 145
|
bitrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ↔ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
147 |
|
oveq2 |
⊢ ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) = ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
148 |
147
|
oveq1d |
⊢ ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) ) |
149 |
38 138
|
negsubd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐶 ↑ 2 ) − ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
150 |
136
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ∈ ℂ ) |
151 |
38 150
|
nncand |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) |
152 |
149 151
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) |
153 |
152
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) ) |
154 |
135
|
recnd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℂ ) |
155 |
154 81 87
|
divcan3d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) |
156 |
153 155
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝐶 ↑ 2 ) + - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) |
157 |
148 156
|
sylan9eqr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) |
158 |
157
|
ex |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) = - ( ( 𝐶 ↑ 2 ) − ( ( 𝐴 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) |
159 |
146 158
|
sylbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) ) |
160 |
159
|
imp |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( 𝐶 ↑ 2 ) + ( ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( 𝑌 ↑ 2 ) ) + ( 𝑇 · 𝑌 ) ) ) / ( 𝐴 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) |
161 |
108 129 160
|
3eqtrd |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ) |
162 |
30 31 19
|
divcan2d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) = ( 𝐶 − ( 𝐵 · 𝑌 ) ) ) |
163 |
162
|
oveq1d |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) + ( 𝐵 · 𝑌 ) ) ) |
164 |
33 34
|
npcand |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) |
165 |
163 164
|
eqtrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) |
166 |
165
|
adantr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) |
167 |
161 166
|
jca |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ( ( ( ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · ( ( 𝐶 − ( 𝐵 · 𝑌 ) ) / 𝐴 ) ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) |
168 |
21 29 167
|
rspcedvd |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) ∧ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) → ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) |
169 |
168
|
ex |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 → ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ) ) |
170 |
11 169
|
impbid |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ+ ∧ 𝑌 ∈ ℝ ) → ( ∃ 𝑥 ∈ ℝ ( ( ( 𝑥 ↑ 2 ) + ( 𝑌 ↑ 2 ) ) = ( 𝑅 ↑ 2 ) ∧ ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑌 ) ) = 𝐶 ) ↔ ( ( 𝑄 · ( 𝑌 ↑ 2 ) ) + ( ( 𝑇 · 𝑌 ) + 𝑈 ) ) = 0 ) ) |