Search for blocks/addresses/...
Proofgold Asset
asset id
1689d89399e8d2673f37e27c41dacb1408128d96b3827b7fbe43dfca6e8e1420
asset hash
6347409421566c96140ecabc92197a0bee37df2586b56824df2ea4c73f2add54
bday / block
29749
tx
aa676..
preasset
doc published by
PrQUS..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Param
surj
surj
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Param
omega
omega
:
ι
Known
form100_22_v3
form100_22_v3
:
∀ x0 :
ι → ι
.
not
(
surj
omega
(
prim4
omega
)
x0
)
Param
bij
bij
:
ι
→
ι
→
(
ι
→
ι
) →
ο
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Known
bij_surj
bij_surj
:
∀ x0 x1 .
∀ x2 :
ι → ι
.
bij
x0
x1
x2
⟶
surj
x0
x1
x2
Theorem
form100_22_v1
form100_22_v1
:
not
(
equip
omega
(
prim4
omega
)
)
(proof)
Param
SNoLt
SNoLt
:
ι
→
ι
→
ο
Param
eps_
eps_
:
ι
→
ι
Param
ordsucc
ordsucc
:
ι
→
ι
Param
nat_p
nat_p
:
ι
→
ο
Param
add_SNo
add_SNo
:
ι
→
ι
→
ι
Known
eps_ordsucc_half_add
eps_ordsucc_half_add
:
∀ x0 .
nat_p
x0
⟶
add_SNo
(
eps_
(
ordsucc
x0
)
)
(
eps_
(
ordsucc
x0
)
)
=
eps_
x0
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Param
SNo
SNo
:
ι
→
ο
Known
add_SNo_eps_Lt
add_SNo_eps_Lt
:
∀ x0 .
SNo
x0
⟶
∀ x1 .
x1
∈
omega
⟶
SNoLt
x0
(
add_SNo
x0
(
eps_
x1
)
)
Known
SNo_eps_
SNo_eps_
:
∀ x0 .
x0
∈
omega
⟶
SNo
(
eps_
x0
)
Known
omega_ordsucc
omega_ordsucc
:
∀ x0 .
x0
∈
omega
⟶
ordsucc
x0
∈
omega
Theorem
eps_ordsucc_Lt
:
∀ x0 .
x0
∈
omega
⟶
SNoLt
(
eps_
(
ordsucc
x0
)
)
(
eps_
x0
)
(proof)
Param
real
real
:
ι
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Param
SNoLev
SNoLev
:
ι
→
ι
Param
SNoS_
SNoS_
:
ι
→
ι
Param
minus_SNo
minus_SNo
:
ι
→
ι
Param
abs_SNo
abs_SNo
:
ι
→
ι
Known
real_E
real_E
:
∀ x0 .
x0
∈
real
⟶
∀ x1 : ο .
(
SNo
x0
⟶
SNoLev
x0
∈
ordsucc
omega
⟶
x0
∈
SNoS_
(
ordsucc
omega
)
⟶
SNoLt
(
minus_SNo
omega
)
x0
⟶
SNoLt
x0
omega
⟶
(
∀ x2 .
x2
∈
SNoS_
omega
⟶
(
∀ x3 .
x3
∈
omega
⟶
SNoLt
(
abs_SNo
(
add_SNo
x2
(
minus_SNo
x0
)
)
)
(
eps_
x3
)
)
⟶
x2
=
x0
)
⟶
(
∀ x2 .
x2
∈
omega
⟶
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
SNoS_
omega
)
(
and
(
SNoLt
x4
x0
)
(
SNoLt
x0
(
add_SNo
x4
(
eps_
x2
)
)
)
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
Known
SNoLt_irref
SNoLt_irref
:
∀ x0 .
not
(
SNoLt
x0
x0
)
Param
ordinal
ordinal
:
ι
→
ο
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
binunion
binunion
:
ι
→
ι
→
ι
Param
SetAdjoin
SetAdjoin
:
ι
→
ι
→
ι
Param
Sing
Sing
:
ι
→
ι
Definition
SNoElts_
SNoElts_
:=
λ x0 .
binunion
x0
{
SetAdjoin
x1
(
Sing
1
)
|x1 ∈
x0
}
Param
exactly1of2
exactly1of2
:
ο
→
ο
→
ο
Definition
SNo_
SNo_
:=
λ x0 x1 .
and
(
x1
⊆
SNoElts_
x0
)
(
∀ x2 .
x2
∈
x0
⟶
exactly1of2
(
SetAdjoin
x2
(
Sing
1
)
∈
x1
)
(
x2
∈
x1
)
)
Known
SNoS_I
SNoS_I
:
∀ x0 .
ordinal
x0
⟶
∀ x1 x2 .
x2
∈
x0
⟶
SNo_
x2
x1
⟶
x1
∈
SNoS_
x0
Known
omega_ordinal
omega_ordinal
:
ordinal
omega
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
nat_0
nat_0
:
nat_p
0
Known
ordinal_SNo_
ordinal_SNo_
:
∀ x0 .
ordinal
x0
⟶
SNo_
x0
x0
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Known
add_SNo_0L
add_SNo_0L
:
∀ x0 .
SNo
x0
⟶
add_SNo
0
x0
=
x0
Known
SNo_minus_SNo
SNo_minus_SNo
:
∀ x0 .
SNo
x0
⟶
SNo
(
minus_SNo
x0
)
Known
abs_SNo_minus
abs_SNo_minus
:
∀ x0 .
SNo
x0
⟶
abs_SNo
(
minus_SNo
x0
)
=
abs_SNo
x0
Param
SNoLe
SNoLe
:
ι
→
ι
→
ο
Known
nonneg_abs_SNo
nonneg_abs_SNo
:
∀ x0 .
SNoLe
0
x0
⟶
abs_SNo
x0
=
x0
Known
SNoLtLe
SNoLtLe
:
∀ x0 x1 .
SNoLt
x0
x1
⟶
SNoLe
x0
x1
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
SNoLtLe_or
SNoLtLe_or
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
or
(
SNoLt
x0
x1
)
(
SNoLe
x1
x0
)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Known
SNoLtLe_tra
SNoLtLe_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLe
x1
x2
⟶
SNoLt
x0
x2
Theorem
real_pos_eps_
:
∀ x0 .
x0
∈
real
⟶
SNoLt
0
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
SNoLt
(
eps_
x2
)
x0
)
⟶
x1
)
⟶
x1
(proof)
Known
real_add_SNo
real_add_SNo
:
∀ x0 .
x0
∈
real
⟶
∀ x1 .
x1
∈
real
⟶
add_SNo
x0
x1
∈
real
Known
real_minus_SNo
real_minus_SNo
:
∀ x0 .
x0
∈
real
⟶
minus_SNo
x0
∈
real
Known
add_SNo_minus_Lt2b
add_SNo_minus_Lt2b
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
(
add_SNo
x2
x1
)
x0
⟶
SNoLt
x2
(
add_SNo
x0
(
minus_SNo
x1
)
)
Known
SNo_0
SNo_0
:
SNo
0
Known
SNoS_E2
SNoS_E2
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
SNoS_
x0
⟶
∀ x2 : ο .
(
SNoLev
x1
∈
x0
⟶
ordinal
(
SNoLev
x1
)
⟶
SNo
x1
⟶
SNo_
(
SNoLev
x1
)
x1
⟶
x2
)
⟶
x2
Known
add_SNo_minus_Lt2
add_SNo_minus_Lt2
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x2
(
add_SNo
x0
(
minus_SNo
x1
)
)
⟶
SNoLt
(
add_SNo
x2
x1
)
x0
Known
add_SNo_Lt2_cancel
add_SNo_Lt2_cancel
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
(
add_SNo
x0
x1
)
(
add_SNo
x0
x2
)
⟶
SNoLt
x1
x2
Known
SNo_add_SNo
SNo_add_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
add_SNo
x0
x1
)
Known
add_SNo_0R
add_SNo_0R
:
∀ x0 .
SNo
x0
⟶
add_SNo
x0
0
=
x0
Known
add_SNo_com_3_0_1
add_SNo_com_3_0_1
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
(
add_SNo
x1
x2
)
=
add_SNo
x1
(
add_SNo
x0
x2
)
Known
SNoLt_tra
SNoLt_tra
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x0
x1
⟶
SNoLt
x1
x2
⟶
SNoLt
x0
x2
Known
SNo_add_SNo_3
SNo_add_SNo_3
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNo
(
add_SNo
x0
(
add_SNo
x1
x2
)
)
Known
add_SNo_Lt2
add_SNo_Lt2
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
SNoLt
x1
x2
⟶
SNoLt
(
add_SNo
x0
x1
)
(
add_SNo
x0
x2
)
Known
real_SNo
real_SNo
:
∀ x0 .
x0
∈
real
⟶
SNo
x0
Theorem
real_Lt_SNoS_omega_inter
:
∀ x0 .
x0
∈
real
⟶
∀ x1 .
x1
∈
real
⟶
SNoLt
x0
x1
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
SNoS_
omega
)
(
and
(
SNoLt
x0
x3
)
(
SNoLt
x3
x1
)
)
⟶
x2
)
⟶
x2
(proof)
Definition
inj
inj
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
Definition
atleastp
atleastp
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
inj
x0
x1
x3
⟶
x2
)
⟶
x2
Param
ReplSep
ReplSep
:
ι
→
(
ι
→
ο
) →
(
ι
→
ι
) →
ι
Param
mul_SNo
mul_SNo
:
ι
→
ι
→
ι
Known
PowerI
PowerI
:
∀ x0 x1 .
x1
⊆
x0
⟶
x1
∈
prim4
x0
Known
binunion_Subq_min
binunion_Subq_min
:
∀ x0 x1 x2 .
x0
⊆
x2
⟶
x1
⊆
x2
⟶
binunion
x0
x1
⊆
x2
Known
ReplSepE_impred
ReplSepE_impred
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
ReplSep
x0
x1
x2
⟶
∀ x4 : ο .
(
∀ x5 .
x5
∈
x0
⟶
x1
x5
⟶
x3
=
x2
x5
⟶
x4
)
⟶
x4
Known
mul_SNo_In_omega
mul_SNo_In_omega
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_SNo
x0
x1
∈
omega
Known
nat_2
nat_2
:
nat_p
2
Known
add_SNo_In_omega
add_SNo_In_omega
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
add_SNo
x0
x1
∈
omega
Known
nat_1
nat_1
:
nat_p
1
Known
ordsucc_omega_ordinal
ordsucc_omega_ordinal
:
ordinal
(
ordsucc
omega
)
Known
set_ext
set_ext
:
∀ x0 x1 .
x0
⊆
x1
⟶
x1
⊆
x0
⟶
x0
=
x1
Param
TransSet
TransSet
:
ι
→
ο
Known
TransSet_In_ordsucc_Subq
TransSet_In_ordsucc_Subq
:
∀ x0 x1 .
TransSet
x1
⟶
x0
∈
ordsucc
x1
⟶
x0
⊆
x1
Known
omega_TransSet
omega_TransSet
:
TransSet
omega
Known
binunionE
binunionE
:
∀ x0 x1 x2 .
x2
∈
binunion
x0
x1
⟶
or
(
x2
∈
x0
)
(
x2
∈
x1
)
Known
binunionI1
binunionI1
:
∀ x0 x1 x2 .
x2
∈
x0
⟶
x2
∈
binunion
x0
x1
Known
ReplSepI
ReplSepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 :
ι → ι
.
∀ x3 .
x3
∈
x0
⟶
x1
x3
⟶
x2
x3
∈
ReplSep
x0
x1
x2
Known
mul_SNo_nonzero_cancel
mul_SNo_nonzero_cancel_L
:
∀ x0 x1 x2 .
SNo
x0
⟶
(
x0
=
0
⟶
∀ x3 : ο .
x3
)
⟶
SNo
x1
⟶
SNo
x2
⟶
mul_SNo
x0
x1
=
mul_SNo
x0
x2
⟶
x1
=
x2
Known
SNo_2
SNo_2
:
SNo
2
Known
neq_2_0
neq_2_0
:
2
=
0
⟶
∀ x0 : ο .
x0
Known
omega_SNo
omega_SNo
:
∀ x0 .
x0
∈
omega
⟶
SNo
x0
Param
even_nat
even_nat
:
ι
→
ο
Param
odd_nat
odd_nat
:
ι
→
ο
Known
even_nat_not_odd_nat
even_nat_not_odd_nat
:
∀ x0 .
even_nat
x0
⟶
not
(
odd_nat
x0
)
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Known
mul_nat_mul_SNo
mul_nat_mul_SNo
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
x0
x1
=
mul_SNo
x0
x1
Known
even_nat_double
even_nat_double
:
∀ x0 .
nat_p
x0
⟶
even_nat
(
mul_nat
2
x0
)
Known
add_SNo_com
add_SNo_com
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
add_SNo
x0
x1
=
add_SNo
x1
x0
Known
SNo_1
SNo_1
:
SNo
1
Known
ordinal_ordsucc_SNo_eq
ordinal_ordsucc_SNo_eq
:
∀ x0 .
ordinal
x0
⟶
ordsucc
x0
=
add_SNo
1
x0
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
even_nat_odd_nat_S
even_nat_odd_nat_S
:
∀ x0 .
even_nat
x0
⟶
odd_nat
(
ordsucc
x0
)
Known
ReplE_impred
ReplE_impred
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
prim5
x0
x1
⟶
∀ x3 : ο .
(
∀ x4 .
x4
∈
x0
⟶
x2
=
x1
x4
⟶
x3
)
⟶
x3
Known
binunionI2
binunionI2
:
∀ x0 x1 x2 .
x2
∈
x1
⟶
x2
∈
binunion
x0
x1
Known
add_SNo_cancel_R
add_SNo_cancel_R
:
∀ x0 x1 x2 .
SNo
x0
⟶
SNo
x1
⟶
SNo
x2
⟶
add_SNo
x0
x1
=
add_SNo
x2
x1
⟶
x0
=
x2
Known
SNo_mul_SNo
SNo_mul_SNo
:
∀ x0 x1 .
SNo
x0
⟶
SNo
x1
⟶
SNo
(
mul_SNo
x0
x1
)
Theorem
atleastp_SNoS_ordsucc_omega_Power_omega
atleastp_SNoS_ordsucc_omega_Power_omega
:
atleastp
(
SNoS_
(
ordsucc
omega
)
)
(
prim4
omega
)
(proof)
Param
finite
finite
:
ι
→
ο
Definition
infinite
infinite
:=
λ x0 .
not
(
finite
x0
)
Param
nIn
nIn
:
ι
→
ι
→
ο
Known
finite_ind
finite_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 x2 .
finite
x1
⟶
nIn
x2
x1
⟶
x0
x1
⟶
x0
(
binunion
x1
(
Sing
x2
)
)
)
⟶
∀ x1 .
finite
x1
⟶
x0
x1
Known
Repl_Empty
Repl_Empty
:
∀ x0 :
ι → ι
.
prim5
0
x0
=
0
Known
finite_Empty
finite_Empty
:
finite
0
Known
ReplI
ReplI
:
∀ x0 .
∀ x1 :
ι → ι
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
∈
prim5
x0
x1
Known
SingE
SingE
:
∀ x0 x1 .
x1
∈
Sing
x0
⟶
x1
=
x0
Known
SingI
SingI
:
∀ x0 .
x0
∈
Sing
x0
Known
binunion_finite
binunion_finite
:
∀ x0 .
finite
x0
⟶
∀ x1 .
finite
x1
⟶
finite
(
binunion
x0
x1
)
Known
28148..
Sing_finite
:
∀ x0 .
finite
(
Sing
x0
)
Theorem
Repl_finite
Repl_finite
:
∀ x0 :
ι → ι
.
∀ x1 .
finite
x1
⟶
finite
(
prim5
x1
x0
)
(proof)
Known
Subq_finite
Subq_finite
:
∀ x0 .
finite
x0
⟶
∀ x1 .
x1
⊆
x0
⟶
finite
x1
Known
9b83b..
nat_finite
:
∀ x0 .
nat_p
x0
⟶
finite
x0
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
ordinal_trichotomy_or_impred
ordinal_trichotomy_or_impred
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
∀ x2 : ο .
(
x0
∈
x1
⟶
x2
)
⟶
(
x0
=
x1
⟶
x2
)
⟶
(
x1
∈
x0
⟶
x2
)
⟶
x2
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Theorem
infinite_bigger
infinite_bigger
:
∀ x0 .
x0
⊆
omega
⟶
infinite
x0
⟶
∀ x1 .
x1
∈
omega
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x0
)
(
x1
∈
x3
)
⟶
x2
)
⟶
x2
(proof)