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

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 ⊢ ( 𝜑 → 𝐴 = ( √ ‘ 𝐵 ) )