English
If z ≡ a (mod n) and z ≡ b (mod m) with gcd(n,m)=1, then z ≡ ChineseRemainder(n,m; a,b) (mod nm).
Русский
Если z ≡ a (mod n) и z ≡ b (mod m) при gcd(n,m)=1, то z ≡ ChineseRemainder(n,m;a,b) (mod nm).
LaTeX
$$$\\\\forall n,m \\\\in \\\\mathbb{N},\\\\ gcd(n,m)=1 \\\\Rightarrow \\\\forall a,b,z \\\\in \\\\mathbb{N},\\\\ z \\\\equiv a \\\\pmod{n} \\\\land \\\\ z \\\\equiv b \\\\pmod{m} \\\\Rightarrow \\\\ z \\\\equiv \\text{ChineseRemainder}(n,m;a,b) \\\\pmod{nm}$$$
Lean4
theorem chineseRemainder'_lt_lcm (h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm : m ≠ 0) :
↑(chineseRemainder' h) < lcm n m := by
dsimp only [chineseRemainder']
rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]
have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)
