Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
∀ x0 x1 x2 .
SNo
x0
⟶
x1
∈
omega
⟶
x2
∈
real
⟶
SNo
(
eps_
x1
)
⟶
∃ x3 .
and
(
x3
∈
real
)
(
mul_SNo
x0
x3
=
1
)
.
Claim L1:
SNo
0
The subproof is completed by applying SNo_0.
Claim L2:
1
∈
omega
Apply nat_p_omega with
1
.
The subproof is completed by applying nat_1.
Claim L3:
0
∈
real
The subproof is completed by applying real_0.
Claim L4:
not
(
SNo
(
eps_
1
)
⟶
∃ x0 .
and
(
x0
∈
real
)
(
mul_SNo
0
x0
=
1
)
)
Assume H4:
SNo
(
eps_
1
)
⟶
∃ x0 .
and
(
x0
∈
real
)
(
mul_SNo
0
x0
=
1
)
.
Apply H4 with
False
leaving 2 subgoals.
The subproof is completed by applying SNo_eps_1.
Let x0 of type
ι
be given.
Assume H5:
(
λ x1 .
and
(
x1
∈
real
)
(
mul_SNo
0
x1
=
1
)
)
x0
.
Apply H5 with
False
.
Assume H6:
x0
∈
real
.
Apply mul_SNo_zeroL with
x0
,
λ x1 x2 .
x2
=
1
⟶
False
leaving 2 subgoals.
Apply real_SNo with
x0
.
The subproof is completed by applying H6.
The subproof is completed by applying neq_0_1.
Apply L4.
Apply H0 with
0
,
1
,
0
leaving 3 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying L2.
The subproof is completed by applying L3.
■