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 )