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