Nuprl Definition : prime
prime(a) == (¬(a = 0 ∈ ℤ)) ∧ (¬(a ~ 1)) ∧ (∀b,c:ℤ. ((a | (b * c)) ⇒ ((a | b) ∨ (a | c))))
Definitions occuring in Statement :
assoced: a ~ b,
divides: b | a,
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
multiply: n * m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
equal: s = t ∈ T,
and: P ∧ Q,
not: ¬A,
assoced: a ~ b,
natural_number: $n,
all: ∀x:A. B[x],
int: ℤ,
implies: P ⇒ Q,
multiply: n * m,
or: P ∨ Q,
divides: b | a
FDL editor aliases :
prime
Latex:
prime(a) == (\mneg{}(a = 0)) \mwedge{} (\mneg{}(a \msim{} 1)) \mwedge{} (\mforall{}b,c:\mBbbZ{}. ((a | (b * c)) {}\mRightarrow{} ((a | b) \mvee{} (a | c))))
Date html generated:
2016_05_14-PM-04_20_01
Last ObjectModification:
2015_09_22-PM-06_02_39
Theory : num_thy_1
Home
Index