Metamath Proof Explorer


Theorem resqrtcl

Description: Closure of the square root function. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion resqrtcl ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 resqrex ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃ 𝑦 ∈ ℝ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) )
2 simp1l ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝐴 ∈ ℝ )
3 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
4 sqrtval ( 𝐴 ∈ ℂ → ( √ ‘ 𝐴 ) = ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
5 2 3 4 3syl ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) = ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) )
6 simp3r ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( 𝑦 ↑ 2 ) = 𝐴 )
7 simp3l ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 0 ≤ 𝑦 )
8 rere ( 𝑦 ∈ ℝ → ( ℜ ‘ 𝑦 ) = 𝑦 )
9 8 3ad2ant2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ℜ ‘ 𝑦 ) = 𝑦 )
10 7 9 breqtrrd ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝑦 ) )
11 rennim ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∉ ℝ+ )
12 11 3ad2ant2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( i · 𝑦 ) ∉ ℝ+ )
13 6 10 12 3jca ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) )
14 recn ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
15 14 3ad2ant2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝑦 ∈ ℂ )
16 resqreu ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
17 16 3ad2ant1 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
18 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 ↑ 2 ) = ( 𝑦 ↑ 2 ) )
19 18 eqeq1d ( 𝑥 = 𝑦 → ( ( 𝑥 ↑ 2 ) = 𝐴 ↔ ( 𝑦 ↑ 2 ) = 𝐴 ) )
20 fveq2 ( 𝑥 = 𝑦 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 𝑦 ) )
21 20 breq2d ( 𝑥 = 𝑦 → ( 0 ≤ ( ℜ ‘ 𝑥 ) ↔ 0 ≤ ( ℜ ‘ 𝑦 ) ) )
22 oveq2 ( 𝑥 = 𝑦 → ( i · 𝑥 ) = ( i · 𝑦 ) )
23 neleq1 ( ( i · 𝑥 ) = ( i · 𝑦 ) → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
24 22 23 syl ( 𝑥 = 𝑦 → ( ( i · 𝑥 ) ∉ ℝ+ ↔ ( i · 𝑦 ) ∉ ℝ+ ) )
25 19 21 24 3anbi123d ( 𝑥 = 𝑦 → ( ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )
26 25 riota2 ( ( 𝑦 ∈ ℂ ∧ ∃! 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ↔ ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 ) )
27 15 17 26 syl2anc ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( ( ( 𝑦 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ↔ ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 ) )
28 13 27 mpbid ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 𝑦 )
29 5 28 eqtrd ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) = 𝑦 )
30 simp2 ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → 𝑦 ∈ ℝ )
31 29 30 eqeltrd ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑦 ∈ ℝ ∧ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) ) → ( √ ‘ 𝐴 ) ∈ ℝ )
32 31 rexlimdv3a ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ ( 0 ≤ 𝑦 ∧ ( 𝑦 ↑ 2 ) = 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) )
33 1 32 mpd ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )