Metamath Proof Explorer


Theorem sqrt0

Description: The square root of zero is 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 sqeq0 ( 𝑥 ∈ ℂ → ( ( 𝑥 ↑ 2 ) = 0 ↔ 𝑥 = 0 ) )
6 5 biimpa ( ( 𝑥 ∈ ℂ ∧ ( 𝑥 ↑ 2 ) = 0 ) → 𝑥 = 0 )
7 6 3ad2antr1 ( ( 𝑥 ∈ ℂ ∧ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) → 𝑥 = 0 )
8 7 ex ( 𝑥 ∈ ℂ → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) → 𝑥 = 0 ) )
9 sq0i ( 𝑥 = 0 → ( 𝑥 ↑ 2 ) = 0 )
10 0le0 0 ≤ 0
11 fveq2 ( 𝑥 = 0 → ( ℜ ‘ 𝑥 ) = ( ℜ ‘ 0 ) )
12 re0 ( ℜ ‘ 0 ) = 0
13 11 12 eqtrdi ( 𝑥 = 0 → ( ℜ ‘ 𝑥 ) = 0 )
14 10 13 breqtrrid ( 𝑥 = 0 → 0 ≤ ( ℜ ‘ 𝑥 ) )
15 0re 0 ∈ ℝ
16 eleq1 ( 𝑥 = 0 → ( 𝑥 ∈ ℝ ↔ 0 ∈ ℝ ) )
17 15 16 mpbiri ( 𝑥 = 0 → 𝑥 ∈ ℝ )
18 rennim ( 𝑥 ∈ ℝ → ( i · 𝑥 ) ∉ ℝ+ )
19 17 18 syl ( 𝑥 = 0 → ( i · 𝑥 ) ∉ ℝ+ )
20 9 14 19 3jca ( 𝑥 = 0 → ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) )
21 8 20 impbid1 ( 𝑥 ∈ ℂ → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ 𝑥 = 0 ) )
22 21 adantl ( ( 0 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ↔ 𝑥 = 0 ) )
23 4 22 riota5 ( 0 ∈ ℂ → ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 0 )
24 1 23 ax-mp ( 𝑥 ∈ ℂ ( ( 𝑥 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝑥 ) ∧ ( i · 𝑥 ) ∉ ℝ+ ) ) = 0
25 3 24 eqtri ( √ ‘ 0 ) = 0