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

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