Step |
Hyp |
Ref |
Expression |
1 |
|
0cn |
⊢ 0 ∈ ℂ |
2 |
|
sqrtval |
⊢ ( 0 ∈ ℂ → ( √ ‘ 0 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( √ ‘ 0 ) = ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) |
4 |
|
id |
⊢ ( 0 ∈ ℂ → 0 ∈ ℂ ) |
5 |
|
sqr0lem |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) ↔ 𝑥 = 0 ) |
6 |
5
|
biimpi |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → 𝑥 = 0 ) |
7 |
6
|
ex |
⊢ ( 𝑥 ∈ ℂ → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → 𝑥 = 0 ) ) |
8 |
|
simpr |
⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) |
9 |
5 8
|
sylbir |
⊢ ( 𝑥 = 0 → ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) |
10 |
7 9
|
impbid1 |
⊢ ( 𝑥 ∈ ℂ → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ 𝑥 = 0 ) ) |
11 |
10
|
adantl |
⊢ ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ 𝑥 = 0 ) ) |
12 |
4 11
|
riota5 |
⊢ ( 0 ∈ ℂ → ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 0 ) |
13 |
1 12
|
ax-mp |
⊢ ( ℩ 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 0 |
14 |
3 13
|
eqtri |
⊢ ( √ ‘ 0 ) = 0 |