Nuprl - Proof: prime divs mul via intseg 1

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

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime divs mul via intseg 1

1. p :

2. prime(p)
3. a :

b:

, e:({a..b

}

).

a<b

p | (

i:{a..b

}. e(i))

(

i:{a..b

}. p | e(i))

By:	{Use induction over size b-a of the index set } SideProof

Generated subgoal:

1   k:, b:.
  b-a = k

  (e:({a..b}). a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))
9 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

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