This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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