Nuprl - Proof: only positives prime fed 1

(2steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: only positives prime fed 1

1. f : Prime

2. n :

3.

x:Prime

. n<x

f(x) = 0
4. n =

{2..n+1

}(prime_mset_complete(f))

0<n

By:	Inst: Thm* a:, b:, f:({a..b}). {a..b}(f) Using:[2 \| n+1 \| prime_mset_complete(f)]

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(2steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc