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 )