Theorem sqrtthlem

Description: Lemma for sqrtth . (Contributed by Mario Carneiro, 10-Jul-2013)

	Ref	Expression
Assertion	sqrtthlem	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) )

Proof

Step	Hyp	Ref	Expression
1		sqrtval	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
2	1	eqcomd	⊢ ( 𝐴 ∈ ℂ → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( √ ‘ 𝐴 ) )
3		sqrtcl	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) ∈ ℂ )
4		sqreu	⊢ ( 𝐴 ∈ ℂ → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
5		oveq1	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( 𝑥 ↑ 2 ) = ( ( √ ‘ 𝐴 ) ↑ 2 ) )
6	5	eqeq1d	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) )
7		fveq2	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ ( √ ‘ 𝐴 ) ) )
8	7	breq2d	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ) )
9		oveq2	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( i · 𝑥 ) = ( i · ( √ ‘ 𝐴 ) ) )
10		neleq1	⊢ ( ( i · 𝑥 ) = ( i · ( √ ‘ 𝐴 ) ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) )
11	9 10	syl	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) )
12	6 8 11	3anbi123d	⊢ ( 𝑥 = ( √ ‘ 𝐴 ) → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) ) )
13	12	riota2	⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → ( ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( √ ‘ 𝐴 ) ) )
14	3 4 13	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) ↔ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = ( √ ‘ 𝐴 ) ) )
15	2 14	mpbird	⊢ ( 𝐴 ∈ ℂ → ( ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ ( √ ‘ 𝐴 ) ) ∧ ( i · ( √ ‘ 𝐴 ) ) ∉ ℝ+ ) )