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