Metamath Proof Explorer


Theorem sqr0lem

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

Ref Expression
Assertion sqr0lem ( ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) ↔ 𝐴 = 0 )

Proof

Step Hyp Ref Expression
1 sqeq0 ( 𝐴 ∈ ℂ → ( ( 𝐴 ↑ 2 ) = 0 ↔ 𝐴 = 0 ) )
2 1 biimpa ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 ↑ 2 ) = 0 ) → 𝐴 = 0 )
3 2 3ad2antr1 ( ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) → 𝐴 = 0 )
4 0re 0 ∈ ℝ
5 eleq1 ( 𝐴 = 0 → ( 𝐴 ∈ ℝ ↔ 0 ∈ ℝ ) )
6 4 5 mpbiri ( 𝐴 = 0 → 𝐴 ∈ ℝ )
7 6 recnd ( 𝐴 = 0 → 𝐴 ∈ ℂ )
8 sq0i ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )
9 0le0 0 ≤ 0
10 fveq2 ( 𝐴 = 0 → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ 0 ) )
11 re0 ( ℜ ‘ 0 ) = 0
12 10 11 eqtrdi ( 𝐴 = 0 → ( ℜ ‘ 𝐴 ) = 0 )
13 9 12 breqtrrid ( 𝐴 = 0 → 0 ≤ ( ℜ ‘ 𝐴 ) )
14 rennim ( 𝐴 ∈ ℝ → ( i · 𝐴 ) ∉ ℝ+ )
15 6 14 syl ( 𝐴 = 0 → ( i · 𝐴 ) ∉ ℝ+ )
16 8 13 15 3jca ( 𝐴 = 0 → ( ( 𝐴 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) )
17 7 16 jca ( 𝐴 = 0 → ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) )
18 3 17 impbii ( ( 𝐴 ∈ ℂ ∧ ( ( 𝐴 ↑ 2 ) = 0 ∧ 0 ≤ ( ℜ ‘ 𝐴 ) ∧ ( i · 𝐴 ) ∉ ℝ+ ) ) ↔ 𝐴 = 0 )