Step
*
of Lemma
qmul-zero-div
∀[a:ℚ]. ∀[b:ℤ-o].  (((0/b) * a) = 0 ∈ ℚ)
BY
{ xxx(Auto THEN xxx(Subst ⌜(0/b) = 0 ∈ ℚ⌝ 0⋅ THENA Auto)xxx)xxx }
1
.....equality..... 
1. a : ℚ
2. b : ℤ-o
⊢ (0/b) = 0 ∈ ℚ
2
1. a : ℚ
2. b : ℤ-o
⊢ (0 * a) = 0 ∈ ℚ
Latex:
Latex:
\mforall{}[a:\mBbbQ{}].  \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}].    (((0/b)  *  a)  =  0)
By
Latex:
xxx(Auto  THEN  xxx(Subst  \mkleeneopen{}(0/b)  =  0\mkleeneclose{}  0\mcdot{}  THENA  Auto)xxx)xxx
Home
Index