let h be Integer; :: thesis: ( h <> 0 implies <*2,3*> ^ (Sgm (PrimeDivisors>3 h)) is Chinese_Remainder )
set X = PrimeDivisors>3 h;
set F = Sgm (PrimeDivisors>3 h);
set m = <*2,3*> ^ (Sgm (PrimeDivisors>3 h));
assume A1: h <> 0 ; :: thesis: <*2,3*> ^ (Sgm (PrimeDivisors>3 h)) is Chinese_Remainder
then A2: rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) c= SetPrimes by Th44;
A3: for i being Integer st i in dom (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) holds
(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i is prime

proof

let i be Integer; :: thesis: ( i in dom (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) implies (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i is prime )
assume i in dom (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i is prime
then (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i in rng (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) by FUNCT_1:def 3;
hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i is prime by A2, NEWTON:def 6; :: thesis: verum

end;

A4: len <*2,3*> = 2 by FINSEQ_1:44;
A5: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . 1 = 2 by Th21;
A6: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . 2 = 3 by Th21;
let i, j be Nat; :: according to INT_6:def 2 :: thesis: ( not i in proj1 (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) or not j in proj1 (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) or i = j or (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime )
assume A7: i in dom (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) ; :: thesis: ( not j in proj1 (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) or i = j or (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime )
then A8: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i is prime by A3;
assume A9: j in dom (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) ; :: thesis: ( i = j or (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime )
then A10: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j is prime by A3;
A11: 1 <= j by A9, FINSEQ_3:25;
A12: len (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) = (len <*2,3*>) + (len (Sgm (PrimeDivisors>3 h))) by FINSEQ_1:22;
assume A13: i <> j ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

A14: now :: thesis: ( j > 2 implies ( j - 2 >= 0 + 1 & j - 2 <= len (Sgm (PrimeDivisors>3 h)) & j - 2 in dom (Sgm (PrimeDivisors>3 h)) & (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 & (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime ) )

assume A15: j > 2 ; :: thesis: ( j - 2 >= 0 + 1 & j - 2 <= len (Sgm (PrimeDivisors>3 h)) & j - 2 in dom (Sgm (PrimeDivisors>3 h)) & (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 & (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime )
then reconsider j2 = j - 2 as Element of NAT by INT_1:5;
j2 > 2 - 2 by A15, XREAL_1:8;
hence A16: j - 2 >= 0 + 1 by NAT_1:13; :: thesis: ( j - 2 <= len (Sgm (PrimeDivisors>3 h)) & j - 2 in dom (Sgm (PrimeDivisors>3 h)) & (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 & (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime )
j <= len (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) by A9, FINSEQ_3:25;
then A17: j2 <= (2 + (len (Sgm (PrimeDivisors>3 h)))) - 2 by A4, A12, XREAL_1:7;
hence j - 2 <= len (Sgm (PrimeDivisors>3 h)) ; :: thesis: ( j - 2 in dom (Sgm (PrimeDivisors>3 h)) & (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 & (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime )
thus A18: j - 2 in dom (Sgm (PrimeDivisors>3 h)) by A16, A17, FINSEQ_3:25; :: thesis: ( (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 & (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime )
hence (Sgm (PrimeDivisors>3 h)) . (j - 2) > 3 by A1, Th40; :: thesis: ( (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (Sgm (PrimeDivisors>3 h)) . (j - 2) & (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime )
thus (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j = (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . (2 + j2)
.= (Sgm (PrimeDivisors>3 h)) . (j - 2) by A18, Th23 ; :: thesis: (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime
thus (Sgm (PrimeDivisors>3 h)) . (j - 2) is prime by A1, A18, Th42; :: thesis: verum

end;

1 <= i by A7, FINSEQ_3:25;

per cases then ( i = 1 or i = 2 or i > 2 ) by Lm10;

suppose A19: i = 1 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

per cases ( j = 1 or j = 2 or j > 2 ) by A11, Lm10;

suppose j = 1 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A13, A19; :: thesis: verum

end;

suppose j = 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A5, A6, A8, A10, A19, INT_2:30; :: thesis: verum

end;

suppose A20: j > 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

then ( 2,(Sgm (PrimeDivisors>3 h)) . (j - 2) are_coprime or 2 = (Sgm (PrimeDivisors>3 h)) . (j - 2) ) by A14, INT_2:30, XPRIMES1:2;
hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A14, A19, A20, Th21; :: thesis: verum

end;

end;

end;

suppose A21: i = 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

per cases ( j = 1 or j = 2 or j > 2 ) by A11, Lm10;

suppose j = 1 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A5, A6, A21, INT_2:30, XPRIMES1:2, XPRIMES1:3; :: thesis: verum

end;

suppose j = 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A13, A21; :: thesis: verum

end;

suppose j > 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A6, A14, A21, INT_2:30, XPRIMES1:3; :: thesis: verum

end;

end;

end;

suppose A22: i > 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

then reconsider i2 = i - 2 as Element of NAT by INT_1:5;
i2 > 2 - 2 by A22, XREAL_1:8;
then A23: i2 >= 0 + 1 by NAT_1:13;
i <= len (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) by A7, FINSEQ_3:25;
then A24: i2 <= (2 + (len (Sgm (PrimeDivisors>3 h)))) - 2 by A4, A12, XREAL_1:7;
then A25: i - 2 in dom (Sgm (PrimeDivisors>3 h)) by A23, FINSEQ_3:25;
then A26: (Sgm (PrimeDivisors>3 h)) . (i - 2) > 3 by A1, Th40;
A27: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i = (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . (2 + i2)
.= (Sgm (PrimeDivisors>3 h)) . (i - 2) by A25, Th23 ;
A28: (Sgm (PrimeDivisors>3 h)) . (i - 2) is prime by A1, A25, Th42;

per cases ( j = 1 or j = 2 or j > 2 ) by A11, Lm10;

suppose A29: j = 1 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

( 2,(Sgm (PrimeDivisors>3 h)) . (i - 2) are_coprime or 2 = (Sgm (PrimeDivisors>3 h)) . (i - 2) ) by A28, INT_2:30, XPRIMES1:2;
hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A1, A25, A27, A29, Th40, Th21; :: thesis: verum

end;

suppose j = 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A6, A26, A27, A28, INT_2:30, XPRIMES1:3; :: thesis: verum

end;

suppose A30: j > 2 ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

then reconsider j2 = j - 2 as Element of NAT by A14;

per cases ( i < j or i > j ) by A13, XXREAL_0:1;

suppose i < j ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

then i2 < j2 by XREAL_1:8;
then (Sgm (PrimeDivisors>3 h)) . i2 < (Sgm (PrimeDivisors>3 h)) . j2 by A1, A14, A23, A30, FINSEQ_1:def 14;
hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A8, A14, A27, A30, INT_2:30; :: thesis: verum

end;

suppose i > j ; :: thesis: (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime

then i2 > j2 by XREAL_1:8;
then (Sgm (PrimeDivisors>3 h)) . i2 > (Sgm (PrimeDivisors>3 h)) . j2 by A1, A14, A24, A30, FINSEQ_1:def 14;
hence (<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . i,(<*2,3*> ^ (Sgm (PrimeDivisors>3 h))) . j are_coprime by A8, A14, A27, A30, INT_2:30; :: thesis: verum

end;

end;

end;

end;

end;

end;