---

Step * 2 1 of Lemma int_mod_union_int_mod


1. n : ℕ+
2. m : ℕ+
3. x : ℤ
4. x1 : ℤ
5. x ≡ x1 mod gcd(n;m)
⊢ x = x1 ∈ (ℤ_n ⋃ ℤ_m)
BY
{ ((InstLemma `gcd-reduce` [⌜n⌝;⌜m⌝]⋅ THENA Auto) THEN (InstLemma `gcd-positive` [⌜m⌝;⌜n⌝]⋅ THEN Auto) THEN ExRepD) }

1
1. n : ℕ+
2. m : ℕ+
3. x : ℤ
4. x1 : ℤ
5. x ≡ x1 mod gcd(n;m)
6. g : ℕ
7. a : ℤ
8. b : ℤ
9. x2 : ℤ
10. y : ℤ
11. n = (a * g) ∈ ℤ
12. m = (b * g) ∈ ℤ
13. ((x2 * a) + (y * b)) = 1 ∈ ℤ
14. 0 < gcd(n;m)
⊢ x = x1 ∈ (ℤ_n ⋃ ℤ_m)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbN{}\msupplus{}
3.  x  :  \mBbbZ{}
4.  x1  :  \mBbbZ{}
5.  x  \mequiv{}  x1  mod  gcd(n;m)
\mvdash{}  x  =  x1


By

---

Latex:
((InstLemma  `gcd-reduce`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `gcd-positive`  [\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD)

---

Home Index