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 H_{1}( 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 = H_{1}(i)

A8: for i, j being Nat st i in dom h & j in dom h & i < j holds

h . i,h . j are_coprime

assume A1: ( m >= n & n > 0 ) ; :: thesis: 1 + ((m !) * (idseq n)) is CR_Sequence

set h = 1 + ((m !) * (idseq n));

deffunc H

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 = H

proof

A6:
1 + ((m !) * (idseq n)) is positive-yielding
let i be Nat; :: thesis: ( i in dom (1 + ((m !) * (idseq n))) implies (1 + ((m !) * (idseq n))) . i = H_{1}(i) )

assume A4: i in dom (1 + ((m !) * (idseq n))) ; :: thesis: (1 + ((m !) * (idseq n))) . i = H_{1}(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

.= H_{1}(i)
by A4, A5, FINSEQ_2:49
; :: thesis: verum

end;assume A4: i in dom (1 + ((m !) * (idseq n))) ; :: thesis: (1 + ((m !) * (idseq n))) . i = H

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

.= H

proof

reconsider h = 1 + ((m !) * (idseq n)) as INT -valued non empty positive-yielding FinSequence by A1, A6;
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;

H_{1}(x) > 0
;

hence not r <= 0 by A7, A3; :: thesis: verum

end;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;

H

hence not r <= 0 by A7, A3; :: thesis: verum

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

h is Chinese_Remainder
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 = H_{1}(i) & h . j = H_{1}(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 H_{1}(i) & (h . i) gcd (h . j) divides H_{1}(j) )
by A10, INT_2:def 2;

then A16: (h . i) gcd (h . j) divides H_{1}(j) - H_{1}(i)
by INT_5:1;

A17: g divides H_{1}(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 H_{1}(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;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 = H

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 H

then A16: (h . i) gcd (h . j) divides H

A17: g divides H

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 H

then ( g = 1 or g = - 1 ) by INT_2:13;

hence contradiction by INT_2:def 4; :: thesis: verum

proof

hence
1 + ((m !) * (idseq n)) is CR_Sequence
; :: thesis: verum
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;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