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