let n, m be Nat; :: thesis: ( m >= n & n > 0 implies 1 + ((m !) * (idseq n)) is CR_Sequence )
assume A1: ( m >= n & n > 0 ) ; :: thesis: 1 + ((m !) * (idseq n)) is CR_Sequence
set h = 1 + ((m !) * (idseq n));
deffunc H1( Nat) -> Element of omega = ((m !) * $1) + 1;
A2: len (1 + ((m !) * (idseq n))) = n by CARD_1:def 7;
A3: for i being Nat st i in dom (1 + ((m !) * (idseq n))) holds
(1 + ((m !) * (idseq n))) . i = H1(i)
proof
let i be Nat; :: thesis: ( i in dom (1 + ((m !) * (idseq n))) implies (1 + ((m !) * (idseq n))) . i = H1(i) )
assume A4: i in dom (1 + ((m !) * (idseq n))) ; :: thesis: (1 + ((m !) * (idseq n))) . i = H1(i)
A5: ( dom (1 + ((m !) * (idseq n))) = dom ((m !) * (idseq n)) & dom ((m !) * (idseq n)) = dom (idseq n) ) by VALUED_1:def 2, VALUED_1:def 5;
thus (1 + ((m !) * (idseq n))) . i = 1 + (((m !) * (idseq n)) . i) by A4, VALUED_1:def 2
.= 1 + ((m !) * ((idseq n) . i)) by A4, A5, VALUED_1:def 5
.= H1(i) by A4, A5, FINSEQ_2:49 ; :: thesis: verum
end;
A6: 1 + ((m !) * (idseq n)) is positive-yielding
proof
let r be Real; :: according to PARTFUN3:def 1 :: thesis: ( not r in rng (1 + ((m !) * (idseq n))) or not r <= 0 )
assume r in rng (1 + ((m !) * (idseq n))) ; :: thesis: not r <= 0
then consider x being object such that
A7: ( x in dom (1 + ((m !) * (idseq n))) & (1 + ((m !) * (idseq n))) . x = r ) by FUNCT_1:def 3;
reconsider x = x as Nat by A7;
H1(x) > 0 ;
hence not r <= 0 by A7, A3; :: thesis: verum
end;
reconsider h = 1 + ((m !) * (idseq n)) as INT -valued non empty positive-yielding FinSequence by A1, A6;
A8: for i, j being Nat st i in dom h & j in dom h & i < j holds
h . i,h . j are_coprime
proof
let i, j be Nat; :: thesis: ( i in dom h & j in dom h & i < j implies h . i,h . j are_coprime )
assume A9: ( i in dom h & j in dom h & i < j ) ; :: thesis: h . i,h . j are_coprime
reconsider ji = j - i as Nat by A9, NAT_1:21;
set G = (h . i) gcd (h . j);
A10: ( h . i = H1(i) & h . j = H1(j) ) by A9, A3;
then A11: (h . i) gcd (h . j) >= 1 by NAT_1:14;
assume not h . i,h . j are_coprime ; :: thesis: contradiction
then (h . i) gcd (h . j) > 1 by A11, XXREAL_0:1, INT_2:def 3;
then not (h . i) gcd (h . j) is trivial by NEWTON03:def 1;
then consider g being prime Nat such that
A12: g divides (h . i) gcd (h . j) by NEWTON03:29;
A13: ji <> 0 by A9;
( 0 <= i & j <= n ) by A9, A2, FINSEQ_3:25;
then ji <= n - 0 by XREAL_1:13;
then A14: ji divides m ! by A13, NEWTON:41, A1, XXREAL_0:2;
A15: ( (h . i) gcd (h . j) divides H1(i) & (h . i) gcd (h . j) divides H1(j) ) by A10, INT_2:def 2;
then A16: (h . i) gcd (h . j) divides H1(j) - H1(i) by INT_5:1;
A17: g divides H1(i) by A15, A12, INT_2:9;
g divides (m !) * ji by A12, A16, INT_2:9;
then ( g divides m ! or g divides j - i ) by INT_5:7;
then g divides m ! by A14, INT_2:9;
then g divides i * (m !) by INT_2:2;
then g divides H1(i) - (i * (m !)) by A17, INT_5:1;
then ( g = 1 or g = - 1 ) by INT_2:13;
hence contradiction by INT_2:def 4; :: thesis: verum
end;
h is Chinese_Remainder
proof
let i, j be Nat; :: according to INT_6:def 2 :: thesis: ( not i in dom h or not j in dom h or i = j or h . i,h . j are_coprime )
assume A18: ( i in dom h & j in dom h & i <> j ) ; :: thesis: h . i,h . j are_coprime
( i > j or j > i ) by A18, XXREAL_0:1;
hence h . i,h . j are_coprime by A18, A8; :: thesis: verum
end;
hence 1 + ((m !) * (idseq n)) is CR_Sequence ; :: thesis: verum