(15steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime divs mul via intseg 1 a 1

1. p : 
2. prime(p)
3. a : 
  k:b:.
  b-a = k
  
  (e:({a..b}). a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))


By: <Unproved Leaf>


Generated subgoals:

None

About:
intnatural_numbersubtractmultiplyless_thanlambda
functionequalimpliesall
exists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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