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 ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V ∧ W ∈ ℝ ∧ W ≠ 0 → S ⁢ U + T ⁢ V W ∈ ℝ

Proof

Step Hyp Ref Expression
1 remulcl ⊢ S ∈ ℝ ∧ U ∈ ℝ → S ⁢ U ∈ ℝ
2 1 3adant2 ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ → S ⁢ U ∈ ℝ
3 2 adantr ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V → S ⁢ U ∈ ℝ
4 simpl2 ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V → T ∈ ℝ
5 resqrtcl ⊢ V ∈ ℝ ∧ 0 ≤ V → V ∈ ℝ
6 5 adantl ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V → V ∈ ℝ
7 4 6 remulcld ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V → T ⁢ V ∈ ℝ
8 3 7 readdcld ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V → S ⁢ U + T ⁢ V ∈ ℝ
9 8 3adant3 ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V ∧ W ∈ ℝ ∧ W ≠ 0 → S ⁢ U + T ⁢ V ∈ ℝ
10 simp3l ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V ∧ W ∈ ℝ ∧ W ≠ 0 → W ∈ ℝ
11 simp3r ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V ∧ W ∈ ℝ ∧ W ≠ 0 → W ≠ 0
12 9 10 11 redivcld ⊢ S ∈ ℝ ∧ T ∈ ℝ ∧ U ∈ ℝ ∧ V ∈ ℝ ∧ 0 ≤ V ∧ W ∈ ℝ ∧ W ≠ 0 → S ⁢ U + T ⁢ V W ∈ ℝ