sqrtneg

Description: The square root of a negative number. (Contributed by Mario Carneiro, 9-Jul-2013)

		Ref	Expression
	Assertion	sqrtneg	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{- A} = i \sqrt{A}$

Proof

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2	1	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℂ$
3	2	negcld	$⊢ (A \in ℝ \land 0 \leq A) \to - A \in ℂ$
4		sqrtval	$⊢ - A \in ℂ \to \sqrt{- A} = (ι x \in ℂ \| (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
5	3 4	syl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{- A} = (ι x \in ℂ \| (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
6		sqrtneglem	$⊢ (A \in ℝ \land 0 \leq A) \to ({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+})$
7		ax-icn	$⊢ i \in ℂ$
8		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
9	8	recnd	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℂ$
10		mulcl	$⊢ (i \in ℂ \land \sqrt{A} \in ℂ) \to i \sqrt{A} \in ℂ$
11	7 9 10	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to i \sqrt{A} \in ℂ$
12		oveq1	$⊢ x = i \sqrt{A} \to x^{2} = {i \sqrt{A}}^{2}$
13	12	eqeq1d	$⊢ x = i \sqrt{A} \to (x^{2} = - A \leftrightarrow {i \sqrt{A}}^{2} = - A)$
14		fveq2	$⊢ x = i \sqrt{A} \to ℜ (x) = ℜ (i \sqrt{A})$
15	14	breq2d	$⊢ x = i \sqrt{A} \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (i \sqrt{A}))$
16		oveq2	$⊢ x = i \sqrt{A} \to i x = i i \sqrt{A}$
17		neleq1	$⊢ i x = i i \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i i \sqrt{A} \notin ℝ^{+})$
18	16 17	syl	$⊢ x = i \sqrt{A} \to (i x \notin ℝ^{+} \leftrightarrow i i \sqrt{A} \notin ℝ^{+})$
19	13 15 18	3anbi123d	$⊢ x = i \sqrt{A} \to ((x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow ({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+}))$
20	19	rspcev	$⊢ (i \sqrt{A} \in ℂ \land ({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+})) \to \exists x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
21	11 6 20	syl2anc	$⊢ (A \in ℝ \land 0 \leq A) \to \exists x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
22		sqrmo	$⊢ - A \in ℂ \to \exists^{*} x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
23	3 22	syl	$⊢ (A \in ℝ \land 0 \leq A) \to \exists^{*} x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
24		reu5	$⊢ \exists! x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow (\exists x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \land \exists^{*} x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
25	21 23 24	sylanbrc	$⊢ (A \in ℝ \land 0 \leq A) \to \exists! x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
26	19	riota2	$⊢ (i \sqrt{A} \in ℂ \land \exists! x \in ℂ (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) \to (({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = i \sqrt{A})$
27	11 25 26	syl2anc	$⊢ (A \in ℝ \land 0 \leq A) \to (({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+}) \leftrightarrow (ι x \in ℂ \| (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = i \sqrt{A})$
28	6 27	mpbid	$⊢ (A \in ℝ \land 0 \leq A) \to (ι x \in ℂ \| (x^{2} = - A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})) = i \sqrt{A}$
29	5 28	eqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{- A} = i \sqrt{A}$

Metamath Proof Explorer

Theorem sqrtneg

Proof