cxpsqrt

Description: The complex exponential function with exponent 1 / 2 exactly matches the complex square root function (the branch cut is in the same place for both functions), and thus serves as a suitable generalization to other n -th roots and irrational roots. (Contributed by Mario Carneiro, 2-Aug-2014)

		Ref	Expression
	Assertion	cxpsqrt	$⊢ A \in ℂ \to A^{\frac{1}{2}} = \sqrt{A}$

Proof

Step	Hyp	Ref	Expression
1		halfcn	$⊢ \frac{1}{2} \in ℂ$
2		halfre	$⊢ \frac{1}{2} \in ℝ$
3		halfgt0	$⊢ 0 < \frac{1}{2}$
4	2 3	gt0ne0ii	$⊢ \frac{1}{2} \neq 0$
5		0cxp	$⊢ (\frac{1}{2} \in ℂ \land \frac{1}{2} \neq 0) \to 0^{\frac{1}{2}} = 0$
6	1 4 5	mp2an	$⊢ 0^{\frac{1}{2}} = 0$
7		sqrt0	$⊢ \sqrt{0} = 0$
8	6 7	eqtr4i	$⊢ 0^{\frac{1}{2}} = \sqrt{0}$
9		oveq1	$⊢ A = 0 \to A^{\frac{1}{2}} = 0^{\frac{1}{2}}$
10		fveq2	$⊢ A = 0 \to \sqrt{A} = \sqrt{0}$
11	8 9 10	3eqtr4a	$⊢ A = 0 \to A^{\frac{1}{2}} = \sqrt{A}$
12	11	a1i	$⊢ A \in ℂ \to (A = 0 \to A^{\frac{1}{2}} = \sqrt{A})$
13		ax-icn	$⊢ i \in ℂ$
14		sqrtcl	$⊢ A \in ℂ \to \sqrt{A} \in ℂ$
15	14	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \sqrt{A} \in ℂ$
16		sqmul	$⊢ (i \in ℂ \land \sqrt{A} \in ℂ) \to {i \sqrt{A}}^{2} = i^{2} {\sqrt{A}}^{2}$
17	13 15 16	sylancr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {i \sqrt{A}}^{2} = i^{2} {\sqrt{A}}^{2}$
18		i2	$⊢ i^{2} = - 1$
19	18	a1i	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to i^{2} = - 1$
20		sqrtth	$⊢ A \in ℂ \to {\sqrt{A}}^{2} = A$
21	20	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {\sqrt{A}}^{2} = A$
22	19 21	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to i^{2} {\sqrt{A}}^{2} = -1 A$
23		mulm1	$⊢ A \in ℂ \to -1 A = - A$
24	23	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to -1 A = - A$
25	17 22 24	3eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {i \sqrt{A}}^{2} = - A$
26		cxpsqrtlem	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to i \sqrt{A} \in ℝ$
27	26	resqcld	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {i \sqrt{A}}^{2} \in ℝ$
28	25 27	eqeltrrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to - A \in ℝ$
29		negeq0	$⊢ A \in ℂ \to (A = 0 \leftrightarrow - A = 0)$
30	29	necon3bid	$⊢ A \in ℂ \to (A \neq 0 \leftrightarrow - A \neq 0)$
31	30	biimpa	$⊢ (A \in ℂ \land A \neq 0) \to - A \neq 0$
32	31	adantr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to - A \neq 0$
33	25 32	eqnetrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {i \sqrt{A}}^{2} \neq 0$
34		sq0i	$⊢ i \sqrt{A} = 0 \to {i \sqrt{A}}^{2} = 0$
35	34	necon3i	$⊢ {i \sqrt{A}}^{2} \neq 0 \to i \sqrt{A} \neq 0$
36	33 35	syl	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to i \sqrt{A} \neq 0$
37	26 36	sqgt0d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to 0 < {i \sqrt{A}}^{2}$
38	37 25	breqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to 0 < - A$
39	28 38	elrpd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to - A \in ℝ^{+}$
40		logneg	$⊢ - A \in ℝ^{+} \to \log (- (- A)) = \log (- A) + i π$
41	39 40	syl	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log (- (- A)) = \log (- A) + i π$
42		negneg	$⊢ A \in ℂ \to - (- A) = A$
43	42	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to - (- A) = A$
44	43	fveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log (- (- A)) = \log A$
45	39	relogcld	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log (- A) \in ℝ$
46	45	recnd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log (- A) \in ℂ$
47		picn	$⊢ π \in ℂ$
48	13 47	mulcli	$⊢ i π \in ℂ$
49		addcom	$⊢ (\log (- A) \in ℂ \land i π \in ℂ) \to \log (- A) + i π = i π + \log (- A)$
50	46 48 49	sylancl	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log (- A) + i π = i π + \log (- A)$
51	41 44 50	3eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \log A = i π + \log (- A)$
52	51	oveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\frac{1}{2}) \log A = (\frac{1}{2}) (i π + \log (- A))$
53		adddi	$⊢ (\frac{1}{2} \in ℂ \land i π \in ℂ \land \log (- A) \in ℂ) \to (\frac{1}{2}) (i π + \log (- A)) = (\frac{1}{2}) i π + (\frac{1}{2}) \log (- A)$
54	1 48 46 53	mp3an12i	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\frac{1}{2}) (i π + \log (- A)) = (\frac{1}{2}) i π + (\frac{1}{2}) \log (- A)$
55	52 54	eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\frac{1}{2}) \log A = (\frac{1}{2}) i π + (\frac{1}{2}) \log (- A)$
56		2cn	$⊢ 2 \in ℂ$
57		2ne0	$⊢ 2 \neq 0$
58		divrec2	$⊢ (i π \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{i π}{2} = (\frac{1}{2}) i π$
59	48 56 57 58	mp3an	$⊢ \frac{i π}{2} = (\frac{1}{2}) i π$
60	13 47 56 57	divassi	$⊢ \frac{i π}{2} = i (\frac{π}{2})$
61	59 60	eqtr3i	$⊢ (\frac{1}{2}) i π = i (\frac{π}{2})$
62	61	oveq1i	$⊢ (\frac{1}{2}) i π + (\frac{1}{2}) \log (- A) = i (\frac{π}{2}) + (\frac{1}{2}) \log (- A)$
63	55 62	eqtrdi	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\frac{1}{2}) \log A = i (\frac{π}{2}) + (\frac{1}{2}) \log (- A)$
64	63	fveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{(\frac{1}{2}) \log A} = e^{i (\frac{π}{2}) + (\frac{1}{2}) \log (- A)}$
65	47 56 57	divcli	$⊢ \frac{π}{2} \in ℂ$
66	13 65	mulcli	$⊢ i (\frac{π}{2}) \in ℂ$
67		mulcl	$⊢ (\frac{1}{2} \in ℂ \land \log (- A) \in ℂ) \to (\frac{1}{2}) \log (- A) \in ℂ$
68	1 46 67	sylancr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\frac{1}{2}) \log (- A) \in ℂ$
69		efadd	$⊢ (i (\frac{π}{2}) \in ℂ \land (\frac{1}{2}) \log (- A) \in ℂ) \to e^{i (\frac{π}{2}) + (\frac{1}{2}) \log (- A)} = e^{i (\frac{π}{2})} e^{(\frac{1}{2}) \log (- A)}$
70	66 68 69	sylancr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{i (\frac{π}{2}) + (\frac{1}{2}) \log (- A)} = e^{i (\frac{π}{2})} e^{(\frac{1}{2}) \log (- A)}$
71		efhalfpi	$⊢ e^{i (\frac{π}{2})} = i$
72	71	a1i	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{i (\frac{π}{2})} = i$
73		negcl	$⊢ A \in ℂ \to - A \in ℂ$
74	73	ad2antrr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to - A \in ℂ$
75	1	a1i	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \frac{1}{2} \in ℂ$
76		cxpef	$⊢ (- A \in ℂ \land - A \neq 0 \land \frac{1}{2} \in ℂ) \to {(- A)}^{\frac{1}{2}} = e^{(\frac{1}{2}) \log (- A)}$
77	74 32 75 76	syl3anc	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{\frac{1}{2}} = e^{(\frac{1}{2}) \log (- A)}$
78		ax-1cn	$⊢ 1 \in ℂ$
79		2halves	$⊢ 1 \in ℂ \to (\frac{1}{2}) + (\frac{1}{2}) = 1$
80	78 79	ax-mp	$⊢ (\frac{1}{2}) + (\frac{1}{2}) = 1$
81	80	oveq2i	$⊢ {(- A)}^{(\frac{1}{2}) + (\frac{1}{2})} = {(- A)}^{1}$
82		cxp1	$⊢ - A \in ℂ \to {(- A)}^{1} = - A$
83	74 82	syl	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{1} = - A$
84	81 83	eqtrid	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{(\frac{1}{2}) + (\frac{1}{2})} = - A$
85		rpcxpcl	$⊢ (- A \in ℝ^{+} \land \frac{1}{2} \in ℝ) \to {(- A)}^{\frac{1}{2}} \in ℝ^{+}$
86	39 2 85	sylancl	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{\frac{1}{2}} \in ℝ^{+}$
87	86	rpcnd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{\frac{1}{2}} \in ℂ$
88	87	sqvald	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {({(- A)}^{\frac{1}{2}})}^{2} = {(- A)}^{\frac{1}{2}} {(- A)}^{\frac{1}{2}}$
89		cxpadd	$⊢ ((- A \in ℂ \land - A \neq 0) \land \frac{1}{2} \in ℂ \land \frac{1}{2} \in ℂ) \to {(- A)}^{(\frac{1}{2}) + (\frac{1}{2})} = {(- A)}^{\frac{1}{2}} {(- A)}^{\frac{1}{2}}$
90	74 32 75 75 89	syl211anc	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{(\frac{1}{2}) + (\frac{1}{2})} = {(- A)}^{\frac{1}{2}} {(- A)}^{\frac{1}{2}}$
91	88 90	eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {({(- A)}^{\frac{1}{2}})}^{2} = {(- A)}^{(\frac{1}{2}) + (\frac{1}{2})}$
92	74	sqsqrtd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {\sqrt{- A}}^{2} = - A$
93	84 91 92	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {({(- A)}^{\frac{1}{2}})}^{2} = {\sqrt{- A}}^{2}$
94	86	rprege0d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to ({(- A)}^{\frac{1}{2}} \in ℝ \land 0 \leq {(- A)}^{\frac{1}{2}})$
95	39	rpsqrtcld	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \sqrt{- A} \in ℝ^{+}$
96	95	rprege0d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to (\sqrt{- A} \in ℝ \land 0 \leq \sqrt{- A})$
97		sq11	$⊢ (({(- A)}^{\frac{1}{2}} \in ℝ \land 0 \leq {(- A)}^{\frac{1}{2}}) \land (\sqrt{- A} \in ℝ \land 0 \leq \sqrt{- A})) \to ({({(- A)}^{\frac{1}{2}})}^{2} = {\sqrt{- A}}^{2} \leftrightarrow {(- A)}^{\frac{1}{2}} = \sqrt{- A})$
98	94 96 97	syl2anc	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to ({({(- A)}^{\frac{1}{2}})}^{2} = {\sqrt{- A}}^{2} \leftrightarrow {(- A)}^{\frac{1}{2}} = \sqrt{- A})$
99	93 98	mpbid	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to {(- A)}^{\frac{1}{2}} = \sqrt{- A}$
100	77 99	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{(\frac{1}{2}) \log (- A)} = \sqrt{- A}$
101	72 100	oveq12d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{i (\frac{π}{2})} e^{(\frac{1}{2}) \log (- A)} = i \sqrt{- A}$
102	64 70 101	3eqtrd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to e^{(\frac{1}{2}) \log A} = i \sqrt{- A}$
103		cxpef	$⊢ (A \in ℂ \land A \neq 0 \land \frac{1}{2} \in ℂ) \to A^{\frac{1}{2}} = e^{(\frac{1}{2}) \log A}$
104	1 103	mp3an3	$⊢ (A \in ℂ \land A \neq 0) \to A^{\frac{1}{2}} = e^{(\frac{1}{2}) \log A}$
105	104	adantr	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to A^{\frac{1}{2}} = e^{(\frac{1}{2}) \log A}$
106	43	fveq2d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \sqrt{- (- A)} = \sqrt{A}$
107	39	rpge0d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to 0 \leq - A$
108	28 107	sqrtnegd	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \sqrt{- (- A)} = i \sqrt{- A}$
109	106 108	eqtr3d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to \sqrt{A} = i \sqrt{- A}$
110	102 105 109	3eqtr4d	$⊢ ((A \in ℂ \land A \neq 0) \land A^{\frac{1}{2}} = - \sqrt{A}) \to A^{\frac{1}{2}} = \sqrt{A}$
111	110	ex	$⊢ (A \in ℂ \land A \neq 0) \to (A^{\frac{1}{2}} = - \sqrt{A} \to A^{\frac{1}{2}} = \sqrt{A})$
112	80	oveq2i	$⊢ A^{(\frac{1}{2}) + (\frac{1}{2})} = A^{1}$
113		cxpadd	$⊢ ((A \in ℂ \land A \neq 0) \land \frac{1}{2} \in ℂ \land \frac{1}{2} \in ℂ) \to A^{(\frac{1}{2}) + (\frac{1}{2})} = A^{\frac{1}{2}} A^{\frac{1}{2}}$
114	1 1 113	mp3an23	$⊢ (A \in ℂ \land A \neq 0) \to A^{(\frac{1}{2}) + (\frac{1}{2})} = A^{\frac{1}{2}} A^{\frac{1}{2}}$
115		cxp1	$⊢ A \in ℂ \to A^{1} = A$
116	115	adantr	$⊢ (A \in ℂ \land A \neq 0) \to A^{1} = A$
117	112 114 116	3eqtr3a	$⊢ (A \in ℂ \land A \neq 0) \to A^{\frac{1}{2}} A^{\frac{1}{2}} = A$
118		cxpcl	$⊢ (A \in ℂ \land \frac{1}{2} \in ℂ) \to A^{\frac{1}{2}} \in ℂ$
119	1 118	mpan2	$⊢ A \in ℂ \to A^{\frac{1}{2}} \in ℂ$
120	119	sqvald	$⊢ A \in ℂ \to {(A^{\frac{1}{2}})}^{2} = A^{\frac{1}{2}} A^{\frac{1}{2}}$
121	120	adantr	$⊢ (A \in ℂ \land A \neq 0) \to {(A^{\frac{1}{2}})}^{2} = A^{\frac{1}{2}} A^{\frac{1}{2}}$
122	20	adantr	$⊢ (A \in ℂ \land A \neq 0) \to {\sqrt{A}}^{2} = A$
123	117 121 122	3eqtr4d	$⊢ (A \in ℂ \land A \neq 0) \to {(A^{\frac{1}{2}})}^{2} = {\sqrt{A}}^{2}$
124		sqeqor	$⊢ (A^{\frac{1}{2}} \in ℂ \land \sqrt{A} \in ℂ) \to ({(A^{\frac{1}{2}})}^{2} = {\sqrt{A}}^{2} \leftrightarrow (A^{\frac{1}{2}} = \sqrt{A} \lor A^{\frac{1}{2}} = - \sqrt{A}))$
125	119 14 124	syl2anc	$⊢ A \in ℂ \to ({(A^{\frac{1}{2}})}^{2} = {\sqrt{A}}^{2} \leftrightarrow (A^{\frac{1}{2}} = \sqrt{A} \lor A^{\frac{1}{2}} = - \sqrt{A}))$
126	125	biimpa	$⊢ (A \in ℂ \land {(A^{\frac{1}{2}})}^{2} = {\sqrt{A}}^{2}) \to (A^{\frac{1}{2}} = \sqrt{A} \lor A^{\frac{1}{2}} = - \sqrt{A})$
127	123 126	syldan	$⊢ (A \in ℂ \land A \neq 0) \to (A^{\frac{1}{2}} = \sqrt{A} \lor A^{\frac{1}{2}} = - \sqrt{A})$
128	127	ord	$⊢ (A \in ℂ \land A \neq 0) \to (\neg A^{\frac{1}{2}} = \sqrt{A} \to A^{\frac{1}{2}} = - \sqrt{A})$
129	128	con1d	$⊢ (A \in ℂ \land A \neq 0) \to (\neg A^{\frac{1}{2}} = - \sqrt{A} \to A^{\frac{1}{2}} = \sqrt{A})$
130	111 129	pm2.61d	$⊢ (A \in ℂ \land A \neq 0) \to A^{\frac{1}{2}} = \sqrt{A}$
131	130	ex	$⊢ A \in ℂ \to (A \neq 0 \to A^{\frac{1}{2}} = \sqrt{A})$
132	12 131	pm2.61dne	$⊢ A \in ℂ \to A^{\frac{1}{2}} = \sqrt{A}$

Metamath Proof Explorer

Theorem cxpsqrt

Proof