Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Richard Penner
Short Studies
Additions for square root; absolute value
resqrtval
Next ⟩
imsqrtval
Metamath Proof Explorer
Ascii
Unicode
Theorem
resqrtval
Description:
Real part of the complex square root.
(Contributed by
RP
, 18-May-2024)
Ref
Expression
Assertion
resqrtval
⊢
A
∈
ℂ
→
ℜ
⁡
A
=
A
+
ℜ
⁡
A
2
Proof
Step
Hyp
Ref
Expression
1
sqrtcval
⊢
A
∈
ℂ
→
A
=
A
+
ℜ
⁡
A
2
+
i
⁢
if
ℑ
⁡
A
<
0
−
1
1
⁢
A
−
ℜ
⁡
A
2
2
1
fveq2d
⊢
A
∈
ℂ
→
ℜ
⁡
A
=
ℜ
⁡
A
+
ℜ
⁡
A
2
+
i
⁢
if
ℑ
⁡
A
<
0
−
1
1
⁢
A
−
ℜ
⁡
A
2
3
sqrtcvallem5
⊢
A
∈
ℂ
→
A
+
ℜ
⁡
A
2
∈
ℝ
4
neg1rr
⊢
−
1
∈
ℝ
5
1re
⊢
1
∈
ℝ
6
4
5
ifcli
⊢
if
ℑ
⁡
A
<
0
−
1
1
∈
ℝ
7
6
a1i
⊢
A
∈
ℂ
→
if
ℑ
⁡
A
<
0
−
1
1
∈
ℝ
8
sqrtcvallem3
⊢
A
∈
ℂ
→
A
−
ℜ
⁡
A
2
∈
ℝ
9
7
8
remulcld
⊢
A
∈
ℂ
→
if
ℑ
⁡
A
<
0
−
1
1
⁢
A
−
ℜ
⁡
A
2
∈
ℝ
10
3
9
crred
⊢
A
∈
ℂ
→
ℜ
⁡
A
+
ℜ
⁡
A
2
+
i
⁢
if
ℑ
⁡
A
<
0
−
1
1
⁢
A
−
ℜ
⁡
A
2
=
A
+
ℜ
⁡
A
2
11
2
10
eqtrd
⊢
A
∈
ℂ
→
ℜ
⁡
A
=
A
+
ℜ
⁡
A
2