---

Step * of Lemma int_mod_isect_int_mod

∀[n,m:ℕ+].  ℤ_n ⋂ ℤ_m ≡ ℤ_lcm(n;m)
BY
{ (Auto
   THEN All (Unfold `int_mod`)
   THEN (InstLemma `isect2_quotient`[⌜ℤ⌝;⌜λ2x y.x ≡ y mod n⌝;λ2x y.x ≡ y mod m]⋅
         THENA (Auto THEN Repeat (D 0) THEN Auto THEN RelRST THEN Auto)
         )
   THEN ((InstLemma `ext-eq_transitivity` [⌜x,y:ℤ//(x ≡ y mod n) ⋂ x,y:ℤ//(x ≡ y mod m)⌝;⌜x,y:ℤ//((x ≡ y mod n)
                                                                                          ∧ (x ≡ y mod m))⌝]⋅
          THENM BHyp -1 
          THENM Auto)
         THENA ((Auto THEN Try ((BLemma `equiv_rel_and` THEN Auto)))
                THEN Try (Complete ((Repeat (D 0) THEN Auto THEN RelRST THEN Auto)))
                )
         )
   THEN All Thin) }

1
1. n : ℕ+
2. m : ℕ+
⊢ x,y:ℤ//((x ≡ y mod n) ∧ (x ≡ y mod m)) ≡ x,y:ℤ//(x ≡ y mod lcm(n;m))

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}\msupplus{}].    \mBbbZ{}\_n  \mcap{}  \mBbbZ{}\_m  \mequiv{}  \mBbbZ{}\_lcm(n;m)


By

---

Latex:
(Auto
  THEN  All  (Unfold  `int\_mod`)
  THEN  (InstLemma  `isect2\_quotient`[\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  \mequiv{}  y  mod  n\mkleeneclose{};\mlambda{}\msubtwo{}x  y.x  \mequiv{}  y  mod  m]\mcdot{}
              THENA  (Auto  THEN  Repeat  (D  0)  THEN  Auto  THEN  RelRST  THEN  Auto)
              )
  THEN  ((InstLemma  `ext-eq\_transitivity`  [\mkleeneopen{}x,y:\mBbbZ{}//(x  \mequiv{}  y  mod  n)  \mcap{}  x,y:\mBbbZ{}//(x  \mequiv{}  y  mod  m)\mkleeneclose{};
                \mkleeneopen{}x,y:\mBbbZ{}//((x  \mequiv{}  y  mod  n)  \mwedge{}  (x  \mequiv{}  y  mod  m))\mkleeneclose{}]\mcdot{}
                THENM  BHyp  -1 
                THENM  Auto)
              THENA  ((Auto  THEN  Try  ((BLemma  `equiv\_rel\_and`  THEN  Auto)))
                            THEN  Try  (Complete  ((Repeat  (D  0)  THEN  Auto  THEN  RelRST  THEN  Auto)))
                            )
              )
  THEN  All  Thin)

---

Home Index