Metamath Proof Explorer


Theorem sqrt0

Description: Square root of zero. (Contributed by Mario Carneiro, 9-Jul-2013)

Ref Expression
Assertion sqrt0 ( √ ‘ 0 ) = 0

Proof

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