Step | Hyp | Ref
| Expression |
1 | | resqrex 13839 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ∃𝑦 ∈ ℝ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) |
2 | | simp1l 1078 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → 𝐴 ∈ ℝ) |
3 | | recn 9905 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
4 | | sqrtval 13825 |
. . . . . 6
⊢ (𝐴 ∈ ℂ →
(√‘𝐴) =
(℩𝑥 ∈
ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+))) |
5 | 2, 3, 4 | 3syl 18 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (√‘𝐴) = (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉
ℝ+))) |
6 | | simp3r 1083 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (𝑦↑2) = 𝐴) |
7 | | simp3l 1082 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → 0 ≤ 𝑦) |
8 | | rere 13710 |
. . . . . . . . 9
⊢ (𝑦 ∈ ℝ →
(ℜ‘𝑦) = 𝑦) |
9 | 8 | 3ad2ant2 1076 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (ℜ‘𝑦) = 𝑦) |
10 | 7, 9 | breqtrrd 4611 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → 0 ≤ (ℜ‘𝑦)) |
11 | | rennim 13827 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → (i
· 𝑦) ∉
ℝ+) |
12 | 11 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (i · 𝑦) ∉
ℝ+) |
13 | 6, 10, 12 | 3jca 1235 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → ((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉
ℝ+)) |
14 | | recn 9905 |
. . . . . . . 8
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℂ) |
15 | 14 | 3ad2ant2 1076 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → 𝑦 ∈ ℂ) |
16 | | resqreu 13841 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉
ℝ+)) |
17 | 16 | 3ad2ant1 1075 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → ∃!𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉
ℝ+)) |
18 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥↑2) = (𝑦↑2)) |
19 | 18 | eqeq1d 2612 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑥↑2) = 𝐴 ↔ (𝑦↑2) = 𝐴)) |
20 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (ℜ‘𝑥) = (ℜ‘𝑦)) |
21 | 20 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (0 ≤ (ℜ‘𝑥) ↔ 0 ≤
(ℜ‘𝑦))) |
22 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (i · 𝑥) = (i · 𝑦)) |
23 | | neleq1 2888 |
. . . . . . . . . 10
⊢ ((i
· 𝑥) = (i ·
𝑦) → ((i ·
𝑥) ∉
ℝ+ ↔ (i · 𝑦) ∉
ℝ+)) |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((i · 𝑥) ∉ ℝ+ ↔ (i
· 𝑦) ∉
ℝ+)) |
25 | 19, 21, 24 | 3anbi123d 1391 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+)
↔ ((𝑦↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑦) ∧ (i
· 𝑦) ∉
ℝ+))) |
26 | 25 | riota2 6533 |
. . . . . . 7
⊢ ((𝑦 ∈ ℂ ∧
∃!𝑥 ∈ ℂ
((𝑥↑2) = 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+)) → (((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
↔ (℩𝑥
∈ ℂ ((𝑥↑2)
= 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+)) = 𝑦)) |
27 | 15, 17, 26 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (((𝑦↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
↔ (℩𝑥
∈ ℂ ((𝑥↑2)
= 𝐴 ∧ 0 ≤
(ℜ‘𝑥) ∧ (i
· 𝑥) ∉
ℝ+)) = 𝑦)) |
28 | 13, 27 | mpbid 221 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (℩𝑥 ∈ ℂ ((𝑥↑2) = 𝐴 ∧ 0 ≤ (ℜ‘𝑥) ∧ (i · 𝑥) ∉ ℝ+))
= 𝑦) |
29 | 5, 28 | eqtrd 2644 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (√‘𝐴) = 𝑦) |
30 | | simp2 1055 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → 𝑦 ∈ ℝ) |
31 | 29, 30 | eqeltrd 2688 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ 𝑦 ∈ ℝ ∧ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴)) → (√‘𝐴) ∈ ℝ) |
32 | 31 | rexlimdv3a 3015 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) → (∃𝑦 ∈ ℝ (0 ≤ 𝑦 ∧ (𝑦↑2) = 𝐴) → (√‘𝐴) ∈ ℝ)) |
33 | 1, 32 | mpd 15 |
1
⊢ ((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) |