Metamath Proof Explorer

Theorem sqrtthlem

Description: Lemma for sqrtth . (Contributed by Mario Carneiro, 10-Jul-2013)

		Ref	Expression
	Assertion	sqrtthlem	$⊢ A \in ℂ \to ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+})$

Proof

Step	Hyp	Ref	Expression
1		sqrtval	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
2	1	eqcomd	$⊢ A \in ℂ \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A}$
3		sqrtcl	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$
4		sqreu	$⊢ A \in ℂ \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
5		oveq1	$⊢ x = \sqrt{A} \to x^{2} = {\sqrt{A}}^{2}$
6	5	eqeq1d	$⊢ x = \sqrt{A} \to (x^{2} = A \leftrightarrow {\sqrt{A}}^{2} = A)$
7		fveq2	$⊢ x = \sqrt{A} \to ℜ (x) = ℜ (\sqrt{A})$
8	7	breq2d	$⊢ x = \sqrt{A} \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (\sqrt{A}))$
9		oveq2	$⊢ x = \sqrt{A} \to i x = i \sqrt{A}$
10		neleq1	$⊢ i x = i \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{A} \notin ℝ^{+})$
11	9 10	syl	$⊢ x = \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{A} \notin ℝ^{+})$
12	6 8 11	3anbi123d	$⊢ x = \sqrt{A} \to ((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+}))$
13	12	riota2	$⊢ (\sqrt{A} \in ℂ \land \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to (({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A})$
14	3 4 13	syl2anc	$⊢ A \in ℂ \to (({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A})$
15	2 14	mpbird	$⊢ A \in ℂ \to ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+})$