theorem Th28: :: NUMBER16:28

for p being Prime
for k being Nat holds
( ( p |-count (Product (primesFinS k)) = 1 implies primeindex p < k ) & ( primeindex p < k implies p |-count (Product (primesFinS k)) = 1 ) & ( p |-count (Product (primesFinS k)) = 0 implies primeindex p >= k ) & ( primeindex p >= k implies p |-count (Product (primesFinS k)) = 0 ) )