sqreu

Description: Existence and uniqueness for the square root function in general. (Contributed by Mario Carneiro, 9-Jul-2013)

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

Proof

Step	Hyp	Ref	Expression
1		abscl	$⊢ A \in ℂ \to \|A\| \in ℝ$
2	1	recnd	$⊢ A \in ℂ \to \|A\| \in ℂ$
3		subneg	$⊢ (\|A\| \in ℂ \land A \in ℂ) \to \|A\| - (- A) = \|A\| + A$
4	2 3	mpancom	$⊢ A \in ℂ \to \|A\| - (- A) = \|A\| + A$
5	4	eqeq1d	$⊢ A \in ℂ \to (\|A\| - (- A) = 0 \leftrightarrow \|A\| + A = 0)$
6		negcl	$⊢ A \in ℂ \to - A \in ℂ$
7	2 6	subeq0ad	$⊢ A \in ℂ \to (\|A\| - (- A) = 0 \leftrightarrow \|A\| = - A)$
8	5 7	bitr3d	$⊢ A \in ℂ \to (\|A\| + A = 0 \leftrightarrow \|A\| = - A)$
9		ax-icn	$⊢ i \in ℂ$
10		absge0	$⊢ A \in ℂ \to 0 \leq \|A\|$
11	1 10	jca	$⊢ A \in ℂ \to (\|A\| \in ℝ \land 0 \leq \|A\|)$
12		eleq1	$⊢ \|A\| = - A \to (\|A\| \in ℝ \leftrightarrow - A \in ℝ)$
13		breq2	$⊢ \|A\| = - A \to (0 \leq \|A\| \leftrightarrow 0 \leq - A)$
14	12 13	anbi12d	$⊢ \|A\| = - A \to ((\|A\| \in ℝ \land 0 \leq \|A\|) \leftrightarrow (- A \in ℝ \land 0 \leq - A))$
15	11 14	syl5ib	$⊢ \|A\| = - A \to (A \in ℂ \to (- A \in ℝ \land 0 \leq - A))$
16	15	impcom	$⊢ (A \in ℂ \land \|A\| = - A) \to (- A \in ℝ \land 0 \leq - A)$
17		resqrtcl	$⊢ (- A \in ℝ \land 0 \leq - A) \to \sqrt{- A} \in ℝ$
18	16 17	syl	$⊢ (A \in ℂ \land \|A\| = - A) \to \sqrt{- A} \in ℝ$
19	18	recnd	$⊢ (A \in ℂ \land \|A\| = - A) \to \sqrt{- A} \in ℂ$
20		mulcl	$⊢ (i \in ℂ \land \sqrt{- A} \in ℂ) \to i \sqrt{- A} \in ℂ$
21	9 19 20	sylancr	$⊢ (A \in ℂ \land \|A\| = - A) \to i \sqrt{- A} \in ℂ$
22		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 ℝ^{+})$
23	16 22	syl	$⊢ (A \in ℂ \land \|A\| = - A) \to ({i \sqrt{- A}}^{2} = - (- A) \land 0 \leq ℜ (i \sqrt{- A}) \land i i \sqrt{- A} \notin ℝ^{+})$
24		negneg	$⊢ A \in ℂ \to - (- A) = A$
25	24	adantr	$⊢ (A \in ℂ \land \|A\| = - A) \to - (- A) = A$
26	25	eqeq2d	$⊢ (A \in ℂ \land \|A\| = - A) \to ({i \sqrt{- A}}^{2} = - (- A) \leftrightarrow {i \sqrt{- A}}^{2} = A)$
27	26	3anbi1d	$⊢ (A \in ℂ \land \|A\| = - A) \to (({i \sqrt{- A}}^{2} = - (- A) \land 0 \leq ℜ (i \sqrt{- A}) \land i i \sqrt{- A} \notin ℝ^{+}) \leftrightarrow ({i \sqrt{- A}}^{2} = A \land 0 \leq ℜ (i \sqrt{- A}) \land i i \sqrt{- A} \notin ℝ^{+}))$
28	23 27	mpbid	$⊢ (A \in ℂ \land \|A\| = - A) \to ({i \sqrt{- A}}^{2} = A \land 0 \leq ℜ (i \sqrt{- A}) \land i i \sqrt{- A} \notin ℝ^{+})$
29		oveq1	$⊢ x = i \sqrt{- A} \to x^{2} = {i \sqrt{- A}}^{2}$
30	29	eqeq1d	$⊢ x = i \sqrt{- A} \to (x^{2} = A \leftrightarrow {i \sqrt{- A}}^{2} = A)$
31		fveq2	$⊢ x = i \sqrt{- A} \to ℜ (x) = ℜ (i \sqrt{- A})$
32	31	breq2d	$⊢ x = i \sqrt{- A} \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (i \sqrt{- A}))$
33		oveq2	$⊢ x = i \sqrt{- A} \to i x = i i \sqrt{- A}$
34		neleq1	$⊢ i x = i i \sqrt{- A} \to (i x \notin ℝ^{+} \leftrightarrow i i \sqrt{- A} \notin ℝ^{+})$
35	33 34	syl	$⊢ x = i \sqrt{- A} \to (i x \notin ℝ^{+} \leftrightarrow i i \sqrt{- A} \notin ℝ^{+})$
36	30 32 35	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 ℝ^{+}))$
37	36	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 ℝ^{+})$
38	21 28 37	syl2anc	$⊢ (A \in ℂ \land \|A\| = - A) \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
39	38	ex	$⊢ A \in ℂ \to (\|A\| = - A \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
40	8 39	sylbid	$⊢ A \in ℂ \to (\|A\| + A = 0 \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
41		resqrtcl	$⊢ (\|A\| \in ℝ \land 0 \leq \|A\|) \to \sqrt{\|A\|} \in ℝ$
42	1 10 41	syl2anc	$⊢ A \in ℂ \to \sqrt{\|A\|} \in ℝ$
43	42	recnd	$⊢ A \in ℂ \to \sqrt{\|A\|} \in ℂ$
44	43	adantr	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \sqrt{\|A\|} \in ℂ$
45		addcl	$⊢ (\|A\| \in ℂ \land A \in ℂ) \to \|A\| + A \in ℂ$
46	2 45	mpancom	$⊢ A \in ℂ \to \|A\| + A \in ℂ$
47	46	adantr	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \|A\| + A \in ℂ$
48		abscl	$⊢ \|A\| + A \in ℂ \to \|\|A\| + A\| \in ℝ$
49	46 48	syl	$⊢ A \in ℂ \to \|\|A\| + A\| \in ℝ$
50	49	recnd	$⊢ A \in ℂ \to \|\|A\| + A\| \in ℂ$
51	50	adantr	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \|\|A\| + A\| \in ℂ$
52	46	abs00ad	$⊢ A \in ℂ \to (\|\|A\| + A\| = 0 \leftrightarrow \|A\| + A = 0)$
53	52	necon3bid	$⊢ A \in ℂ \to (\|\|A\| + A\| \neq 0 \leftrightarrow \|A\| + A \neq 0)$
54	53	biimpar	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \|\|A\| + A\| \neq 0$
55	47 51 54	divcld	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \frac{\|A\| + A}{\|\|A\| + A\|} \in ℂ$
56	44 55	mulcld	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in ℂ$
57		eqid	$⊢ \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})$
58	57	sqreulem	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to ({\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A \land 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})) \land i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})$
59		oveq1	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to x^{2} = {\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2}$
60	59	eqeq1d	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to (x^{2} = A \leftrightarrow {\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A)$
61		fveq2	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to ℜ (x) = ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}))$
62	61	breq2d	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to (0 \leq ℜ (x) \leftrightarrow 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})))$
63		oveq2	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to i x = i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})$
64		neleq1	$⊢ i x = i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})$
65	63 64	syl	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to (i x \notin ℝ^{+} \leftrightarrow i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})$
66	60 62 65	3anbi123d	$⊢ x = \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \to ((x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}) \leftrightarrow ({\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A \land 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})) \land i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+}))$
67	66	rspcev	$⊢ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \in ℂ \land ({\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})}^{2} = A \land 0 \leq ℜ (\sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|})) \land i \sqrt{\|A\|} (\frac{\|A\| + A}{\|\|A\| + A\|}) \notin ℝ^{+})) \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
68	56 58 67	syl2anc	$⊢ (A \in ℂ \land \|A\| + A \neq 0) \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
69	68	ex	$⊢ A \in ℂ \to (\|A\| + A \neq 0 \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+}))$
70	40 69	pm2.61dne	$⊢ A \in ℂ \to \exists x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
71		sqrmo	$⊢ A \in ℂ \to \exists^{*} x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$
72		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 ℝ^{+}))$
73	70 71 72	sylanbrc	$⊢ A \in ℂ \to \exists! x \in ℂ (x^{2} = A \land 0 \leq ℜ (x) \land i x \notin ℝ^{+})$

Metamath Proof Explorer

Theorem sqreu

Proof