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 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ )