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)\leftrightarrow A=0$$

Proof

Step	Hyp	Ref	Expression
1		sqeq0	$$⊢A\in ℂ\to \left(A^2=0\leftrightarrow 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 ℝ\leftrightarrow 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	eqtrdi	$$⊢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)\leftrightarrow A=0$$