theorem :: DIOPHAN1:10

for n being Nat
for r being Real
for cn, cd being Integer st cn = (c_n r) . n & cd = (c_d r) . n & cn <> 0 holds
cn,cd are_coprime