Metamath Proof Explorer


Theorem eqsqrt2d

Description: A deduction for showing that a number equals the square root of another. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Hypotheses eqsqrtd.1 ( 𝜑𝐴 ∈ ℂ )
eqsqrtd.2 ( 𝜑𝐵 ∈ ℂ )
eqsqrtd.3 ( 𝜑 → ( 𝐴 ↑ 2 ) = 𝐵 )
eqsqrt2d.4 ( 𝜑 → 0 < ( ℜ ‘ 𝐴 ) )
Assertion eqsqrt2d ( 𝜑𝐴 = ( √ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqsqrtd.1 ( 𝜑𝐴 ∈ ℂ )
2 eqsqrtd.2 ( 𝜑𝐵 ∈ ℂ )
3 eqsqrtd.3 ( 𝜑 → ( 𝐴 ↑ 2 ) = 𝐵 )
4 eqsqrt2d.4 ( 𝜑 → 0 < ( ℜ ‘ 𝐴 ) )
5 0re 0 ∈ ℝ
6 1 recld ( 𝜑 → ( ℜ ‘ 𝐴 ) ∈ ℝ )
7 ltle ( ( 0 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 0 < ( ℜ ‘ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) )
8 5 6 7 sylancr ( 𝜑 → ( 0 < ( ℜ ‘ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) )
9 4 8 mpd ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐴 ) )
10 reim ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
11 1 10 syl ( 𝜑 → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
12 4 gt0ne0d ( 𝜑 → ( ℜ ‘ 𝐴 ) ≠ 0 )
13 11 12 eqnetrrd ( 𝜑 → ( ℑ ‘ ( i · 𝐴 ) ) ≠ 0 )
14 rpre ( ( i · 𝐴 ) ∈ ℝ+ → ( i · 𝐴 ) ∈ ℝ )
15 14 reim0d ( ( i · 𝐴 ) ∈ ℝ+ → ( ℑ ‘ ( i · 𝐴 ) ) = 0 )
16 15 necon3ai ( ( ℑ ‘ ( i · 𝐴 ) ) ≠ 0 → ¬ ( i · 𝐴 ) ∈ ℝ+ )
17 13 16 syl ( 𝜑 → ¬ ( i · 𝐴 ) ∈ ℝ+ )
18 1 2 3 9 17 eqsqrtd ( 𝜑𝐴 = ( √ ‘ 𝐵 ) )