Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
CSNo
x0
.
Let x1 of type
ι
be given.
Assume H1:
SNo
x1
.
Assume H2:
mul_SNo
(
add_SNo
(
exp_SNo_nat
(
CSNo_Re
x0
)
2
)
(
exp_SNo_nat
(
CSNo_Im
x0
)
2
)
)
x1
=
1
.
Claim L3:
...
...
Claim L4:
...
...
Apply mul_CSNo_mul_SNo with
x1
,
CSNo_Re
x0
,
λ x2 x3 .
mul_CSNo
x0
(
add_CSNo
x3
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_CSNo
x1
(
CSNo_Im
x0
)
)
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L3.
Apply mul_CSNo_mul_SNo with
x1
,
CSNo_Im
x0
,
λ x2 x3 .
mul_CSNo
x0
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
x3
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying L4.
Claim L5:
...
...
Claim L6:
...
...
Claim L7:
...
...
Claim L8:
...
...
Claim L9:
...
...
Claim L10:
...
...
Claim L11:
...
...
Claim L12:
...
...
Claim L13:
...
...
Apply CSNo_ReIm_split with
mul_CSNo
x0
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
,
1
leaving 4 subgoals.
Apply CSNo_mul_CSNo with
x0
,
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
The subproof is completed by applying CSNo_1.
Apply Re_1 with
λ x2 x3 .
CSNo_Re
(
mul_CSNo
x0
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
=
x3
.
Apply mul_CSNo_CRe with
x0
,
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
,
λ x2 x3 .
x3
=
1
leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L11.
Apply add_CSNo_CRe with
mul_SNo
x1
(
CSNo_Re
x0
)
,
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
x3
)
(
minus_SNo
(
mul_SNo
(
CSNo_Im
(
add_CSNo
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
(
CSNo_Im
x0
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
Apply add_CSNo_CIm with
mul_SNo
x1
(
CSNo_Re
x0
)
,
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
CSNo_Re
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
)
(
minus_SNo
(
mul_SNo
x3
(
CSNo_Im
x0
)
)
)
=
1
leaving 3 subgoals.
The subproof is completed by applying L6.
The subproof is completed by applying L10.
Apply minus_CSNo_CRe with
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
x3
)
)
(
minus_SNo
(
mul_SNo
(
add_SNo
(
CSNo_Im
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
CSNo_Im
(
minus_CSNo
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
(
CSNo_Im
x0
)
)
)
=
1
leaving 2 subgoals.
The subproof is completed by applying L9.
Apply minus_CSNo_CIm with
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
,
λ x2 x3 .
add_SNo
(
mul_SNo
(
CSNo_Re
x0
)
(
add_SNo
(
CSNo_Re
(
mul_SNo
x1
(
CSNo_Re
x0
)
)
)
(
minus_SNo
(
CSNo_Re
(
mul_CSNo
Complex_i
(
mul_SNo
x1
(
CSNo_Im
x0
)
)
)
)
)
)
)
(
minus_SNo
...
)
=
1
leaving 2 subgoals.
...
...
...
■