Step
*
1
of Lemma
divides_anti_sym
1. a : ℤ
2. b : ℤ
3. a | b
4. b | a
⊢ a = ± b
BY
{ ((Rewrite (RevLemmaC `divides_of_absvals`) 3 THENM Rewrite (RevLemmaC `divides_of_absvals`) 4) THENA Auto) }
1
1. a : ℤ
2. b : ℤ
3. |a| | |b|
4. |b| | |a|
⊢ a = ± b
Latex:
Latex:
1. a : \mBbbZ{}
2. b : \mBbbZ{}
3. a | b
4. b | a
\mvdash{} a = \mpm{} b
By
Latex:
((Rewrite (RevLemmaC `divides\_of\_absvals`) 3 THENM Rewrite (RevLemmaC `divides\_of\_absvals`) 4)
THENA Auto
)
Home
Index