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	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → ( ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) / 𝑊 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		remulcl	⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑆 · 𝑈 ) ∈ ℝ )
2	1	3adant2	⊢ ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) → ( 𝑆 · 𝑈 ) ∈ ℝ )
3	2	adantr	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( 𝑆 · 𝑈 ) ∈ ℝ )
4		simpl2	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → 𝑇 ∈ ℝ )
5		resqrtcl	⊢ ( ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) → ( √ ‘ 𝑉 ) ∈ ℝ )
6	5	adantl	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( √ ‘ 𝑉 ) ∈ ℝ )
7	4 6	remulcld	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( 𝑇 · ( √ ‘ 𝑉 ) ) ∈ ℝ )
8	3 7	readdcld	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ) → ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) ∈ ℝ )
9	8	3adant3	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) ∈ ℝ )
10		simp3l	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → 𝑊 ∈ ℝ )
11		simp3r	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → 𝑊 ≠ 0 )
12	9 10 11	redivcld	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 𝑇 ∈ ℝ ∧ 𝑈 ∈ ℝ ) ∧ ( 𝑉 ∈ ℝ ∧ 0 ≤ 𝑉 ) ∧ ( 𝑊 ∈ ℝ ∧ 𝑊 ≠ 0 ) ) → ( ( ( 𝑆 · 𝑈 ) + ( 𝑇 · ( √ ‘ 𝑉 ) ) ) / 𝑊 ) ∈ ℝ )