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