Metamath Proof Explorer

Theorem itscnhlinecirc02plem2

Description: Lemma 2 for itscnhlinecirc02p . (Contributed by AV, 10-Mar-2023)

Ref Expression
Hypotheses itscnhlinecirc02plem2.d ⊢ 𝐷 = ( 𝑋 − 𝐴 )
itscnhlinecirc02plem2.e ⊢ 𝐸 = ( 𝐵 − 𝑌 )
itscnhlinecirc02plem2.c ⊢ 𝐶 = ( ( 𝐵 · 𝑋 ) − ( 𝐴 · 𝑌 ) )
Assertion itscnhlinecirc02plem2 ( ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑋 ∈ ℝ ∧ 𝑌 ∈ ℝ ) ∧ 𝐵 ≠ 𝑌 ) ∧ ( 𝑅 ∈ ℝ ∧ ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) < ( 𝑅 ↑ 2 ) ) ) → 0 < ( ( - ( 2 · ( 𝐷 · 𝐶 ) ) ↑ 2 ) − ( 4 · ( ( ( 𝐸 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) − ( ( 𝐸 ↑ 2 ) · ( 𝑅 ↑ 2 ) ) ) ) ) ) )

Proof

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