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