Metamath Proof Explorer


Theorem itsclc0lem3

Description: Lemma for theorems about intersections of lines and circles in a real Euclidean space of dimension 2 . (Contributed by AV, 2-May-2023)

Ref Expression
Hypotheses itsclc0lem3.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
itsclc0lem3.d 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
Assertion itsclc0lem3 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 itsclc0lem3.q 𝑄 = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) )
2 itsclc0lem3.d 𝐷 = ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) )
3 simpr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝑅 ∈ ℝ )
4 3 resqcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( 𝑅 ↑ 2 ) ∈ ℝ )
5 1 resum2sqcl ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝑄 ∈ ℝ )
6 5 3adant3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝑄 ∈ ℝ )
7 6 adantr ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝑄 ∈ ℝ )
8 4 7 remulcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( ( 𝑅 ↑ 2 ) · 𝑄 ) ∈ ℝ )
9 simpl3 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝐶 ∈ ℝ )
10 9 resqcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( 𝐶 ↑ 2 ) ∈ ℝ )
11 8 10 resubcld ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → ( ( ( 𝑅 ↑ 2 ) · 𝑄 ) − ( 𝐶 ↑ 2 ) ) ∈ ℝ )
12 2 11 eqeltrid ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) ∧ 𝑅 ∈ ℝ ) → 𝐷 ∈ ℝ )