let n be Nat; :: thesis: 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
let r be Real; :: thesis: for cn, cd being Integer st cn = (c_n r) . n & cd = (c_d r) . n & cn <> 0 holds
cn,cd are_coprime
let cn, cd be Integer; :: thesis: ( cn = (c_n r) . n & cd = (c_d r) . n & cn <> 0 implies cn,cd are_coprime )
(c_d r) . (n + 1) in NAT by REAL_3:50;
then reconsider cd2 = (c_d r) . (n + 1) as Integer ;
reconsider cn2 = (c_n r) . (n + 1) as Integer ;
assume that
A2: cn = (c_n r) . n and
A3: cd = (c_d r) . n and
A4: cn <> 0 ; :: thesis: cn,cd are_coprime
assume A5: not cn,cd are_coprime ; :: thesis: contradiction
A6: (cn2 * cd) - (cn * cd2) = (- 1) |^ n by A2, A3, REAL_3:64;
consider cn0, cd0 being Integer such that
A8: cn = (cn gcd cd) * cn0 and
A9: cd = (cn gcd cd) * cd0 and
cn0,cd0 are_coprime by A4, INT_2:23;
cn gcd cd <> 0 by A4, INT_2:5;
then cn gcd cd >= 0 + 1 by INT_1:7;
then A11: cn gcd cd > 1 by A5, INT_2:def 3, XXREAL_0:1;
A12: (- 1) |^ n = ((cn2 * (cn gcd cd)) * cd0) - (cn * cd2) by A6, A9
.= (cn gcd cd) * ((cn2 * cd0) - (cn0 * cd2)) by A8 ;
A13: 1 = |.((- 1) |^ n).| by SERIES_2:1
.= |.((cn gcd cd) * ((cn2 * cd0) - (cn0 * cd2))).| by A12
.= |.(cn gcd cd).| * |.((cn2 * cd0) - (cn0 * cd2)).| by COMPLEX1:65
.= (cn gcd cd) * |.((cn2 * cd0) - (cn0 * cd2)).| by ABSVALUE:def 1 ;
(cn gcd cd) " < 1 by A11, XREAL_1:212;
then |.((cn2 * cd0) - (cn0 * cd2)).| < 1 by A13, XCMPLX_1:210;
then |.((cn2 * cd0) - (cn0 * cd2)).| = 0 by NAT_1:14;
hence contradiction by A13; :: thesis: verum