Metamath Proof Explorer

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

Proof

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