Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
CSNo
x0
.
Claim L1:
...
...
Claim L2:
...
...
Claim L3:
...
...
Claim L4:
...
...
Claim L5:
...
...
Claim L6:
...
...
Claim L7:
...
...
Claim L8:
...
...
Claim L9:
...
...
Claim L10:
...
...
Claim L11:
...
...
Claim L12:
...
...
Claim L13:
...
...
Claim L14:
...
...
Claim L15:
...
...
Claim L16:
...
...
Claim L17:
...
...
Claim L18:
...
...
Claim L19:
...
...
Claim L20:
...
...
Claim L21:
...
...
Claim L22:
...
...
Claim L23:
...
...
Claim L24:
...
...
Claim L25:
...
...
Claim L26:
...
...
Claim L27:
...
...
Claim L28:
...
...
Claim L29:
...
...
Claim L30:
...
...
Claim L31:
...
...
Claim L32:
...
...
Claim L33:
...
...
Claim L34:
...
...
Claim L35:
...
...
Claim L36:
...
...
Claim L37:
...
...
Claim L38:
...
...
Claim L39:
...
...
Claim L40:
...
...
Claim L41:
...
...
Claim L42:
...
...
Claim L43:
...
...
Claim L44:
...
...
Claim L45:
...
...
Claim L46:
...
...
Claim L47:
...
...
Claim L48:
...
...
Apply SNoLt_trichotomy_or_impred with
CSNo_Im
x0
,
0
,
exp_CSNo_nat
(
If_i
(
or
(
SNoLt
(
CSNo_Im
x0
)
0
)
(
and
(
CSNo_Im
x0
=
0
)
(
SNoLt
(
CSNo_Re
x0
)
0
)
)
)
(
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
)
(
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
)
2
=
x0
leaving 5 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying SNo_0.
Assume H49:
SNoLt
(
CSNo_Im
x0
)
0
.
Claim L50:
...
...
Apply If_i_1 with
or
(
SNoLt
(
CSNo_Im
x0
)
0
)
(
and
(
CSNo_Im
x0
=
0
)
(
SNoLt
(
CSNo_Re
x0
)
0
)
)
,
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
,
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
,
λ x1 x2 .
exp_CSNo_nat
x2
2
=
x0
leaving 2 subgoals.
The subproof is completed by applying L50.
Apply CSNo_ReIm_split with
exp_CSNo_nat
(
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
)
2
,
x0
leaving 4 subgoals.
The subproof is completed by applying L43.
The subproof is completed by applying H0.
Apply exp_CSNo_nat_2 with
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
,
λ x1 x2 .
CSNo_Re
x2
=
CSNo_Re
x0
leaving 2 subgoals.
The subproof is completed by applying L41.
Apply mul_CSNo_CRe with
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
,
SNo_pair
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
)
(
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
)
,
λ x1 x2 .
x2
=
CSNo_Re
x0
leaving 3 subgoals.
The subproof is completed by applying L41.
The subproof is completed by applying L41.
Apply CSNo_Re2 with
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
CSNo_Re
x0
)
(
modulus_CSNo
x0
)
)
)
,
minus_SNo
(
sqrt_SNo_nonneg
(
mul_SNo
(
eps_
1
)
(
add_SNo
(
minus_SNo
(
CSNo_Re
x0
)
)
(
modulus_CSNo
x0
)
)
)
)
,
λ x1 x2 .
add_SNo
(
mul_SNo
x2
x2
)
...
=
...
leaving 3 subgoals.
...
...
...
...
...
...
■