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