Def  {i...} == {j:| ij }

is mentioned by

Thm*  x:{2...}, y:. prime(y)  x | y  x = y	[prime_nat_divby_self_only]
Thm*  x:{2...}. p:{2...}. px & prime(p) & p | x	[prime_or_smaller_prime_factor]
Thm*  x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc	[prime_or_smaller_prime_factor2]
Thm*  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))	[composite_with_prime_factor]
Thm*  i,j:{2...}. i<ij & j<ij	[factors_smaller]
Thm*  i:{2...}, j:. j<ij	[factor_smaller2]
Thm*  i:{2...}, j:{1...}. j<ij	[factor_smaller]

In prior sections: int 1 int 2

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html