Nuprl - Proof: prime divs mul via intseg 1 a

(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. 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 of the index set } k:, b:. b-a = k (e:({a..b}). a<b p \| ( i:{a..b}. e(i)) (i:{a..b}. p \| e(i))) Asserted

Generated subgoals:

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

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

2 4. k:, b:.
4. b-a = k
4.
4. (e:({a..b}). a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))
  b:, e:({a..b}).
  a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i))
2 steps

About:

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

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