Step
*
1
of Lemma
int_mod_isect_int_mod
1. n : ℕ+
2. m : ℕ+
⊢ x,y:ℤ//((x ≡ y mod n) ∧ (x ≡ y mod m)) ≡ x,y:ℤ//(x ≡ y mod lcm(n;m))
BY
{ ((RepeatFor 2 (D 0) THENM (QuotientElimForEquality (-1)⋅ THEN Try (EqTypeCD)))
THENA (Auto THEN Try ((BLemma `equiv_rel_and` THEN Auto)))
) }
1
1. n : ℕ+
2. m : ℕ+
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ ℤ) ∧ (y ∈ ℤ) ∧ (x ≡ y mod n) ∧ (x ≡ y mod m)))
6. x ∈ ℤ
7. x1 ∈ ℤ
8. x ≡ x1 mod n
9. x ≡ x1 mod m
⊢ x ≡ x1 mod lcm(n;m)
2
1. n : ℕ+
2. m : ℕ+
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ ℤ) ∧ (y ∈ ℤ) ∧ (x ≡ y mod lcm(n;m))))
6. x ∈ ℤ
7. x1 ∈ ℤ
8. x ≡ x1 mod lcm(n;m)
⊢ x ≡ x1 mod n
3
1. n : ℕ+
2. m : ℕ+
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ ℤ) ∧ (y ∈ ℤ) ∧ (x ≡ y mod lcm(n;m))))
6. x ∈ ℤ
7. x1 ∈ ℤ
8. x ≡ x1 mod lcm(n;m)
9. x ≡ x1 mod n
⊢ x ≡ x1 mod m
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. m : \mBbbN{}\msupplus{}
\mvdash{} x,y:\mBbbZ{}//((x \mequiv{} y mod n) \mwedge{} (x \mequiv{} y mod m)) \mequiv{} x,y:\mBbbZ{}//(x \mequiv{} y mod lcm(n;m))
By
Latex:
((RepeatFor 2 (D 0) THENM (QuotientElimForEquality (-1)\mcdot{} THEN Try (EqTypeCD)))
THENA (Auto THEN Try ((BLemma `equiv\_rel\_and` THEN Auto)))
)
Home
Index