Metamath Proof Explorer

Theorem sqrtdiv

Description: Square root distributes over division. (Contributed by Mario Carneiro, 5-May-2016)

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

Proof

Step Hyp Ref Expression
1 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
2 1 adantlr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( A / B ) e. RR )
3 elrp 
 |-  ( B e. RR+ <-> ( B e. RR /\ 0 < B ) )
4 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
5 3 4 sylan2b 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> 0 <_ ( A / B ) )
6 resqrtcl 
 |-  ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) -> ( sqrt ` ( A / B ) ) e. RR )
7 2 5 6 syl2anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` ( A / B ) ) e. RR )
8 7 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` ( A / B ) ) e. CC )
9 rpsqrtcl 
 |-  ( B e. RR+ -> ( sqrt ` B ) e. RR+ )
10 9 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` B ) e. RR+ )
11 10 rpcnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` B ) e. CC )
12 10 rpne0d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` B ) =/= 0 )
13 8 11 12 divcan4d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( ( ( sqrt ` ( A / B ) ) x. ( sqrt ` B ) ) / ( sqrt ` B ) ) = ( sqrt ` ( A / B ) ) )
14 rprege0 
 |-  ( B e. RR+ -> ( B e. RR /\ 0 <_ B ) )
15 14 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( B e. RR /\ 0 <_ B ) )
16 sqrtmul 
 |-  ( ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) /\ ( B e. RR /\ 0 <_ B ) ) -> ( sqrt ` ( ( A / B ) x. B ) ) = ( ( sqrt ` ( A / B ) ) x. ( sqrt ` B ) ) )
17 2 5 15 16 syl21anc 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` ( ( A / B ) x. B ) ) = ( ( sqrt ` ( A / B ) ) x. ( sqrt ` B ) ) )
18 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> A e. RR )
19 18 recnd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> A e. CC )
20 rpcn 
 |-  ( B e. RR+ -> B e. CC )
21 20 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> B e. CC )
22 rpne0 
 |-  ( B e. RR+ -> B =/= 0 )
23 22 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> B =/= 0 )
24 19 21 23 divcan1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( ( A / B ) x. B ) = A )
25 24 fveq2d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` ( ( A / B ) x. B ) ) = ( sqrt ` A ) )
26 17 25 eqtr3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( ( sqrt ` ( A / B ) ) x. ( sqrt ` B ) ) = ( sqrt ` A ) )
27 26 oveq1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( ( ( sqrt ` ( A / B ) ) x. ( sqrt ` B ) ) / ( sqrt ` B ) ) = ( ( sqrt ` A ) / ( sqrt ` B ) ) )
28 13 27 eqtr3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ B e. RR+ ) -> ( sqrt ` ( A / B ) ) = ( ( sqrt ` A ) / ( sqrt ` B ) ) )