Metamath Proof Explorer

Theorem divsqrtid

Description: A real number divided by its square root. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Assertion divsqrtid ( 𝐴 ∈ ℝ+ → ( 𝐴 / ( √ ‘ 𝐴 ) ) = ( √ ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpre ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
2 rpge0 ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ 𝐴 )
3 remsqsqrt ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐴 ) ) = 𝐴 )
4 1 2 3 syl2anc ⊢ ( 𝐴 ∈ ℝ+ → ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐴 ) ) = 𝐴 )
5 4 oveq1d ⊢ ( 𝐴 ∈ ℝ+ → ( ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐴 ) ) / ( √ ‘ 𝐴 ) ) = ( 𝐴 / ( √ ‘ 𝐴 ) ) )
6 1 recnd ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
7 6 sqrtcld ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ ℂ )
8 rpsqrtcl ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ∈ ℝ+ )
9 8 rpne0d ⊢ ( 𝐴 ∈ ℝ+ → ( √ ‘ 𝐴 ) ≠ 0 )
10 7 7 9 divcan4d ⊢ ( 𝐴 ∈ ℝ+ → ( ( ( √ ‘ 𝐴 ) · ( √ ‘ 𝐴 ) ) / ( √ ‘ 𝐴 ) ) = ( √ ‘ 𝐴 ) )
11 5 10 eqtr3d ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 / ( √ ‘ 𝐴 ) ) = ( √ ‘ 𝐴 ) )