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	$⊢ Q = A^{2} + B^{2}$
		itsclc0lem3.d	$⊢ D = R^{2} Q - C^{2}$
	Assertion	itsclc0lem3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to D \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		itsclc0lem3.q	$⊢ Q = A^{2} + B^{2}$
2		itsclc0lem3.d	$⊢ D = R^{2} Q - C^{2}$
3		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to R \in ℝ$
4	3	resqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to R^{2} \in ℝ$
5	1	resum2sqcl	$⊢ (A \in ℝ \land B \in ℝ) \to Q \in ℝ$
6	5	3adant3	$⊢ (A \in ℝ \land B \in ℝ \land C \in ℝ) \to Q \in ℝ$
7	6	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to Q \in ℝ$
8	4 7	remulcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to R^{2} Q \in ℝ$
9		simpl3	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to C \in ℝ$
10	9	resqcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to C^{2} \in ℝ$
11	8 10	resubcld	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to R^{2} Q - C^{2} \in ℝ$
12	2 11	eqeltrid	$⊢ ((A \in ℝ \land B \in ℝ \land C \in ℝ) \land R \in ℝ) \to D \in ℝ$