---

Step * 2 1 1 of Lemma int_mod_union_int_mod


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)
BY
{ Assert ⌜gcd(n;m) = g ∈ ℤ⌝⋅ }

1
.....assertion..... 
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)
⊢ gcd(n;m) = g ∈ ℤ

2
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)
15. gcd(n;m) = g ∈ ℤ
⊢ 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)
6.  g  :  \mBbbN{}
7.  a  :  \mBbbZ{}
8.  b  :  \mBbbZ{}
9.  x2  :  \mBbbZ{}
10.  y  :  \mBbbZ{}
11.  n  =  (a  *  g)
12.  m  =  (b  *  g)
13.  ((x2  *  a)  +  (y  *  b))  =  1
14.  0  <  gcd(n;m)
\mvdash{}  x  =  x1


By

---

Latex:
Assert  \mkleeneopen{}gcd(n;m)  =  g\mkleeneclose{}\mcdot{}

---

Home Index