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 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ+ ) → ( √ ‘ ( 𝐴 / 𝐵 ) ) = ( ( √ ‘ 𝐴 ) / ( √ ‘ 𝐵 ) ) )