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

Proof

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