sqrtneglem

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

		Ref	Expression
	Assertion	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 ℝ^{+})$

Proof

Step	Hyp	Ref	Expression
1		ax-icn	$⊢ i \in ℂ$
2		resqrtcl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℝ$
3		recn	$⊢ \sqrt{A} \in ℝ \to \sqrt{A} \in ℂ$
4	2 3	syl	$⊢ (A \in ℝ \land 0 \leq A) \to \sqrt{A} \in ℂ$
5		sqmul	$⊢ (i \in ℂ \land \sqrt{A} \in ℂ) \to {i \sqrt{A}}^{2} = i^{2} {\sqrt{A}}^{2}$
6	1 4 5	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to {i \sqrt{A}}^{2} = i^{2} {\sqrt{A}}^{2}$
7		i2	$⊢ i^{2} = - 1$
8	7	a1i	$⊢ (A \in ℝ \land 0 \leq A) \to i^{2} = - 1$
9		resqrtth	$⊢ (A \in ℝ \land 0 \leq A) \to {\sqrt{A}}^{2} = A$
10	8 9	oveq12d	$⊢ (A \in ℝ \land 0 \leq A) \to i^{2} {\sqrt{A}}^{2} = -1 A$
11		recn	$⊢ A \in ℝ \to A \in ℂ$
12	11	adantr	$⊢ (A \in ℝ \land 0 \leq A) \to A \in ℂ$
13	12	mulm1d	$⊢ (A \in ℝ \land 0 \leq A) \to -1 A = - A$
14	6 10 13	3eqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to {i \sqrt{A}}^{2} = - A$
15		renegcl	$⊢ \sqrt{A} \in ℝ \to - \sqrt{A} \in ℝ$
16		0re	$⊢ 0 \in ℝ$
17		reim0	$⊢ - \sqrt{A} \in ℝ \to ℑ (- \sqrt{A}) = 0$
18		recn	$⊢ - \sqrt{A} \in ℝ \to - \sqrt{A} \in ℂ$
19		imre	$⊢ - \sqrt{A} \in ℂ \to ℑ (- \sqrt{A}) = ℜ ((- i) (- \sqrt{A}))$
20	18 19	syl	$⊢ - \sqrt{A} \in ℝ \to ℑ (- \sqrt{A}) = ℜ ((- i) (- \sqrt{A}))$
21	17 20	eqtr3d	$⊢ - \sqrt{A} \in ℝ \to 0 = ℜ ((- i) (- \sqrt{A}))$
22		eqle	$⊢ (0 \in ℝ \land 0 = ℜ ((- i) (- \sqrt{A}))) \to 0 \leq ℜ ((- i) (- \sqrt{A}))$
23	16 21 22	sylancr	$⊢ - \sqrt{A} \in ℝ \to 0 \leq ℜ ((- i) (- \sqrt{A}))$
24	2 15 23	3syl	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq ℜ ((- i) (- \sqrt{A}))$
25		mul2neg	$⊢ (i \in ℂ \land \sqrt{A} \in ℂ) \to (- i) (- \sqrt{A}) = i \sqrt{A}$
26	1 4 25	sylancr	$⊢ (A \in ℝ \land 0 \leq A) \to (- i) (- \sqrt{A}) = i \sqrt{A}$
27	26	fveq2d	$⊢ (A \in ℝ \land 0 \leq A) \to ℜ ((- i) (- \sqrt{A})) = ℜ (i \sqrt{A})$
28	24 27	breqtrd	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq ℜ (i \sqrt{A})$
29		ixi	$⊢ i i = - 1$
30	29	oveq1i	$⊢ i i \sqrt{A} = -1 \sqrt{A}$
31		mulass	$⊢ (i \in ℂ \land i \in ℂ \land \sqrt{A} \in ℂ) \to i i \sqrt{A} = i i \sqrt{A}$
32	1 1 31	mp3an12	$⊢ \sqrt{A} \in ℂ \to i i \sqrt{A} = i i \sqrt{A}$
33		mulm1	$⊢ \sqrt{A} \in ℂ \to -1 \sqrt{A} = - \sqrt{A}$
34	30 32 33	3eqtr3a	$⊢ \sqrt{A} \in ℂ \to i i \sqrt{A} = - \sqrt{A}$
35	4 34	syl	$⊢ (A \in ℝ \land 0 \leq A) \to i i \sqrt{A} = - \sqrt{A}$
36		sqrtge0	$⊢ (A \in ℝ \land 0 \leq A) \to 0 \leq \sqrt{A}$
37		le0neg2	$⊢ \sqrt{A} \in ℝ \to (0 \leq \sqrt{A} \leftrightarrow - \sqrt{A} \leq 0)$
38		lenlt	$⊢ (- \sqrt{A} \in ℝ \land 0 \in ℝ) \to (- \sqrt{A} \leq 0 \leftrightarrow \neg 0 < - \sqrt{A})$
39	15 16 38	sylancl	$⊢ \sqrt{A} \in ℝ \to (- \sqrt{A} \leq 0 \leftrightarrow \neg 0 < - \sqrt{A})$
40	37 39	bitrd	$⊢ \sqrt{A} \in ℝ \to (0 \leq \sqrt{A} \leftrightarrow \neg 0 < - \sqrt{A})$
41	2 40	syl	$⊢ (A \in ℝ \land 0 \leq A) \to (0 \leq \sqrt{A} \leftrightarrow \neg 0 < - \sqrt{A})$
42	36 41	mpbid	$⊢ (A \in ℝ \land 0 \leq A) \to \neg 0 < - \sqrt{A}$
43		elrp	$⊢ - \sqrt{A} \in ℝ^{+} \leftrightarrow (- \sqrt{A} \in ℝ \land 0 < - \sqrt{A})$
44	2 15	syl	$⊢ (A \in ℝ \land 0 \leq A) \to - \sqrt{A} \in ℝ$
45	44	biantrurd	$⊢ (A \in ℝ \land 0 \leq A) \to (0 < - \sqrt{A} \leftrightarrow (- \sqrt{A} \in ℝ \land 0 < - \sqrt{A}))$
46	43 45	bitr4id	$⊢ (A \in ℝ \land 0 \leq A) \to (- \sqrt{A} \in ℝ^{+} \leftrightarrow 0 < - \sqrt{A})$
47	42 46	mtbird	$⊢ (A \in ℝ \land 0 \leq A) \to \neg - \sqrt{A} \in ℝ^{+}$
48	35 47	eqneltrd	$⊢ (A \in ℝ \land 0 \leq A) \to \neg i i \sqrt{A} \in ℝ^{+}$
49		df-nel	$⊢ i i \sqrt{A} \notin ℝ^{+} \leftrightarrow \neg i i \sqrt{A} \in ℝ^{+}$
50	48 49	sylibr	$⊢ (A \in ℝ \land 0 \leq A) \to i i \sqrt{A} \notin ℝ^{+}$
51	14 28 50	3jca	$⊢ (A \in ℝ \land 0 \leq A) \to ({i \sqrt{A}}^{2} = - A \land 0 \leq ℜ (i \sqrt{A}) \land i i \sqrt{A} \notin ℝ^{+})$

Metamath Proof Explorer

Theorem sqrtneglem

Proof