Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
x0
∈
complex
.
Let x1 of type
ι
be given.
Assume H1:
x1
∈
complex
.
Apply complex_I with
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
CSNo_Re
x1
)
)
(
minus_SNo
(
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Im
x1
)
)
)
,
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
CSNo_Im
x1
)
)
(
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Re
x1
)
)
leaving 2 subgoals.
Apply real_add_SNo with
mul_SNo
(
CSNo_Re
x0
)
(
CSNo_Re
x1
)
,
minus_SNo
(
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Im
x1
)
)
leaving 2 subgoals.
Apply real_mul_SNo with
CSNo_Re
x0
,
CSNo_Re
x1
leaving 2 subgoals.
Apply complex_Re_real with
x0
.
The subproof is completed by applying H0.
Apply complex_Re_real with
x1
.
The subproof is completed by applying H1.
Apply real_minus_SNo with
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Im
x1
)
.
Apply real_mul_SNo with
CSNo_Im
x0
,
CSNo_Im
x1
leaving 2 subgoals.
Apply complex_Im_real with
x0
.
The subproof is completed by applying H0.
Apply complex_Im_real with
x1
.
The subproof is completed by applying H1.
Apply real_add_SNo with
mul_SNo
(
CSNo_Re
x0
)
(
CSNo_Im
x1
)
,
mul_SNo
(
CSNo_Im
x0
)
(
CSNo_Re
x1
)
leaving 2 subgoals.
Apply real_mul_SNo with
CSNo_Re
x0
,
CSNo_Im
x1
leaving 2 subgoals.
Apply complex_Re_real with
x0
.
The subproof is completed by applying H0.
Apply complex_Im_real with
x1
.
The subproof is completed by applying H1.
Apply real_mul_SNo with
CSNo_Im
x0
,
CSNo_Re
x1
leaving 2 subgoals.
Apply complex_Im_real with
x0
.
The subproof is completed by applying H0.
Apply complex_Re_real with
x1
.
The subproof is completed by applying H1.
■