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 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 remulcl 
 |-  ( ( S e. RR /\ U e. RR ) -> ( S x. U ) e. RR )
2 1 3adant2 
 |-  ( ( S e. RR /\ T e. RR /\ U e. RR ) -> ( S x. U ) e. RR )
3 2 adantr 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( S x. U ) e. RR )
4 simpl2 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> T e. RR )
5 resqrtcl 
 |-  ( ( V e. RR /\ 0 <_ V ) -> ( sqrt ` V ) e. RR )
6 5 adantl 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( sqrt ` V ) e. RR )
7 4 6 remulcld 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( T x. ( sqrt ` V ) ) e. RR )
8 3 7 readdcld 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) ) -> ( ( S x. U ) + ( T x. ( sqrt ` V ) ) ) e. RR )
9 8 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 )
10 simp3l 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> W e. RR )
11 simp3r 
 |-  ( ( ( S e. RR /\ T e. RR /\ U e. RR ) /\ ( V e. RR /\ 0 <_ V ) /\ ( W e. RR /\ W =/= 0 ) ) -> W =/= 0 )
12 9 10 11 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 )