Step |
Hyp |
Ref |
Expression |
1 |
|
itscnhlinecirc02plem2.d |
⊢ 𝐷 = ( 𝑋 − 𝐴 ) |
2 |
|
itscnhlinecirc02plem2.e |
⊢ 𝐸 = ( 𝐵 − 𝑌 ) |
3 |
|
itscnhlinecirc02plem2.c |
⊢ 𝐶 = ( ( 𝐵 · 𝑋 ) − ( 𝐴 · 𝑌 ) ) |
4 |
|
simpl1l |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝐴 ∈ ℝ ) |
5 |
|
simpl1r |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝐵 ∈ ℝ ) |
6 |
|
simpl2l |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝑋 ∈ ℝ ) |
7 |
|
simpl2r |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝑌 ∈ ℝ ) |
8 |
|
eqid |
⊢ ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) |
9 |
|
simprl |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝑅 ∈ ℝ ) |
10 |
|
simprr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) |
11 |
|
simpl3 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 𝐵 ≠ 𝑌 ) |
12 |
4 5 6 7 1 2 8 9 10 11
|
itscnhlinecirc02plem1 |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 0 < ( ( - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) |
13 |
|
simplr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℝ ) |
14 |
13
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐵 ∈ ℂ ) |
15 |
|
simprl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℝ ) |
16 |
15
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑋 ∈ ℂ ) |
17 |
14 16
|
mulcomd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝑋 ) = ( 𝑋 · 𝐵 ) ) |
18 |
|
simpll |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℝ ) |
19 |
18
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐴 ∈ ℂ ) |
20 |
|
simprr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℝ ) |
21 |
20
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝑌 ∈ ℂ ) |
22 |
19 21
|
mulcomd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · 𝑌 ) = ( 𝑌 · 𝐴 ) ) |
23 |
17 22
|
oveq12d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑋 ) − ( 𝐴 · 𝑌 ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) |
24 |
16 19 14
|
subdird |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝑋 − 𝐴 ) · 𝐵 ) = ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) ) |
25 |
14 21 19
|
subdird |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 − 𝑌 ) · 𝐴 ) = ( ( 𝐵 · 𝐴 ) − ( 𝑌 · 𝐴 ) ) ) |
26 |
24 25
|
oveq12d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) + ( ( 𝐵 − 𝑌 ) · 𝐴 ) ) = ( ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐵 · 𝐴 ) − ( 𝑌 · 𝐴 ) ) ) ) |
27 |
14 19
|
mulcomd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐵 · 𝐴 ) = ( 𝐴 · 𝐵 ) ) |
28 |
27
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝐴 ) − ( 𝑌 · 𝐴 ) ) = ( ( 𝐴 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) |
29 |
28
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐵 · 𝐴 ) − ( 𝑌 · 𝐴 ) ) ) = ( ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) ) |
30 |
16 14
|
mulcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑋 · 𝐵 ) ∈ ℂ ) |
31 |
19 14
|
mulcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ ) |
32 |
21 19
|
mulcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝑌 · 𝐴 ) ∈ ℂ ) |
33 |
30 31 32
|
npncand |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑋 · 𝐵 ) − ( 𝐴 · 𝐵 ) ) + ( ( 𝐴 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) |
34 |
26 29 33
|
3eqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) + ( ( 𝐵 − 𝑌 ) · 𝐴 ) ) = ( ( 𝑋 · 𝐵 ) − ( 𝑌 · 𝐴 ) ) ) |
35 |
23 34
|
eqtr4d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐵 · 𝑋 ) − ( 𝐴 · 𝑌 ) ) = ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) + ( ( 𝐵 − 𝑌 ) · 𝐴 ) ) ) |
36 |
1
|
oveq1i |
⊢ ( 𝐷 · 𝐵 ) = ( ( 𝑋 − 𝐴 ) · 𝐵 ) |
37 |
2
|
oveq1i |
⊢ ( 𝐸 · 𝐴 ) = ( ( 𝐵 − 𝑌 ) · 𝐴 ) |
38 |
36 37
|
oveq12i |
⊢ ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) = ( ( ( 𝑋 − 𝐴 ) · 𝐵 ) + ( ( 𝐵 − 𝑌 ) · 𝐴 ) ) |
39 |
35 3 38
|
3eqtr4g |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → 𝐶 = ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) |
40 |
39
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐷 · 𝐶 ) = ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) |
41 |
40
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 2 · ( 𝐷 · 𝐶 ) ) = ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ) |
42 |
41
|
negeqd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → - ( 2 · ( 𝐷 · 𝐶 ) ) = - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ) |
43 |
42
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) = ( - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ↑ 2 ) ) |
44 |
39
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 𝐶 ↑ 2 ) = ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) ) |
45 |
44
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) = ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) |
46 |
45
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) = ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) |
47 |
46
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) = ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) |
48 |
43 47
|
oveq12d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ) → ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) |
49 |
48
|
3adant3 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) → ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) |
50 |
49
|
adantr |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) = ( ( - ( 2 · ( 𝐷 · ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( ( ( 𝐷 · 𝐵 ) + ( 𝐸 · 𝐴 ) ) ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) |
51 |
12 50
|
breqtrrd |
⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 0 < ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) ) |