This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqrtmul

Description: Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion sqrtmul 
|- ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` ( A x. B ) ) = ( ( sqrt ` A ) x. ( sqrt ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> A e. RR )
2 simprl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> B e. RR )
3 1 2 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( A x. B ) e. RR )
4 mulge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( A x. B ) )
5 resqrtcl 
 |-  ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> ( sqrt ` ( A x. B ) ) e. RR )
6 3 4 5 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` ( A x. B ) ) e. RR )
7 resqrtcl 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( sqrt ` A ) e. RR )
8 7 adantr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` A ) e. RR )
9 resqrtcl 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( sqrt ` B ) e. RR )
10 9 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` B ) e. RR )
11 8 10 remulcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` A ) x. ( sqrt ` B ) ) e. RR )
12 sqrtge0 
 |-  ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> 0 <_ ( sqrt ` ( A x. B ) ) )
13 3 4 12 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( sqrt ` ( A x. B ) ) )
14 sqrtge0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> 0 <_ ( sqrt ` A ) )
15 14 adantr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( sqrt ` A ) )
16 sqrtge0 
 |-  ( ( B e. RR /\ 0 <_ B ) -> 0 <_ ( sqrt ` B ) )
17 16 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( sqrt ` B ) )
18 8 10 15 17 mulge0d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> 0 <_ ( ( sqrt ` A ) x. ( sqrt ` B ) ) )
19 resqrtth 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( ( sqrt ` A ) ^ 2 ) = A )
20 resqrtth 
 |-  ( ( B e. RR /\ 0 <_ B ) -> ( ( sqrt ` B ) ^ 2 ) = B )
21 19 20 oveqan12d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( sqrt ` A ) ^ 2 ) x. ( ( sqrt ` B ) ^ 2 ) ) = ( A x. B ) )
22 8 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` A ) e. CC )
23 10 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` B ) e. CC )
24 22 23 sqmuld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( ( sqrt ` A ) x. ( sqrt ` B ) ) ^ 2 ) = ( ( ( sqrt ` A ) ^ 2 ) x. ( ( sqrt ` B ) ^ 2 ) ) )
25 resqrtth 
 |-  ( ( ( A x. B ) e. RR /\ 0 <_ ( A x. B ) ) -> ( ( sqrt ` ( A x. B ) ) ^ 2 ) = ( A x. B ) )
26 3 4 25 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` ( A x. B ) ) ^ 2 ) = ( A x. B ) )
27 21 24 26 3eqtr4rd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( ( sqrt ` ( A x. B ) ) ^ 2 ) = ( ( ( sqrt ` A ) x. ( sqrt ` B ) ) ^ 2 ) )
28 6 11 13 18 27 sq11d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` ( A x. B ) ) = ( ( sqrt ` A ) x. ( sqrt ` B ) ) )