| 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 ) ) |