Proofgold Object

λ x0 . {x1 ∈ RealsStruct_N x0|and (RealsStruct_lt x0 (RealsStruct_one x0) x1) (∀ x2 . x2 ∈ RealsStruct_Npos x0 ⟶ RealsStruct_divides x0 x2 x1 ⟶ or (x2 = RealsStruct_one x0) (x2 = x1))}

type
ι → ι

theory
HotG

name
RealsStruct_Primes

definition
PUVyd..

Megalodon
RealsStruct_Primes

proofgold address
TMRZK..^{RealsStruct_Primes}

creator
5857 Pr6Pc../493d3..

owner
5857 Pr6Pc../493d3..

term root
96c4c..