let a1, a2 be Integer; :: thesis: for n1, n2 being Nat st n1 > 0 & n2 > 0 holds
for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1 * n2) solves_CRT a1,n1,a2,n2
let n1, n2 be Nat; :: thesis: ( n1 > 0 & n2 > 0 implies for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1 * n2) solves_CRT a1,n1,a2,n2 )
assume that
A1: n1 > 0 and
A2: n2 > 0 ; :: thesis: for x being Integer st x solves_CRT a1,n1,a2,n2 holds
x mod (n1 * n2) solves_CRT a1,n1,a2,n2
let x be Integer; :: thesis: ( x solves_CRT a1,n1,a2,n2 implies x mod (n1 * n2) solves_CRT a1,n1,a2,n2 )
assume A3: x solves_CRT a1,n1,a2,n2 ; :: thesis: x mod (n1 * n2) solves_CRT a1,n1,a2,n2
A4: x mod n1 = a1 mod n1 by A3, NAT_D:64;
(x mod (n1 * n2)) mod n1 = x mod n1 by A2, RADIX_1:7;
hence x mod (n1 * n2),a1 are_congruent_mod n1 by A1, A4, NAT_D:64; :: according to NUMBER14:def 1 :: thesis: x mod (n1 * n2),a2 are_congruent_mod n2
A5: x mod n2 = a2 mod n2 by A3, NAT_D:64;
(x mod (n1 * n2)) mod n2 = x mod n2 by A1, RADIX_1:7;
hence x mod (n1 * n2),a2 are_congruent_mod n2 by A2, A5, NAT_D:64; :: thesis: verum