Metamath Proof Explorer

Theorem sqr0lem

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

Ref Expression
Assertion sqr0lem ${⊢}\left({A}\in ℂ\wedge \left({{A}}^{2}=0\wedge 0\le \Re \left({A}\right)\wedge \mathrm{i}{A}\notin {ℝ}^{+}\right)\right)↔{A}=0$

Proof

Step Hyp Ref Expression
1 sqeq0 ${⊢}{A}\in ℂ\to \left({{A}}^{2}=0↔{A}=0\right)$
2 1 biimpa ${⊢}\left({A}\in ℂ\wedge {{A}}^{2}=0\right)\to {A}=0$
3 2 3ad2antr1 ${⊢}\left({A}\in ℂ\wedge \left({{A}}^{2}=0\wedge 0\le \Re \left({A}\right)\wedge \mathrm{i}{A}\notin {ℝ}^{+}\right)\right)\to {A}=0$
4 0re ${⊢}0\in ℝ$
5 eleq1 ${⊢}{A}=0\to \left({A}\in ℝ↔0\in ℝ\right)$
6 4 5 mpbiri ${⊢}{A}=0\to {A}\in ℝ$
7 6 recnd ${⊢}{A}=0\to {A}\in ℂ$
8 sq0i ${⊢}{A}=0\to {{A}}^{2}=0$
9 0le0 ${⊢}0\le 0$
10 fveq2 ${⊢}{A}=0\to \Re \left({A}\right)=\Re \left(0\right)$
11 re0 ${⊢}\Re \left(0\right)=0$
12 10 11 syl6eq ${⊢}{A}=0\to \Re \left({A}\right)=0$
13 9 12 breqtrrid ${⊢}{A}=0\to 0\le \Re \left({A}\right)$
14 rennim ${⊢}{A}\in ℝ\to \mathrm{i}{A}\notin {ℝ}^{+}$
15 6 14 syl ${⊢}{A}=0\to \mathrm{i}{A}\notin {ℝ}^{+}$
16 8 13 15 3jca ${⊢}{A}=0\to \left({{A}}^{2}=0\wedge 0\le \Re \left({A}\right)\wedge \mathrm{i}{A}\notin {ℝ}^{+}\right)$
17 7 16 jca ${⊢}{A}=0\to \left({A}\in ℂ\wedge \left({{A}}^{2}=0\wedge 0\le \Re \left({A}\right)\wedge \mathrm{i}{A}\notin {ℝ}^{+}\right)\right)$
18 3 17 impbii ${⊢}\left({A}\in ℂ\wedge \left({{A}}^{2}=0\wedge 0\le \Re \left({A}\right)\wedge \mathrm{i}{A}\notin {ℝ}^{+}\right)\right)↔{A}=0$