Metamath Proof Explorer

Theorem itsclc0lem1

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
	Assertion	itsclc0lem1	$⊢ ((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		remulcl	$⊢ (S \in ℝ \land U \in ℝ) \to S U \in ℝ$
2	1	3adant2	$⊢ (S \in ℝ \land T \in ℝ \land U \in ℝ) \to S U \in ℝ$
3	2	adantr	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to S U \in ℝ$
4		simpl2	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to T \in ℝ$
5		resqrtcl	$⊢ (V \in ℝ \land 0 \leq V) \to \sqrt{V} \in ℝ$
6	5	adantl	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to \sqrt{V} \in ℝ$
7	4 6	remulcld	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to T \sqrt{V} \in ℝ$
8	3 7	readdcld	$⊢ ((S \in ℝ \land T \in ℝ \land U \in ℝ) \land (V \in ℝ \land 0 \leq V)) \to S U + T \sqrt{V} \in ℝ$
9	8	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 ℝ$
10		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 ℝ$
11		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$
12	9 10 11	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 ℝ$