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 e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> ( ( ( S x. U ) - ( T x. ( sqrt ` V ) ) ) / W ) e. RR )

Proof

Step Hyp Ref Expression
1 simp1
 |-  ( ( S e. RR /\ T e. RR /\ U e. RR ) -> S e. RR )
2 simp3
 |-  ( ( S e. RR /\ T e. RR /\ U e. RR ) -> U e. RR )
3 1 2 remulcld
 |-  ( ( S e. RR /\ T e. RR /\ U e. RR ) -> ( S x. U ) e. RR )
4 3 adantr
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( S x. U ) e. RR )
5 simpl2
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> T e. RR )
6 resqrtcl
 |-  ( ( V e. RR /\ 0 <_ V ) -> ( sqrt ` V ) e. RR )
7 6 adantl
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( sqrt ` V ) e. RR )
8 5 7 remulcld
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( T x. ( sqrt ` V ) ) e. RR )
9 4 8 resubcld
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( ( S x. U ) - ( T x. ( sqrt ` V ) ) ) e. RR )
10 9 3adant3
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> ( ( S x. U ) - ( T x. ( sqrt ` V ) ) ) e. RR )
11 simp3l
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> W e. RR )
12 simp3r
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> W =/= 0 )
13 10 11 12 redivcld
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> ( ( ( S x. U ) - ( T x. ( sqrt ` V ) ) ) / W ) e. RR )