Metamath Proof Explorer


Theorem eqsqrtd

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 ) = 𝐵 )
eqsqrtd.4 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐴 ) )
eqsqrtd.5 ( 𝜑 → ¬ ( i · 𝐴 ) ∈ ℝ+ )
Assertion eqsqrtd ( 𝜑𝐴 = ( √ ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eqsqrtd.1 ( 𝜑𝐴 ∈ ℂ )
2 eqsqrtd.2 ( 𝜑𝐵 ∈ ℂ )
3 eqsqrtd.3 ( 𝜑 → ( 𝐴 ↑ 2 ) = 𝐵 )
4 eqsqrtd.4 ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐴 ) )
5 eqsqrtd.5 ( 𝜑 → ¬ ( i · 𝐴 ) ∈ ℝ+ )
6 sqreu ( 𝐵 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
7 reurmo ( ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
8 2 6 7 3syl ( 𝜑 → ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
9 df-nel ( ( i · 𝐴 ) ∉ ℝ+ ↔ ¬ ( i · 𝐴 ) ∈ ℝ+ )
10 5 9 sylibr ( 𝜑 → ( i · 𝐴 ) ∉ ℝ+ )
11 3 4 10 3jca ( 𝜑 → ( ( 𝐴 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) )
12 sqrtcl ( 𝐵 ∈ ℂ → ( √ ‘ 𝐵 ) ∈ ℂ )
13 2 12 syl ( 𝜑 → ( √ ‘ 𝐵 ) ∈ ℂ )
14 sqrtthlem ( 𝐵 ∈ ℂ → ( ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐵 ) ) ∧ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) )
15 2 14 syl ( 𝜑 → ( ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐵 ) ) ∧ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) )
16 oveq1 ( 𝑥 = 𝐴 → ( 𝑥 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
17 16 eqeq1d ( 𝑥 = 𝐴 → ( ( 𝑥 ↑ 2 ) = 𝐵 ↔ ( 𝐴 ↑ 2 ) = 𝐵 ) )
18 fveq2 ( 𝑥 = 𝐴 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝐴 ) )
19 18 breq2d ( 𝑥 = 𝐴 → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ 𝐴 ) ) )
20 oveq2 ( 𝑥 = 𝐴 → ( i · 𝑥 ) = ( i · 𝐴 ) )
21 neleq1 ( ( i · 𝑥 ) = ( i · 𝐴 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝐴 ) ∉ ℝ+ ) )
22 20 21 syl ( 𝑥 = 𝐴 → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝐴 ) ∉ ℝ+ ) )
23 17 19 22 3anbi123d ( 𝑥 = 𝐴 → ( ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( 𝐴 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) )
24 oveq1 ( 𝑥 = ( √ ‘ 𝐵 ) → ( 𝑥 ↑ 2 ) = ( ( √ ‘ 𝐵 ) ↑ 2 ) )
25 24 eqeq1d ( 𝑥 = ( √ ‘ 𝐵 ) → ( ( 𝑥 ↑ 2 ) = 𝐵 ↔ ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 ) )
26 fveq2 ( 𝑥 = ( √ ‘ 𝐵 ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( √ ‘ 𝐵 ) ) )
27 26 breq2d ( 𝑥 = ( √ ‘ 𝐵 ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐵 ) ) ) )
28 oveq2 ( 𝑥 = ( √ ‘ 𝐵 ) → ( i · 𝑥 ) = ( i · ( √ ‘ 𝐵 ) ) )
29 neleq1 ( ( i · 𝑥 ) = ( i · ( √ ‘ 𝐵 ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) )
30 28 29 syl ( 𝑥 = ( √ ‘ 𝐵 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) )
31 25 27 30 3anbi123d ( 𝑥 = ( √ ‘ 𝐵 ) → ( ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐵 ) ) ∧ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) ) )
32 23 31 rmoi ( ( ∃* 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ∧ ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) ∧ ( ( √ ‘ 𝐵 ) ∈ ℂ ∧ ( ( ( √ ‘ 𝐵 ) ↑ 2 ) = 𝐵 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐵 ) ) ∧ ( i · ( √ ‘ 𝐵 ) ) ∉ ℝ+ ) ) ) → 𝐴 = ( √ ‘ 𝐵 ) )
33 8 1 11 13 15 32 syl122anc ( 𝜑𝐴 = ( √ ‘ 𝐵 ) )