Step
*
5
of Lemma
qeq-functionality
1. a7 : ℤ
2. a5 : ℤ
3. a6 : ℤ-o
4. a2 : ℤ
5. a3 : ℤ-o
6. (a7 * a6 =z a5) = tt
⊢ (a7 * a3 =z a2) = (a5 * a3 =z a2 * a6)
BY
{ (((RWO "eqtt_to_assert" (-1) THENM RW assert_pushdownC (-1)) THENA Auto)
THEN RevHypSubst' (-1) 0
THEN Thin (-1)
THEN (BLemma `iff_imp_equal_bool`⋅ THENA Auto)
THEN RW assert_pushdownC 0⋅
THEN Auto) }
1
1. a7 : ℤ
2. a5 : ℤ
3. a6 : ℤ-o
4. a2 : ℤ
5. a3 : ℤ-o
6. (a7 * a3) = a2 ∈ ℤ
⊢ ((a7 * a6) * a3) = (a2 * a6) ∈ ℤ
2
1. a7 : ℤ
2. a5 : ℤ
3. a6 : ℤ-o
4. a2 : ℤ
5. a3 : ℤ-o
6. ((a7 * a6) * a3) = (a2 * a6) ∈ ℤ
⊢ (a7 * a3) = a2 ∈ ℤ
Latex:
Latex:
1. a7 : \mBbbZ{}
2. a5 : \mBbbZ{}
3. a6 : \mBbbZ{}\msupminus{}\msupzero{}
4. a2 : \mBbbZ{}
5. a3 : \mBbbZ{}\msupminus{}\msupzero{}
6. (a7 * a6 =\msubz{} a5) = tt
\mvdash{} (a7 * a3 =\msubz{} a2) = (a5 * a3 =\msubz{} a2 * a6)
By
Latex:
(((RWO "eqtt\_to\_assert" (-1) THENM RW assert\_pushdownC (-1)) THENA Auto)
THEN RevHypSubst' (-1) 0
THEN Thin (-1)
THEN (BLemma `iff\_imp\_equal\_bool`\mcdot{} THENA Auto)
THEN RW assert\_pushdownC 0\mcdot{}
THEN Auto)
Home
Index