Metamath Proof Explorer

Theorem sqrtdiv

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

Ref Expression
Assertion sqrtdiv ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 rerpdivcl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2 1 adantlr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
3 elrp ⊢ ( 𝐵 ∈ ℝ+ ↔ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) )
4 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 / 𝐵 ) )
5 3 4 sylan2b ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 0 ≤ ( 𝐴 / 𝐵 ) )
6 resqrtcl ⊢ ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
7 2 5 6 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℝ )
8 7 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) ∈ ℂ )
9 rpsqrtcl ⊢ ( 𝐵 ∈ ℝ+ → ( √ ‘ 𝐵 ) ∈ ℝ+ )
10 9 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ 𝐵 ) ∈ ℝ+ )
11 10 rpcnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ 𝐵 ) ∈ ℂ )
12 10 rpne0d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ 𝐵 ) ≠ 0 )
13 8 11 12 divcan4d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( ( ( √ ‘ ( 𝐴 / 𝐵 ) ) · ( √ ‘ 𝐵 ) ) / ( √ ‘ 𝐵 ) ) = ( √ ‘ ( 𝐴 / 𝐵 ) ) )
14 rprege0 ⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
16 sqrtmul ⊢ ( ( ( ( 𝐴 / 𝐵 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝐵 ) ) ∧ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( √ ‘ ( 𝐴 / 𝐵 ) ) · ( √ ‘ 𝐵 ) ) )
17 2 5 15 16 syl21anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( ( √ ‘ ( 𝐴 / 𝐵 ) ) · ( √ ‘ 𝐵 ) ) )
18 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
19 18 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
20 rpcn ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
21 20 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
22 rpne0 ⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
23 22 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
24 19 21 23 divcan1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) · 𝐵 ) = 𝐴 )
25 24 fveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( ( 𝐴 / 𝐵 ) · 𝐵 ) ) = ( √ ‘ 𝐴 ) )
26 17 25 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( ( √ ‘ ( 𝐴 / 𝐵 ) ) · ( √ ‘ 𝐵 ) ) = ( √ ‘ 𝐴 ) )
27 26 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( ( ( √ ‘ ( 𝐴 / 𝐵 ) ) · ( √ ‘ 𝐵 ) ) / ( √ ‘ 𝐵 ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ 𝐵 ) ) )
28 13 27 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ 𝐵 ) ) )