Metamath Proof Explorer

Theorem resqrtthlem

Description: Lemma for resqrtth . (Contributed by Mario Carneiro, 9-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		sqrtval	$⊢ A \in ℂ \to \sqrt{A} = (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
3	2	eqcomd	$⊢ A \in ℂ \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A}$
4	1 3	syl	$⊢ A \in ℝ \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A}$
5	4	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to (ι x \in ℂ \| (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = \sqrt{A}$
6		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
7	6	recnd	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℂ$
8		resqreu	$⊢ (A \in ℝ \land 0 \leq A) \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
9		oveq1	$⊢ x = \sqrt{A} \to x^{2} = {\sqrt{A}}^{2}$
10	9	eqeq1d	$⊢ x = \sqrt{A} \to (x^{2} = A \leftrightarrow {\sqrt{A}}^{2} = A)$
11		fveq2	$⊢ x = \sqrt{A} \to ℜ (x) = ℜ (\sqrt{A})$
12	11	breq2d	$⊢ x = \sqrt{A} \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (\sqrt{A}))$
13		oveq2	$⊢ x = \sqrt{A} \to i x = i \sqrt{A}$
14		neleq1	$⊢ i x = i \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{A} \notin ℝ^{+})$
15	13 14	syl	$⊢ x = \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{A} \notin ℝ^{+})$
16	10 12 15	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 ℝ^{+}))$
17	16	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})$
18	7 8 17	syl2anc	$⊢ (A \in ℝ \land 0 \leq A) \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})$
19	5 18	mpbird	$⊢ (A \in ℝ \land 0 \leq A) \to ({\sqrt{A}}^{2} = A \land 0 \leq ℜ (\sqrt{A}) \land i \sqrt{A} \notin ℝ^{+})$