Search for blocks/addresses/...
Proofgold Asset
asset id
01deda1c3488cb60edda5ff2d77eb1f932ba664ff3790ca553e2ea6a28dc619b
asset hash
a9529ce49ce79142cc701896b00c8558eb4b9f926c7fe07940a2661e889b04d7
bday / block
29757
tx
00571..
preasset
doc published by
PrQUS..
Param
omega
omega
:
ι
Definition
and
and
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x1
⟶
x2
)
⟶
x2
Param
mul_nat
mul_nat
:
ι
→
ι
→
ι
Definition
divides_nat
divides_nat
:=
λ x0 x1 .
and
(
and
(
x0
∈
omega
)
(
x1
∈
omega
)
)
(
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
omega
)
(
mul_nat
x0
x3
=
x1
)
⟶
x2
)
⟶
x2
)
Known
and3I
and3I
:
∀ x0 x1 x2 : ο .
x0
⟶
x1
⟶
x2
⟶
and
(
and
x0
x1
)
x2
Param
nat_p
nat_p
:
ι
→
ο
Known
nat_p_omega
nat_p_omega
:
∀ x0 .
nat_p
x0
⟶
x0
∈
omega
Known
mul_nat_p
mul_nat_p
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
nat_p
(
mul_nat
x0
x1
)
Known
omega_nat_p
omega_nat_p
:
∀ x0 .
x0
∈
omega
⟶
nat_p
x0
Known
andI
andI
:
∀ x0 x1 : ο .
x0
⟶
x1
⟶
and
x0
x1
Theorem
divides_nat_mulR
divides_nat_mulR
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
divides_nat
x0
(
mul_nat
x0
x1
)
(proof)
Known
mul_nat_com
mul_nat_com
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
mul_nat
x0
x1
=
mul_nat
x1
x0
Theorem
divides_nat_mulL
divides_nat_mulL
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
divides_nat
x1
(
mul_nat
x0
x1
)
(proof)
Definition
Subq
Subq
:=
λ x0 x1 .
∀ x2 .
x2
∈
x0
⟶
x2
∈
x1
Param
ordsucc
ordsucc
:
ι
→
ι
Definition
or
or
:=
λ x0 x1 : ο .
∀ x2 : ο .
(
x0
⟶
x2
)
⟶
(
x1
⟶
x2
)
⟶
x2
Known
nat_inv_impred
nat_inv_impred
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
orIL
orIL
:
∀ x0 x1 : ο .
x0
⟶
or
x0
x1
Known
orIR
orIR
:
∀ x0 x1 : ο .
x1
⟶
or
x0
x1
Definition
False
False
:=
∀ x0 : ο .
x0
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Definition
nIn
nIn
:=
λ x0 x1 .
not
(
x0
∈
x1
)
Known
In_irref
In_irref
:
∀ x0 .
nIn
x0
x0
Known
nat_ordsucc_in_ordsucc
nat_ordsucc_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
∈
ordsucc
x0
Known
nat_ordsucc
nat_ordsucc
:
∀ x0 .
nat_p
x0
⟶
nat_p
(
ordsucc
x0
)
Known
nat_0_in_ordsucc
nat_0_in_ordsucc
:
∀ x0 .
nat_p
x0
⟶
0
∈
ordsucc
x0
Theorem
nat_le1_cases
nat_le1_cases
:
∀ x0 .
nat_p
x0
⟶
x0
⊆
1
⟶
or
(
x0
=
0
)
(
x0
=
1
)
(proof)
Definition
composite_nat
composite_nat
:=
λ x0 .
and
(
x0
∈
omega
)
(
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
∀ x3 : ο .
(
∀ x4 .
and
(
x4
∈
omega
)
(
and
(
and
(
1
∈
x2
)
(
1
∈
x4
)
)
(
mul_nat
x2
x4
=
x0
)
)
⟶
x3
)
⟶
x3
)
⟶
x1
)
⟶
x1
)
Definition
prime_nat
prime_nat
:=
λ x0 .
and
(
and
(
x0
∈
omega
)
(
1
∈
x0
)
)
(
∀ x1 .
x1
∈
omega
⟶
divides_nat
x1
x0
⟶
or
(
x1
=
1
)
(
x1
=
x0
)
)
Known
xm
xm
:
∀ x0 : ο .
or
x0
(
not
x0
)
Known
dneg
dneg
:
∀ x0 : ο .
not
(
not
x0
)
⟶
x0
Param
ordinal
ordinal
:
ι
→
ο
Known
ordinal_In_Or_Subq
ordinal_In_Or_Subq
:
∀ x0 x1 .
ordinal
x0
⟶
ordinal
x1
⟶
or
(
x0
∈
x1
)
(
x1
⊆
x0
)
Known
nat_p_ordinal
nat_p_ordinal
:
∀ x0 .
nat_p
x0
⟶
ordinal
x0
Known
nat_1
nat_1
:
nat_p
1
Known
In_no2cycle
In_no2cycle
:
∀ x0 x1 .
x0
∈
x1
⟶
x1
∈
x0
⟶
False
Known
In_0_1
In_0_1
:
0
∈
1
Known
mul_nat_0L
mul_nat_0L
:
∀ x0 .
nat_p
x0
⟶
mul_nat
0
x0
=
0
Known
mul_nat_0R
mul_nat_0R
:
∀ x0 .
mul_nat
x0
0
=
0
Known
mul_nat_1R
mul_nat_1R
:
∀ x0 .
mul_nat
x0
1
=
x0
Theorem
prime_nat_or_composite_nat
prime_nat_or_composite_nat
:
∀ x0 .
x0
∈
omega
⟶
1
∈
x0
⟶
or
(
prime_nat
x0
)
(
composite_nat
x0
)
(proof)
Known
nat_complete_ind
nat_complete_ind
:
∀ x0 :
ι → ο
.
(
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
x0
x2
)
⟶
x0
x1
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
91381..
divides_nat_ref
:
∀ x0 .
nat_p
x0
⟶
divides_nat
x0
x0
Known
58a75..
:
∀ x0 x1 .
nat_p
x0
⟶
nat_p
x1
⟶
0
∈
x0
⟶
1
∈
x1
⟶
x0
∈
mul_nat
x0
x1
Known
nat_trans
nat_trans
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
x1
∈
x0
⟶
x1
⊆
x0
Known
e4e38..
divides_nat_tra
:
∀ x0 x1 x2 .
divides_nat
x0
x1
⟶
divides_nat
x1
x2
⟶
divides_nat
x0
x2
Theorem
prime_nat_divisor_ex
prime_nat_divisor_ex
:
∀ x0 .
nat_p
x0
⟶
1
∈
x0
⟶
∀ x1 : ο .
(
∀ x2 .
and
(
prime_nat
x2
)
(
divides_nat
x2
x0
)
⟶
x1
)
⟶
x1
(proof)
Param
add_nat
add_nat
:
ι
→
ι
→
ι
Known
mul_nat_SR
mul_nat_SR
:
∀ x0 x1 .
nat_p
x1
⟶
mul_nat
x0
(
ordsucc
x1
)
=
add_nat
x0
(
mul_nat
x0
x1
)
Known
df9cc..
mul_nat_Subq_L
:
∀ x0 x1 .
nat_p
x0
⟶
nat_p
x1
⟶
x0
⊆
x1
⟶
∀ x2 .
nat_p
x2
⟶
mul_nat
x2
x0
⊆
mul_nat
x2
x1
Known
ordinal_ordsucc_In_Subq
ordinal_ordsucc_In_Subq
:
∀ x0 .
ordinal
x0
⟶
∀ x1 .
x1
∈
x0
⟶
ordsucc
x1
⊆
x0
Known
ordsuccI2
ordsuccI2
:
∀ x0 .
x0
∈
ordsucc
x0
Known
add_nat_SL
add_nat_SL
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
add_nat
(
ordsucc
x0
)
x1
=
ordsucc
(
add_nat
x0
x1
)
Known
nat_0
nat_0
:
nat_p
0
Known
add_nat_0L
add_nat_0L
:
∀ x0 .
nat_p
x0
⟶
add_nat
0
x0
=
x0
Known
9cc32..
:
∀ x0 .
nat_p
x0
⟶
∀ x1 .
nat_p
x1
⟶
∀ x2 .
nat_p
x2
⟶
x1
∈
x2
⟶
add_nat
x1
x0
∈
add_nat
x2
x0
Theorem
nat_1In_not_divides_ordsucc
nat_1In_not_divides_ordsucc
:
∀ x0 x1 .
1
∈
x0
⟶
divides_nat
x0
x1
⟶
not
(
divides_nat
x0
(
ordsucc
x1
)
)
(proof)
Definition
bij
bij
:=
λ x0 x1 .
λ x2 :
ι → ι
.
and
(
and
(
∀ x3 .
x3
∈
x0
⟶
x2
x3
∈
x1
)
(
∀ x3 .
x3
∈
x0
⟶
∀ x4 .
x4
∈
x0
⟶
x2
x3
=
x2
x4
⟶
x3
=
x4
)
)
(
∀ x3 .
x3
∈
x1
⟶
∀ x4 : ο .
(
∀ x5 .
and
(
x5
∈
x0
)
(
x2
x5
=
x3
)
⟶
x4
)
⟶
x4
)
Definition
equip
equip
:=
λ x0 x1 .
∀ x2 : ο .
(
∀ x3 :
ι → ι
.
bij
x0
x1
x3
⟶
x2
)
⟶
x2
Definition
finite
finite
:=
λ x0 .
∀ x1 : ο .
(
∀ x2 .
and
(
x2
∈
omega
)
(
equip
x0
x2
)
⟶
x1
)
⟶
x1
Definition
infinite
infinite
:=
λ x0 .
not
(
finite
x0
)
Param
Sep
Sep
:
ι
→
(
ι
→
ο
) →
ι
Definition
primes
primes
:=
Sep
omega
prime_nat
Param
nat_primrec
nat_primrec
:
ι
→
(
ι
→
ι
→
ι
) →
ι
→
ι
Definition
Pi_nat
Pi_nat
:=
λ x0 :
ι → ι
.
nat_primrec
1
(
λ x1 x2 .
mul_nat
x2
(
x0
x1
)
)
Known
nat_primrec_0
nat_primrec_0
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
nat_primrec
x0
x1
0
=
x0
Theorem
Pi_nat_0
Pi_nat_0
:
∀ x0 :
ι → ι
.
Pi_nat
x0
0
=
1
(proof)
Known
nat_primrec_S
nat_primrec_S
:
∀ x0 .
∀ x1 :
ι →
ι → ι
.
∀ x2 .
nat_p
x2
⟶
nat_primrec
x0
x1
(
ordsucc
x2
)
=
x1
x2
(
nat_primrec
x0
x1
x2
)
Theorem
Pi_nat_S
Pi_nat_S
:
∀ x0 :
ι → ι
.
∀ x1 .
nat_p
x1
⟶
Pi_nat
x0
(
ordsucc
x1
)
=
mul_nat
(
Pi_nat
x0
x1
)
(
x0
x1
)
(proof)
Known
nat_ind
nat_ind
:
∀ x0 :
ι → ο
.
x0
0
⟶
(
∀ x1 .
nat_p
x1
⟶
x0
x1
⟶
x0
(
ordsucc
x1
)
)
⟶
∀ x1 .
nat_p
x1
⟶
x0
x1
Known
ordsuccI1
ordsuccI1
:
∀ x0 .
x0
⊆
ordsucc
x0
Theorem
Pi_nat_p
Pi_nat_p
:
∀ x0 :
ι → ι
.
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
nat_p
(
x0
x2
)
)
⟶
nat_p
(
Pi_nat
x0
x1
)
(proof)
Known
neq_1_0
neq_1_0
:
1
=
0
⟶
∀ x0 : ο .
x0
Known
mul_nat_0_inv
mul_nat_0_inv
:
∀ x0 .
x0
∈
omega
⟶
∀ x1 .
x1
∈
omega
⟶
mul_nat
x0
x1
=
0
⟶
or
(
x0
=
0
)
(
x1
=
0
)
Theorem
Pi_nat_0_inv
Pi_nat_0_inv
:
∀ x0 :
ι → ι
.
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
nat_p
(
x0
x2
)
)
⟶
Pi_nat
x0
x1
=
0
⟶
∀ x2 : ο .
(
∀ x3 .
and
(
x3
∈
x1
)
(
x0
x3
=
0
)
⟶
x2
)
⟶
x2
(proof)
Known
EmptyE
EmptyE
:
∀ x0 .
nIn
x0
0
Known
ordsuccE
ordsuccE
:
∀ x0 x1 .
x1
∈
ordsucc
x0
⟶
or
(
x1
∈
x0
)
(
x1
=
x0
)
Theorem
Pi_nat_divides
Pi_nat_divides
:
∀ x0 :
ι → ι
.
∀ x1 .
nat_p
x1
⟶
(
∀ x2 .
x2
∈
x1
⟶
nat_p
(
x0
x2
)
)
⟶
∀ x2 .
x2
∈
x1
⟶
divides_nat
(
x0
x2
)
(
Pi_nat
x0
x1
)
(proof)
Known
equip_sym
equip_sym
:
∀ x0 x1 .
equip
x0
x1
⟶
equip
x1
x0
Known
ordinal_Empty
ordinal_Empty
:
ordinal
0
Known
Empty_Subq_eq
Empty_Subq_eq
:
∀ x0 .
x0
⊆
0
⟶
x0
=
0
Known
SepE2
SepE2
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x1
x2
Known
SepI
SepI
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
x0
⟶
x1
x2
⟶
x2
∈
Sep
x0
x1
Known
SepE
SepE
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
and
(
x2
∈
x0
)
(
x1
x2
)
Known
SepE1
SepE1
:
∀ x0 .
∀ x1 :
ι → ο
.
∀ x2 .
x2
∈
Sep
x0
x1
⟶
x2
∈
x0
Theorem
form100_11_infinite_primes
form100_11_infinite_primes
:
infinite
primes
(proof)