Metamath Proof Explorer

Theorem resqrtthlem

Description: Lemma for resqrtth . (Contributed by Mario Carneiro, 9-Jul-2013)

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

Proof

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