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 ) |