Metamath Proof Explorer

Theorem itsclc0lem2

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

		Ref	Expression
	Assertion	itsclc0lem2	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V) \land (W \in ℝ \land W \neq 0)) \to \frac{S U - T \sqrt{V}}{W} \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (S \in ℝ \land T \in ℝ \land U \in ℝ) \to S \in ℝ$
2		simp3	$⊢ (S \in ℝ \land T \in ℝ \land U \in ℝ) \to U \in ℝ$
3	1 2	remulcld	$⊢ (S \in ℝ \land T \in ℝ \land U \in ℝ) \to S U \in ℝ$
4	3	adantr	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to S U \in ℝ$
5		simpl2	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to T \in ℝ$
6		resqrtcl	$⊢ (V \in ℝ \land 0 \leq V) \to \sqrt{V} \in ℝ$
7	6	adantl	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to \sqrt{V} \in ℝ$
8	5 7	remulcld	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to T \sqrt{V} \in ℝ$
9	4 8	resubcld	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to S U - T \sqrt{V} \in ℝ$
10	9	3adant3	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V) \land (W \in ℝ \land W \neq 0)) \to S U - T \sqrt{V} \in ℝ$
11		simp3l	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V) \land (W \in ℝ \land W \neq 0)) \to W \in ℝ$
12		simp3r	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V) \land (W \in ℝ \land W \neq 0)) \to W \neq 0$
13	10 11 12	redivcld	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V) \land (W \in ℝ \land W \neq 0)) \to \frac{S U - T \sqrt{V}}{W} \in ℝ$