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

Metamath Proof Explorer

Theorem sqrtmulii

Description: Square root distributes over multiplication. (Contributed by NM, 30-Jul-1999)

Ref Expression
Hypotheses sqrtthi.1 ⊢ 𝐴 ∈ ℝ
sqr11.1 ⊢ 𝐵 ∈ ℝ
sqrmuli.1 ⊢ 0 ≤ 𝐴
sqrmuli.2 ⊢ 0 ≤ 𝐵
Assertion sqrtmulii ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1 ⊢ 𝐴 ∈ ℝ
2 sqr11.1 ⊢ 𝐵 ∈ ℝ
3 sqrmuli.1 ⊢ 0 ≤ 𝐴
4 sqrmuli.2 ⊢ 0 ≤ 𝐵
5 1 2 sqrtmuli ⊢ ( ( 0 ≤ 𝐴 ∧ 0 ≤ 𝐵 ) → ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) ) )
6 3 4 5 mp2an ⊢ ( √ ‘ ( 𝐴 · 𝐵 ) ) = ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐵 ) )