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